A constructive mechanization of Lambda Calculus in Coq

This repository is about an axiom free intuitionistic and inductive Coq development of untyped Lambda Calculus theory and its relation to Computability theory. The main goal is to provide tools to implement intuitionistic undecidability results in Coq, mainly about satisfiability or provability problems for various logics.

The proof plan follows relatively closely the translation by R. Cori of the excellent book

Lambda-Calculus: Types and Models by Jean-Louis Krivine

• confluence of beta, beta and beta-eta reduction with proofs also inspired from the work of T. Nipkow
• (strong) head reduction, representation of recursive algorithms/functions (with correctness proofs), fixpoint combinators, (lambda) undecidability of the "normalizable" predicate
• intersection types systems D and D-Omega, characterization of head normalizability, leftmost normalizability and strong normalizability, also inspired from Strict Intersection Types for the Lambda Calculus by S. v. Bakel.
• encoding of Combinatory Logic into Lambda calculus.

Converting the proof into intuitionistic ones needed some work but not too much. Most of the proofs of the book are intuitionistic but some arguments and definitions are not:

1. Well-foundedness is defined in the classical way: no sequence can decrease indefinitely. This is of course replaced with Coq standard definition: every hereditary predicate is full. I remind that contrary to classical logic, those two definitions are not intuitionistically equivalent;
2. Similarily, strongly normalizable terms are defined as those which are accessible for the reverse of beta (or head or ...) reduction; Accessibility is defined in Coq as the least hereditary relation;
3. Proposition 3.18 page 53 is a instance of König's lemma which is a weak form of the axiom of choice. This can be replaced with an induction on the accessibility predicate that holds for strongly normalizable terms.
4. The definition of (strong) representation on page 32 that is used in the proof of the encoding of recursive functions into lambda terms uses a disjunction on the undecidable predicate of termination (of the computation of a recursive function). This needs to be replaced by an intuitionistic implication because you cannot intuitionistically break the disjunction P or not P when the predicate P is not decidable. So that definition of (strong) representation needed a more involved modification to be compatible with an intuitionistic setting.

In the course of the mechanization of those results, I did only find two reasonning mistakes that occur both in the original french textbook (1990) and in the english translation mentionned earlier. This is a very low error rate ! The page references and the numbering below correspond to R. Cori's translation:

1. Lemma 2.5 and 2.6 page 33: Lemma 2.5 states a result for every closed terms and is used in the proof of Lemma 2.6 for a term which contains a free variable. Fortunately, Lemma 2.5 can straightforwardly be generalized to arbitrary terms. So this is no big deal. Btw, I do not understand why the statement of Lemma 2.5 is restricted to closed terms.
2. On page 69, in the proof of the typability of strongly normalizable terms (Thm 4.17), the measure N(τ) which is used in that inductive proof does not always decrease. For instance N((v)t₁) = N(t₁) when v is a variable and t₁ is a strongly normalizable term. I recall that N(τ) measures the sum of the lengths of all the possible normalizations of τ. Correcting this mistake is a bit more complicated:
   • Either the measure has to be changed: for instance, the length of normalizations should not be the number of steps but the number of symbols used to write those normalizations. But this requires additional definitions.
   • Or combine the measure N(τ) with a measure of the size of τ into a lexicographic product (this is how it is done in the implementation).
   Besides changing the induction principle, the rest of the proof does not need to be modified.

I would like to point out two results which are also mechanized as consequences of that work and are not part of Krivine's book:

1. any total recursive function f : N → N can be represented by a Coq term t_f : nat → nat (which can be computed from the algorithm that describes f);
2. there exists a (computable) "universal" lambda term that, applied to the Church numerals, enumerates all the closed lambda terms up to beta equivalence.

The code is distributed under the CeCILL v2 Free Software Licence Agreement and can be accessed from the archive Lambda_Calculus_1.0.tar.gz. This archive contains a Makefile and the _CoqProject. It has been tested with Coq and CoqIde 8.5pl2.

This project is developed by Dominique Larchey-Wendling. The development is ongoing on Mercurial SCM repository on BitBucket. Please do not hesitate to contact me to get access to the development branch of the project.