[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)?

There are two ways of reading the question, depending on whether
"(lambda-)+A is closed under (ext)" means:

1) every model of (lambda-)+A satisfies (ext), or

2) the (open) term model of (lambda-)+A satisfies (ext).

I think the first reading is the more standard one in this context,
but in any case it is worth pointing out the difference, to avoid
confusion.

Under the second reading, there certainly is an *infinite* set of such
equations: simply (recursively) add all equations M=N such that Mx=Nx
already holds. I don't know if there is a finite set.

Under the first reading, there is no set of equations, finite or
infinite, with Phil's property. If there was such a set of equations,
it would immediately imply the following:

Consequence: every quotient of an extensional lambda algebra is
extensional.

This is because equational properties are preserved by quotients.
Thus, if one can find an extensional lambda algebra with a
non-extensional quotient, this will show that the answer to Phil's
question is "no". I do not have my copy of Barendregt's book handy,
but if my memory serves me right, we can get an example as follows:

Consider the closed term algebra A of the lambda-beta-eta calculus
(with no constant symbols).  A beautiful construction by Plotkin shows
that this algebra is not extensional. (There are closed terms M and N
such that MP = NP for every *closed* term P, but not Mx = Nx).
However, the closed term algebra A' of the lambda-beta-eta calculus
with a single constant symbol *is* extensional. Finally, A is a
quotient of A' (just map the constant symbol to any closed term).

-- Peter


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