((λa.(λb.(λc.D) C) B) A)Consider program D that requires A, B & C which themselves stand alone:
((λabc.D) A B C)Recall that functions i, d, z, H and K are primordial.
Here we do some arithmetic Church’s way:
((λYS.(λrpamP. (p(P(r6)(r3))); Client on this line ) (Y(λrn.zn(λd.H)(λD.S(r(dn)))i)) ; r (read; native integers to Church) (λn.ni0) ; p (write; Church integers to native) (λxy.xSy) ; a, add (λxyz.x(yz)) ; m, multiply (λxy.yx) ; P, power ) (λf.(λx.f(λy.xxy))(λx.f(λy.xxy))) ; Y combinator (λnfx.f(nfx)) ; S (Church number successor) )The above expression yields 63. The following expressions, when substituted for (p(P(r6)(r3))) above, yield the indicated results.
All of this development of arithmetic is within the bald language with Church’s abbreviations; the native arithmetic is relegated solely to input/output. It is notable that each of the three functions add, multiply and power stand alone as short expressions with no infrastructure beyond S, the successor function. Recursion is normally used in defining arithmetic but here it is only for the definition of r which converts to Church numbers.
To get this far starting with set theory takes many pages of ideas solely in support of arithmetic. Further I know no how-to (computational) version of arithmetic based on set theory, but I suspect that such is possible.
See the predecessor function in action.