An Agda proof of the Church-Rosser theorem for a simply typed lambda calculus with general recursion.


An Agda proof of the Church-Rosser theorem for a simply typed lambda calculus
with general recursion.  I have checked it with Agda- and

I wanted to use a lambda calculus with general recursion because I wanted to be
sure that I could not "cheat" in my proof of the Church-Rosser theorem by using
strong normalization to lift local confluence to global confluence.  I added
general recursion to the simply typed lambda calculus (STLC) by adding fixpoints
of types for arbitrary (invariant) type functors.  This give both recursive
types and allows one to define a fixpoint combinator.

The STLC itself has no polymorphism, but one can use the polymorphism in Agda to
define terms polymorphically.  This allows one to simulate rank-1 polymorphism.

A simple, normal-order lambda calculus interpreter is also defined.

The proof of the Church-Rosser theorem very loosely follows the proof described
in "Church-Rosser Made Easy" by Dexter Kozen (DOI 10.3233/FI-2010-206).  I
define a type of terms with some subset of beta-redexes marked.  Redexes can be
marked in various "colours".  I defined a bottom-up traversal to reduce those
marked redexes for a subset of colours.  This traversal eliminates marked
redexes of those colours.  Redexes of other colours are tracked and may be
duplicated (or eliminated) by substitution.  The key lemma
(STLC.Marked.marked-reduce-twice) says that when you eliminate a subset of
coloured redexes this way, and then eliminate the rest of the colours, the
resulting term is the same as if you eliminated all marked redexes in a single

Types.agda         - Definition of types and type substitution for the STLC
Terms.agda         - Definition of terms and term substitution for the STLC
Beta.agda          - Definition of the "reduces to" relation on terms.
Normalize.agda     - A normal order STLC interpreter
Marked.agda        - Definition of terms with marked beta-redexes and bottom-up
                     reduction of marked redexs.
ChurchRosser.agda  - The Church-Rosser theorem.

Disclaimer:  This is not an official Google product (experimental or otherwise),
it is just code that happens to be owned by Google.