How to deal with Binders?

Question

When reasoning about programming languages in a deep embedding, $\alpha$-equivalence, binders and capture-avoiding substitution quickly can become tedious. Complex binders may introduce multiple bound variables in the same scope.

There has been much research about binders, the POPLMark challenge (ref) has an entire focus on them. For example the following techniques are amongst the available submissions:

• de Bruijn
• (weak) HOAS
• locally nameless
• named variables
• nominal approach

Other techniques include Nameless, Painless (ref) and sorts, Bindings as Bounded Natural Functors (pdf) and probably more.

---

What approach do you recommend for which proof assistants? Are there certain tools/libraries that you use?

Answer 1

There are already a lot of choices pointed out on Jesper Cockx's blog. Usually, the properties you would like to establish includes

• Equations of compositions of substitutions. For example, $E[x/A][y/B]$ should be equal to $E[y/B][x/A[y/B]]$, provided that $B$ does not contain $x$. (Hopefully my notation is self-evident.) This equation will take on various forms in different formulations. For example, with de Bruijn indices it becomes $E[\delta][\sigma] = E[[\sigma] \circ \delta]$, where $[\_]$ turns a substitution into a function on terms, and a substitution is a function from dBIs to terms.
• Equations concerning weakening, i.e. adding a variable that is not present. This is not needed if weakening is no-op.
• $\alpha$-equivalence is an equivalence, and it is congruent, e.g. if $A \sim B$ then $\lambda x. A \sim \lambda x. B$.
• No exotic terms exists. This is exclusively a problem with HOAS-related approaches.

There are also some choices when defining substitution:

• You may want to define a subcollection of substitution called renaming. They only passes variables around, and therefore is easier to deal with. In particular, the composition of renaming is very simple. Also, renaming never creates redexes, which makes it very important when proving normalization-related properties.
• You may want to formalize only order preserving renamings, or you may allow arbitrary permutations. In dependent types you probably don't have a choice.
• You may want to represent substitution/renaming with an inductive type (something like a list, but may contain more information based on your specific needs), or you may want to use functions, e.g. use a function from variables to terms to represent substitution. Functions are easier to simplify, and somewhat more flexible. But without function extensionality you would need extra work to prove some equalities (you probably can still prove them, though). Also, in implementations, functions are usually slower.

However, I would also like to point out that there is now an increasing trend (on reasoning, not implementing) to simply abandon any binding. This, among with a set of other techniques, is called algebraic type theory, because it reduces type theory to a more or less algebraic theory.

Answer 2

This is kind of silly but I haven't really seen it concretely written down anywhere.

Given a system of first-order logic you don't need to have a concrete system of terms at all but can only use variables. You can emulate terms using total functional relations. Substitution then becomes the much simpler to implement renaming of variables.

As an example take Peano arithmetic.

You have axioms the terms are total functional

$$ \top \vdash \exists! x. \text{O}(x)$$ $$ \top \vdash \forall x. \exists! y. \text{S}(x, y) $$

Distinctness becomes something like

$$ \top \vdash \forall x y. \neg( \text{O}(y) \wedge \text{S}(x, y) )$$

This becomes quite quite painful to work with in practice and is probably mostly useful in metatheory.

An uglier multisorted mechanical translation of the untyped lambda calculus might be something like the following.

All terms are converted to relations

$$ R \mathrel{::=} \text{var}(x, e) \mid \text{lam}(x, e_1, e_2) \mid \text{app}(e_1, e_2, e_3) \mid \text{subst}(x, e_1, e_2, e_3)$$

Do not confuse variables within the theory of lambda calculus with variables within the framework of first order logic.

All terms are axiomized as total functional.

$$\vdash \forall x. \exists! e. \text{var}(x, e) $$ $$\vdash \forall e_1 e_2. \exists! e_3. \text{app}(e_1, e_2, e_3) $$ $$\vdash \forall x e_1. \exists! e_2. \text{lam}(x, e_1, e_2) $$ $$\vdash \forall x e_1 e_2. \exists! e_3. \text{subst}(x, e_1, e_2, e_3) $$

Beta reduction becomes something like

$$ \vdash \forall x e_1 e_3 e_4.(\exists e_2. \text{lam}(x, e_1, e_2) \wedge \text{app}(e_2, e_3, e_4)) \iff \text{subst}(x, e_1, e_3, e_4) $$

Of course you wouldn't usually do something like this in practice. Things become completely unreadable sigils. Axiomizing capture avoiding substitution like this would also be hellish. But it's in an interesting thing to have in your toolkit and could be merely difficult instead of hellish if you compiled down from a higher level.

In practice among other tweaks you would probably want to take advantage of the relational style and make substitution a partial function instead of total functional. I just wanted to explain the mechanical nature of the translation.