Lambda calculus + Church numerals

From: Paul Neave
Subject: Lambda calculus + Church numerals
Date: Tue, 23 Jan 2001 14:23:21 +0000
Message-ID: <94k44p$gcf$2@m1.cs.man.ac.uk>

I've got a few questions on Church numerals, if anyone's heard of them before.
Church numerals represent numbers as terms of untyped lambda-calculus as:
Cn = lambda f. lambda x. fn(x)
where f0(t) = t
and   fn+1(t) - f(fn(t))

Apparently.

Now if I have arithmetic operations defined as:
add = lambda x. lambda y. lambda p. lambda q. (x(p))((y(p))(q))
multiply = lambda x. lambda y. lambda z. x(y(z))

How can I show:
(add(Cm))(Cn) = Cm+n       and
(multiply(Cm))(Cn) = Cm*n    ?


Something to do with repeatedly using alpha and beta reductions.

No doubt this makes no sense whatsoever, but I'd appreciate any help.


One other thing - does anyone know of a really useful site that can
explain de Bruijn notation to me?

Thanks a lot in advance,
Paul (bewildered).

Re: Lambda calculus + Church numerals Kent M Pitman
Re: Lambda calculus + Church numerals Lieven Marchand

From: Kent M Pitman
Subject: Re: Lambda calculus + Church numerals
Date: Tue, 23 Jan 2001 15:05:51 +0000
Message-ID: <sfwd7de2trk.fsf@world.std.com>

Paul Neave <····@neave.com> writes:

> I've got a few questions on Church numerals, if anyone's heard of 
> them before.
>
> How can I show:
> (add(Cm))(Cn) = Cm+n       and
> (multiply(Cm))(Cn) = Cm*n    ?

This wouldn't happen to be homework, would it?  If so, you should
definitely say so.  People here don't like being tricked into doing
someone's homework for them.  If it's not homework, you might want to
say how the issue came up...

From: Lieven Marchand
Subject: Re: Lambda calculus + Church numerals
Date: Tue, 23 Jan 2001 17:50:57 +0000
Message-ID: <m366j6kvi6.fsf@localhost.localdomain>

Paul Neave <····@neave.com> writes:

> I've got a few questions on Church numerals, if anyone's heard of them before.
> Church numerals represent numbers as terms of untyped lambda-calculus as:
> Cn = lambda f. lambda x. fn(x)
> where f0(t) = t
> and   fn+1(t) - f(fn(t))
> 
> Apparently.
> 
> Now if I have arithmetic operations defined as:
> add = lambda x. lambda y. lambda p. lambda q. (x(p))((y(p))(q))
> multiply = lambda x. lambda y. lambda z. x(y(z))
> 
> How can I show:
> (add(Cm))(Cn) = Cm+n       and
> (multiply(Cm))(Cn) = Cm*n    ?
> 
> 
> Something to do with repeatedly using alpha and beta reductions.
> 
> No doubt this makes no sense whatsoever, but I'd appreciate any help.
> 
> 
> One other thing - does anyone know of a really useful site that can
> explain de Bruijn notation to me?

You can read Barendregts standard work online at
http://reference.elpress.com/readittoc.jsp?Book=0444875085

Despite the inspiration Lisp got from lambda calculus, I think you'd
be better of trying comp.theory for your question.

-- 
Lieven Marchand <···@village.uunet.be>
Gla�r ok reifr skyli gumna hverr, unz sinn b��r bana.