Reprezentowanie powiązanych zmiennych za pomocą funkcji od zastosowań do segregatorów

Problem reprezentowania zmiennych powiązanych w składni, a zwłaszcza podstawiania unikania przechwytywania, jest dobrze znany i ma wiele rozwiązań: zmienne nazwane z równoważnością alfa, wskaźniki de Bruijna, lokalna bezimienność, zbiory nominalne itp.

Ale wydaje się, że istnieje inne dość oczywiste podejście, którego jednak nigdzie nie widziałem. Mianowicie, w podstawowej składni mamy tylko jeden termin „zmienny”, zapisany powiedzmy , a następnie osobno dajemy funkcję, która mapuje każdą zmienną na spoiwo, w którego zakresie się ona znajduje. Tak jak termin $\bullet$$\lambda$

zostanie napisane , a funkcja odwzorowuje pierwszą ∙ na pierwszą λ, a drugą ∙ na drugą λ . Jest to więc coś w rodzaju wskaźników de Bruijna, tylko zamiast „liczyć λs ”, gdy wycofujesz się z terminu, aby znaleźć odpowiednie spoiwo, po prostu oceniasz funkcję. (Reprezentując to jako strukturę danych w implementacji, pomyślałbym o wyposażeniu każdego obiektu o zmiennej wartości w prosty wskaźnik / odniesienie do odpowiedniego obiektu o charakterze wiążącym).$\lambda. (\lambda. \bullet\bullet)$$\bullet$$\lambda$$\bullet$$\lambda$$\lambda$

Oczywiście nie jest to rozsądne, aby pisać składnię na stronie, aby ludzie mogli ją przeczytać, ale wtedy też nie są to wskaźniki de Bruijna. Wydaje mi się, że ma to matematyczny sens, w szczególności sprawia, że ​​bardzo łatwo jest zastąpić unikanie przechwytywania: wystarczy wpisać termin, który zastępujesz i wziąć połączenie funkcji wiążących. To prawda, że ​​nie ma pojęcia „zmiennej zmiennej”, ale (ponownie) tak naprawdę nie ma też indeksów de Bruijna; w obu przypadkach termin zawierający wolne zmienne jest reprezentowany z przodu z listą segregatorów „kontekstowych”.

Czy coś mi brakuje i jest jakiś powód, dla którego ta reprezentacja nie działa? Czy są problemy, które sprawiają, że jest o wiele gorzej niż inne, że nie warto brać pod uwagę? (Jedyny problem, jaki mogę teraz wymyślić, to to, że zestaw terminów (wraz z ich wiążącymi funkcjami) nie jest zdefiniowany indukcyjnie, ale nie wydaje się to nie do pokonania.) Czy są też miejsca, w których zostały użyte?

Odpowiedzi Andreja i Łukasza są dobre, ale chciałem dodać dodatkowe komentarze.

Aby powtórzyć to, co powiedział Damiano, ten sposób przedstawiania wiązania za pomocą wskaźników jest tym, który sugerują siatki próbne, ale najwcześniejsze miejsce, w którym widziałem go dla wyrażeń lambda, było w starym eseju Knutha:

• Donald Knuth (1970). Przykłady semantyki formalnej. W Sympozjum na temat semantyki języków algorytmicznych , E. Engeler (red.), Lecture Notes in Mathematics 188, Springer.

Na stronie 234 narysował następujący schemat (który nazwał „strukturą informacji”) reprezentującą termin :$(\lambda y.\lambda z.yz)x$

Ten rodzaj graficznej reprezentacji terminów lambda był również badany niezależnie (i głębiej) w dwóch tezach na początku lat siedemdziesiątych, zarówno przez Christophera Wadswortha (1971, Semantics and Pragmatics of the Lambda-Calculus ), jak i Richarda Statmana (1974, Structural Complexity dowodów ). Obecnie takie diagramy są często nazywane „wykresami λ” (patrz na przykład ten artykuł ).

Zauważ, że termin na diagramie Knutha jest liniowy , w tym sensie, że każda wolna lub związana zmienna występuje dokładnie jeden raz - jak wspomnieli inni, istnieją nietrywialne problemy i wybory, które należy podjąć, próbując rozszerzyć tego rodzaju reprezentację na nie warunki liniowe.

Z drugiej strony, jeśli chodzi o warunki liniowe, myślę, że to świetnie! Liniowość wyklucza potrzebę kopiowania, więc otrzymujesz zarówno równoważność jak i podstawienie „za darmo”. Są to te same zalety, co HOAS, i faktycznie zgadzam się z Rodolphe Lepigre, że istnieje związek (jeśli nie dokładnie równoważność) między dwiema formami reprezentacji: istnieje poczucie, że te struktury graficzne mogą być naturalnie interpretowane jako diagramy ciągów , reprezentujących endomorfizmy obiektu zwrotnego w zwartej zamkniętej dwukategorii (podałem krótkie wyjaśnienie tego$\alpha$ tutaj ).

Nie jestem pewien, w jaki sposób twoja funkcja zmiennej do spoiwa byłaby reprezentowana i do jakiego celu chcesz jej użyć. Jeśli używasz wskaźników wstecznych, to jak zauważył Andrej, złożoność obliczeniowa podstawienia nie jest lepsza niż klasyczna zmiana nazw alfa.

