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
Lambda-Calculus: Types and Models
by Jean-Louis Krivine
All the principal results of chapters 1-4 and 6 are implemented, including the translation from
recursive functions into lambda terms and the characterization of strongly normalizable terms
using typability in system D:
- 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"
- 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:
- 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
- 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;
- 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.
- 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:
- 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.
- 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)t1) = N(t1) when v is a variable and t1 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
Besides changing the induction principle, the rest of the proof does not need to be modified.
- 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
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).
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:
The first result establishes formally that the Coq well-founded recursion
scheme is powerful enough to be able to represent any total computable function.
- any total recursive function f : N → N can be represented by
a Coq term tf : nat → nat (which can be computed
from the algorithm that describes f);
- there exists a (computable) "universal" lambda term that, applied
to the Church numerals, enumerates all the closed lambda terms up to
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.