The hyperoperation sequence lends itself very naturally
to an implementation in λ calculus.
Note that there are a few differences between [this] encoding of the
integers and the standard Church encoding.
What is standardly 'ZERO' is here 'ONE' because it simplifies the
rank-elevation of the hyperoperation. Consequently the resulting
arithmetic is not defined over 0 but I prefer it that way;
expressions such 0 to the power of 0 are indeterminate in analysis and
it shouldn't be any different here.
(The standard definition of the hyperoperation sequence
defines the operations for 0.)
I've also swapped the order of the arguments of the integer encodings
because the equivalence of
λ f. λ x. f x {normally 'ONE'}
and
λ f. f
irritates me ...
-- from JR
let rec
ONE = lambda x. lambda f. x, {NB.}
TWO = lambda x. lambda f. f x,
THREE = lambda x. lambda f. f (f x),
FOUR = lambda x. lambda f. f (f (f x)),
HYPEROP = lambda r. lambda b.
r (lambda e. lambda x. lambda f. e (f (b x f)) f)
(lambda h. lambda e. e b h),
PLUS = HYPEROP ONE,
TIMES = HYPEROP TWO,
POWER = HYPEROP THREE,
TETRATION = HYPEROP FOUR,
PRINT = lambda n. n 'I' (lambda m. 'I'::m)
in PRINT (TETRATION TWO THREE)
{by JR 20/8/2009}