Static Wikipedia February 2008 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu

Web Analytics
Cookie Policy Terms and Conditions Théorème de Rice - Wikipédia

Théorème de Rice

Un article de Wikipédia, l'encyclopédie libre.

En théorie de la calculabilité, le théorème de Rice dit que toute propriété non triviale (c.-à-d. qui n'est pas toujours vraie ou toujours fausse) sur la sémantique dénotationnelle d'un langage de programmation Turing-complet est indécidable. Il s'agit d'une généralisation du problème de l'arrêt.

Ce théorème est la reformulation « intuitive » du corollaire B de la publication originale de Rice (1953).

Sommaire

[modifier] Description et preuve intuitive

Tout d'abord, rappelons qu'il n'existe pas de programme halt permettant de savoir si un programme prog s'arrête ou non avec une chaîne de bits ch en entrée (pour une preuve voir la page sur le problème de l'arrêt). On peut obtenir un résultat plus général.

Précisons quelques notations: prog(ch) est la chaîne obtenue en sortie si on ne boucle pas en lançant prog avec ch en entrée, on note ch_prog la chaîne codant le programme prog, et ch1,ch2 désigne la chaîne obtenue en concaténant les deux chaînes ch1 et ch2.

Supposons par exemple, qu'il existe un programme square tel que square(ch_prog,ch) retourne 1 si on ne boucle pas et que prog(ch) code le carré de l'entier codé par ch, et 0 sinon.

On peut alors construire le programme trouble suivant, dans lequel prog est un programme quelconque et ch2 une chaîne quelconque:

trouble(ch1)

1. faire prog(ch2)

2. retourne le carré de l'entier codé par ch1

Nous obtenons que trouble(ch1) existe et code le carré de l'entier codé par ch1 si et seulement si prog s'arrête avec ch2 en entrée. Ainsi, si square existe, alors halt existe; or on sait que halt n'existe pas.

Dans notre exemple au-dessus on peut remplacer square par n'importe quelle fonction, ce qui nous permet de prouver le théorème de Rice: Pour toute fonction f et tout programme prog, il n'existe pas de programme pour vérifier que prog est une implantation de f.

[modifier] Impact pratique

La formulation pratique de ce théorème est qu'il n'existe pour aucune propriété intéressante (non triviale) portant sur le résultat final d'un programme un algorithme permettant, au vu du code source d'un programme, de décider s'il satisfait cette propriété. De telles propriétés indécidables incluent:

  • « le programme ne termine pas par une erreur d'exécution »
  • « le programme calcule un résultat correct par rapport à la spécification »

En d'autres termes, aucune méthode d'analyse statique de programmes ne peut donner des résultats sûrs et dans un temps fini pour tous les programmes quels qu'ils soient, et ce quelle que soit la propriété à tester. La restriction ne s'applique en revanche pas forcément aux seuls programmes de taille donnée.

Par exemple, un ramasse-miettes (logiciel qui libère la mémoire inutilisée) optimal et sûr est impossible; en effet, savoir si l'on doit libérer ou non la mémoire dépend du comportement futur du système, qu'il est impossible de prévoir. Ceci explique que toutes les techniques de ramasse-miettes soient conservatrices, et puissent garder en mémoire des blocs inutiles, permettant ainsi des fuites de mémoire.

Ainsi, dans le programme suivant en langage C (supposons que p n'intervienne pas ailleurs), déterminer si l'on doit libérer le bloc mémoire sitôt après son allocation est équivalent à décider le problème de l'arrêt sur f().

char *p = malloc(1000);
f();
*p = 1;

[modifier] Définition formelle

[modifier] Première partie

On suppose que l'on travaille avec un langage de programmation Turing-complet (toutes les fonctions calculables en un sens intuitif, voir thèse de Church-Turing, peuvent se programmer dans ce langage). Soit φ(x,y) le résultat de l'évaluation du programme x sur l'entrée y ∈ ℕ. Si le programme x ne termine pas pour l'entrée y la fonction φ n'est pas définie pour ces entrées, il s'agit donc d'une fonction nécessairement partielle, φ(x,y) ne désigne pas forcément quelquechose (on peut ajouter ⊥ pour désigner la valeur spéciale « ne termine pas »). Notons P un ensemble de programmes calculant des fonctions partielles (certaines pouvant être partout définies, on ne précisera plus dans la suite) de ℕ dans ℕ. Supposons que l'ensemble des x tels que y ↦ φ(x,y) est dans P soit récursif. Alors, P = ∅ ou P est l'ensemble de tous les programmes (calculant une fonction partielle de ℕ dans ℕ).

Dit autrement, d'après le théorème de Rice, tout ensemble de programmes extensionnel, c'est à dire contenant tous les programmes calculant une fonction partielle donnée dès qu'il en contient un, et non trivial, c'est à dire différent de l'ensemble des programmes et de ∅, n'est pas un ensemble récursif.

Si l'on veut vraiment formaliser il faut dire ce que sont les programmes. Pour ce genre de propriété une représentation assez grossière suffit. Dans la théorie de la calculabilité (ou récursivité) initiée par Kleene, les programmes sont codés par des entiers (en informatique ce sont bien des suites de lettres, donc de bits, donc ultimement des entiers). La fonction φ est la fonction partielle d'énumération de Kleene : c'est une fonction récursive partielle de ℕ × ℕ ↦ ℕ qui énumère toutes les fonctions récursives partielles de ℕ ↦ ℕ, qui sont donc les fonctions φx : y ↦ φ(x,y). L'entier x est appelé indice (ou code) de la fonction φx. Tout comme il y a clairement une infinité de programmes calculant la même fonction (on peut ajouter autant que l'on veut des instructions à un programme qui n'ont pas d'effet sur le résultat), une fonction récursive partielle possède une infinité d'indices.

Un ensemble d'entiers (donc d'indices de fonctions récursives partielles) W est dit extensionnel quand deux entiers i et j qui sont les indices d'une même fonction récursive partielle sont soit tous deux dans W, soit tous deux hors de W :

i, j ∈ ℕ [(iW et φi = φi) ⇒ jW]

Le théorème de Rice, affirme alors que :

Théorème de Rice. Un sous-ensemble extensionnel de ℕ non trivial (différent de ℕ et de ∅) n'est pas récursif.

Il faut remarquer que toutes ces notions, interprétées au sens strict sur les entiers, sont sensibles au codage. Il s'agit donc bien de résultats sur les fonctions calculables.

[modifier] Seconde partie

Du point de vue des ensembles récursivement énumérables, le théorème de Rice dit que toute propriété non triviale sur ces ensembles est indécidable. Une telle propriété est dite monotone si, et seulement si, pour tous ensembles récursivement énumérables A et B tels que A est inclus dans B, on a P(A) -> P(B). Par exemple, "A est un ensemble fini" n'est pas monotone, alors que "A contient l'élément x" l'est. Alors, aucune propriété non-monotone sur les ensembles récursivement énumérables n'est récursivement énumérable (ou semi-décidable).

[modifier] Démonstration du théorème de Rice

On montre que la décision du problème de l'arrêt peut se réduire à la décision de toute propriété non triviale sur un ensemble récursivement énumérable. On représente tout ensemble récursivement énumérable par la machine de Turing qui l'accepte. Soit P une propriété décidable et non triviale sur les ensembles récursivement énumérables. Soit P(∅)="Faux" (si ce n'est pas le cas, on raisonne pareillement avec la négation de P). Donc, il existe un ensemble récursivement énumérable A qui satisfait P. Soit K une machine de Turing qui accepte A. P étant décidable, il existe donc une machine de Turing MP qui, pour toute représentation d'une machine de Turing, décide si l'ensemble récursivement énumérable accepté par cette machine satisfait P ou non.

Dès lors, on construit une machine de Turing H prenant en entrée la représentation d'une machine de Turing M suivie d'une entrée x. L'algorithme de H est le suivant :

1. Construire la représentation d'une machine de Turing T qui, sur une entrée d :
  • Simule l'exécution de M sur x
  • Simule l'exécution de K sur d et renvoie le résultat.
2. Simuler l'exécution de MP sur la représentation de T et renvoyer le résultat.

Si M s'arrête sur x, l'ensemble accepté par T est A. Cet ensemble satisfaisant P, la seconde phase de l'algorithme renverra "Vrai". Si M ne s'arrête pas sur x, l'ensemble accepté par T est ∅. Cet ensemble ne satisfaisant pas P, la seconde phase de l'algorithme renverra "Faux".

La machine H calcule donc de manière totale le problème de l'arrêt. Celui-ci étant indécidable, par contradiction, P est donc indécidable.

[modifier] Démonstration de la seconde partie

De manière analogue, on montre que la semi décision de la négation du problème de l'arrêt peut se réduire à la semi-décision de toute propriété non-monotone sur les ensembles récursivement énumérables.

Soit P une propriété non-monotone et semi-décidable. Il existe donc deux ensembles récursivement énumérables A et B, calculés respectivement par des machines de Turing MA et MB tels que :

  • A est inclus dans B
  • A satisfait P
  • B ne satisfait pas P.

De plus, il existe une machine de Turing MP qui, pour toute représentation d'une machine de Turing, s'arrête et accepte si l'ensemble récursivement énumérable accepté par cette machine satisfait P.

Dès lors, on peut construire une machine de Turing H prenant en entrée la représentation d'une machine de Turing M suivie d'une entrée x dont l'algorithme est le suivant :

1 Construire la représentation d'une machine de Turing T qui, sur une entrée y :
1 Exécute en parallèle
  • MA sur y
  • MB sur y
  • M sur x
2 Accepte y si
  • MA accepte y ou bien
  • MB accepte y ET M s'arrête sur x
2 Exécuter MP sur la représentation de T et renvoyer le résultat.

Par «exécuter en parallèle», on entend que la machine T exécute un pas MA sur y, puis un pas de MB sur y, puis un pas de M sur x, puis un second pas de MA sur y, et ainsi de suite. Autrement dit, on «entrelace» les pas de calcul d'une machine avec ceux de l'autre machine.

Si M s'arrête sur x, T accepte y si, et seulement si MA ou MB accepte y, et comme A est inclus dans B, cela reviens à dire si et seulement si y appartient à B. Donc, T accepte exactement l'ensemble B, qui, par hypothèse, ne vérifie pas P. Par consiquent, MP n'accepte pas T. (P étant supposé semi-décidable, MP peut même ne pas s'arrêter du tout) Si M ne s'arrête pas sur x, T accepte y si et seulement si y appartient à A. T accepte donc exactement l'ensemble A qui, par hypothèse, satisfait P. Par conséquent, MP accepte T (et finit donc par s'arrêter, par définition de la semi-décidabilité). La machine H calcule donc la négation du problème de l'arrêt. Celui-ci n'étant pas semi-décidable, par contradiction, P ne peut donc pas être semi-décidable.

[modifier] Références

  • Hartley Rogers, Jr, Theory of Recursive Functions and Effective Computability, MIT Press, ISBN 0262680521, page 34
  • H. G. Rice, Classes of Recursively Enumerable Sets and Their Decision Problems, Transactions of the American Mathematical Society, volume 74, numéro 2, mars 1953 (JSTOR)
  • Pierre Wolper, Introduction à la calculabilité, InterÉditions, 1991, ISBN 2100048538
  • Neil D. Jones, Computability and Complexity From a Programming Perspective, MIT Press, ISBN 0262100649
Portail de l'informatique – Accédez aux articles de Wikipédia concernant l’informatique.
Static Wikipedia 2008 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -

Static Wikipedia 2007 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -

Static Wikipedia 2006 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu