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

Re: Is extensionality equational in the absence of xi?

P.S.: in my attempt to answer Phil Wadler's question, I assumed that
the set A of equations he was looking for was supposed to consist only
of equations that are valid in the usual beta-eta sense (i.e., such
that (lambda-)+A is still contained in (lambda)+(ext)).

If one allows A to contain equations that are not consequences of
(lambda)+(ext), then my answer does not apply. And indeed, it is then
possible to find an equational theory which entails (ext): for
instance, the inconsistent theory (axiomatized by the single equation
x=y).

Perhaps more interesting is the question whether there is a consistent
set of equations that does the trick. -- Peter

Peter Selinger wrote:
> 
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> 
> 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
> > 
> > 
> > 
> > 	
> > 
>