The problem of representing bound variables in syntax, and in particular that of capture-avoiding substitution, is well-known and has a number of solutions: named variables with alpha-equivalence, de Bruijn indices, locally namelessness, nominal sets, etc.

But there seems to be another fairly obvious approach, which I have nevertheless not seen used anywhere. Namely, in the basic syntax we have only one "variable" term, written say $\bullet$, and then separately we give a function that maps each variable to a binder in whose scope it lies. So a $\lambda$-term like

$$ \lambda x. (\lambda y. x y)$$

would be written $\lambda. (\lambda. \bullet\bullet)$, and the function would map the first $\bullet$ to the first $\lambda$ and the second $\bullet$ to the second $\lambda$. So it's kind of like de Bruijn indices, only instead of having to "count $\lambda$s" as you back out of the term to find the corresponding binder, you just evaluate a function. (If representing this as a data structure in an implementation, I would think of equipping each variable-term object with a simple pointer/reference to the corresponding binder-term object.)

Obviously this is not sensible for writing syntax on a page for humans to read, but then neither are de Bruijn indices. It seems to me that it makes perfect sense mathematically, and in particular it makes capture-avoiding substitution very easy: just drop in the term you are substituting and take the union of the binding functions. It's true that it doesn't have a notion of "free variable", but then (again) neither do de Bruijn indices really; in either case a term containing free variables is represented a term with a list of "context" binders in front.

