# Re: Is extensionality equational in the absence of xi?

```Philip Wadler wrote:

> Question: Is it possible to extend (lambda-) by a finite set of
> equations A such that (lambda-)+A is closed under (ext)?

(Recall that (lambda) is the theory whose derivation rules are:

(I)     (\x.M)N  =  M[x:=N]             (beta)
(II.1)  M = M                           (reflexivity)
(II.2)  M = N => N = M                  (symmetry)
(II.3)  L = M, M = N => L = N           (transitivity)
(II.4)  M = N => ML = NL                (congruence)
(II.5)  M = N => LM = LN                (congruence)
(II.6)  M = N => \x.M = \x.N            (xi),

that (lambda-) is (lambda) without rule (xi) and that rule (ext) is:

Mx = Nx => M = N, x not in M    (ext).)

This does not seem possible, according to the following.

Proposition   Let A be any finite set of equations M = N such that
M,N are closed and (lambda)+(eta) |- M = N.
(i)   There are closed beta-equivalent terms P,Q such that P = Q
cannot be derived from (lambda-)+A.
(ii)  There are closed eta-equivalent terms P,Q such that P = Q
cannot be derived from (lambda-)+A.

It follows that there is no finite set A of closed equations valid in
(lambda)+(ext) such that (lambda-)+A is closed under (xi). A fortiori
no such theory (lambda-)+A is closed under (ext) since (lambda-)+(ext)
is closed under (xi). Furthermore, no such theory (lambda-)+A is even
closed under the rule:

C[\x.Mx] = C[M], x not in M     (eta+)

Definition   Let us say that a closed term C is "indelible in an
equational theory (T)" if for all closed terms M such that
(T) |- C = M, C is a subterm of M.

Lemma of the Indelible Term   Let A be any finite set of equations
M = N such that M, N are closed and (lambda)+(eta) |- M = N.
Let C be a closed lambda-term such that:
- C is of the form C = \x.B[x],
- C occurs in no member of an equation of A,
- Every proper subterm of C is open.
Then C is indelible in (lambda-)+A.

The proposition above comes at once from this last lemma, whose proof
is detailed in the Appendix below. Indeed, any term C of the form
C = \x1...xn.x1 and larger than all the members of the equations of A
fulfills all the assumptions of the lemma and is therefore indelible
in the theory (lambda-)+A. Consequently, we do not have:

(lambda-)+A  |-  C = \x1...xn.(\z.z)x1,
nor:
(lambda-)+A  |-  C = \x1...xn z. x1 z.

It is very likely in my opinion that we have more generally:

CONJECTURE:  For all finite set A of equations with closed members,
if the theory (lambda-)+A is consistent, then it is not closed under
rule (xi) nor (ext).

Luckily, this conjecture is trivial in its most unusual subcase, i.e.
in case (lambda-)+A is consistent but not (lambda)+A as for e.g.:

A = {Omega = \xy.x, Omega' = \xy.y},

where Omega = (\x.xx)(\x.xx) and Omega' = (\x.(\z.z)xx)(\x.(\z.z)xx).

At last, the above proposition can straightforwardly be extended to
sets A of equations valid in the theory (H) = (lambda)+(eta)+U, where
U is the set of the equations M = N such that M and N are unsolvable
closed terms (see [Bar84], Definition 4.1.6): We only have to add the
contraction rule (Omega):

M -> Omega, if M is unsolvable and M # Omega,

to the reduction relation ->>bec in the proof of the Lemma of the
Indelible Term below. We can derive from this slight generalization
that the above conjecture also holds for semi-sensible theories (i.e.
in case (lambda)+A does not equate a solvable term with an unsolvable
one), but this does not bring us much nearer a general answer.

Thierry Joly.
--
[Bar84] H.P. Barendregt, The Lambda-Calculus, North-Holland, 1984.

Original message by Phil Wadler:

> The theory (lambda) has the following derivation rules:
>
>       (I)     (\x.M)N  =  M[x:=N]             (beta)
>       (II.1)  M = M                           (reflexivity)
>       (II.2)  M = N => N = M                  (symmetry)
>       (II.3)  L = M, M = N => L = N           (transitivity)
>       (II.4)  M = N => ML = NL                (congruence)
>       (II.5)  M = N => LM = ZL                (congruence)
>       (II.6)  M = N => \x.M = \x.N            (xi)
>
> In the presence of these rules, then extensionality
>
>               Mx = Nx => M = N                (ext)
>
> is equivalent to (eta)
>
>               \x.Mx = M                       (eta)
>
> Define (lambda-) to be (lambda) without rule (xi).  It is easy
> to check that (lambda-)+(ext) is closed under (xi).
>
> Question: Is it possible to extend (lambda-) by a finite set of
> equations A such that (lambda-)+A is closed under (ext)?
>
> We cannot solve this trivially by taking A=(ext) or A=(eta)+(xi),
> because A must be a set of equations of the form M=N, which rules
> out conditional equations like (ext) and (xi).
>
> For combinatory logic CL there is such a set of equations, called
> A_beta_eta, see Barendregt 7.3.15.  Further, CL+A_beta_eta is provably
> equivalent to (lambda)+(ext), but this proof relies on (xi).
>
> Cheers,  -- P
----------------------------------------------------------------------

APPENDIX : Proof of the Lemma of the Indelible Term

Convention:  Every lambda-term is considered here up to the
alpha-renaming of its bound variables, hence the symbol =
between lambda-terms actually denotes alpha-equivalence.

Notation:  Let /\ be the set of every (possibly open) untyped
lambda-term.

Definition I  (i)  (lambda) is the theory whose derivation rules are:

(I)     (\x.M)N  =  M[x:=N]             (beta)
(II.1)  M = M                           (reflexivity)
(II.2)  M = N => N = M                  (symmetry)
(II.3)  L = M, M = N => L = N           (transitivity)
(II.4)  M = N => ML = NL                (congruence)
(II.5)  M = N => LM = LN                (congruence)
(II.6)  M = N => \x.M = \x.N            (xi)

(ii)  (lambda-) is the theory (lambda) without rule (xi).

Definition II  Let us say that a closed term C is "indelible in an
equational theory (T)" if for all closed terms M such that
(T) |- C = M, C is a subterm of M.

General Assumptions:

(1)   A is a finite set of equations M = N such that M,N are closed
and (lambda)+(eta) |- M = N,
(2)   C = \x.B[x] is a closed lambda-term,
(3)   C occurs in no member of an equation of A,
(4)   Every proper subterm of C is open.

The rest of this note is devoted to a proof that under the above
General Assumptions, the term C is indelible in (lambda-)+A.

Definition III  (i)  Let /\c be the set of the (possibly open) untyped
lambda-terms built with the help of an additional constant c.

(ii)  Let M |-> M* be the map of /\ into /\c inductively defined by:

.  x* = x  if x is a variable,
.  (MN)* = M*N*,
.  (\x.M)* =  .  c      if \x.M = C,
.  \x.M*  otherwise.

Lemma 1  For all M in /\:
(i)   C is not a subterm of M*.
(ii)  M*[c:=C] = M.
(iii) For all P in /\, P[c:=C]=M and C does not occur in P => P=M*.
(iv)  If C does not occur in M, then M* = M.
(v)   For all closed N in /\, (M[x:=N])* = M*[x:=N*].

Proof  (i),(ii),(iii).  By straightforward inductions on M.
(iv)  Apply (iii) with P = M.
(v)   Every closed subterm Q of P = M*[x:=N*] must satisfy at least
one of the following:

.  Q is a subterm of M*,
.  Q is a subterm of N*,
.  N* is a proper subterm of Q,

according to its position in P relatively to the ones of the N*'s
substituting the occurrences of x. Since C does not fulfill any of
these conditions by (i) and General Assumption (4), C does not occur
in P; moreover, by (ii):

P[c:=C] = (M*[x:=N*])[c:=C] = (M*[c:=C])[x:=N*[c:=C]] = M[x:=N].

Hence by (iii), we have P = (M[x:=N])* and (v) follows.
Q.E.D.

Definition IV  (i)  Let ->b, ->e, ->c be the least compatible (i.e.
closed under the rules of congruence and xi) relations defined
on /\c^2 such that:

(\x.M)N  ->b  M[x:=N]   for all M,N in /\c,
\x.Mx  ->e  M         for all M s.t. x not free in M
cM  ->c  B[M]      for closed M of /\c only.

(ii)  Define ->bec by:  M ->bec N  iff  M ->b N, M ->e N or M ->c N.
(iii) =bec is the reflexive, symmetrical & transitive closure of the
relation ->bec.
(iv)  ->>bec is the reflexive & transitive closure of ->bec.

Proposition 2  For all closed terms M,N of /\:

(lambda-)+A |- M = N   =>   M* =bec N*.

Proof  Let (lambda-o) be the theory (lambda-) whose rule :

(I)     (\x.M)N  =  M[x:=N]             (beta)

is restricted to the case where N is a closed term. Let M,N be any
closed terms of /\ and suppose that D is a formal derivation tree of
(lambda-)+A |- M = N. It is easily checked that by replacing every
open variable with \x.x in all the members of the equations of D, we
get a correct derivation tree of (lambda-o)+A |- M = N. Therefore, we
only have to establish:

(lambda-o)+A |- M = N   =>   M* =bec N*.

Let us prove M* =bec N* for all M,N of /\ s.t. (lambda-o)+A |- M = N
by induction on the derivation of M = N:

- If the last rule of the derivation is (II.1), (II.2) or (II.3),
then the conclusion follows at once from the induction hypothesis,
since =bec is an equivalence relation.
- If the last rule is a congruence rule, say (II.4), then M = M'L,
N = N'L and M=N is a direct consequence of M'=N'. By ind. hyp. we
get:  M'* =bec N'*  and  M* = M'*L*  =bec  N'*L* = N*.
- If the equation M = N is obtained from rule (I), then we have:
M = (\x.P)Q  and  N = P[x:=Q] for some P,Q of /\ such that Q is
closed.
. If \x.P = C, then by lemma 1 (iv): B[x] = P = P* and thus:
M* = cQ* =bec  B[Q*] = P*[x:=Q*] = N*, by Lemma 1 (v).
. Otherwise, M* = (\x.P*)Q*  =bec  P*[x:=Q*] = N*, by Lemma 1
(v) again.
- At last, if M = N is an equation of A, then by Lemma 1 (iv) and
the General Assumption (3), we get: M* = M and N* = N. Therefore,
M* =bec N*, because M,N are beta-eta-equivalent according to the
General Assumption (1).
Q.E.D.

Definition V  (i)  Let /\'c be the set of the terms M whose syntax is
given by:  M  =  x (variable) | c | MM | <M> (*) | \x.M
(*) only if M is closed.
(ii)  Let ->b', ->e', ->c' be the least compatible (i.e. closed
under the rules of congruence and xi) relations defined on
/\'c^2 such that:

(\x.M)N  ->b'  M[x:=N]   for all M,N in /\'c,
\x.Mx  ->e'  M         for all M s.t. x not free in M,
c M  ->c'  B[M]      for all closed M of /\'c,
<M>  ->c'  B[M]      for all closed M of /\'c.

(iii) Let  M ->bec' N  iff  M ->b' N, M ->e' N or M ->c' N.
(iv)  ->>bec' is the reflexive & transitive closure of ->bec'.
(v)   Let M |-> |M| and f be the maps of /\'c into /\c inductively
defined by:

. |x| = x,              . f(x) = x,
. |c| = c,              . f(c) = c,
. |MN| = |M| |N|,       . f(MN) = f(M)f(N),
. |<M>| = c |M|,        . f(<M>) = B[f(M)],
. |\x.M| = \x.|M|,      . f(\x.M) = \x.f(M).

Lemma 3  For all M,N of /\'c and all T of /\c:

(i)   f(M[x:=N]) = f(M)[x:=f(N)]
(ii)  f(B[M]) = B[f(M)]
(iii) |M| ->>c f(M), where ->>c is the refl.& trans.closure of ->c.
(iv)  M ->>bec' N  =>  f(M) ->>bec' f(N)
(v)   |M| ->>bec T => M ->>bec' Q, |Q| = T for some Q of /\'c.

Proof  (i),(iii).  By straightforward inductions on M.
(ii)  Check more generally by induction on a context C[ ] with no < >
that f(C[M]) = C[f(M)].
(iv)  We can prove:  M ->bec' N  =>  f(M)->>bec f(N)  by induction
on M, using (i) in case:  M = (\x.P)Q ->b' P[x:=Q] = N  and (ii) in
case: M = cP or <P>, M ->e' B[P] = N. (iv) follows by transitivity.
(v)   First suppose |M| ->>bec T is one step reduction ->r (r=b,e,c).
Then T is obtained by contracting a r-redex in |M| and Q can be
obtained by contracting the corresponding r-redex in M. The general
statement follows by transitivity.
Q.E.D.

Lemma 4  (Strip Lemma)
c
M --------> R
|           |
bec|            bec
|           |         M,N,R,S in /\c.
V           V
V     c     V
N - - - ->> S

Proof  We have: M = C[cT] ->c C[B[T]] = N for some C[ ] and T. The
term P = C[<T>] then satisfies: |P|=M & f(P)=R. Hence, |P| ->>bec N
and by Lemma 3 (v), there is Q in /\'c such that P ->>bec' Q, |Q| = N
and the diagram can be completed with the help of Lemma 3 (iii),(iv):

c
M=|P| --------> R=f(P)
|               |
bec|                bec
|               |
V               V
V       c       V
N=|Q| - - - ->> S=f(Q)
Q.E.D.

Proposition 5  ->>bec has the Church-Rosser property.

Proof  We get by transitivity from the Strip Lemma:
c
M ------->> R
|           |
bec|            bec
|           |         M,N,R,S in /\c.
V           V
V     c     V
N - - - ->> S

In particular, ->>c commutes with ->>be and itself; moreover, the
relation ->>be has the Church-Rosser property, according to [Bar84]
(Chapter 3, Theorem 3.3.9 (i)):

c                    c                   be
------->>            ------->>            ------->>
|         |          |         |          |         |
be|          be       c|          c       be|          be
|         |          |         |          |         |
V         V          V         V          V         V
V    c    V          V    c    V          V   be    V
- - - ->>            - - - ->>            - - - ->>

Hence, by Proposition 3.3.5 (i) of [Bar84], the relation ->>bec has
the Church-Rosser property.
Q.E.D.

Since the term c is bec-normal, it follows from Corollary 3.1.13 of
[Bar84] that:

Corollary 6  For all M of /\c:  M =bec c  =>  M ->>bec c.

Proposition 7  The term C is indelible in (lambda-)+A.

Proof  Suppose  (lambda-)+A |- M = C, where M is a closed term of /\.
We have then from Proposition 2: M* =bec C* = c; hence, by Corollary 6
M* ->>bec c. The constant c must therefore occur in M*, otherwise all
the terms P s.t. M* ->>bec P would belong to /\. At last, it follows
from Lemma 1 (ii) that the term C occurs in M = M*[c:=C].

Q.E.D.
----------------------------------------------------------------------
```