Gramática

La gramática del cálculo lambda con naturales extiende la de booleanos de la siguiente manera:

$$\begin{aligned} M &:= \ldots \\ &\mid \zero \\ &\mid \succ{M} \\ &\mid \pred{M} \\ &\mid \isZero{M} \end{aligned}$$

Los términos $\zero$, $\succ{M}$ son usados para representar los números naturales, mientras que $\pred{M}$ y $\isZero{M}$ son operaciones sobre ellos.

Para ahorrarnos escribir $\succ{\succ{\succ{\zero}}}$ para representar el número 3, vamos a usar la notación $\num{3}$, y en general $\num{n}$ para representar el número natural $n$. Pero no es un nuevo término, sino una abreviación de $\succ{\ldots\succ{\zero}}$ con $n$ ocurrencias de $\mathsf{succ}$.