[Prev][Next][Index][Thread]
Confluence and SN property
Date: Thu, 23 Feb 89 22:40:26 -0500
The questions raised my John Mitchell about proofs of
confluence and related topics are of great interest to me,
and I will venture to make the following comments.
First, having been initiated to type theory only recently
(mostly by Val Breazu-Tannen and some visitors such as
Jean Yves Girard, Thierry Coquand, and Samson Abramsky), I apologize
in advance if I fail to give proper credit to people who
ought to be mentioned.
This being said, I have gone on a "binge" trying to understand
what makes Girard's proof of strong normalization really work
(for second order lambda calculus which I will call system F, and
its higher-order extension F_omega). This is a tough
battle, and I had to read quite a few papers.
I found a proof that confluence for F_omega holds under beta-conversion
in Girard's thesis (1972). The method used is basically that
of Tait and Martin Lof. Andre Scedrov has given a similar proof
(book from Boulder Conference, 1987).
Girard also adds product types (and other things)
and states the confluence property for this extended calculus
(but the proof is omitted). It is easy to fill in the details.
Of course, Girard proves strong normalization
for F_omega, and also for F_omega with product types (and other things).
These results for the simply-typed lambda calculus were reproved by
Pottinger and Lambek and Scott (and others).
Now, Girard does not consider eta-conversion, and there
are some subtelties for confluence. As Val Breazu-Tannen shows
in a paper with Thierry Coquand (Special
issue of TCS on TAPSOFT'87), confluence for eta-conversion
alone plus confluence for beta-conversion alone (for system F),
plus commutation of beta and eta, on terms that TYPE CHECK
(otherwise it's false!), and the Hindley-Rosen lemma yield
confluence of system F under beta/eta.
Gerard Huet in his thesis (1976) has a proof of confluence for
the simply typed lambda calculus. He first proves strong
normalization, and then verifies local confluence (both for beta and
eta).
One thing struck me when I was reading all these papers.
Girard in his proof (of SN) uses what I call a typed version of
the candidates of reducibility. By this, I mean that
he deals with indexed families of sets of typed terms satisfying
some properties (the famous CR conditions). This makes
the proofs notationally very involved. Also, with all due respect
to Jean Yves, the fact that he used the same notation for substitution
and for assigning candidates to typed variables, does not make
the proof as clear as it could be.
Tait (1973) in his version of the proof (of SN), uses an untyped version of
the candidates (i.e., sets of untyped terms), and what I
we refer to as the "erasing trick". It is also important to
note that he uses conditions different from Girard's CR's
(this fact was brought to my attention by Coquand).
Later versions of the proof of SN (or more accurately
for some of them, sketch of proof),
also use the erasing trick. It does reduce the complexity of the notation,
and allows a simpler definition of the sets that are assigned to types
(But BEWARE, it is easy to run into problems if one mixes
the untyped and the typed version of the proof).
Incidently, the erasing trick is also in Girard's thesis, but
it is not used to prove SN.
After reading Statman's proof of confluence for the simply typed
lambda calc. (under beta/eta), in which the type structure is
really used in the proof, and John Mitchell's clever extension
of Girard's result (in the erasing trick version) that
applies to sets other than SN terms, Val and I realized
that it is possible to prove confluence for system F
(and F_omega), under beta/eta, by using an adaptation of Girard's
typed version of the candidates, throwing in ideas from
Statman and Mitchell.
In fact, it is possible to prove simultaneously the SN property and
confluence for system F (under beta/eta), and also for F_omega.
My observations are that for SN, as long as reduction on types can be
shown SN, and terms and types are not mixed too much (like in
the theory of construction), the erasing trick works fine.
This is true for system F, and even for F_omega. I don't
know about the theory of constructions, but it is conceivable
that the trick of Harper, Honsell, and Plotkin used for LF
works.
For confluence, I am more skeptical that the erasing trick works,
because too much information can be erased,
and I would agree with Haper's message. However,
a typed version of the candidates, generalized as mentioned above,
works, at least for system F, and F_omega.
I don't know about LF or the theory of constructions, but I suspect
it can be made to work.
The typed version of the candidates seems crucial to prove
certain results. For example, it is used to prove
that adding a many sorted set of algebraic rewrite rules SN on algebraic
terms to system F yields a combined calculus that is also SN
(under beta/eta, and algebraic reduction).
This new result, as well as preservation of confluence when
the algebraic rewrite system is confluent, will appear
in a paper of Val and myself to be presented at ICALP'89.
Since I have been rambling on long enough, I will conclude by saying
that the details of the generalization of the typed version
of the candidates are in a paper that I have written
recently (On Girard's Candidats de Reductibilite).
In this paper, the CR conditions and Tait's conditions are also
compared, and in fact, it is shown that Girard's conditions
imply Tait's conditions. I also report all the bugs (small or big)
that I found in the various proofs I have seen. Most likely,
bugs will be found in my proofs, but c'est la vie!
Send me a note if you want a copy of this paper.
Jean Gallier