views:

162

answers:

2

I am learning lambda calculus but I cant seem to understand the encoding for the number 0.

how is "function that takes in a function and a second value and applies the function zero times on the argument" a zero? Is there any other way to encode zero? Could anyone here help me encode 0?

+1  A: 

See wikipedia:

0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x
Dario
Why the downvotes?
Dario
+4  A: 

A "function that takes in a function and a second value and applies the function zero times on the argument" is, of course, not zero. It's an encoding of zero. When you deal with plain lambda calculus, you have to encode numbers (as well as other primitive types) in some way, and there are a few requirements dictated for each of these types. For example, one requirement for natural numbers is to be able to add 1 to a given number, and another is to be able to distinguish zero from bigger numbers (if you want to know more, look for "Peano Arithmetic"). The popular encoding that Dario quoted gives you these two things, and it is also representing an integer N by a function that does something (encoded as the f argument) N times -- which is a kind of a natural way to use naturals.

There are other encodings that are possible -- for example, once you can represent lists, you can represent N as a list of N items. These encodings have their pros and cons, but the one above is by far the most popular one.

Eli Barzilay
This is a related question I asked in google groups: Say I have a function f. How do I show that this translates to a natural number 0? What other functions do I need in order to infer that my function f behaves like a 0?
kunjaan
If you want to prove that a function `f` is zero under the usual encoding, you need to show that for all `g` (f g x) == x. You don't need to know anything beyond this.
Eli Barzilay