[Prev][Next][Index][Thread]
confluence for typed terms
Date: Mon, 20 Feb 89 16:01:11 PDT
I have some questions and comments regarding confluence for
beta,eta-reduction on typed lambda terms (just simple types
at the moment, but comments on fancy types are welcome).
1) The only published proof I know of is in Statman's
I&C article on logical relations. Are there any others?
In Barendregt's succinct but very informative Appendix,
confluence is left as an exercise.
2) Apart from the logical relations proof, there is another
proof which seems to be folklore (or perhaps it was published
in the 40's). I will sketch this below. Can anyone tell me
where this proof comes from, or if it is published?
"Folk Proof"
There are two common formalizations of the syntax of typed
lambda terms. In one, we use contexts and write the type
of each variable as part of the term. This is the syntax
I prefer, primarily because it generalizes to other type
systems. The alternative is to assume a fixed type for each
variable. I would like to consider the first one first.
Let me try to illustrate the subtlety involved by starting
with a confluence proof outline P-L Curien sent me recently.
"Here is my way of dealing:
erase takes a typed term into its untyped underlying term.
Fact 1: If C|-M->N:a, then erase(M)->erase(N)
Fact 2: If C|-M:a and erase(M)->P then for some N
C|-M->N:a and erase(N)=P
Fact 3: If C|-M:a, C|-M':a and erase(M)=erase(M'), then M=M'
If these are satisfied, then untyped CR will
transfer to typed CR straightforwardly."
Given Facts 1-3, the proof should go as follows.
Suppose typed term C |- M:a reduces to terms N, P
which have the same types in same context (i.e.,
C |- N:a and C |- P:a). We must find term C |- Q:a
with N --> Q and P --> Q. By Fact 1, we have
erase(M) --> erase(N) and erase(M) --> erase(P).
Therefore, by untyped CR, there is untyped R with
erase(N) --> R and erase(P) --> R. By Fact 2, there
is a typed term C |- Q:a with erase(Q) = R and
N --> Q. Similarly, there is a typed term C |- Q':a
with erase(Q') = R and P --> Q'. Now by Fact 3,
we use erase(Q) = erase(Q') to conclude Q=Q'.
This completes the proof.
What I like about Curien's way of putting this is the
explicit use of Fact 3. The problem is that I don't think
"Fact 3" is really true. For example, consider
the terms (\x:a->a. z)(\y:a. y) and (\x:b->b'. z)(\y:b. y).
These have the same type (the type of z), and have syntactically
identical type erasures. However, they are neither
syntactically identical as typed terms, nor alpha
convertible. So the proof breaks down on this point.
(Of course, these terms have a common reduct, so this
a counterexample that can be "patched", This seems the
best we can do, since we can't expect to find
a counterexample to Church-Rosser.)
Another question:
3) Can this proof be fixed?
I am indebted to Furio Honsell for bringing this
issue to my attention several years ago. Some related
discussion appears in the theses of Nederpelt and
van Dalen.
Incidently, the "method" outlined by Curien works for SN,
since we do not need Fact 3. In other words, we may prove SN
for typed terms by proving SN for the erasures.
I published an SN proof (really a restatement
of Girard's proof) using this idea (1986 Lisp and FP conf.),
then found out Tait had written much the same proof some
years earlier. A year later (1987 Boulder category theory
and CS workshop, I think), Barendregt also presented
this proof.
In discussing this situation with Curien, he also pointed out
the following proof method:
Once SN is established, by one way or another, confluence reduces
to local confluence. Thus one way of proving typed CR is to prove
typed local confluence, and this can be done by mimicking the proof
of local confluence of the Lambda-calculus (not a transfer!). A
reference where this is carefully done, in a very great generality
of a very powerful labelling system, is Jean-Jacques Levy's thesis
(Reductions correctes et optimales dans le Lambda-calculus).
I also recall from a discussion with Val Breazu-Tannen a year or
so ago that we were able to agree on the following proof:
Suppose that instead of writing
\x:a.(...), we fix the types of variables. If we restrict alpha
conversion in untyped terms, then we may regard the typed terms
as a subset of the untyped terms, and typed reduction as the
restriction of untyped reduction to this subset. Then
proof outlined by Curien goes through, provided we verify
confluence for the modified version of untyped calculus.
This seems like a reasonable proof if one is familiar with
the untyped proof, but i think it is a bit
more work than the logical relations proof otherwise.
Also, I don't see how to apply it directly to the syntax
with \x:a(...).
Finally, if we drop eta then the situation is somewhat simpler.
For example, Val pointed out to me that Martin-Lof proves
in his 1971 Type:Type paper that beta is CR for all "raw" terms
(terms with types given to variables, but which may not be
well-typed). I think that perhaps Aczel's general method applies
to this case too, but I don;t remember exactly.
John