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
==
Dr. Yong Luo
Computing Laboratory
University of Kent
- Original Message -
From: Conor McBride [EMAIL PROTECTED]
To: epigram@durham.ac.uk
Sent: Friday, November 18, 2005 4:36 PM
Subject: Re: [Epigram] epigram tells me fibs
Yong Luo wrote:
ack 0 n = S n
ack (S m) 0 = ack m (S 0
Since you use elimination rule on both arguments, I was expecting
four cases
like Thorsten did in the previous email. Can we define the Ackermann
function like the following form?
Conor used the official version of the Ackermann function, which just
has three lines, while I used my own
Hi Yong,
Is there documentation on exactly what the elimination constants are?
Epigram was happy with an Ackermann function, which surprised me
slightly.
It is also surprising to me. Ackermann function is a nested function and is
not a primitive recursion. The eliminators in conventional
