Functional - is it possible to define equality within the lambda calculus?

Author

is it possible to define equality within the lambda calculus?

sxyz.xyzy@gmail.com

2007-05-03, 7:04 pm

Hi All,

I've been looking through references and I haven't been able to find a
definition of equality within the lambda calculus. Specifically, I'm
looking for something to fill in the ??? below

eq := \x\y. ???

Is it even possible? It seems like you have to take equality as
primitive (defined outside of the lambda calculus itself) because any
definition ends up being circular.

Thanks!

sxyz

2007-05-03, 7:04 pm

I didn't look here before posting. The answer seems to be 'no'.

http://groups.google.com/group/comp...7879bda5671d4a5

Pascal Costanza

2007-05-03, 7:04 pm

sxyz.xyzy@gmail.com wrote:
> Hi All,
>
> I've been looking through references and I haven't been able to find a
> definition of equality within the lambda calculus. Specifically, I'm
> looking for something to fill in the ??? below
>
> eq := \x\y. ???
>
> Is it even possible? It seems like you have to take equality as
> primitive (defined outside of the lambda calculus itself) because any
> definition ends up being circular.

I think your question is underspecified. What do you mean by "equality?"

Here are some papers that show that "equality" means a whole lotta
different things:
- http://citeseer.ist.psu.edu/grogono00copying.html
- http://www.nhplace.com/kent/PS/EQUAL.html
- http://home.pipeline.com/~hbaker1/ObjectIdentity.html

I can imagine implementing a notion of object identity in terms of the
lambda calculus - all you need is a mechanism that creates guaranteed
unique serial numbers, for example. This could be achieved by a global
counter, which could in turn be realized using a state monad.

So you could possibly "implement" an identity test. But is that what you
want?!?

Pascal

--
My website: http://p-cos.net
Common Lisp Document Repository: http://cdr.eurolisp.org
Closer to MOP & ContextL: http://common-lisp.net/project/closer/

Ivan Jager

2007-05-03, 7:04 pm

On 2007-05-03, sxyz.xyzy@gmail.com <sxyz.xyzy@gmail.com> wrote:
> Hi All,
>
> I've been looking through references and I haven't been able to find a
> definition of equality within the lambda calculus. Specifically, I'm
> looking for something to fill in the ??? below
>
> eq := \x\y. ???
>
> Is it even possible? It seems like you have to take equality as
> primitive (defined outside of the lambda calculus itself) because any
> definition ends up being circular.

What do you mean by equal? eq x y = \forall z, eq (x z) (y z) ? That can
be implemented about as well in lambda calculus as on any other computer
we have. :) (because AFAIK we still don't have anything better than a
turing machine)

If you just mean whether the two expressions are syntactically the same,
that requires looking at the syntax, which you can't do from within the
language. You still don't *need* to define equality as a primitive. You
could, for example, define a different primitive that will let you look
at the syntax, and then define syntactic equality in terms of that...

Now, if you want to assume x and y are church numerals, I'm sure you can
write a function to compare them. (Same would be true for any other
notion of equality that is computable on a turing machine.) So, it all
comes down to what you mean by equal.

Ivan

Chris Smith

2007-05-03, 7:04 pm

<sxyz.xyzy@gmail.com> wrote:
> I've been looking through references and I haven't been able to find a
> definition of equality within the lambda calculus. Specifically, I'm
> looking for something to fill in the ??? below
>
> eq := \x\y. ???
>
> Is it even possible? It seems like you have to take equality as
> primitive (defined outside of the lambda calculus itself) because any
> definition ends up being circular.

The answer, of course, is that given any decidable notion of "equality",
you can write a lambda combinator to decide it. There are combinators
for equality in all sorts of encodings of various data types into the
lambda calculus. You can even encode lambda terms themselves, and
compare them.

What you can't do is get at the syntax of the term itself, as someone
else pointed out.

--
Chris Smith

Sponsored Links