The Coq mailing list

[Conor McBride <ctm AT Cs.Nott.AC.UK>]

Hi all

Oh no! The thing to ask yourselves is, as ever,...

> On Mon, 7 Aug 2006, Fabrice Lemercier wrote:
>
> > What about the following argument taken from
> > Wikipedia?
> >
> > if  f a==g a  for all lambda expressions a, then in
> > particular by taking a to be a variable x not
> > appearing free in f nor g we have  f x == g x  and
> > hence  ? x. f x == ? x. g x,  and so by eta-conversion
> > f == g.

roconnor AT theorem.ca
 wrote:
> You cannot go from f x == g x to \x. f x == \x. g x because in the 
> first case the two x's refer to the same binding, while in the second 
> case the two x's refer to different bindings.
>
> This argument doesn't seem sound in any reasonable lambda calculus, 
> and probably ought to be removed.
...which equality do you mean?

The argument Fabrice cites from Wikipedia is valid when == is taken to 
be the conventional alpha-beta-eta equality of the lambda-calculus. If 
you pick a fresh variable x, and confirm f x == g x, that's the same 
deal as checking \x.f x == \x.g x. Russell's worry about bindings isn't 
a problem in this free-to-bound direction: if you're equal wrt the same 
fresh free variable, then it's trivial to pick alpha-equivalent 
lambda-abstractions, as done above. It's the other way where you have 
the trouble: if \x.f x == \y. g y, then you don't necessarily get f x == 
g y.

However, none of this has anything to do with extensionality. The 
alpha-beta-eta equality is an intensional equality: the above hypothesis 
forall a, f a == g a is a very strong one, because it requires f and g 
to coincide /computationally/ on all argument /expressions/, even 
abstract fresh variables x which inhibit computation. The only way this 
coincidence can happen is that f and g have the same /implementation/.

The precondition for applying extensionality is much weaker, namely that 
the functions coincide /provably/ on all argument /values/. The 
conclusion of extensionality is that the functions are /provably/ equal, 
which is a rather strong statement in Coq. If you can prove two 
expressions are equal, that means they coincide computationally for any 
closed values instantiating their free variables. We should not be 
surprised that the latter fails to follow from the former. Again, 
quicksort and bubblesort are computationally distinct closed terms, so 
they are not provably equal, even though they agree on all inputs.

Equality, like the river-god in the tale about Hercules, is very 
slippery: you cannot trust it in casual conversation; to get the truth, 
you must grab it by the throat.

All the best

Conor


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.