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-126.96.36.199 and stdlib-188.8.131.52. 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.