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
