More Arithmetic

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}
 



 
Also see the other integers.