[Prev][Next][Index][Thread]
Confluence for typed terms
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