Z twojego komentarza do odpowiedzi Andreja wnioskuję, że do pewnego stopnia jesteś zainteresowany dzieleniem się. Mogę tu podać jakieś informacje.

W typowym typowym rachunku lambda osłabienie i skurcz, w przeciwieństwie do innych reguł, nie mają składni.

Dodajmy składnię:

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

Dzięki tej składni każda zmienna jest używana dokładnie dwa razy, raz tam, gdzie jest związana i raz tam, gdzie jest używana. To pozwala nam zdystansować się od konkretnej składni i spojrzeć na ten termin jako wykres, na którym zmienne i terminy są krawędziami.

Ze złożoności algorytmicznej możemy teraz korzystać ze wskaźników nie ze zmiennej na spoiwo, ale ze spoiwa na zmienną i mieć podstawienia w stałym czasie.

Co więcej, ta zmiana formuły pozwala nam śledzić usuwanie, kopiowanie i udostępnianie z większą wiernością. Można pisać reguły, które stopniowo kopiują (lub usuwają) termin podczas udostępniania podtermów. Można to zrobić na wiele sposobów. W niektórych ograniczonych ustawieniach wygrane są dość zaskakujące .

Zbliża się to do tematów sieci interakcji, kombinatorów interakcji, wyraźnego podstawienia, logiki liniowej, optymalnej oceny Lampinga, udostępniania wykresów, logiki światła i innych.

Wszystkie te tematy są dla mnie bardzo ekscytujące i chętnie podam bardziej szczegółowe odniesienia, ale nie jestem pewien, czy którekolwiek z nich jest dla ciebie przydatne i jakie są twoje zainteresowania.

Twoja struktura danych działa, ale nie będzie bardziej wydajna niż inne podejścia, ponieważ musisz skopiować każdy argument przy każdej redukcji wersji beta i musisz wykonać tyle kopii, ile jest wystąpień zmiennej powiązanej. W ten sposób niszczycie dzielenie pamięci między subtermami. W połączeniu z faktem, że proponujesz nieczyste rozwiązanie, które wymaga manipulacji wskaźnikiem, a zatem jest bardzo podatne na błędy, prawdopodobnie nie jest warte kłopotów.

Ale byłbym zachwycony widząc eksperyment! Możesz wziąć lambdai zaimplementować go ze swoją strukturą danych (OCaml ma wskaźniki, nazywane są referencjami ). Bardziej lub mniej, po prostu trzeba wymienić syntax.mli norm.mlze swoimi wersjami. To mniej niż 150 linii kodu.

Inne odpowiedzi dotyczą głównie kwestii związanych z wdrażaniem. Ponieważ wspominasz o swojej głównej motywacji jako robieniu dowodów matematycznych bez zbytniej księgowości, oto główny problem, jaki z tym widzę.

Kiedy mówisz „funkcja, która odwzorowuje każdą zmienną na segregator, w którego zasięgu się ona znajduje”: typ wyjściowy tej funkcji jest z pewnością nieco subtelniejszy niż to sprawia, że ​​brzmi! W szczególności funkcja musi przyjmować wartości w coś w rodzaju „spoiwa rozważanego terminu” - tj. Jakiś zestaw, który różni się w zależności od terminu (i oczywiście nie jest pod żadnym względem podzbiorem większego zestawu otoczenia). Tak więc w podstawieniu nie możesz po prostu „wziąć unii funkcji wiązania”: musisz także ponownie zindeksować ich wartości, zgodnie z pewną mapą od segregatorów w oryginalnych terminach do segregatorów w wyniku podstawienia.

Te reindeksacje z pewnością powinny być „rutynowe”, w tym sensie, że można je rozsądnie zamiatać pod dywan lub ładnie zapakować pod względem jakiejś funkcjonalności lub natury. To samo dotyczy księgowości związanej z pracą z nazwanymi zmiennymi. Ogólnie rzecz biorąc, wydaje mi się prawdopodobne, że przy takim podejściu byłoby co najmniej tyle samo księgowości, co w przypadku bardziej standardowych podejść.

Pomijając to, jest to bardzo atrakcyjne pod względem koncepcyjnym podejście i chciałbym zobaczyć, jak to dokładnie opracowano - mogę sobie wyobrazić, że może rzucić inne światło na niektóre aspekty składni niż standardowe podejście.

$\lambda$Lazy.t zastosowania, którego używam poniżej).

Ogólnie rzecz biorąc, uważam, że jest to fajna reprezentacja, ale wymaga pewnej księgowości ze wskazówkami, aby uniknąć zerwania wiążących linków. Można by chyba zmienić kod, aby używał zmiennych pól, ale kodowanie w Coq byłoby wtedy mniej bezpośrednie. Nadal jestem przekonany, że jest to bardzo podobne do HOAS, chociaż struktura wskaźnika jest wyraźna. Jednak obecność Lazy.tsugeruje, że możliwe jest oszacowanie kodu w niewłaściwym czasie. W moim kodzie nie ma to miejsca, ponieważ w danym forcemomencie może wystąpić tylko podstawienie zmiennej zmienną (a nie na przykład ocena).

(* 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
*)