[Haskell-cafe] Gödel's System T
Petr Pudlak
deb at pudlak.name
Wed Nov 10 13:42:00 EST 2010
Hi,
I was reading the paper "Total Functional Programming" [1]. I
encountered an interesting note on p. 759 that primitive recursion in a
higher-order language allows defining much larger set of function than
classical primitive recursion (which, for example, cannot define
Ackermann's function). And that this is studied in in Gödel's System T.
It also states that this larger set of primitive functions includes all
functions whose totality can be proved in first order logic.
I was searching the Internet but I couldn't find a resource (a paper, a
book) that would explain this in detail, give proofs etc. I'd be happy
if someone could give me some directions.
Thanks,
Petr
[1] http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20101110/2adcf09c/attachment.bin
More information about the Haskell-Cafe
mailing list