#Lambda calculus, 10-5 (using Church encoding and De Bruijn indeces)
λλ(1λ13)λ1 ##Explanation Without De Bruijn indeces: λa,b.(b λc.ca)λc.c:

λa,b.                                                 define the anonymous function f(a,b)=
     (b                                                apply the following function b times
        λc.                                                    the anonymous function g(c)=
           ca)                 apply c to a because of church encoding this is equal to a^c
              λc.c                              the identity function, 1 in church encoding

If you define exp_a(x)=a^x this program defines a↑↑b=exp_a^b(1) where ^b denotes function itteration.

I'm not sure if this is allowed because ca is technically equivalent to a^c how ever it is not a real built-in and only a side effect of the way integers are encoded in lambda calculus.

Lambda calculus, 10-5

(using Church encoding and De Bruijn indeces)
λλ(1λ13)λ1

Explanation

Without De Bruijn indeces: λa,b.(b λc.ca)λc.c:

λa,b.                                                 define the anonymous function f(a,b)=
     (b                                                apply the following function b times
        λc.                                                    the anonymous function g(c)=
           ca)                 apply c to a because of church encoding this is equal to a^c
              λc.c                              the identity function, 1 in church encoding

If you define exp_a(x)=a^x this program defines a↑↑b=exp_a^b(1) where ^b denotes function itteration.

I'm not sure if this is allowed because ca is technically equivalent to a^c how ever it is not a real built-in and only a side effect of the way integers are encoded in lambda calculus.