Merupakan variabel terikat dengan fungsi dari kegunaan untuk binder

Masalah yang merepresentasikan variabel terikat dalam sintaksis, dan khususnya substitusi yang menghindari penangkapan, telah diketahui dan memiliki sejumlah solusi: variabel bernama dengan kesetaraan alfa, indeks de Bruijn, tanpa nama lokal, set nominal, dll.

Tetapi tampaknya ada pendekatan lain yang cukup jelas, yang saya lihat belum pernah digunakan di mana pun. Yaitu, dalam sintaksis dasar kita hanya memiliki satu istilah "variabel", ditulis katakan , dan kemudian secara terpisah kita memberikan fungsi yang memetakan setiap variabel ke pengikat yang cakupannya terletak. Jadi seperti λ -term$\bullet$$\lambda$

akan ditulis , dan fungsinya akan memetakan pertama ke pertama dan kedua ke kedua . Jadi itu semacam indeks de Bruijn, hanya alih-alih harus "menghitung λ s" saat Anda kembali keluar dari istilah untuk menemukan binder yang sesuai, Anda hanya mengevaluasi suatu fungsi. (Jika menyatakan ini sebagai struktur data dalam implementasi, saya akan berpikir untuk melengkapi setiap objek variabel-istilah dengan pointer / referensi sederhana ke objek istilah pengikat yang sesuai.)$\lambda. (\lambda. \bullet\bullet)$$\bullet$$\lambda$$\bullet$$\lambda$$\lambda$

Jelas ini tidak masuk akal untuk menulis sintaks pada halaman untuk dibaca manusia, tetapi tidak ada indeks de Bruijn. Sepertinya bagi saya itu masuk akal secara matematis, dan khususnya itu membuat penggantian-hindarkan sangat mudah: cukup masukkan istilah yang Anda gantikan dan gunakan penyatuan fungsi pengikatan. Memang benar bahwa itu tidak memiliki gagasan "variabel bebas", tetapi kemudian (lagi) tidak melakukan indeks de Bruijn benar-benar; dalam kedua kasus istilah yang berisi variabel bebas diwakili istilah dengan daftar "konteks" pengikat di depan.

Apakah saya kehilangan sesuatu dan ada alasan mengapa representasi ini tidak berfungsi? Adakah masalah yang membuatnya jauh lebih buruk daripada yang lain sehingga tidak layak dipertimbangkan? (Satu-satunya masalah yang dapat saya pikirkan saat ini adalah bahwa himpunan istilah (bersama dengan fungsi pengikatannya) tidak didefinisikan secara induktif, tetapi itu tampaknya tidak dapat diatasi.) Atau apakah sebenarnya ada tempat di mana ia telah digunakan?

Jawaban Andrej dan Łukasz merupakan poin yang bagus, tetapi saya ingin menambahkan komentar tambahan.

Untuk menggemakan apa yang dikatakan Damiano, cara ini untuk mewakili pengikat menggunakan pointer adalah yang disarankan oleh jaring-bukti, tetapi tempat paling awal di mana saya melihatnya untuk istilah lambda adalah dalam esai lama oleh Knuth:

• Donald Knuth (1970). Contoh semantik formal. Dalam Simposium tentang Semantik Bahasa Algoritmik , E. Engeler (ed.), Catatan Kuliah di Matematika 188, Springer.

Pada halaman 234, ia menggambar diagram berikut (yang ia sebut "struktur informasi") yang mewakili istilah :$(\lambda y.\lambda z.yz)x$

Representasi grafis dari istilah lambda ini juga dipelajari secara independen (dan lebih dalam) dalam dua tesis pada awal 1970-an, baik oleh Christopher Wadsworth (1971, Semantik dan Pragmatik dari Lambda-Calculus ) dan oleh Richard Statman (1974, Structural Complexity) dari Bukti ). Saat ini, diagram seperti itu sering disebut sebagai "λ-grafik" (lihat contoh makalah ini ).

Perhatikan bahwa istilah dalam diagram Knuth adalah linier , dalam arti bahwa setiap variabel bebas atau terikat terjadi tepat satu kali - seperti yang telah disebutkan orang lain, ada masalah dan pilihan non-sepele yang dibuat untuk mencoba memperluas representasi semacam ini ke non istilah -linier.

$\alpha$

Saya tidak yakin bagaimana fungsi variabel-ke-pengikat Anda akan diwakili dan untuk tujuan apa Anda ingin menggunakannya. Jika Anda menggunakan back-pointer maka seperti yang dicatat Andrej kompleksitas komputasi substitusi tidak lebih baik dari penggantian nama alpha klasik.

Dari komentar Anda pada jawaban Andrej, saya menyimpulkan bahwa sampai batas tertentu Anda tertarik untuk berbagi. Saya dapat memberikan beberapa masukan di sini.

Dalam kalkulus lambda yang diketik khas, melemah dan kontraksi, bertentangan dengan aturan lain, tidak memiliki sintaks.

