Church numerals $\overline{0} = \lambda fx. x$ and $\overline{n} = \lambda f x. f^n x$ are provisions for applying a function $n$ times to an argument. An alternate system of numerals, possibly attributable to Kleene, is $\overline{0} = \lambda x. x$ and $\overline{n+1} = [F, \overline{n}]$, where $[\,,\,]$ represents pairing and $F$ is the boolean value $\textit{false}$.

Can these numerals also be viewed as $n$ applications of a function? More concretely, without using the $Y$ combinator, is it possible to construct a lambda term $t$, such that $t$ applied to the Kleene numeral $\overline{n}$ and lambda terms $f$ and $x$ reduces to $f^n x$?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.