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: Wed, 22 Feb 89 19:06:38 EST
Sender: meyer@theory.LCS.MIT.EDU

Date: Wed, 22 Feb 89 16:58:04 EST

I think confluence arguments which proceed via erasure must leave out
some interesting cases.  We know due to Klop's example that the Church-
Rosser fails in the type-free lambda-calculus with surjective pairing, but
it holds in the simple typed lambda-calculus with eta-reduction and
surjective pairing --- see my paper "The Church-Rosser Theorem for the
Typed Lambda-calculus with Surjective Pairing", Notre Dame Journal of
Formal Logic, vol. 22 (1981), pp. 264-268.

The argument given in the paper just cited applies to a calculus in which
types are assigned to terms once and for all.  Confluence is derived from
a proof of local confluence for a restricted kind of reduction called
predicative reduction, but a strong normalization argument is NOT used
in the proof.

Hope that helps.

Regards,

Garrel Pottinger