Am I missing something and there is some reason this representation doesn't work? Are there problems that make it so much worse than the others that it's not worth considering? (The only problem I can think of right now is that the set of terms (together with their binding functions) is not inductively defined, but that doesn't seem insurmountable.) Or are there actually places where it has been used?

  • 2
    I don't know about drawbacks. Maybe formalization (e.g. in a proof assistant) is heavier? I'm not sure... What I know is that there's nothing technically wrong: this way of seeing lambda-terms is the one suggested by their representation as proof nets, so proof-net-aware people (like myself) implicitly use it all the time. But proof-net-aware people are very rare :-) So maybe it's really a matter of tradition. PS: I added a couple of loosely related tags to make the question more visible (hopefully). – Damiano Mazza Sep 7 at 8:44
  • Isn't this approach equivalent to higher-order abstract syntax (i.e., representing binders as functions in the host language)? In a sense, using a function as a binder establishes pointers to binders implicitly, in the representation of closures. – Rodolphe Lepigre Sep 7 at 9:41
  • 2
    @RodolpheLepigre I don't think so. In particular, my understanding is that HOAS is only correct when the metatheory is fairly weak, whereas this approach is correct in an arbitrary metatheory. – Mike Shulman Sep 7 at 11:21
  • 3
    Right, so each binder uses a unique (within the tree) variable name (the pointer to it is one automatically). This is the Barendregt convention. But when you substitute, you must rebuild (in C) the thing you're substituting to continue to have unique names. Otherwise (in general) you're using the same pointers for multiple subtrees, and can get variable capture. The rebuilding is alpha renaming. Presumably something similar happens depending on the specifics of your encoding of trees as sets? – Dan Doel Sep 7 at 14:04
  • 3
    @DanDoel Ah, interesting. I thought it was so obvious as to not need mentioning that you would drop in a separate copy of the term being substituted at every occurrence of the variable it's being substituted for; otherwise you wouldn't have a syntax tree any more! It didn't occur to me to think of this copying as alpha-renaming, but now that you point it out I can see it. – Mike Shulman Sep 7 at 17:27

Andrej's and Łukasz's answers make good points, but I wanted to add additional comments.

To echo what Damiano said, this way of representing binding using pointers is the one suggested by proof-nets, but the earliest place where I saw it for lambda terms was in an old essay by Knuth:

  • Donald Knuth (1970). Examples of formal semantics. In Symposium on Semantics of Algorithmic Languages, E. Engeler (ed.), Lecture Notes in Mathematics 188, Springer.

On page 234, he drew the following diagram (which he called an "information structure") representing the term $(\lambda y.\lambda z.yz)x$:

Knuth's diagram for $(\lambda y.\lambda z.yz)x$

This kind of graphical representation of lambda terms was also studied independently (and more deeply) in two theses in the early 1970s, both by Christopher Wadsworth (1971, Semantics and Pragmatics of the Lambda-Calculus) and by Richard Statman (1974, Structural Complexity of Proofs). Nowadays, such diagrams are often referred to as "λ-graphs" (see for example this paper).

Observe that the term in Knuth's diagram is linear, in the sense that every free or bound variable occurs exactly once -- as others have mentioned, there are non-trivial issues and choices to be made in trying to extend this kind of representation to non-linear terms.

On the other hand, for linear terms I think it's great! Linearity precludes the need for copying, and so you get both $\alpha$-equivalence and substitution "for free". These are the same advantages as HOAS, and I actually agree with Rodolphe Lepigre that there is a connection (if not exactly an equivalence) between the two forms of representation: there is a sense in which these graphical structures may be naturally interpreted as string diagrams, representing endomorphisms of a reflexive object in a compact closed bicategory (I gave a brief explanation of that here).

I'm not sure how your variable-to-binder-function would be represented and for what purpose you'd like to use it. If you are using back-pointers then as Andrej noted the computational complexity of substitution is not better than classical alpha-renaming.

From your comment on Andrej's answer I infer that to some extent you are interested in sharing. I can provide some input here.

In a typical typed lambda calculus, weakening and contraction, contrary to other rules, do not have syntax.

$$ \frac{\Gamma \vdash t : T}{\Gamma, x:A \vdash t : T} \;\mathtt{W}$$ $$ \frac{\Gamma, x_1 : A, x_2 : A \vdash t : T}{\Gamma, x:A \vdash t : T} \;\mathtt{C}$$

Let's add some syntax:

$$ \frac{\Gamma \vdash t : T}{\Gamma, x:A \vdash W_x(t) : T} \;\mathtt{W}$$ $$ \frac{\Gamma, x_1 : A, x_2 : A \vdash t : T}{\Gamma, x:A \vdash C_x^{x_1,x_2}(t) : T} \;\mathtt{C}$$

$C_a^{b,c}(\cdot)$ is 'using up' variable $a$ and binding variables $b,c$. I've learned of that idea from one of Ian Mackie's "An Interaction Net Implementation of Closed Reduction".

With that syntax, every variable is used exactly twice, once where it is bound and once where it is used. This allows us to distance ourselves from a particular syntax and look at the term as a graph where variables and terms are edges.

From algorithmic complexity, we can now use pointers not from a variable to a binder, but from binder to variable and have substitutions in a constant time.

Moreover, this reformulation allows us to track erasure, copying and sharing with more fidelity. One can write rules that incrementally copy (or erase) a term while sharing subterms. There are many ways to do that. In some restricted settings the wins are quite surprising.

This is getting close to the topics of interaction nets, interaction combinators, explicit substitution, linear logic, Lamping's optimal evaluation, sharing graphs, light logics and other.

All these topics are very exciting for me and I'd gladly give more specific references but I'm not sure whether any of this is useful to you and what are your interests.

Your data structure works but it won't be more efficient than other approaches because you need to copy every argument on every beta reduction, and you have to make as many copies as there are occurrences of the bound variable. This way you keep destroying memory sharing between subterms. Combined with the fact that you're proposing a non-pure solution that involves pointer manipulations, and is therefore very error-prone, it's probably not worth the trouble.

But I'd be delighted to see an experiment! You could take lambda and implement it with your data-structure (OCaml has pointers, they're called references). More or less, you just have to replace syntax.ml and norm.ml with your versions. That's less than 150 lines of code.

  • Thanks! I admit I wasn't really thinking very hard about implementations but mainly about being able to do mathematical proofs without bothering about either de Bruijn bookkeeping or alpha-renaming. But is there any chance that an implementation could retain some memory sharing by not making copies "until necessary", i.e. until the copies would diverge from each other? – Mike Shulman Sep 7 at 20:03
  • Sure, you could do copy-on-write sort of thing, the operating systems people have been doing these tricks for a long time. One would have to provide some evidence that it's going to work better than established solutions. A lot will depend on usage patterns. For instance, do most arguments to $\beta$-redeces get duplicated, or are they mostly used in a linear fashion? In a typical redex $(\lambda x . e_1) \, e_2$, which one is typically larger, $e_1$ or $e_2$? By the way, explicit substitions are a way to do things lazily as well. – Andrej Bauer Sep 7 at 20:37
  • 2
    Regarding mathematical proofs, I've now gone through a good deal of formalization of type-theoretic syntax, my experience is that advantages are obtained when we generalize the setup and make it more abstract, not when we make it more concrete. For instance, we can parametrize the syntax with "any good way of treating binding". When we do so, it's more difficult to make mistakes. I have also formalized type theory with de Bruijn indices. It's not too terrible, especially if you have dependent types around that prevent you from doing nonsensical things. – Andrej Bauer Sep 7 at 20:39
  • 2
    To add, I have worked on an implementation that used basically this technique (but with unique integers and maps, not pointers), and I wouldn't really recommend it. We definitely had a lot of bugs where we missed cloning things properly (in no small part due to trying to avoid it when possible). But I think there's a paper by some GHC folks where they do advocate it (they used a hash function to generate the unique names, I believe). It might depend what exactly you're doing. In my case it was type inference/checking, and it seems pretty poorly suited there. – Dan Doel Sep 7 at 23:12
  • @MikeShulman For algorithms of reasonable (Elementary) complexity (to a large extent amount of copying and erasing), the so called 'abstract part' of Lamping's optimal reduction is not making copies until necessary. The abstract part is also the non-controversial part as opposed to the full algorithm which requires some annotations that can dominate the computation. – Łukasz Lew Sep 7 at 23:32

