The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 7 Aug 2006, Fabrice Lemercier wrote:

> > You cannot. Eta allows you to identify very similar
> > functions but not,
> > say, quicksort and bubble sort.
>
> 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.

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.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''