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

jeanas (2024-09-13T00:02:13Z)

> Mais en général, les gens qui s'intéressent à ce sujet s'intéressent plutôt aux classes de complexité « basses » comme P ou L, rarement plus haut que EXPTIME, et en tout cas ils restent sagement à l'intérieur de ELEMENTARY (qui est l'ensemble des problèmes résolubles par une machine de Turing en un temps qui peut être borné, en fonction de la taille de l'entrée, ou d'ailleurs de l'entrée elle-même, par une tour d'exponentielle de hauteur constante). Là aussi, j'ai un peu envie de troller en disant que c'est parce que la science appliquée domine tellement les choses qu'on oublie qu'il y a toutes sortes de questions mathématiques intéressantes à résoudre bien au-delà.

Le troll touche bien sa cible chez moi, alors tu me permettras de réagir même douze ans après 🙂

Disons que j'ai un peu le même sentiment que si tu disais « C'est parce que la science appliquée domine tellement les choses qu'on se cantonne toujours à l'algèbre linéaire dans ℝ ou ℂ, et qu'on oublie qu'il y a toutes sortes de questions intéressantes sur les corps finis, les corps de fonctions et les corps de p-adiques ». Certes, c'est sans doute en partie parce que l'algèbre linéaire numérique est omniprésente en ingéniérie, mais je pense que c'est plus fondamental, l'algèbre linéaire sur ℝ et ℂ a énormément de liens avec dans d'autres domaines des maths pures y compris éloignés de l'algèbre (wronskien en analyse, théorème de Kirchhoff en combinatoire, etc. etc. etc., avec ta culture, tu dois connaître des exemples à la pelle), et qu'il y a juste moins de connexions de ce type avec, disons, les espaces vectoriels p-adiques.

Ben c'est un peu la même chose, énormément des problèmes qu'on rencontre en algo, graphes, automates/vérif, géométrie algorithmique, logique, que sais-je, bref, dans à peu près tous les domaines de l'info théorique, sont complets pour une des fameuses classes NL, P, NP, PSPACE, etc., et l'écrasante majorité sont dans ELEMENTARY, donc c'est assez normal de s'intéresser à ça.

Maintenant, il y a aussi des motivations intrinsèques, et je pense que la complexité descriptive en est une assez convaincante (par exemple PH correspond à la logique du second ordre et ELEMENTARY à la logique d'ordre supérieur, ça justifie la naturalité de ces classes).

Et puis il y a aussi une classe de complexité moins connue mais quand même fondamentale et qui brouille les pistes, c'est P/poly. Elle n'est pas contenue dans ELEMENTARY, pour la simple raison qu'elle contient des problèmes indécidables (de tous les degrés de Turing même, vu qu'elle contient trivialement tout langage unaire ; et pour autant il y a de très bonnes raisons de considérer NP ⊆ P/poly comme à peu près aussi improbable que P = NP).

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: bd114a


Recent comments