Représenter les variables liées avec une fonction des utilisations aux classeurs

Le problème de la représentation des variables liées dans la syntaxe, et en particulier celui de la substitution évitant la capture, est bien connu et a plusieurs solutions: variables nommées avec équivalence alpha, indices de Bruijn, localement sans nom, ensembles nominaux, etc.

Mais il semble y avoir une autre approche assez évidente, que je n'ai pourtant pas vue utilisée nulle part. À savoir, dans la syntaxe de base, nous n'avons qu'un seul terme "variable", écrit par exemple , puis séparément nous donnons une fonction qui mappe chaque variable à un classeur dans la portée duquel elle se trouve. Donc, un -term comme$\bullet$$\lambda$

serait écrit , et la fonction mapperait le premier au premier et le second au second . C'est donc un peu comme les indices de Bruijn, mais au lieu d'avoir à "compter s" lorsque vous reculez pour trouver le liant correspondant, vous évaluez simplement une fonction. (Si cela représente une structure de données dans une implémentation, je penserais à équiper chaque objet à terme variable d'un simple pointeur / référence vers l'objet à terme de liant correspondant.)∙ λ ∙ λ $\lambda. (\lambda. \bullet\bullet)$$\bullet$$\lambda$$\bullet$$\lambda$$\lambda$

Évidemment, cela n'est pas judicieux pour écrire la syntaxe sur une page que les humains peuvent lire, mais les indices de Bruijn ne le sont pas non plus. Il me semble que cela a un sens mathématique parfait, et en particulier il rend la substitution évitant la capture très facile: il suffit de laisser tomber le terme que vous remplacez et de prendre l'union des fonctions de liaison. Il est vrai qu'il n'a pas de notion de "variable libre", mais alors (encore) les indices de Bruijn non plus; dans les deux cas, un terme contenant des variables libres est représenté par un terme avec une liste de classeurs "contextuels" devant.

Suis-je en train de manquer quelque chose et il y a une raison pour laquelle cette représentation ne fonctionne pas? Y a-t-il des problèmes qui le rendent tellement pire que les autres que cela ne vaut pas la peine d'être considéré? (Le seul problème auquel je peux penser en ce moment est que l'ensemble des termes (ainsi que leurs fonctions de liaison) ne sont pas définis par induction, mais cela ne semble pas insurmontable.) Ou existe-t-il réellement des endroits où il a été utilisé?

Les réponses d'Andrej et de Łukasz soulèvent de bons points, mais je voulais ajouter des commentaires supplémentaires.

Pour faire écho à ce que Damiano a dit, cette façon de représenter la liaison à l'aide de pointeurs est celle suggérée par les réseaux de preuves, mais le premier endroit où je l'ai vu pour les termes lambda était dans un ancien essai de Knuth:

• Donald Knuth (1970). Exemples de sémantique formelle. Dans Symposium on Semantics of Algorithmic Languages , E. Engeler (éd.), Lecture Notes in Mathematics 188, Springer.

