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

> 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.

> 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.

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 !

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.

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.