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

>>30
What's interesting is that if you have another implementation that agrees with this one, you can prove things with either or and they apply to both.