typed versus untyped CR proofs

To: types@theory.LCS.MIT.EDU
Subject: typed versus untyped CR proofs
From: jr.hindley <majrh%PYR.SWAN.AC.UK@mitvma.mit.edu>
Date: Fri, 24 Feb 89 10:46:52 EST
Sender: meyer@theory.LCS.MIT.EDU

Date:       Fri, 24 Feb 89 15:25:13 GMT

To John Mitchell from Roger Hindley on confluence for typed
terms.

You are right, trying to prove the Church-Rosser theorem
for typed terms via the theorem for untyped terms will
give translation problems.

But why go to all that trouble?  Take any proof for untyped
terms and read through it, putting in types.  It stays valid.

For example, one can do this with the Tait-Martin-Lof proof
in either the form given in Barendregt's book or in the A

Appendix 1 to Hindley & Seldin 'Intro. to Combinators & \-calc.'

As remarked in H&S p.322, the main reason for the proof staying
valid is that contracting a redex in a typed term P does not
change the type of P.  So all the residuals of other redexes
when a redex R is contracted will have the same types as the
redexes they came from.  Or, if redex-residual arguments are not
to the reader's taste, the induction on structure that is at the
heart of Barendregt's exposition of the Tait-Martin-Lof proof
is not destroyed when types are added; it simply goes through
without change.

The reason I prefer not to deduce typed CR from untyped CR
is that I think of the typed system as being in a way simpler
than the untyped, because all its reductions terminate.
So CR for this system is in a way weaker than for untyped terms.
(As you say, it can be deduced from the termination property
and local confluence.)  So, why use a stronger result to get
a weaker, when a direct proof of the weaker is no longer?

Yours via Types-net,   Roger Hindley.