[Prev][Next][Index][Thread]
Update on Named Variables & Church Rosser.
Dear Colleague,
This to clarify any confusion that might have resulted from the two
postings in the thread: "Barendregt was right after all ... almost". The
issue being addressed is formalised proofs of equational properties of
higher-order languages.
Both Ford-Mason [FM] and Vestergaard-Brotherston [VB] take as their
starting point a presentation of the terms of the lambda-calculus which is
based on first-order abstract syntax with one-sorted variables (as a
first). However, from there-on the two lines of work differ both in
technology and in their aims.
[FM] initially defines alpha-equivalence classes and then proves
confluence for a beta-relation defined directly on the
alpha-equivalence classes. This involves the study of suitable proof
principles for the equivalence classes. The aim is to study the use
of the PVS theorem prover for practical programming language purposes,
such as establishing the CIU theorem for a general class of languages,
http://mcs.une.edu.au/~pvs/.
[VB] in contrast aims to formally justify pen-and-paper proof practices and
thus define all reduction relations at the level of the first-order
abstract syntax, as is common informal practice. Central parts of the
proofs are (i) the use of a formal variant of the Barendregt Variable
Convention to make the treatment of alpha and beta modular and (ii) the
formal study of the preservation and reflection of the confluence property
under the collapse of an equivalence relation. The approach has been
extended to a number of other equational properties both for the
lambda-calculus [VB,V] and for a calculus of linking with first-class
modules [Wells-V], http://iml.univ-mrs.fr/~vester/Writings/index.html.
In fairness, we should make reference to new work by Peter Homeier in
HOL, http://www.cis.upenn.edu/~hol/lamcr/. Homeier is similar in style
to [FM] but introduces different methods and thus proof principles for
dealing with alpha-equivalence classes.
FM & VB.