0

I was reading about Church encoding, and couldn't figure out some of the grammar of function applications (in terms of Church numerals). In particular, the examples I've seen thus far apply to unary functions $f$, i.e. something like $n \space f \space x \equiv f^n \space x$.

What does it mean for a binary function $f_2$ to have (can't figure out the arity etc.):

$ n \space f_2 \space x \space y $ ?

Here, it's not clear to me what a $f^n_2$ can mean.

The motivation of the question is to understand the body of the following predecessor function from Wikipedia page linked earlier:

$ pred \equiv \lambda n.\lambda f. \lambda x. n \space (\lambda g. \lambda h. (g \space f)) \space (\lambda u.x) \space (\lambda u.u) $

(i.e. $ \space n \space (\lambda g. \lambda h. (g \space f)) \space (\lambda u.x) \space (\lambda u.u) $ )

Also, I tried to understand this using e.g.

$n \space (+) \space 1 \space 2$

, but couldn't figure out what's the correct meaning.

Jean Marie
  • 81,803
tinlyx
  • 1,534

1 Answers1

1

First, in the lambda calculus, there are only unary functions. What seems like a binary/ternary/... function is really just a unary function thanks to currying/schoenfinkelisation.

Now, the question itself is really about what the 'encoding' actually is. Suppose that we have, for each natural number $n$, a combinator $C_n$, and also combinators $C_s,C_p, C_+, C_-, C_\times$ (which are supposed to respectively represent successor, predecessor, addition, subtraction, and multiplication).

Suppose that these combinators have some nice properties such as

  1. $C_{n+1}$ is the $\beta$-normal form of $C_s C_n$,
  2. $C_{m+n}$ is the $\beta$-normal form of $C_+ C_m N_n$,
  3. $C_{mn}$ is the $\beta$-normal form of $C_\times C_m C_n$,
  4. $C_n$ is the $\beta$-normal form of $C_p C_{n+1}$ etc.

So we see that these combinators allow us to do some basic arithmetic in the lambda calculus, where for example, we can find out what the sum of two numbers $m$ and $n$ is by finding the $\beta$-normal form of $C_+ C_m C_n$.

This is what an encoding is supposed to achieve, and why Church's encoding is called what it is. The actual implementation does not matter, and what the interaction of these combinators with other combinators is does not matter. All that matters is that with each other they behave in the way that we expect the natural numbers and their basic operations to behave.

So for example, the fact that $\ulcorner n \urcorner fx = f^n x$ is only important in this context in that it implies things like $\ulcorner succ \urcorner \ulcorner n\urcorner = \ulcorner n+1\urcorner$.

tci
  • 1,005