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
