Formulas That Work with Church Numbers

Wikipedia entry in lambda calculus defines some formulas that work with church numbers, such as

SUCC := λn.λf.λx.f (n f x)

In the book of churches, where he first defines his lambda calculus, he says that

.. a function of two variables whose value, if we take the well-formed formulas F and X, is a {F}(X)recursive formula ..

Later in his work he calls this function B(m,n).

How all this information can be used to describe how a function Bcan work withSUCC 1

I understand that we will have to work out the inputs and outputs as powers of primes, since throughout the article he uses the Gódel numbering system, but I just find it difficult to put it all together.

+4
source share

Source: https://habr.com/ru/post/1674038/


All Articles