the lambda

We can define a successor function, which takes a number n and returns n + 1 by adding an additional application of f:

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

Because the m-th composition of f composed with the n-th composition of f gives the m+n-th composition of f, addition can be defined as follows:

    PLUS := λm.λn.λf.λx.m f (n f x)

PLUS can be thought of as a function taking two natural numbers as arguments and returning a natural number; it can be verified that

    PLUS 2 3

and

    5

are equivalent lambda expressions. Since adding m to a number n can be accomplished by adding 1 m times, an equivalent definition is:

    PLUS := λm.λn.m SUCC n

>>44
Good fucking god, you finally answered. But you should act more mature, you're not 13 anymore.

I'm concerned about you because you abuse ellipsis and emoticons, and shitpost to the point of making some threads unbearable.