Yong Luo wrote:
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)
Did you check this example in Epigram? Conor
