The Church-Rosser Theorem for the Lambda Calculus

A Proof in Higher Order Logic


For many years the Church-Rosser theorem has been a milestone in the treatment of the lambda calculus. It describes the confluence property, that if an expression may be evaluated in two different ways, both will lead to the same result. This paper describes a formulation of the proof within the Higher Order Logic (HOL) theorem prover. This follows the proof by Tait/Martin-Löf, preserving the elegance of the classic presentation by Barendregt. In particular, we justify for this proof the controversial Barendregt Variable Convention (BVC), which to some seemed unsound given the possibility of capture. This work exemplifies a prototypical foundation for analyzing general programming languages.

This page gives information about this proof of the Church-Rosser theorem. It contains postscript and PDF versions of the paper. It also contains the full source code for the Higher Order Logic theorem prover to perform all proofs described in the paper. In addition, this page describes packages of supporting software, which supply needed tools to support the automated proof in the Higher Order Logic theorem prover.

Papers

A Proof of the Church-Rosser Theorem for the Lambda Calculus in Higher Order Logic (PDF).
Briefing charts in postscript and PDF.
Given as a Category B paper at TPHOLs'2001, the 14th International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, September 3-6, 2001.

Quotient Types (PDF).
Briefing charts in postscript and PDF.
Given as a Category B paper at TPHOLs'2001, the 14th International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, September 3-6, 2001.

Software

Proof of the Church-Rosser Theorem for the Lambda Calculus

Here is a complete proof of the Church-Rosser Theorem for the Lambda Calculus, in source code for the Higher Order Logic theorem prover, version Hol98 Taupo-5 or Taupo-6. This is version 1.2 of this proof, as of August 31, 2001.
lamcr12.tar.gz. (Compressed tar archive, 118,589 bytes)

The source code for this proof also contains all the software packages mentioned below.

Quotient Types

Here is a package for creating a new type as the quotient of an existing type, divided into equivalence classes according to an equivalence relation. The package creates the new quotient type, defines functions to map back and forth between the old and new types, and proves theorems about their behavior. It also supports defining a family of new types with the same pair, sum, and list structure as the original types.
Paper: postscript and pdf.
Code: quotient.sig and quotient.sml.

Mutually Recursive Rule Induction

Myra Van Inwegen has written a package for defining relations by mutually recursive rule induction. This package automatically proves theorems for the new relations' rules, the inversions of the rules, and weak and strong rule induction principles. The package has been ported to Hol98, version Taupo-5 or Taupo-6.
Code: ind_rel.sig and ind_rel.sml.
Myra's original version was for Hol90.

Mutually Recursive Structural Induction

Using Hol98 version Taupo-5, one can create mutually recursive types using the Hol_datatype function. In addition, one can define mutually recursive functions according to the recursive structure of the types. However, there is no automation provided in the standard Taupo-5 system to prove theorems about these functions by mutually recursive structural induction. This capability is now provided here as a tactic, MUTUAL_INDUCT_THEN.
Code: MutualIndThen.sig and MutualIndThen.sml.

Conditional Rewriting

Here is a package to do rewriting of goals by the conclusions of implications, even if the antecedents have not yet been proven. The author calls this "conditional rewriting."
Code: cond_rewrite.sig and cond_rewrite.sml.

The author appreciates all comments. See the documentation for email address.

People

Papers

Related Sites on HOL