Re: Tetration operator in functional programming

[Christian Sievers]

Tim Sweeney wrote:

> In mathematics, there is a progression between the operators of addition,
> multiplication, exponentiation, etc., known as the Ackermann hierarchy.
> 
> The next operation in the sequence is often called "tetration" and refers to
> iterated exponentiation.  Let us write a^b for "a raised to the power of b",
> and then a-->b for b raised to its own power a times, i.e.:
> 
> 1-->b = b
> 2-->b = b^b
> 3-->b = (b^b)^b
> ...

This looks strange, as (b^b)^b = b^(b^2), or generally
n-->b = b^(b^(n-1)). A quick web search showed me tetration as

  b ^^ 1     = b
  b ^^ (n+1) = b ^ (b ^^ n)

so b^^3 = b^(b^b); clearly a more interesting (and faster growing) definition.

> Now I am trying to understand the type-theory analogy to tetration. Given
> "unit" as the one-valued type, "bool" as the two-valued type, "three" as the
> three-valued type (isomorphic to "maybe bool"), etc., clearly:
> 
> unit-->t  ~= t
> bool-->t  ~= t->t
> three-->t ~= (t->t)->t
> four-->t  ~= ((t->t)->t)->t

As  b^a ~= a->b,  this is still correct.

> So, what is going on here?  "bool->t" is the type of identity functions on
> t; "three-->t" is especially interesting because it is the type of fixpoint
> operator from t->t to t.
> 
> This hints that there may be some computational utility here.  Is there a
> useful type-theory interpretation of tetration?
> 
> And is there a useful interpretation of tetration on infinitary types, like
> lists, i.e. list(nat)-->nat?  In particular, I am interested in defining the

Hmm. Taking nat as fixpoint of maybe, we might reason

t^^nat = t^^(fixp maybe) = t^^(1+fixp maybe) = t ^ t^^(fixp maybe) =
t ^ (t^^nat) = (t^^nat) -> t,

which reminds me vaguely to domains of untyped lambda calculus.


HTH,
Christian Sievers