>It should reflect arithmetic laws of tetration, which for example
>relate (b ^^ (a1*a2)) with b^^a1 and b^^a2 or so, but are there any?
>So how should (a,b)-->t be defined?
I couldn't find any papers on this topic, so I'm trying to work out the laws
now. The interesting ones are (a*b)^^c and (a
I had some more ideas on Tim Sweeney's thoughts:
First of all, I was releaved to see that the definition can be
extended to
b ^^ 0 = 1
(a functional programmer's favourite number must be zero!),
or for types
void --> t ~= unit
> Now I am trying to understand the type-theory analogy to tetrat
Christian Sievers wrote:
> 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.
Faster gr
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 f
There is a neat isomorphism between mathematics and type theory. Using ~=
to indicate isomorphism, we have (roughly):
sum of numbers ~= disjoint union of types
product numbers~= cartesian product of types
exponentiation ~= function spaces
"sigma" summations ~= dependent products
"pi"
