>
> Primitive recursion + function types give you all functions provable
> total in Arithmetic, Goedel proved this (that's where System T comes
> from).
>
Hello, Thorsten,
In practice, it is sometimes not easy to change a non-primitive recursion to
a primitive one.
Here is another example which is similar to the Ackermann function.
f 0 n = S n
f (S 0) n = S (S n)
f (S (S m)) 0 = f m (S 0)
f (S (S m)) (S n) =
f (S m) (f m n) +
f m (f (S m) n) +
f m (f (S m) (S n)) +
f (S m) (f (S (S m)) n)
>From a programmer's point of view, he/she might just want to define the
function as it is. And if we allow partially defined function in type
theory, and with pattern matching, this function can be easily defined.
Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent
