Discussion:Théorème de Rice

Remise en forme

Il faudrait peut-être uniformiser un peu cet article : j'ai l'impression que l'ensemble des contributeurs (y compris moi) ont apporté leur pierre avec leurs propres notations et point de vue, ce qui rends l'article difficile à comprendre. Par exemple, j'avais écrit la première version de la démonstration du strict point de vue des machines de Turing, alors qu'en fait, cette "approche" n'est quasiment pas utilisée dans la définition... Quelqu'un travaille encore sur cet article ? Jamian 13 octobre 2006 à 10:28 (CEST)

le théorème de rice indécidable...

Le théorème de Rice travaille sur des algorithmes qui ne sont pas dans le domaine de définition de l'utilisation des machines de Turing. (cf:Thèse de Church, Algorithme d'Euclide, la page de discutions du Problème de l'arrêt)

Au mieux ce théorème met en évidence les cas à ne pas (re)produire.

Pour une machine de Turing il n'existe pas la notion de "non-trivial", tout est oui ou non. Tout autre cas est un bug de conception logique du programme.(cf: la page de discutions du Problème de l'arrêt)

Le fait est que créer une boucle infinie dans un programme est un bug(erreur humaine) ce qui rend ce cas hors domaine de définition pour les machines de Turing.(cf: la page de discutions du Problème de l'arrêt)

Ppignol (d) 10 juin 2009 à 12:48 (CEST)

comme je vous l'ai dit, le théorème de Rice travaille sur des problèmes, pas des algorithmes.

La notion de trivialité repose sur une propriété de l'ensemble des sorties possibles d'une machine de Turing en fonction de ses paramètres : la propriété est triviale si, et seulement si elle a la même valeur de vérité pour tous les éléments de cet ensemble. ceci est parfaitement défini.

La sortie d'une machine de Turing n'est par ailleurs pas forcément une réponse "oui" ou "non". Beaucoup de papiers prennent pour sémantique d'une MT l'état de son ruban à la fin de l'exécution, qui peut donc avoir plus de deux valeurs...

Jamian (d) 10 juin 2009 à 15:38 (CEST)

Quand on parle de machines de Turing, on parle d'algorithmes (cf: impacts pratiques) ! Désolé de vous contredire. Une machine de Turing n'a pas dans ses spécifications d'optimiser un bug. Quand vous savez pas de quoi vous parlez, taisez-vous. Tant que vous restez dans les maths, c'est moi qui fermerais ma gueule. Mais dès que vous passez dans les machines de Turing, vous tombez dans mon domaine et un bug, en algorithmique, n'a pas à être optimisé. Donc, ne venez pas me chercher sur mon terrain !Ppignol (d) 2 août 2010 à 13:06 (CEST)

Visiblement, une année entière de réflexion sur le sujet n'a pas suffit à vous faire comprendre mon propos (ce que je conçois fort aisément, la calculabilité étant l'une des matières les plus subtiles du domaine de l'informatique). Peut-être une explication sur une autre facette vous éclairera-t-elle : d'un point de vue formel, on peut considérer un algorithme comme une fonction d'un état de la machine qui l'exécute vers un autre état de cette même machine. De même, une machine de Turing peut être vue comme une fonction mettant en relation l'état initial de sa bande à l'état final de celle-ci, ou, dans les problèmes de décision, vers un élément de l'espace booléen.

Supposons même, pour vous faire plaisir, que l'on ne considère pas l'ensemble des algorithmes indéfinis en un point de cet ensemble (ce que vous appelez "pas dans la définition des machines de Turing"). Le théorème de Rice dit alors qu'il est impossible d'écrire un algorithme permettant de dire si la sortie d'un autre algorithme vérifie telle ou telle propriété (non triviale), car alors, il serait possible d'écrire très facilement un autre algorithme qui tromperait le premier, d'où contradiction.

Quant à votre prétendue comparaison de nos domaines de compétences, je ne connais pas votre cursus, et vous ne connaissez pas le mien. Je vous prie donc vous calmer à ce sujet, tout déballage de médailles ou revendication de "terrains" exclusif (on se croirait dans une guerre de gangs) étant totalement hors de propos.

Bien à vous,

Jamian (d) 2 août 2010 à 18:42 (CEST)

(PS : on m'a souvent dit que seuls les informaticiens et les matheux savent se différencier les uns des autres...)

(PPS : et, je préfère mettre encore une fois le doigt dessus, observez bien que décider d'une propriété non triviale donnée sur les fonctions définies plus haut est donc un... "problème" indécidable, i.e. pour lequel il n'existe pas d' "algorithme". Soit dit en passant, l'association d'un algorithme à une fonction d'un état de la machine dans un autre est unique dans un sens, mais pas dans l'autre, étant donné qu'il existe plusieurs algorithmes pour un même problème (souvenez-vous : le tri du tableau, qui peut se faire via maints algorithmes différents, mais dont le résultat sera strictement le même. Tri du tableau <-> problème, tri bulles, quicksort ou tri fusion <-> algorithmes. Je vous laisse deviner lequel de l'ensemble des problèmes ou de l'ensemble des algorithmes correspond le plus à l'ensemble des fonctions d'un état de la machine dans un autre (surtout si on veut se limiter aux algos qui terminent, et donc aux fonctions décidables). Jamian (d) 3 août 2010 à 22:39 (CEST)

Quant à vous, observez que un algorithme tombant dans le théorème de rice est un algorithme inutile à l'homme et n'a donc pas à être spécifié. Si il à malencontreusement été spécifié à la machine de turing par l'homme c'est donc que c'est la responsabilité de l'homme et non celle de la machine de retrouver et corriger l'erreur. De plus la démonstration à été modifié donc je ne devais pas avoir si tort que cela sur le FOND ! cf: http://www.larecherche.fr/savoirs/autre/verifier-programmes-prouvant-theoremes-01-10-2007-85463 Ppignol (d) 19 juillet 2013 à 01:30 (CEST)

Théorie algorithmique des jeux

Bonjour, il semble y avoir des applications en théorie algorithmique des jeux (article que je viens de créer), si quelqu'un veut vérifier... --Roll-Morton (discuter) 18 février 2016 à 14:43 (CET)

Bonjour Roll-Morton, as-tu des références à ce sujet ? --Fschwarzentruber (discuter) 30 novembre 2017 à 22:01 (CET)

Ramasse-miette

balayage de feuilles

Je pense que le ramasse-miette ne relève pas du Théorème de Rice, car un ramasse-miette (ou glaneur de cellule) est un processus infini qui travaille en concurrence avec un autre processus infini producteur de miettes (ou de cellules). Un ramasse-miette ne peut donc pas être codé par une machine de Turing (ou un programme). Dit autrement, il n'y a pas de fonction calculable qui correspondrait à ce que "calcule" un ramasse miette, si tant est qu'un ramasse-miette calcule une valeur. De façon imagée, un ramasse-miette est comme le jardinier en automne qui balaie constamment les feuilles que le vent fait tomber. --Pierre de Lyon (discuter) 5 novembre 2017 à 16:32 (CET)

J'ai supprimé le paragraphe. --Pierre de Lyon (discuter) 7 novembre 2017 à 10:01 (CET)

Vérification de programmes

Attention aux derniers modifs ! Là, on a l'impression que le test et le model checking sont des analyses statiques. --Fschwarzentruber (discuter) 23 novembre 2017 à 13:25 (CET)

Je suis pour supprimer cette référence au test et à la vérification de modèles. Mais par prudence j'ai hésité à le faire? --Pierre de Lyon (discuter) 23 novembre 2017 à 14:06 (CET)

C'est moi qui est rajouté ça. Au contraire, je pense que c'est important d'en parler. Si on avait des techniques systématiques pour faire de la vérif en pratique, le test n'aurait quasiment aucun intérêt ; pareil pour le model checking. Mais le mieux serait en effet, de trouver une source qui dise ça. On doit bien trouver cela. Je suis pour rajouter "référence nécessaire". --Fschwarzentruber (discuter) 23 novembre 2017 à 15:55 (CET)

Oui mais il faut que cela soit énoncé clairement, ce qui n'était pas le cas. Ceci dit, le model checking est une méthode d'analyse statique, pas le test. On peut citer à ce propos Djistra: « Le test de programmes peut être une façon très efficace de montrer la présence de bugs mais est désespérément inadéquat pour prouver leur absence ». --Pierre de Lyon (discuter) 23 novembre 2017 à 16:45 (CET)

Ah bah, il faut améliorer ! Mais là, en lisant la phrase dans l'article, on a l'impression que le test est une méthode d'analyse statique. Ce n'est pas le cas. Pour le model checking, oui, ça se discute si c'est de la l'analyse statique ou pas (d'un côté, on déplie toutes les exécutions donc on exécute, donc ce n'est pas "statique", de l'autre, on exécute plutôt des exécutions d'un modèle abstrait donc c'est "statique", bref), mais pas besoin de rentrer dans une polémique. Du coup, pour éviter la polémique, on parle de model checking dans une autre phrase ? :) Quant à citer Dijkstra, très bonne idée ! Merci à toi et bonne soirée. --Fschwarzentruber (discuter) 23 novembre 2017 à 16:53 (CET)

Je vais proposer une rédaction consensuelle. --Pierre de Lyon (discuter) 23 novembre 2017 à 18:01 (CET)

Merci ! Et merci pour la citation. Par contre, je ne suis pas tout à fait d'accord avec "Mais alors que la vérification de modèles démontre les bonnes propriétés : correction par rapport à la spécification". Le model checker dit "c'est tout bon" si la spécification (temporelle) est vérifiée, et si elle ne l'est pas, le model checker exhibe une exécution contre-exemple du programme qui ne répond pas à la spécification. Le seul hic, c'est qu'un model checker travaille sur des abstractions de programme (souvent avec du rafinement, ce processus de rafinement pouvant ne pas terminer). Aussi, par rapport au théorème de Rice, (mais ce n'est pas très grave pour une première lecture), le model checking c'est pour des proprammes qui ne s'arrêtent pas forcément comme des systèmes réactifs etc. Mais pour wikipedia, le mieux c'est de trouver une bonne source qui raconte ça (ou qui raconte autre chose d'ailleurs). Je propose d'améliorer encore la rédaction sur l'exposition faite dans "Formal Verification of Concurrent Embedded Software", p. 16, en disant qu'il y a toujours de la place pour faire de la vérification.

1. en faisant du test

2. en faisant des approximations

3. ou alors faire de la vérif sur des systèmes avec un nombre fini d'états

Puis, on parle d'analyse statique et de model checking. Mais on peut en discuter encore un peu avant. Et ça serait bien d'avoir plusieurs autres sources. Ah, et il faut aussi parler des assistants de preuve.

Une bonne source accessible en français est

* Gérard Berry La vérification de modèles (model checking), Leçon du Collège de France du 25 mars 2015.

Ceci dit, je te laisse agir et écrire, car je ne suis pas un spécialiste. --Pierre de Lyon (discuter) 23 novembre 2017 à 18:59 (CET)

Théorème de Rice pour les ensembles

J'ai mis en forme le paragraphe Théorème de Rice pour les ensembles. Je ne suis pas sûr d'avoir fait quelque chose de correct. Est-ce qu'un spécialiste du théorème de Rice pourrait le relire ? --Pierre de Lyon (discuter) 24 novembre 2017 à 13:23 (CET)

Liste de tâches à effectuer sur cet article

Je vous propose cette liste de tâches, qui est bien sûr subjective. Donc à discuter.

• Bien expliquer l'intérêt de la section "Un cas particulier : la fonction réalisée par un programme". Est-ce un intérêt pédagogique ? Si oui, y-a-t-il une source ?
• Sourcer la section sur les différentes présentations du théorème. Reformuler un peu. Dire que des fois, c'est présenté comme un exo dans les bouquins, parfois, il y a un chapitre consacré, etc. Comparer les formalismes.
• Que faire des démonstrations ? Si on les garde, il faut les sourcer, les comparer, les remettre dans un contexte historique afin de faire le tour du sujet. Sinon, ce n'est peut-être pas assez encyclopédique et cela ressemble trop à un cours ou à un catalogue de démonstrations.

--Fschwarzentruber (discuter) 27 novembre 2017 à 21:58 (CET)

Pour info, en ce qui concerne la démonstration sur les ensembles et la variante (non semi-décidabilité des propriétés non monotones), j'avais repris la démonstration que donne Kozen (Automata and Computability - Lecture 34). Jamian (discuter) 29 novembre 2017 à 13:46 (CET)

Chaque section est maintenant sourcée. Sources pour chaque version du théorème, source pour les différentes démonstrations. Les différentes démonstrations sont intéressantes car elles permettent de mieux comprendre les différentes variantes de ce théorème. Ne devrait-on pas enlever le bandeau Cet article ne cite pas suffisamment ses sources? Il y a 20 sources distinctes qui couvrent toutes les sections Yves de Louvain-le-Ñeuve(discuter) 30 novembre 2017 à 22:41 (CET)

Merci pour votre travail. D'accord aussi pour garder les démonstrations. Que pensez-vous de mettre les démonstrations dans des cadres ouvrables et fermables et de les mettre sous les énoncés des théorèmes ? Là, on ne voit pas bien par exemple à quoi faire référence "Démonstration pour les ensembles (variante du théorème)" (si on lit en détail, on comprend, mais ça ne saute pas aux yeux). Bonne journée à vous tous.--Fschwarzentruber (discuter) 1 décembre 2017 à 11:38 (CET)

PS : Je suis complétement d'accord d'enlever le bandeau. Mais je ne sais pas si c'est à nous de le faire. --Fschwarzentruber (discuter) 6 décembre 2017 à 09:40 (CET)

Si c'est bien à nous de le faire. --Pierre de Lyon (discuter) 6 décembre 2017 à 09:44 (CET)

tout langage L dont les mots décrivent des machines de Turing

Je ne comprends pas cette phrase parce que je ne sais pas ce qu'est un mot qui décrit une machine de Turing. Ne serait-ce pas plutôt le langage engendré par une machine de Turing? Autrement dit on inverse la phrase: il ne s'agit pas d'un langage qui décrit des machines de Turing (décrire une septuplet par un mot n'est pas chose aisé), mais plutôt du langage décrit (ou engendré) par une machine de Turing. --Pierre de Lyon (discuter) 29 novembre 2017 à 13:18 (CET)

Non, dans le contexte, on parle bien de mots décrivant complètement une machine de Turing, comme ce que l'on donnerait en entrée d'une Machine de Turing universelle. Jamian (discuter) 29 novembre 2017 à 13:31 (CET)

C'est ça. Un mot code la table de transition d'une machine de Turing. On suppose sans perte de généralité que tout mot code une machine. --Fschwarzentruber (discuter) 29 novembre 2017 à 15:03 (CET)

Excusez-moi de faire dissensus, mais le théorème de Rice sur les langages, s'énonce sur les langages engendrés L(M) par les machines de Turing M. Voici ma version

Si P est une propriété non triviale sur les langages récursivement ́enumérables le problème de savoir si pour toute machine M, le langage L(M) satisfait P (autrement dit P(L(M)) est indécidable.

--Pierre de Lyon (discuter) 29 novembre 2017 à 16:00 (CET)

C'est exactement la même chose que ce qu'il y a dans le livre de Sipser et ce qu'il y a écrit dans wikipedia. Et non, c'est bien un langage de descriptions de machines de Turing. De manière équivalente, le problème de décision suivant est indécidable :

Entrée : une description d'une machine M

Sortie : oui, si L(M) satisfait P, non sinon

est indécidable. L'entrée du problème est bien une description d'une machine. Donc le langage associé au problème de décision est bien un langage de mots qui décrivent des machines. De manière équivalente, L = {<M> | L(M) satisfait P} est indécidable. Ou de manière équivalente, tout langage L non trivial qui contient des mots <M>, et qui est stable dans le sens suivant "l'appartenance de la description d'une machine M au langage ne dépend que du langage accepté par M" est indécidable. C'est ce qui est écrit dans wikipedia et dans le livre de Sipser aussi. --Fschwarzentruber (discuter) 29 novembre 2017 à 16:19 (CET)

Je note bien ce que tu dis qui va dans mon sens. Il ne s'agit pas du « langage L dont les mots décrivent les machines de Turing » (ce qu'il y a dans wikipédia aujourd'hui), mais du langage de la machine de Turing. Comme je vis en 2017 (pas en 1936) et que je programme en langage de haut niveau, je préfère donner en entrée une machine et pas un codage d'une machine par un mot. Donc on a un d'un côté une machine M et de l'autre le langage L(M) de la machine. --Pierre de Lyon (discuter) 30 novembre 2017 à 09:40 (CET)

« langage L dont les mots décrivent les machines de Turing » n'est pas clair. On devrait plutôt dire « langage L contenant des mots qui décrivent les machines de Turing ». En moins précis : « sous-ensemble L de machines ». Tout sous-ensemble L de machines qui est stable par sémantique (i.e. si M est dans L et que L(M) = L(M'), alors M' est aussi dans L) et non trivial est indécidable. Mais, je préfère coller à la source (le livre de Sipser), qui parle de « langage L contenant des mots qui décrivent les machines de Turing ». — Le message qui précède, non signé, a été déposé par Fschwarzentruber‎ (discuter), le 30 novembre 2017 à 09:31‎

Non ce ne sont pas des langages de mots qui décrivent des machines, mais des machines de Turing qui décrivent des langages de mots. Je ne connais pas le livre de Sipser, mais je connais des livres (que je ne nommerai pas) qui écrivent des choses fausses (heureusement seulement dans les démonstrations, qu'en général personne ne lit) sur les machines de Turing. C'est bien embarrassant quand on prépare un cours. --Pierre de Lyon (discuter) 30 novembre 2017 à 10:58 (CET)

Oui, les livres peuvent contenir des erreurs bien sûr. Mais je ne pense pas que le livre de Sipser contienne une erreur sur le théorème de Rice. Le langage L correspond au problème de décision discuté plus haut. Le langage L est le langage des instances positives de ce problème de décision. C'est donc l'ensemble (des codages) de machines M tel que L(M) satisfait P. --Fschwarzentruber (discuter) 30 novembre 2017 à 11:28 (CET)

Je ne prétends pas que le livre fasse une erreur sur le théorème de Rice. Je dis que ce qui est écrit dans Wikipédia aujourd'hui prête à confusion. Nous disons toi et moi qu'il n'y a pas à parler de langage de codage de machines de Turing (ou d'ensembles de de machines). Je répète notre formulation à laquelle tu adhères, si je comprends bien: Si P est une propriété non triviale sur les langages récursivement ́enumérables le problème de savoir si pour toute machine M, le langage L(M) satisfait P (autrement dit P(L(M)) est indécidable. --Pierre de Lyon (discuter) 30 novembre 2017 à 11:46 (CET)

En surfant sur internet je trouve cette page sur le théorème de Rice par van Glabbeck de Stanford. Il met en gras about the language recognized by Turing machines qui est ce que je dis depuis le début, à savoir que l'on parle de « propriété » sur les machines et de « langages » reconnus par les machines de Turing. Sa formulation est mutatis mutandi la mienne. --Pierre de Lyon (discuter) 30 novembre 2017 à 11:56 (CET)

La formulation ci-dessus avec le problème de décision est celle de mon cours. Pour une source meilleure que Sipser sur ce sujet, je propose Wolper.

Merci pour cet échange. Juste notre désaccord est sur la forme, pas sur le fond. Ce qu'écrit Sipser est juste et équivalent à ce que tu dis, et à ce que dit van Glabbeck. C'est juste que Sipser utilise aussi le mot "langage" pour l'ensemble des instances positives. Je suis d'accord que c'est confus. Je propose de prendre le temps de réfléchir. Je vais citer Wolper comme source secondaire par contre. --Fschwarzentruber (discuter) 30 novembre 2017 à 13:58 (CET)

Proposition écrite sous forme de négation

Je constate qu'il y a deux propositions écrites sous forme de négations:

• « le programme ne rend jamais de valeurs nulles »
• « le programme ne termine jamais par une erreur d'exécution »

J'en avais enlevé une (la deuxième) et elle a été rétablie. Mettre sous forme négative n'a aucun sens puisqu'il s'agit d'un problème de décision. « Décider » c'est affirmer si oui ou non la proposition est vraie ou non. Pire, je pense que mettre la proposition sous forme négative peut troubler le lecteur, car il pourrait croire que décider la proposition sous forme négative pourrait être différent de décider la proposition sous forme positive. --Pierre de Lyon (discuter) 6 décembre 2017 à 09:53 (CET)

Bonjour, tu préfères les formulations suivantes ?

• « les valeurs de retour du programme sont toujours non-nulles »
• « le programme termine toujours sans erreur d'exécution »

--Fschwarzentruber (discuter) 6 décembre 2017 à 10:35 (CET)

Je constate que dans la formulation de la première, il y a une négation. Je propose:

• « Le programme peut rendre une valeur nulle »,
• « Le programme peut se terminer sur une erreur d'exécution ».

qui montre l'émergence de logiques modales, à cause de la modalité « peut ». Mais au moins, il n'y a pas de négation. --Pierre de Lyon (discuter) 6 décembre 2017 à 10:55 (CET)

--Pierre de Lyon (discuter) 6 décembre 2017 à 10:55 (CET)

Je vois. Mais l'idée derrière « les valeurs de retour du programme sont toujours non-nulles » et « le programme termine toujours sans erreur d'exécution » est que cela correspond à des besoins pratiques. 1) La propriété « les valeurs de retour du programme sont toujours non-nulles » est l'exemple discuté dans l'introduction du chapitre sur le théorème de Rice dans le livre de Gilles Lesventes et Olivier Ridoux. Je trouve qu'il a un sens pratique : on peut toujours diviser par le nombre retourné par le programme, puisque le nombre retourné est non nul. 2) Aussi, « le programme termine toujours sans erreur d'exécution » est une propriété que l'on vérifie en pratique. Généralement, on n'aime pas quand un programme peut faire une erreur ;). Si la négation gêne des lecteurs, quid de remplacer "non nul" par "différent de 0" ? --Fschwarzentruber (discuter) 6 décembre 2017 à 12:04 (CET)