On 11 November 2010 11:43, Petr Pudlak <deb@pudlak.name> wrote:
Thanks Dan, the book is really interesting, all parts of it. It looks like I'll read the whole book.


Watch out for the decidability issue though :-

    http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.6483

Aaron

 
 Best regards,
 Petr


On Wed, Nov 10, 2010 at 05:21:16PM -0500, Dan Doel wrote:
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

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)

iQEcBAEBAgAGBQJM29b+AAoJEC5dcKNjBzhn7CAH/1DYIpZcWenZs4D+cPW2V9+F
oET+abW2MgdRPPRquDT4qd/nLnI4XhTiiJEZq8mwfAY4OXBUjHnXLKTlKWyHkgCH
zIRPIXWj0PSHNX+2yAB7muhWmOJv/BfrS9DOKsUDF3Qirtl9kc9x9SkWkVuRe2Yf
JSAp+biYQkTSQg2MntHuprqTn783lfsLyKOvtNkybk3Kt+Ft7dzPmQgtgXCd5fPm
eKI1D3b5H5NOH4cwYYUKejpc+8mptTdJVy6Hw8USI4e+hnoe62CZ/2bBf/lOyoCB
UwNJ09sT5yepyA2DimvI3yZX33OB/K24xfPhsnvHaWAHyz3AkdeMG21eertnmtM=
=zOw9
-----END PGP SIGNATURE-----

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe