Representing bound variables with a function from uses to binders

Question

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?

Answer 1

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$:

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).

Answer 2

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.

Answer 3

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.

Answer 4

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.

Answer 5

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