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

Lambda calculus and surjective pairing

Date: Thu, 7 Mar 91 14:56:34 GMT+0100

		   A SIMPLE PROOF OF NON CONFLUENCE OF
		 LAMBDA-CALCULUS WITH SURJECTIVE PAIRING
				    by
		 Pierre-Louis Curien and The're`se Hardin

Recently I (Curien--ed) found a new counterexample showing the non
confluence of untyped Lambda-calculus extended with surjective pairing.
The proof was quite simple. The're`se Hardin then revisited my proof, and
the result is so strikingly simple and short that it seems to me that this
forum is an appropriate place for announcing this small result, with its
complete proof.

Indeed J.-W. Klop's original proof is quite involved (it makes use of a
standardization result, in particular). We hope that the following, very
elementary proof will be of some help to further popularize J.W. Klop's
insight.  The counter-example proposed here is indeed very close to Klop's
counter-example.

Let us recall the calculus:

Consider untyped Lambda-calculus, with three constants D, F, S, standing
respectively for pairing, first and second projection. (Or more simply
just a constant D.) Take as rules:

(beta)

D(Fx)(Sx)  -> x    (or more simply Dxx -> x)
F(Dxy) -> x
S(Dxy) -> y
(the two last rules are optional)

Consider
        B = YC   where C = YV  where V = \xy.D(F(Ey))(S(E(xy)))

(E is some variable, Y is Turing fixpoint).

(For the record, Klop's counter example is Y(Y( \xy.ED(Fy)(S(xy)))).)

One first observes, for any M:
(*)      CM ->* VCM ->* D((F(EM))(S(E(CM))).

One has thus
        B->*CB->*D((F(EB))(S(E(CB)))
        ->*D((F(E(CB)))(S(E(CB)))->E(CB)=def A
and
        B->* CB ->* CA  (since B->*A)

We shall show that A and CA cannot have a common reduct, thus that
the reduction is not confluent.

Any term K can be written uniquely as K = E(E(...(EK')...)) where K' is
not of the form EK''.  We say that those E's are K's head E's.  Take a
common reduct K of A and CA which has a minimum number of head E's. We
analize the reduction of CA to K.

First C and A are reduced independently.
        C -> (\z.z(Yz))V  (no choice)
        ->* (\z.zZ)V     (where Yz->*Z, hence C=YV->*Z[V/z])
        -> V(Z[V/z])
        ->* VC'  (where Z[V/z]->*C')
        ->\y.D(F(Ey))(S(E(C'y)))
        ->* \y.D(F(Ey))(S(EC''))   (where C'y->*C'')

Can surjective pairing be applied? Only if C'y->*y, which implies Cy->*y.
But one has, by (*), Cy ->* D((F(Ey))(S(E(Cy))). If Cy->*y, then
D((F(Ey))(S(E(Cy)))->*Ey, hence Cy->*Ey, and this provides a
counter-example to confluence. Thus we may assume that the independent
reduction of C stops as above. We have:

        CA ->* D(F(EA')(S(E(C''[A'/y])))    (where A->*A')
        ->* EQ    (where A'->*Q, C''[A'/y]->*Q)
        ->* K
(the only way to reach K which has the form EL is to apply
surjective pairing at some stage).

But observe:

a) Q has less head E's than K, since all the head E's of EQ are left
untouched by any reduction from EQ.

b) A->*A'->*Q  and CA->*C'A'->*C''[A'/y]->*Q
Thus Q is a common reduct of A and CA with less head E's than K:
contradiction.

PS: remark for Klop counterexample hackers: we believe that what makes
this version easier than Klop's original term is that in our example the
creation of new head E's is conditioned by the application of a surjective
pairing.

PPS: This counterexample came to my mind when trying to settle a
conjecture in the paper Exlicit substitutions (Abadi-Cardelli-Curien-
Le'vy, POPL 90), that a system of explicit substitutions with substitution
metavariables is not confluent. This conjecture is now settled, taking
profit of the countexample presented here, and the detailed proof will
appear in a new paper by Curien-Hardin-Le'vy, which will extend a paper by
Hardin-Le'vy, A Confluent Calculus of Substitution (presented at the
INRIA-ICOT meeting of November 89).

Thanks to Jean-Jacques Le'vy and Jon Willem Klop, who kindly read
this and made comments.