A mechanical proof of the Church-Rosser theorem

Reviewer: Doris C. Appleby

The Church-Rosser (CR) theorem, which dates from 1936, implies the consistency of Churchs lambda calculus, a formalization of function theory. In Shankars notation, X :2WZ Y if X and Y are lambda terms (functions of a single variable) and X can be reduced to Y through repeated use of the transformation rules. Shankar then states the CR theorem as “If X :2WZ Y and X :2WZ Z, then there exists a W such that Y :2WZ W and Z :2WZ W.” Because of the shape of a diagram representing the CR theorem, this relationship between X, Y, Z, and W is called the diamond property. Since the original proof of the CR theorem was inelegant and complicated, over thirty years were devoted to alternate methods. In 1972, Martin-Lo¨f published a much simplified proof based on lectures by W. Tait. This proof was later mechanized by deBruijn using the AUTOMATH proof-checking system. The Boyer-Moore theorem prover (BMTP) is closely related to the notation of the LISP programming language, which is itself based on the lambda calculus. Most theorems cannot be proved directly using the BMTP and must be structured through a series of lemmas, which are submitted to and verified by the BMTP, saved, and then used in the main proof. The BMTP is experimental and is continually being tested and improved. This paper presents a proof of the CR theorem that is based on the Martin-Lo¨fTait proof and is similar to the work of deBruijn. Shankar formalizes transformation rules using a process called a “walk,” which reduces term X to term Y through a series of steps, each of which preserves the diamond property. The proof is structured in five steps: (1)a formalization of the lambda calculus; (2)verification of the diamond property for walks following the deBruijn notation; (3)the Church-Rosser theorem; (4)proving that a reduction is the transitive closure of a walk for particular terms; and (5)translation back and forth between the standard lambda notation (recognized by the BMTP) and the deBruijn notation, which eliminates renaming of variables and thus simplifies the proof of the CR theorem. Although he presents no new results, Shankar claims that the proof tells us a great deal about the BMTP. Some of the complex lemmas are easier to convey to the BMTP than to express in English, counterexamples to failed theses are automatically generated, and proofs involving recursion or induction are accomplished in a particularly straightforward manner. This is a well-written paper that should be accessible to advanced undergraduates. It might be a good start for a student interested in formal methods of program verification. The complete code as presented to the BMTP is included in a fourteen-page appendix.