Re: [Haskell-cafe] Gödel's System T

[Aaron Gray]

On 11 November 2010 11:43, Petr Pudlak <deb at 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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20101111/8388e217/attachment.html