# What's wrong with my beta reduction of pred c_0 on Church numerals?

I'm trying to calculate $\text{pred}\, c_0$, where $\text{pred}$ is the previous church encoded number and $c_0$ is the number $0$ ($\lambda s. \lambda z. z$).

The formula for $\text{pred}$ is $\lambda n. \lambda s. \lambda z. n (\lambda g. \lambda h. h (g s))(\lambda u.z)(\lambda v.v)$

My $\beta$ reduction looks like this so far (I've underlined the function and the applied parameter)

$$\text{pred}\, c_0 \to \lambda s. \lambda z. c_0 \underline{(\lambda g. \lambda h. h (g s))}\text{ }\underline{(\lambda u.z)}(\lambda v.v) \to$$

$$\lambda s. \lambda z. c_0 (\lambda h. h (\underline{(\lambda u.z)}\text{ } \underline{s}))(\lambda v.v) \to$$

$$\lambda s. \lambda z. c_0 \underline{(\lambda h. h z)}\text{ }\underline{(\lambda v.v)} \to$$

$$\lambda s. \lambda z. \underline{c_0}\text{ } \underline{z} \to$$

$$\lambda s. \lambda z. (???)$$

$$\mathrm{pred}\, c_0 \to \lambda s. \lambda z. c_0 \underline{(\lambda g. \lambda h. h (g s))} \; \underline{(\lambda u.z)}(\lambda v.v)$$

Nope, that's not a redex.

You have a term of the form $c_0 M N P$. That's $c_0 M N$ applied to $P$. It could be parenthesised as $((c_0 M) N) P$. This is how lambda calculus encodes functions with multiple arguments: by applying the function to one argument, and then applying the result to the next argument, and so on. Since this construction is very common, parentheses are omitted: function application associates to the left.

Once you expand the abbreviations, there is only one redex in $\mathrm{pred}\,c_o$, which is $(\lambda n. []) c_0$. This is very intuitive: $\mathrm{pred}$ is a function that takes a numeral as an argument, and the first thing you to to kick off the calculation is to apply the function to the numeral.

• I see... So what I did was, instead of using $M$ as a parameter of the function $c0$, I used $c0$'s parameter $N$ as a parameter of $M$, which was actually just a parameter of $c0$? I basically applied a parameter to a parameter? Thanks in advance! – Clash Sep 5 '13 at 6:51
• @Clash Yes, the term is $c_0 M N P$, i.e. $((c_0 M)N)P$, and you calculated $(M N)$ which doesn't occur as a subterm. – Gilles 'SO- stop being evil' Sep 5 '13 at 6:58
• How come if it's $c_2$ instead of $c_0$ the redex is then $\mathrm{pred}\, c_2 \to \lambda s. \lambda z. \underline{c_2(\lambda g. \lambda h. h (g s))} \; \underline{(\lambda u.z)}(\lambda v.v)$? – Clash Sep 5 '13 at 18:04
• @Clash That's the second redex, after reducing the $\lambda n. …$ that appears when you replace pred by its definition. – Gilles 'SO- stop being evil' Sep 5 '13 at 18:21
• Sorry, what do you mean? I just replaced $c_0$ with $c_2$ from the first equation. However the first equation the redex is processed like this $\text{pred} c_0 \to \lambda s. \lambda z. \underline{c_0} \underline{(\lambda g. \lambda h. h (g s))}\text{ }(\lambda u.z)(\lambda v.v) \to$ – Clash Sep 5 '13 at 18:24