Mari kita tambahkan beberapa sintaks:

$C_a^{b,c}(\cdot)$$a$$b,c$

Dengan sintaks itu, setiap variabel digunakan tepat dua kali, sekali di mana ia terikat dan sekali di mana ia digunakan. Ini memungkinkan kita untuk menjauhkan diri dari sintaksis tertentu dan melihat istilah tersebut sebagai grafik di mana variabel dan istilahnya bertepi.

Dari kompleksitas algoritmik, kita sekarang dapat menggunakan pointer bukan dari variabel ke binder, tetapi dari binder ke variabel dan memiliki substitusi dalam waktu yang konstan.

Selain itu, reformulasi ini memungkinkan kita melacak penghapusan, penyalinan, dan berbagi dengan lebih setia. Seseorang dapat menulis aturan yang secara bertahap menyalin (atau menghapus) suatu istilah saat berbagi subterms. Ada banyak cara untuk melakukan itu. Dalam beberapa pengaturan terbatas , kemenangannya cukup mengejutkan .

Ini semakin dekat dengan topik jaring interaksi, kombinator interaksi, substitusi eksplisit, logika linier, evaluasi optimal Lamping, berbagi grafik, logika ringan dan lainnya.

Semua topik ini sangat menarik bagi saya dan saya dengan senang hati memberikan referensi yang lebih spesifik, tetapi saya tidak yakin apakah semua ini bermanfaat bagi Anda dan apa minat Anda.

Struktur data Anda berfungsi tetapi tidak akan lebih efisien daripada pendekatan lain karena Anda perlu menyalin setiap argumen pada setiap pengurangan beta, dan Anda harus membuat salinan sebanyak mungkin karena ada kemunculan variabel terikat. Dengan cara ini Anda terus menghancurkan pembagian memori antara subterma. Dikombinasikan dengan fakta bahwa Anda mengusulkan solusi non-murni yang melibatkan manipulasi pointer, dan karenanya sangat rawan kesalahan, mungkin tidak sepadan dengan masalahnya.

Tapi saya akan senang melihat percobaan! Anda dapat mengambil lambdadan mengimplementasikannya dengan struktur data Anda (OCaml memiliki pointer, mereka disebut referensi ). Lebih atau kurang, Anda hanya perlu mengganti syntax.mldan norm.mldengan versi Anda. Itu kurang dari 150 baris kode.

Jawaban lain sebagian besar membahas masalah implementasi. Karena Anda menyebutkan motivasi utama Anda melakukan pembuktian matematis tanpa terlalu banyak pembukuan, berikut adalah masalah utama yang saya lihat.

Ketika Anda mengatakan "fungsi yang memetakan setiap variabel ke pengikat yang memiliki cakupannya": tipe output dari fungsi ini sedikit lebih halus daripada yang membuatnya terdengar! Secara khusus, fungsi harus mengambil nilai dalam sesuatu seperti "pengikat istilah yang sedang dipertimbangkan" - yaitu beberapa set yang bervariasi tergantung pada istilah (dan jelas bukan subset dari set ambient yang lebih besar dengan cara yang bermanfaat). Jadi dalam substitusi, Anda tidak bisa hanya "mengambil penyatuan fungsi pengikatan": Anda juga harus mengindeks ulang nilai-nilai mereka, menurut beberapa peta dari binder dalam istilah asli ke binder dalam hasil substitusi.

Pengindeksan ulang ini tentunya harus "rutin", dalam arti bahwa mereka dapat disapu dengan baik di bawah karpet, atau dikemas dengan baik dalam hal semacam fungsi atau kealamian. Tetapi hal yang sama berlaku untuk pembukuan yang terlibat dalam bekerja dengan variabel bernama. Jadi secara keseluruhan, tampaknya bagi saya bahwa akan ada paling sedikit pembukuan yang terlibat dengan pendekatan ini dibandingkan dengan pendekatan yang lebih standar.

Selain itu, ini adalah pendekatan yang sangat menarik secara konseptual, dan saya ingin melihatnya bekerja dengan hati-hati - saya bisa membayangkan itu mungkin memberikan cahaya yang berbeda pada beberapa aspek sintaksis daripada pendekatan standar lakukan.

$\lambda$Lazy.t

Secara keseluruhan, saya pikir itu adalah representasi yang keren, tetapi melibatkan beberapa pembukuan dengan pointer, untuk menghindari putusnya tautan yang mengikat. Itu mungkin untuk mengubah kode untuk menggunakan bidang yang bisa berubah saya kira, tetapi pengkodean dalam Coq kemudian akan menjadi kurang langsung. Saya masih yakin bahwa ini sangat mirip dengan HOAS, walaupun struktur pointer dibuat eksplisit. Namun, keberadaan Lazy.tmenyiratkan bahwa beberapa kode mungkin dievaluasi pada waktu yang salah. Ini bukan kasus dalam kode saya karena hanya penggantian variabel dengan variabel yang dapat terjadi pada forcewaktu (dan bukan evaluasi misalnya).

