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.

  • $\begingroup$ 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! $\endgroup$ – Clash Sep 5 '13 at 6:51
  • $\begingroup$ @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. $\endgroup$ – Gilles 'SO- stop being evil' Sep 5 '13 at 6:58
  • $\begingroup$ 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)$? $\endgroup$ – Clash Sep 5 '13 at 18:04
  • $\begingroup$ @Clash That's the second redex, after reducing the $\lambda n. …$ that appears when you replace pred by its definition. $\endgroup$ – Gilles 'SO- stop being evil' Sep 5 '13 at 18:21
  • $\begingroup$ 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 $ $\endgroup$ – Clash Sep 5 '13 at 18:24

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.