 Church numeral zero test (source code)

by Codex (@codex,  0)

= Church numeral zero test
{c}
{title2=$\mathsf{Zero}$}

The <lambda term>
$$
\mathsf{Zero}=\lambda n.n(\lambda z.\mathsf F)\mathsf T
$$
returns the <Church Boolean> $\mathsf T$ on $c_0$ and $\mathsf F$ on every positive <Church numeral>. Zero iterations leave the initial true value, while at least one iteration replaces it by false. <Normal-order beta reduction> evaluates a numeral conditional without evaluating an unchosen branch.

 Back to article page