(* Representation of a term of the λ-calculus. *)
type term =
  | FVar of string      (* Free variable  *)
  | BVar of bvar        (* Bound variable *)
  | Appl of term * term (* Application    *)
  | Abst of abst        (* Abstraction    *)

(* A bound variable is a pointer to the corresponding binder. *)
and bvar = abst

(* A binder is represented as its body in which the bound variable points to
   the binder itself. Note that we need to use a thunk to be able to work
   underneath a binder (for substitution, evaluation, ...). A name can be
   given for easy printing, but no renaming is done. Only “visual capture”
   can happen since pointers are established the right way, even if names
   can clash. *)
and abst = { body : term Lazy.t ; name : string }

(* Terms can be built with recursive values for abstractions. *)

(* Krivine's notation is used for application (function in parentheses). *)

let id    : term = (* λx.x        *)
  Abst(let rec id = {body = lazy (BVar(id)); name = "x"} in id)

let idid  : term = (* (λx.x) λx.x *)
  Appl(id, id)

let delta : term = (* λx.(x) x *)
  Abst(let rec d = {body = lazy (Appl(BVar(d), BVar(d))); name = "x" } in d)

let weird : term = (* (λx.x) λy.(λx.(x) x) (C) y *)
  Appl(id, Abst(let rec x = {body = lazy (Appl(delta, Appl(FVar("C"),
    BVar(x)))); name = "y"} in x))

let omega : term = (* (λx.(x) x) λx.(x) x *)
  Appl(delta, delta)

(* Printing function is immediate. *)
let rec print : out_channel -> term -> unit = fun oc t ->
  match t with
  | FVar(x)   -> output_string oc x
  | BVar(x)   -> output_string oc x.name
  | Appl(t,u) -> Printf.fprintf oc "(%a) %a" print t print u
  | Abst(f)   -> Printf.fprintf oc "λ%s.%a" f.name print (Lazy.force f.body)

(* Substitution of variable [x] by [v] in the term [t]. Occurences of [x] in
   [t] are identified using physical equality ([BVar] case). The subtle case
   is [Abst], because we need to reestablish the physical link between the
   binder and the variable it binds. *)
let rec subst_var : bvar -> term -> term -> term = fun x t v ->
  match t with
  | FVar(_)   -> t
  | BVar(y)   -> if y == x then v else t
  | Appl(t,u) -> Appl(subst_var x t v, subst_var x u v)
  | Abst(f)   ->
      (* First compute the new body. *)
      let fv = subst_var x (Lazy.force f.body) v in
      (* Reestablish the physical link, using [subst_var] itself again. This
         requires a second traversal of the term. We could probably do both
         at once, but who cares the complexity is linear in [t] anyway. *)
      Abst(let rec g = {f with body = lazy (subst_var f fv (BVar(g)))} in g)

(* Actual substitution function. *)
let subst : abst -> term -> term = fun f v ->
  subst_var f (Lazy.force f.body) v

(* Normalization function (all the way, even under binders). *)
let rec eval : term -> term = fun t ->
  match t with
  | Appl(t,u) ->
      begin
        let v = eval u in
        match eval t with
        | Abst(f) -> eval (subst f v)
        | t       -> Appl(t,v)
      end
  | Abst(f)   ->
      (* Actual computation in the body. *)
      let fv = eval (Lazy.force f.body) in
      (* Here, the physical link is reestablished, but it is important to note
         that the computation of evaluation is done above. So the part below
         only takes a linear time in the size of the normal form of the body
         of the abstraction. *)
      Abst(let rec g = {f with body = lazy (subst_var f fv (BVar(g)))} in g)
  | _         ->
      t

let _ = Printf.printf "id         = %a\n%!" print id
let _ = Printf.printf "eval id    = %a\n%!" print (eval id)

let _ = Printf.printf "idid       = %a\n%!" print idid
let _ = Printf.printf "eval idid  = %a\n%!" print (eval idid)

let _ = Printf.printf "delta      = %a\n%!" print delta
let _ = Printf.printf "eval delta = %a\n%!" print (eval delta)

let _ = Printf.printf "omega      = %a\n%!" print omega
(* The following obviously loops. *)
(*let _ = Printf.printf "eval omega = %a\n%!" print (eval omega)*)

let _ = Printf.printf "weird      = %a\n%!" print weird
let _ = Printf.printf "eval weird = %a\n%!" print (eval weird)

(* Output produced:
id         = λx.x
eval id    = λx.x
idid       = (λx.x) λx.x
eval idid  = λx.x
delta      = λx.(x) x
eval delta = λx.(x) x
omega      = (λx.(x) x) λx.(x) x
weird      = (λx.x) λy.(λx.(x) x) (C) y
eval weird = λy.((C) y) (C) y
*)