confluence for typed terms

To: types@theory.LCS.MIT.EDU
Subject: confluence for typed terms
From: Robert Harper <Robert.Harper@proof.ergo.cs.cmu.edu>
Date: Thu, 23 Feb 89 20:48:55 EST
In-Reply-To: Your message of Mon, 20 Feb 89 21:21:58 -0500. <8902210221.AA03615@stork.LCS.MIT.EDU>
Sender: meyer@theory.LCS.MIT.EDU

Date: Thu, 23 Feb 89 15:59:57 EST

Garrel Pottinger's R combinator is reminiscent of the reduction given in
Harper, Honsell, and Plotkin "A Framework for Defining Logics."  There we use
a similar translation to prove strong normalization for the LF lambda calculus
(which not only has type labels but there are reductions within labels.)  I
have tried to adapt the SN argument to CR, and believe that it cannot work.

First, if I understand Pottinger's note correctly, then the system he
describes is not Church-Rosser.  That is, if we take as the following rule
of reduction

		R A X Y  =>  X Y

then we get the following incompleteable split:

		R y (\x. R z (\x.x) x)

		       R/\eta
		       /  \
      R y (\x. (\x.x) x)  R y (R z (\x.x))

Only the left-hand side has a redex, and its contractum is R y (\x.x).

If instead we take the reduction rule

		R A X  =>  X

then the system is Church-Rosser since we can define R to be \uv.v.  (It seems
that the former R isn't definable similarly because we want to rule out
reduction of R A X; otherwise you get just this case.)

Unfortunately does not seem to help in a proof of Church-Rosser for the
original calculus with type labels because if you study the completion of the
diamond in the calculus with R (whether or not R is a primitive), you will
see that in certain cases the completion involves reductions that may not be
mimicked in the original term.  That is, we cannot "lift" the diamond from the
calculus without labels to the calculus with labels.

Moreover, it seems to me that a proof based on logical relations cannot work
for systems with reductions in the type labels.  The reason is that it seems
to be crucial to a logical relations-based proof that if Mx has the desired
property (WCR,CR,SN,...), then M does (where x is a variabe and M is a labeled
term).  This property does NOT hold for Church-Rosser because the split can
occur in the label as in

	(\x:BAD.M) x

Since we may always throw away BAD by a beta-reduction, the whole term is WCR
if M is, but \x:BAD.M is, by hypothesis, not WCR.

I have another idea for a proof using "intro-based" rather than "elim-based"
logical relations (see Prawitz's "Ideas and Results in Proof Theory" for a
discussion), but I have not yet had time to work out the details.  The point
is to admit a lambda abstraction into a function space only if the label has
the property (WCR,CR,...); an elim-based approach admits anything that behaves
right when applied, which we saw is too weak.

Bob Harper