[Prev][Next][Index][Thread]

On confluence of simply typed Beta

Date: Wed, 2 May 90 22:50:08 +0200

I would like to communicate the following proof of confluence of Beta
in the simply typed Lambda-calculus, which makes use of weak
normalization only. It stands as a nice curiosity between the proofs
which mimick the proof of untyped Beta+Eta confluence, and those which
rely on strong normalization. It is an illustration of the following
general technique to transfer confluence from a system to another.

Let me first explain the general technique. One may establish the
confluence of a system A, by making use of a translation of A into a
system B via a mapping G s.t.

        A1) B is confluent
        A2) A is weakly normalizing
        A3)  If a -> a' in A, then G(a) and G(a')  are B-interconvertible
        A4) G translates A-normal forms injectively to B-normal forms.

It is easy to see that A1-A4 entail the confluence of A.

        Here is how I use the technique to show the confluence of Beta
in the simply typed Lambda-calculus. It is rather easy to prove strong
termination of the following restriction of the b- reduction:
        (Lambda x.M)N -> M[N/x] only when N is in normal form.  Here
is a short argument, adapted from, say the book of
Girard-Lafont-Taylor, chapter 4: with every term P associate the
multiset of the degrees (i.e. the size of the type A[B of lx.M) of the
redexes (Lambda x.M)N of P. Then the restricted reduction relation
strictly decreases this measure (the fundamental fact being that
created redexes have smaller degrees than the creating redex).
        It is also easy to show that the restricted relation is still
locally confluent.
        Now take Beta as A, restricted Beta as B, and identity as G.
A1,A2 and A4 clearly hold. We show A3 as follows. Suppose (Lambda
x.M)N is an unrestricted redex. Let P be the restricted normal form of
N. Then the following sequence of equalities is provable in the
restricted system B:
        (Lambda x.M)N = (Lambda x.M)P = M[P/x] = M[N/x]

Is this technique known in anyway? I know for example that the same
general technique, but without axiom A2, which then allows to
establish the unique normal form property, has been fruitfully applied
by J.-W. Klop and R. de Vrijer to establish the unique normal form
property of Lambda-calculus with surjective pairing.

I, together with Giorgio Ghelli, made recently an extensive use of
this general technique to show the confluence of various reduction
systems (including Beta+Eta+"terminal object") in the system F<:, a
second order Lambda-calculus with bounded quantification and a maximum
("terminal") type. These results will appear as a tech report before
the summer.

We would be interested about possible other uses of the technique.

Pierre-Louis Curien