Barendregt's Substitution Lemma

Let us explain one of our results with a simple proof about the lambda calculus. An informal "pencil-and-paper" proof there looks typically as follows (this one is taken from Barendregt's classic book on the lambda calculus):

2.1.16. Substitution Lemma: If x≠y and x not free in L, then
M[x:=N][y:=L] = M[y:=L][x:=N[y:=L]].
Proof: By induction on the structure of M.
Case 1. M is a variable.
Case 1.1. M=x. Then both sides equal N[y:=L] since x≠y.
Case 1.2. M=y. Then both sides equal L, for x not free in L implies L[x:=...]=L.
Case 1.3. M=z≠x,y. Then both sides equal z.
Case 2. M=λz.M1.
By the variable convention we may assume that z≠x,y and z is not free in N, L. Then by the induction hypothesis
(λz.M1)[x:=N][y:=L] = λz.M1[x:=N][y:=L]
  = λz.M1[y:=L][x:=N[y:=L]]
  = (λz.M1)[y:=L][x:=N[y:=L]].
Case 3. M=M1 M2.
Then the statement follows again from the induction hypothesis.

We want to make it as easy as possible to formalise such informal proofs (and more complicated ones). Inspired by the PoplMark Challenge, we want that masses use theorem assistants to do their formal proofs.

Since the kind of informal reasoning illustrated by Barendregt's proof is very common in the literature on programming languages, it might be surprising that implementing his proof in a theorem assistant is not a trivial task. This is because he relies implicitly on some assumptions and conventions. For example he states in his book:

2.1.12. Convention. Terms that are α-congruent are identified. So now we write λx.x=λy.y, etcetera.
2.1.13. Variable Convention. If M1,...,Mn occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free variables.

The first convention is crucial for the proof above as it allows one to deal with the variable case by using equational reasoning - one can just calculate what the results of the substitutions are. If one uses un-equated, or raw, lambda-terms, the same kind of reasoning cannot be performed (the reasoning then has to be modulo α-equivalence, which causes a lot of headaches in the lambda-case.) But if the data-structure over which the proof is formulated is α-equivalence classes of lambda-terms, then what is the principle "by induction over the structure of M"? There is an induction principle "over the structure" for (un-equated) lambda-terms. But quotening lambda-terms by α-equivalence does not automatically lead to such a principle for α-equivalence classes. This seems to be a point that is nearly always ignored in the literature. In fact it takes, as we have shown in [1] and [2], some serious work to provide such an induction principle for α-equivalence classes.

The second problem for an implementation of Barendregt's proof is his use of the variable convention: there is just no proof-principle "by convention" in a theorem assistant. Taking a closer look at Barendregt's reasoning, it turns out that for a proof obligation of the form "for all α-equated lambda-terms λz.M1...", he does not establish this proof obligation for all λz.M1, but only for some carefully chosen α-equated lambda-terms, namely the ones for which z is not free in x,y,N and L. This style of reasoning clearly needs some justification and in fact depends on some assumptions of the "context" of the induction. By "context" of the induction we mean the variables x,y,N and L. When employing the variable convention in a formal proof, one always implicitly assumes that one can choose a fresh name for this context. This might, however, not always be possible, for example when the context already mentions all names. Also we found out recently that the use of the variable convention in proofs by rule-induction can lead to faulty reasoning [5]. So our work introduces safeguards that ensure that the use of the variable convention is always safe.

One might conclude from our comments about Barendregt's proof that it is no proof at all. This is, however, not the case! With Nominal Isabelle and its infrastructure one can easily formalise his reasoning. One first has to declare the structure of α-equated lambda-terms as a nominal datatype:

atom_decl name nominal_datatype term = Var "name" | App "term" "term" | Lam "«name»term"

Note though, that nominal datatypes are not datatypes in the traditional sense, but stand for α-equivalence classes. Indeed we have for terms of type term the equation(!)

lemma alpha: "Lam [a].(Var a) = Lam [b].(Var b)"

which does not hold for traditional datatypes (note that we write lambda-abstractions as Lam [a].t). The proof of the substitution lemma can then be formalised as follows:

lemma substitution_lemma: assumes asm: "x≠y" "x#L" shows "M[x:=N][y:=L] = M[y:=L][x:=N[y:=L]]" using asm by (nominal_induct M avoiding: x y N L rule: term.induct) (auto simp add: forget fresh_fact)

where the assumption "x is fresh for L", written x#L, encodes the usual relation of "x not free in L". The method nominal_induct takes as arguments the variable over which the induction is performed (here M), and the context of the induction, which consists of the variables mentioned in the variable convention (that is the part in Barendregt's proof where he writes "...we may assume that z≠x,y and z is not free in N,L"). The last argument of nominal_induct specifies which induction rule should be applied - in this case induction over α-equated lambda-terms, an induction-principle Nominal Isabelle provides automatically when the nominal datatype term is defined. The implemented proof of the substitution lemma proceeds then completely automatically, except for the need of having to mention the facts forget and fresh_fact, which are proved separately (also by induction over α-equated lambda-terms).

The lemma forget shows that if x is not free in L, then L[x:=...]=L (Barendregt's Case 1.2). Its formalised proof is as follows:

lemma forget: assumes asm: "x#L" shows "L[x:=P] = L" using asm by (nominal_induct L avoiding: x P rule: term.induct) (auto simp add: abs_fresh fresh_atm)

In this proof abs_fresh is an automatically generated lemma that establishes when x is fresh for a lambda-abstraction, namely x#Lam [z].P' if and only if x=z or (x≠z and x#P'); fresh_atm states that x#y if and only if x≠y. The lemma fresh_fact proves the property that if z does not occur freely in N and L then it also does not occur freely in N[y:=L]. This fact can be formalised as follows:

lemma fresh_fact: assumes asm: "z#N" "z#L" shows "z#N[y:=L]" using asm by (nominal_induct N avoiding: z y L rule: term.induct) (auto simp add: abs_fresh fresh_atm)

Although the latter lemma does not appear explicitly in Barendregt's reasoning, it is required in the last step of the lambda-case (Case 2) where he pulls the substitution from under the binder z (the interesting step is marked with a •):

 λz.(M1[y:=L][x:=N[y:=L]]) 
=(λz.M1[y:=L])[x:=N[y:=L]]  •
=(λz.M1)[y:=L][x:=N[y:=L]] 

After these 22 lines one has a completely formalised proof of the substitution lemma. This proof does not rely on any axioms, apart from the ones on which HOL is built.


References

[1] Nominal Reasoning Techniques in Isabelle/HOL. In Journal of Automatic Reasoning, 2008, Vol. 40(4), 327-356. [ps].
[2] A Formal Treatment of the Barendregt Variable Convention in Rule Inductions (Christian Urban and Michael Norrish) Proceedings of the ACM Workshop on Mechanized Reasoning about Languages with Variable Binding and Names (MERLIN 2005). Tallinn, Estonia. September 2005. Pages 25-32. © ACM, Inc. [ps] [pdf]
[3] A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL (Christian Urban and Stefan Berghofer) Proceedings of the 3rd International Joint Conference on Automated Deduction (IJCAR 2006). In volume 4130 of Lecture Notes in Artificial Intelligence. Seattle, USA. August 2006. Pages 498-512. © Springer Verlag [ps]
[4] A Head-to-Head Comparison of de Bruijn Indices and Names. (Stefan Berghofer and Christian Urban) Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2006). Seattle, USA. ENTCS. Pages 53-67. [ps]
[5] Barendregt's Variable Convention in Rule Inductions. (Christian Urban, Stefan Berghofer and Michael Norrish) Proceedings of the 21th Conference on Automated Deduction (CADE 2007). In volume 4603 of Lecture Notes in Artificial Intelligence. Bremen, Germany. July 2007. Pages 35-50. © Springer Verlag [ps]
[6] Mechanising the Metatheory of LF. (Christian Urban, James Cheney and Stefan Berghofer) In Proc. of the 23rd IEEE Symposium on Logic in Computer Science (LICS 2008), IEEE Computer Society, June 2008. Pages 45-56. [pdf] More information elsewhere.
[7] Proof Pearl: A New Foundation for Nominal Isabelle. (Brian Huffman and Christian Urban) In Proc. of the 1st Conference on Interactive Theorem Proving (ITP 2010). In volume 6172 in Lecture Notes in Computer Science, Pages 35-50, 2010. [pdf]
[8] General Bindings and Alpha-Equivalence in Nominal Isabelle. (Christian Urban and Cezary Kaliszyk) In Proc. of the 20th European Symposium on Programming (ESOP 2011). In Volume 6602 of Lecture Notes in Computer Science, Pages 480-500, 2011. [pdf]

Last modified: Mon May 9 05:35:17 BST 2011 [Validate this page.]