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