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

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.
----------------------------------------------------------------------