Confluence for typed terms

To: types@theory.LCS.MIT.EDU
Subject: Confluence for typed terms
From: oravax!garrel@wrath.cs.cornell.edu (Garrel Pottinger)
Date: Thu, 23 Feb 89 13:43:16 EST
Sender: meyer@theory.LCS.MIT.EDU
Date: Thu, 23 Feb 89 11:33:33 EST
To: jcm@ra.stanford.edu, types@theory.LCS.MIT.EDU

In my second message on this subect, I suggested taking \ x:A.X as
shorthand for R A (\ x.X), where the latter term is supposed to
stand for the result of restricting the value of \ x.X to the the
type for which A stands.  Along the way, I used this idea to analyze
the behavior of the term \ x:y.(\ x:z.x)x in a calculus where we
we have just a  single style of variable, observing that the apparent
conflict with confluence which results from using "eta-conversion"
vanishes if we work things out via R and real eta-conversion.  The
purpose of this note is to point out that the Church-Rosser does, indeed,
fail in the calculus with R, but, as it seems to me, it fails in
an illuminating way.

In order to fix ideas, let me say for the record that I will be discussing
a calculus where terms are built up from variables and R by means of
application and ordinary, unlabelled lambda abstraction.  Reduction
and conversion are defined from the following contraction rules in the
usual way:

(beta) (\ x.X)Y contr Sub[Y/x/X]

(eta)  \ x.X x contr X, provided x is not free in X

(R)    R X Y Z contr Y Z

I use "inflation" to denote the converse of reduction.

Now, in the calculus just described, we have:

R infl \ x.\ y.\ z.R x y z     (eta), three times

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

  red  \ x.\ y.y               (eta)

and, since R and \ x.\y.y are normal, the Church-Rosser fails.

Given what R is supposed to mean, it's hardly surprising that something
has gone wrong here --- there is no semantical basis for the step
licensed by (R), since nothing tells us that x has a type as its value,
y has a type of the form x >-> w, and z : x.  And, obviously, nothing
could tell us this, so things go wrong becuase we have tried to use
R in a situation where we can't say anything about types.  This is silly,
becuase we need types to describe correctly how R should behave.

It is perhaps worth observing that if we drop (eta) from the calculus
under discussion, then we get a calculus in which the Church-Rosser
does hold.  This can be proved by considering the multivariate lambda
calculus, in which \ x1 ... xn.X is NOT identified with \ x1. ... \ xn.X
if n > 1.  In the multivariate calculus, redexes have the form
(\ x1 ... xn.X) Y1 ... Yn, and if m < n, then (\ x1 ... xn.X) Y1 ... Ym
is NOT a redex.  It turns out that the Church-Rosser holds for the
multivariate calculus and mapping R to \ x y z.y z will embed the calculus
discussed above, less (eta), isomorphically in the multivariate calculus.
This suffices to prove the Church-Rosser for the calculus in question.

I close with (1) a remark that runs back to my first message on confluence
for typed terms and (2) a commercial.

Remark:  I think this message and the one immediately preceding it provide
considerable further evidence that arguments based on type erasure aren't
the way to go about dealing with confluence for typed terms.

Commercial:  The multivariate lambda calculus is really pretty neat.  If
your interest is piqued, send a note to me asking for a copy of "A Tour
of the Multivariate Lambda Calculus".

Regards,

Garrel Pottinger