zero = (λs(λz.z)) = (λsz.z) = H = true
one = (λs(λz(sz))) = (λsz.sz)
two = (λs(λz(s(sz)))) = (λsz.s(sz))
pr = (λn.ni0)
Y = (λ (f) ((λ (x) (f (λ (y) ((x x) y)))) (λ (x) (f (λ (y) ((x x) y)))))) ; Scheme
Y = (λf.((λx.(f(λy.(xxy))))(λx.(f(λy.(xxy)))))) Y-combinator
S = (λnfx.f(nfx)) ; Successor function for Church numbers
(pr zero) = ((λn.ni0) (λsz.z)) => 0
(pr one) =  ((λn.ni0) (λsz.sz)) => 1
(pr two) =  ((λn.ni0) (λsz.s(sz))) => 2
(pr (S two)) = ((λn.ni0) ((λnfx.f(nfx)) (λsz.s(sz)))) => 3

(define (rd n) (if (zero? n) C0 (S (rd (- n 1))))) ; Scheme
rd = (λrn.(zn(λd.H)(λD.(S(r(dn))))i))
(Y rd) = ((λf.((λx.(f(λy.(xxy))))(λx.(f(λy.(xxy)))))) (λrn.(zn(λd.H)(λD.(S(r(dn))))i)))
((Y rd) 0) = (((λf.((λx.(f(λy.(xxy))))(λx.(f(λy.(xxy)))))) (λrn.(zn(λd.H)(λD.((λnfx.f(nfx))(r(dn))))i))) 0) -> function, maybe 0
(pr ((Y rd) 0)) = ((λn.ni0) (((λf.((λx.(f(λy.(xxy))))(λx.(f(λy.(xxy)))))) (λrn.(zn(λd.H)(λD.((λnfx.f(nfx))(r(dn))))i))) 0)) -> 0
(pr ((Y rd) 7)) = ((λn.ni0) (((λf.((λx.(f(λy.(xxy))))(λx.(f(λy.(xxy)))))) (λrn.(zn(λd.H)(λD.((λnfx.f(nfx))(r(dn))))i))) 7)) -> 7

The λ platform provides non-negative integers less then 2⁶³ natively. Arabic numerals are read by the compiler to produce these native numbers and such values are the only sort that can be printed. Church provided a scheme for modeling numbers as pure functions, but the number n in his scheme consumes an amount of space proportional to n. The native numbers are efficient in storage. The only operations on native numbers are increment, decrement and zero-test. These values are bound to i, d and z in the initial environ. Upon these foundations, provided by the platform, the functions pr and (Y rd) are defined above to translate between the two sorts of numbers. Y is the Y-combinator, invented by Church, and makes the function rd recursive. You can do Church arithmetic if you wish using (Y rd) and pr for input and output.

The rd function deserves some explication. (((zn)H) (S(r(dn)))) might seem to suffice. It tests n for being zero and chooses H (zero) if so, and the successor of reading n−1 otherwise. The platform evaluates arguments before calling functions, however, and we cannot afford to compute both cases for that leads to infinite regress instead of finishing the value we want. Using (((zn)(λd.H))(λD.(S(r(dn))))) instead selects two functions both of which are produced for the truth value of (zn) to choose between. This results in some function that must be called to get the answer we want, but only one of the bodies of those functions will be evaluated this way and the calculation finishes. The argument to the chosen function is irrelevant. The Y-combinator, for recursion, is easy to use and hard to understand.