Other answers are mostly discussing implementation issues. Since you mention your main motivation as doing mathematical proofs without too much bookkeeping, here is the main issue I see with that.

When you say “a function that maps each variable to a binder in whose scope it lies”: the output type of this function is surely a bit subtler than that makes it sound! Specifically, the function must take values in something like “the binders of the term under consideration” — i.e. some set which varies depending on the term (and isn’t obviously a subset of a larger ambient set in any useful way). So in substitution, you can’t just “take the union of the binding functions”: you also have to reindex their values, according to some map from binders in the original terms to binders in the result of the substitution.

These reindexings should surely be “routine”, in the sense that they could be reasonably either swept under the rug, or packaged nicely in terms of some sort of functoriality or naturality. But the same is true of the bookkeeping involved in working with named variables. So overall, it seems likely to me that there would be at least as much bookkeeping involved with this approach as with more standard approaches.

This aside, though, it’s a conceptually very appealing approach, and I’d love to see it carefully worked out — I can well imagine it might throw a different light on some aspects of syntax than the standard approaches do.

  • keeping track of the scope of each variable indeed requires bookkeeping, but don't jump to the conclusion that one always needs to restrict to well-scoped syntax! Operations such as substitution and beta reduction can be defined even on ill-scoped terms, and my suspicion is that if one wanted to formalize this approach (which again, is really the approach of proof-nets/"λ-graphs") in a proof assistant, one would first implement the more general operations, and then prove that they preserve the property of being well-scoped. – Noam Zeilberger Sep 13 at 1:21
  • (Agreed that it is worth trying out... although I wouldn't be surprised if somebody already has in the context of formalizing proof-nets/λ-graphs.) – Noam Zeilberger Sep 13 at 1:23
  • 2

Here is my attempt at encoding the $\lambda$-calculus using your approach (in OCaml, with several explanations in comments). It is actually possible to define terms as circular values, which means that this representation has a good chance to work well in Coq. Note that it would require a coinductive type in the representation of closures (to account for the Lazy.t the I use below).

Overall, I think that it is a cool representation, but it involves some bookkeeping with pointers, to avoid breaking binding links. It would be possible to change the code to use mutable fields I guess, but encoding in Coq would then be less direct. I am still convinced that this is very similar to HOAS, although the pointer structure is made explicit. However, the presence of Lazy.t implies that it is possible for some code to be evaluated at the wrong time. This is not the case in my code as only substitution of a variable with a variable may happen at force time (and not evaluation for example).

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

Your Answer

 
discard

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.