Hyperoperations in Lambda Calculus

Exponentiation, due to J.B Rosser, is defined by:

\[\boldsymbol{A}_\uparrow = \lambda xy.yx\]

Then one has, for all \(m, n \in \mathbb{N}\) (except for \(m = 0\)):

\[\boldsymbol{A}_\uparrow \boldsymbol{c}_n \boldsymbol{c}_m = \boldsymbol{c}_{n \uparrow m}\]

Note that we use Knuth's up-arrow notation. Based on this intuitive definition of exponentiation, we can define tetration (iterated exponentiation) in a straightforward way:

\[\boldsymbol{A}_{\uparrow \uparrow} = \lambda xy.y (\boldsymbol{A}_\uparrow x) \boldsymbol{c}_1\]

Similarly, for pentation (iterated tetration):

\[\boldsymbol{A}_{\uparrow \uparrow \uparrow} = \lambda xy.y (\boldsymbol{A}_{\uparrow \uparrow} x) \boldsymbol{c}_1\]