An Agda proof of the Church-Rosser theorem for a simply typed lambda calculus with general recursion.
root
An Agda proof of the Church-Rosser theorem for a simply typed lambda calculus
with general recursion. I have checked it with Agda-2.4.2.2 and
stdlib-2.4.2.3.
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
pass.
src/STLC:
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.