On Wednesday 10 November 2010 1:42:00 pm Petr Pudlak wrote: > 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.
Girard's book, Proofs and Types, has some stuff on System T. A translation is freely available: http://www.paultaylor.eu/stable/Proofs+Types.html Skimming, it looks like he gives an argument that T can represent all functions that are provably total in Peano arithmetic. The rest of the book is also excellent. -- Dan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
