Zero and one are defined by the successor function.

$$ \begin{align*} &0 ≡ λsz.z \\ &1 ≡ λsz.s(z) \end{align*} $$

But why? $λsz.z$ is irreducible to a value. If I call this function on some value, I get back $z$, which is merely a variable in itself. If I call the function on two values, I get back the second value, which is not necessarily zero.

And yet we're just assigning the function the value $0$? Why? Why not assign zero to say $λs.(λz.xyt)$. This seems arbitrary.

This is from the arithmetic section of: http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf

  • $\begingroup$ If you apply $\lambda s z.z$ to a value you get back $\lambda z.z$. Note that $\lambda s z.z$ is shorthand for $\lambda s.\lambda z.z$. $\endgroup$ Dec 4 '16 at 22:55

The natural numbers don't exist natively in the world of lambda calculus, and so if we want to use them, we have to define them somehow. You are describing the Church numerals, one possible definition which supports arithmetic. Church defines $n$ to be the function $(s,z) \mapsto s^{(n)}(z)$ that maps a pair $(s,z)$ into an $n$-fold application of $s$ to $z$. In particular, when $n = 0$ we get $(s,z) \mapsto z$.

Why this definition and not any other one? No reason. It is just a common definition, but you can use any other definition you like, or even come up with a new one. This particular definition supports arithmetic – you can define addition, multiplication and so on. See Wikipedia for the details.

  • $\begingroup$ Thanks. It still feels very opaque. If integers don't exist natively and we want to define them, them why not say 1≡ 1 and so on---just wholesale include them? I feel like this is a more common definition of numbers. You say there’s no reason for the Church definition. However, my definition does have a good reason behind it--- it is simple, immediately transparent, and is a convention both within and without this field. // In other words, what’s the advantage of such a definition? $\endgroup$
    – JDG
    Dec 3 '16 at 8:17
  • 1
    $\begingroup$ You don't have "1" in lambda calculus, just like you don't have pigs and orcas there. If you want "1" then you have to define it as a lambda term. $\endgroup$ Dec 3 '16 at 8:24
  • $\begingroup$ to create lambda calculus, I’m sure various operators and ideas had to be defined. Before those definitions, lambda calculus wasn’t there. Something had to be axiomatic, right? Integers can also be defined axiomatically. Maybe I’m missing the point? Say we don’t to do it axiomatic. I’m reading the wikipedia entry. It seems to say that there is a function whose role is to generate integers. Each successive application increments by 1. So, in reality, it is not a definition of integers but rather a definition of addition. It’s a prefix function. Here’s a sensible, transparent shorthand: +^n x. x $\endgroup$
    – JDG
    Dec 3 '16 at 8:41
  • 2
    $\begingroup$ I think that the point that you're missing is that in lambda calculus we don't have to define the natural numbers axiomatically. Rather, we can define them inside the formalism. That's just like in set theory: we don't define the natural numbers as foreign axioms, since in set theory everything is a set. Instead, we define them using a successor operation. In lambda calculus, everything is a function, and so you have to define your numerals as functions. $\endgroup$ Dec 3 '16 at 9:03
  • 1
    $\begingroup$ I wish it was explained in those terms---especially because a very common avenue to lambda calculus is functional programming and not set theory. Thank you very much. I’ll write up an answer that summarizes these ideas. $\endgroup$
    – JDG
    Dec 3 '16 at 9:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.