À la page 234, il a dessiné le diagramme suivant (qu'il a appelé une "structure d'information") représentant le terme :$(\lambda y.\lambda z.yz)x$

Ce type de représentation graphique des termes lambda a également été étudié de manière indépendante (et plus approfondie) dans deux thèses au début des années 1970, à la fois par Christopher Wadsworth (1971, Semantics and Pragmatics of the Lambda-Calculus ) et par Richard Statman (1974, Structural Complexity des preuves ). De nos jours, de tels diagrammes sont souvent appelés "graphiques λ" (voir par exemple cet article ).

Observez que le terme dans le diagramme de Knuth est linéaire , dans le sens où chaque variable libre ou liée se produit exactement une fois - comme d'autres l'ont mentionné, il y a des problèmes et des choix non triviaux à faire en essayant d'étendre ce type de représentation à des non - termes linéaires.

$\alpha$

Je ne sais pas comment votre fonction variable-liant serait représentée et dans quel but vous souhaitez l'utiliser. Si vous utilisez des pointeurs arrière, comme Andrej l'a noté, la complexité de calcul de la substitution n'est pas meilleure que l'alpha-renommage classique.

À partir de votre commentaire sur la réponse d'Andrej, j'en déduis que vous êtes dans une certaine mesure intéressé à partager. Je peux fournir quelques informations ici.

Dans un calcul lambda typé typique, l'affaiblissement et la contraction, contrairement à d'autres règles, n'ont pas de syntaxe.

Ajoutons une syntaxe:

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

Avec cette syntaxe, chaque variable est utilisée exactement deux fois, une fois où elle est liée et une fois où elle est utilisée. Cela nous permet de nous éloigner d'une syntaxe particulière et de considérer le terme comme un graphique où les variables et les termes sont des arêtes.

De la complexité algorithmique, nous pouvons maintenant utiliser des pointeurs non pas d'une variable à un liant, mais de liant à variable et avoir des substitutions dans un temps constant.

De plus, cette reformulation nous permet de suivre l'effacement, la copie et le partage avec plus de fidélité. On peut écrire des règles qui copient (ou effacent) de façon incrémentielle un terme tout en partageant des sous-termes. Il y a plusieurs façons de procéder. Dans certains contextes restreints, les victoires sont assez surprenantes .

Cela se rapproche des sujets des réseaux d'interaction, des combinateurs d'interaction, de la substitution explicite, de la logique linéaire, de l'évaluation optimale de Lamping, du partage des graphiques, de la logique lumineuse et autres.

Tous ces sujets sont très excitants pour moi et je me ferais un plaisir de vous donner des références plus spécifiques mais je ne sais pas si tout cela vous est utile et quels sont vos intérêts.

Votre structure de données fonctionne, mais elle ne sera pas plus efficace que les autres approches, car vous devez copier chaque argument à chaque réduction bêta et vous devez faire autant de copies qu'il y a d'occurrences de la variable liée. De cette façon, vous continuez de détruire le partage de mémoire entre les sous-termes. Combiné avec le fait que vous proposez une solution non pure qui implique des manipulations de pointeurs, et est donc très sujette aux erreurs, cela ne vaut probablement pas la peine.

Mais je serais ravi de voir une expérience! Vous pouvez le prendre lambdaet l'implémenter avec votre structure de données (OCaml a des pointeurs, ils sont appelés références ). Plus ou moins, il vous suffit de remplacer syntax.mlet norm.mlavec vos versions. C'est moins de 150 lignes de code.

D'autres réponses traitent principalement des problèmes de mise en œuvre. Puisque vous mentionnez votre principale motivation comme faire des preuves mathématiques sans trop de comptabilité, voici le principal problème que je vois avec cela.

Lorsque vous dites "une fonction qui mappe chaque variable à un classeur dans la portée duquel elle se trouve": le type de sortie de cette fonction est sûrement un peu plus subtil que cela la fait sonner! Plus précisément, la fonction doit prendre des valeurs dans quelque chose comme «les liants du terme considéré» - c'est-à-dire un ensemble qui varie en fonction du terme (et n'est évidemment pas un sous-ensemble d'un ensemble ambiant plus grand de quelque manière utile). Donc, en substitution, vous ne pouvez pas simplement "prendre l'union des fonctions de liaison": vous devez également réindexer leurs valeurs, selon une correspondance entre les liants dans les termes d'origine et les liants dans le résultat de la substitution.

Ces réindexations devraient sûrement être «routinières», dans le sens où elles pourraient être raisonnablement soit balayées sous le tapis, soit bien emballées en termes de fonction ou de naturalité. Mais il en va de même pour la comptabilité impliquée dans le travail avec les variables nommées. Donc, dans l'ensemble, il me semble probable qu'il y aurait au moins autant de comptabilité impliquée dans cette approche qu'avec des approches plus standard.

Ceci mis à part, cependant, c'est une approche conceptuellement très attrayante, et j'aimerais que cela soit soigneusement élaboré - je peux bien imaginer que cela pourrait jeter un éclairage différent sur certains aspects de la syntaxe que les approches standard.

$\lambda$Lazy.t

Dans l'ensemble, je pense que c'est une représentation sympa, mais cela implique une comptabilité avec des pointeurs, pour éviter de rompre les liens de liaison. Il serait possible de changer le code pour utiliser des champs mutables je suppose, mais l'encodage en Coq serait alors moins direct. Je suis toujours convaincu que cela est très similaire à HOAS, bien que la structure du pointeur soit explicite. Cependant, la présence de Lazy.timplique qu'il est possible qu'un code soit évalué au mauvais moment. Ce n'est pas le cas dans mon code car seule la substitution d'une variable par une variable peut se produire à la forcefois (et pas d'évaluation par exemple).

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