Lambda calculus + Church numerals
Paul Neave
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).
Torben AEgidius Mogensen
>I've got a few questions on Church numerals, if anyone's heard of them before.
I would think most of us have.
>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.
It makes perfect sense. I suggest you use induction: Show
1) add C0 Cn = C(0+n)
2) add Cm Cn = C(m+n) => add C(m+1) Cn = C(m+1+n)
and similarly for multiplication.
>One other thing - does anyone know of a really useful site that can
>explain de Bruijn notation to me?
It is simple enough: The idea is to replace variable names in function
bodies with numbers that count the number of lambda's you have to
cross (when walking up the syntax tree) to get to the place the
variable is bound. Hence, a variable that is bound by the immediately
enclosing lambda is replaced by 0, a variable that is bound at the
next enclising lambda by 1 etc. After this, lambdas no longer have
attached names. Examples (where "\" is lambda):
\x.x becomes \.0
\x.\y.x y becomes \.\.1 0
\x.(\y.y x) x becomes \.(\.0 1) 0
Note in the last example that the last x is replaced by 0 even though
there textually is a lambda (\y) between \x and x. This is because
this lambda isn't higher than x in the syntax tree. Note also that the
two occurences of x are replaced by two different numbers, since one
is embedded in a lambda-abstraction and the other isn't.
Note that since every lambda will be immediately followed by a ".", we
can omit this, so "\.(\.0 1) 0" becomes "\(\0 1) 0".
Torben Mogensen (tor...@diku.dk)
Neelakantan Krishnaswami
wrote:
>
>> One other thing - does anyone know of a really useful site that can
>> explain de Bruijn notation to me?
>
> It is simple enough: The idea is to replace variable names in
> function bodies with numbers that count the number of lambda's you
> have to cross (when walking up the syntax tree) to get to the place
> the variable is bound. Hence, a variable that is bound by the
> immediately enclosing lambda is replaced by 0, a variable that is
> bound at the next enclising lambda by 1 etc. After this, lambdas no
> longer have attached names.
For me, the "a-ha" experience for de Bruijn indices was looking at an
actual implementation of an interpreter.
In the first course on interpreters, the environment is usually stored
as a list of name-value pairs, and a simple optimization is to change
the environment from a list of name-value pairs into a linked list of
values, and then turn each variable reference in the AST into an
offset into the list. This makes variable lookups go much faster, and
is exactly what de Bruijn indices are.
Incidentally, for languages with multiple argument functions, is there
some theory as nice as de Bruijn indices to formalize the frame/offset
pairs used to build environments there?
Neel
Gerard Huet
>Incidentally, for languages with multiple argument functions, is there
>some theory as nice as de Bruijn indices to formalize the frame/offset
>pairs used to build environments there?
Yes indeed. I looked at the problem in the context of Bohm's separability
theorem. The problem arose in the representation of Bohm trees, which are
potentially infinite lambda-terms, represented as layers of head normal forms.
Each layer has the shape \x1 x2 ... xn.h(M1, ..., Mp) where h is the head
variable. The correct extension of de Bruijn indices to this situation is to
represent h with a pair of natural numbers. One names the layer above where h
is bound, a la de Bruijn. The other one indexes in the layer. For instance,
if h is x2, then it is represented as Index(0,2); 0 since h is locally bound, and
2 because the local indexing goes left to right, and NOT right to left as we
would have thought by the de Bruijn analogy. Left to right is the proper
way because we want the indexing to be invariant by eta-expansion.
Details may be found in section 1.7 of my paper "An analysis of Bohm's theorem"
Theoretical Computer Science 121 (1993) 145-167 where all definitions are given
as executable CAML programs - no handvawing with maths, just explicit ML code.
I was very pleased to basically rediscover the ALGOL display mechanism.
It may also be pointed out that I had no difficulty computing on infinite Bohm
trees in a strict language. No flames intended, of course.
--
Gerard Huet
----------------------------------------------
INRIA -- BP 105 -- F-78153 Le Chesnay Cedex
Tel.: +33 1 39 63 54 60 Fax: +33 1 39 63 56 84
Email: Gerar...@inria.fr
WWW: http://pauillac.inria.fr/~huet/index.html
----------------------------------------------
Markus Mottl
[snip; small typo corrected]
> No handwaving with maths, just explicit ML code.
I like this statement, even more so since it comes from Gerard Huet! :-)
Regards,
Markus Mottl
--
Markus Mottl, mo...@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl
Neelakantan Krishnaswami
>Neel asked:
>>Incidentally, for languages with multiple argument functions, is there
>>some theory as nice as de Bruijn indices to formalize the frame/offset
>>pairs used to build environments there?
>
> Yes indeed. I looked at the problem in the context of Bohm's
>
> Details may be found in section 1.7 of my paper "An analysis of
> Bohm's theorem" Theoretical Computer Science 121 (1993) 145-167
> where all definitions are given as executable CAML programs - no
> handvawing with maths, just explicit ML code.
Thank you, this was exactly what I was looking for!
Neel