In lambda calculus what is the correct definition of numbers

635 Views Asked by At

As a programmer I have been diving into functional programming and am therefore interested about the math behind all of the languages.

I had a small course of lambda calculus at university, but recently wanted to fresh up my knowledge about the matter. I found some great but fairly old resources on the web.

When it comes to numbers however my course and the document I was reading did not align.

Course:
0 = Lx.x
n + 1 = Cons Fls n [with Cons = Lz.z M N and false = Lxy.y]

Document:
0 = Lsz.z (equals Fls)
1 = Lsz.s(z)
2 = Lsz.s(s(z))
etc...

At first sight this looks like a different approach, is there something I am missing? Or is it possible to approach numbers in different ways and you just determine your functions and expressions based on what your definition of the number is?

1

There are 1 best solutions below

1
On BEST ANSWER

Any representation that has suitable reduction properties will do. The document is presenting the Church numerals, in which a natural number $n$ is represented by the operation that iterates a function $n$ times. This is by far the most common way to do it. Your course notes are apparently representing $n$ as a list of $n$ elements each of which is equal to the function $\lambda x\cdot\lambda y\cdot y$ (which is commonly used to represent $\mathsf{false}$). All that matters is that you have exactly one normal form for each natural number $n$ and that you can give $\lambda$-terms that represent the arithmetic operations. You may find this Wikipedia article helpful.