completeness of equality for well-defined functions

[Abram Demski]

To those who know something about lambda calculus,

I found this book chapter:

http://www.cl.cam.ac.uk/teaching/Lectures/funprog-jrh-1996/chapter2.ps.gz

On pages 17-18 (section 2.3.6), eta-conversion is discussed. It sounds
as if what it is saying is that alpha-beta-eta convertibility *always*
holds when two lambda-calculus functions which are always-defined (ie,
reduce to a normal form for any arguments they are given) and give the
same results [modulo alpha-conversion perhaps] for all arguments. In
other words, that notion of equivalence is different from what one
might call mathematical equality *only* for expressions which don't
have normal forms, or functions which sometimes evaluate to such
expressions. Is this correct? It is really possible to write a program
that will prove two programs equivalent whenever such is the case and
neither programs contain infinite loops?

Thanks,

--
Abram Demski
http://dragonlogic-ai.blogspot.com/
http://groups.google.com/group/one-logic

[Luke Palmer]

On Mon, Dec 21, 2009 at 2:22 PM, Abram Demski <abram...@gmail.com> wrote:
> To those who know something about lambda calculus,
>
> I found this book chapter:
>
> http://www.cl.cam.ac.uk/teaching/Lectures/funprog-jrh-1996/chapter2.ps.gz
>
> On pages 17-18 (section 2.3.6), eta-conversion is discussed. It sounds
> as if what it is saying is that alpha-beta-eta convertibility *always*
> holds when two lambda-calculus functions which are always-defined (ie,
> reduce to a normal form for any arguments they are given) and give the
> same results [modulo alpha-conversion perhaps] for all arguments. In
> other words, that notion of equivalence is different from what one
> might call mathematical equality *only* for expressions which don't
> have normal forms, or functions which sometimes evaluate to such
> expressions. Is this correct? It is really possible to write a program
> that will prove two programs equivalent whenever such is the case and
> neither programs contain infinite loops?

I believe that is correct, but it is not as strong as you think. That
only applies to functions whose domains are the entire connected space
of functions. I.e. if you defined the naturals as a subset of lambda
terms, then it is possible to write two functions that agree on the
naturals and disagree elsewhere, and their terms will not be
convertible.

Luke

[Abram Demski]

Luke,

Hmm, is it possible to test whether something is a number or not, in
an always-terminating way? If so, your example could be taken care of
by wrapping the two functions in question with a function that takes a
function and returns the function modified to have some default output
when handed non-numbers. Then, the two modified functions would be
equal everywhere, therefore they would be provably equal everywhere,
therefore the original functions would be provably equal with respect
to numbers.

Something tells me this isn't possible. :) Perhaps one could use the
Y-combinator to construct an "infinite number" which would make any
such is-a-number predicate go into a non-terminating evaluation?

Also, do you know if there is any similar result for combinator
calculus? Is there a type of reduction that can be added to S and K
reduction to achieve the same sort of extensional normal form?

--Abram

> --
>
> You received this message because you are subscribed to the Google Groups "One Logic" group.
> To post to this group, send email to one-...@googlegroups.com.
> To unsubscribe from this group, send email to one-logic+...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/one-logic?hl=en.