Comments on Personne n'aime les fonctions primitives récursives ?

Arnaud Spiwack (2012-11-16T11:23:17Z)

> Je ne sais pas si je considérerais le système T comme un « langage de programmation ».

Ça dépend ce qu'on prend comme définition de système T et de langage de programmation, je suppose.

Dans mon sens de théoricien des types (ce mot est moins élégant que type theorist, mais plus que théorie-des-typiste ou théorie-des-typicien…) il s'agit du λ-calcul simplement typé avec un type nat (avec 0 et S, comme constructeurs) et l'opérateur de recursion primitive à chaque type.

J'utilise le terme langage de programmation assez largement (en particulier n'importe quoi dont la sémantique s'explique à base de règle de réécriture).

> Mais à ce sujet, en a-t-on une analyse du point de vue de la théorie de la preuve (àla Pohlers, Rathjen, et al.) ?
> Par exemple, sait-on décrire l'ordinal de preuve du système T (à définir proprement…) ?

Je ne suis pas expert du tout, mais pour autant que je sache, le système T a été introduit par Gödel, parce que les fonctions (à plusieurs arguments entiers naturels à valeur dans les entiers naturels) définissables dedans sont précisément les fonctions qu'on prouve totales dans l'arithmétique (de premier ordre) de Heyting.

Ruxor (2012-11-16T10:03:46Z)

@Arnaud Spiwack: Je ne sais pas si je considérerais le système T comme un « langage de programmation ».

Mais à ce sujet, en a-t-on une analyse du point de vue de la théorie de la preuve (àla Pohlers, Rathjen, et al.) ? Par exemple, sait-on décrire l'ordinal de preuve du système T (à définir proprement…) ? Ou sait-on au moins le comparer à des théories comme Kripke-Platek ou des fragments de l'arithmétique du second ordre ?

Si je crois ce que <URL: http://books.google.fr/books?id=MfTMDeCq7ukC&pg=PA193 > suggère à demi-mot, l'ordinal de preuve du système T devrait être l'ordinal de Bachmann-Howard. Ce qui suggère de comparer avec ce qu'on peut démontrer dans Kripke-Platek, et aussi de comparer les fonctions définissables dans le système T avec les fonctions primitives récursives après ε₀ itérations du saut de Kleene. Il faudrait plonger dans le livre de Schwichtenberg et Wainer.

Arnaud Spiwack (2012-11-16T07:45:53Z)

> on ne peut pas faire une machine primitive récursive universelle[…]
> Et c'est la principale raison pour laquelle on ne veut pas d'un langage de
> programmation qui n'autoriserait que les fonctions primitives récursives

Il faut se méfier de ce genre de jugement. D'abord, c'est vrai de tout langage de programmation total (c'est-à-dire où toutes les fonctions terminent) il ne peut pas exprimer naturellement son interpréteur. Ça ne les empêche pas d'être utiles ou intéressants. Cela étant dit la plupart des langages totaux sont beaucoup plus puissants que pr (le plus simple, c'est le système T, qui n'a que le récurseur primitif sur N mais qui peut retourner des fonctions, c'est assez facile d'y coder la fonction d'Ackermann).

Par ailleurs, il n'y a rien qui empêche d'écrire la fonction qui exécute "les n premiers pas de l'interpréteur". On ne peut juste pas en prendre la limite comme une fonction pr.

Arthur Milchior (2012-11-16T07:06:14Z)

Merci pour cette visite hors d'Elementary. J'ai déjà travaillé sur des tours d'exponentielle, je ne savais pas qu'il existait un monde au delà.

Quant au fait que les informaticiens théorique s'intéressent à des trucs appliqués, franchement, c'est une excellente vanne !

DM (2012-11-16T03:29:05Z)

Sinon en effet la diagonalisation sur les fonctions primitives récursives, montrant qu'on ne peut pas définir l'interpréteur pour ce langage à l'intérieur de lui-même, est curieusement plus rare que la fonction d'Ackermann. Je pense que c'est parce que cette dernière a une définition raisonnable ne faisant pas intervenir de théorie de la preuve ou de syntaxe de programme.

DM (2012-11-16T03:27:40Z)

C'est amusant que tu cites les diktats de la science appliquée comme cause de la non-étude des classes de complexité supérieures ou des degrés de Turing au delà, disons, de récursivement énumérable. Je donne parfois en exercice des preuves style "montrer que tel truc n'est ni récursivement énumérable ni de complémentaire récursivement énumérable"…

Surtout, j'ai tendance, ces derniers temps, à citer l'étude de la structure fine des degrés de Turing comme exemple de sujet parfaitement respectable mais dont l'étude est "gratuite" (au sens de: n'apportera pas grand chose sauf à une ultra-minorité de gens), et ce dans des discussions relatives à ce qu'il faut ou non enseigner.


You can post a comment using the following fields:
Name or nick (mandatory):
Web site URL (optional):
Email address (optional, will not appear):
Identifier phrase (optional, see below):
Attempt to remember the values above?
The comment itself (mandatory):

Optional message for moderator (hidden to others):

Spam protection: please enter below the following signs in reverse order: 5b2586


Recent comments