[Prev][Next][Index][Thread]
Re: Is extensionality equational in the absence of xi?

To: types@cis.upenn.edu

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

From: Peter Selinger <selinger@dead.stanford.edu>

Date: Thu, 15 Mar 2001 18:47:55 0800 (PST)

Cc: wadler@research.belllabs.com (Philip Wadler)

DeliveryDate: Thu Mar 15 21:51:57 2001

InReplyTo: <200103152347.f2FNlgG08938@saul.cis.upenn.edu> from "Peter Selinger" at Mar 15, 2001 03:44:20 PM
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 betaeta 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
> nonextensional 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 lambdabetaeta 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 lambdabetaeta 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
> >
> >
> >
> >
> >
>