| Liste Articles: [0-A] [A-C] [C-F] [F-J] [J-M] [M-P] [P-S] [S-Z] | Liste Catégories | Une page au hasard | Pages liées | ||||||
Le problème de la décision, en allemand Entscheidungsproblem, est le problème en logique symbolique consistant à trouver un algorithme qui décide pour un ensemble de prédicat du premier ordre s'ils sont universellement valide ou non. Alonzo Church et Alan Turing montrèrent indépendamment en 1936 que cela est impossible. Cela a comme conséquence particulière de prouver qu'il est impossible de décider de manière algorithmique si certains énoncés en arithmétique sont vrais ou faux.
La question remonte à Gottfried Leibniz qui, au dix septième siècle, après avoir construit une machine opérationelle de calcul mécanique, rêva de construire une machine qui pouvait manipuler des symboles afin de déteminer les vrais valeurs des énoncés mathématiques. Il compris que le premier pas serait d'avoir un langage formel clair et la plus importante partie de son travail ultérieur sera dirigé vers ce but. En 1928, David Hilbert et Wilhelm Ackermann posèrent la question dans les formes soulignées ci-dessous.
Un énoncé du premier ordre est appelé universellement valide ou logiquement valide s'il suit les axiomes du prédicat de calcul au premier degré. Le théorème de complétude énonce que si un énoncé est universellement valide si et seulement s'il est vrai dans toute interprétation de la formule dans un modèle.
Avant que l'on puisse répondre à la question, la notion d'algorithme doit être définie formellement. Cela fut fait par Alonzo Church en 1936 avec le concept de la calculabilité effective basée sur son lambda-calcul et par Alan Turing la même année avec son concept de la Machine de Turing. Les deux approches sont équivalentes, une instance de la Thèse Church-Turing.
La réponse négative au problème de la décision fut alors donné par Alonzo Church qui prouva qu'il n'y a pas d'algorithme (défini via des fonctions récursives) qui décide pour deux expressions de calculs lambda si elles sont équivalentes ou non. Il s'appuya fortement sur des travaux antérieurs de Stephen Kleene. Turing réduit le problème du Problème d'une fin et ses travaux sont considérés comme beaucoup plus influents que ceux de Church. Les découvertes des deux auteurs furent largement influencés par les recherches de Kurt Gödel sur le théorème d'incomplétude, particulièrement par la méthode d'assigner des nombres à des formules logiques afin de réduire la logique à l'arithmétique.
Dans la théorie de la calculabilité, un problème est un ensemble de questions de longueur finie (chaine de caractères) assocoées à un ensemble de réponses de longueur finie(chaine de caractères). Un problème de décision est un problème dont la réponse est oui ou non. Un exemple courant est « Étant donné un nombre entier, est-il premier ? » Une instance de ce problème de décision est « Est-ce que 17 est premier ? »
Généralement un problème de décision est formalisé par un problème consistant à décider si une chaîne de caractères donnée à un ensemble de chaînes de caractères spécifié, aussi appelé un système formel. L'ensemble contient exactement les questions dont la réponse est oui. Le problème de décision ci-dessus pourrait être formalisé par le langage des chaînes de caractères de 1 et de 0 qui sont la représentation binaire d'un nombre entier.
S'il y a un algorithme qui permet de décider correctement pour toute entrée si elle appartient au langage, ce problème est dit décidable (et le langage est dit récursif) sinon il est dit indécidable. S'il y a un algorithme qui répond toujours oui quand la chaîne appartient au langage mais qui peut tourner en boucle sans jamais s'arrêter si elle n'appartient pas au langage alors le problème est dit partiellement décidable (et le langage est dit récursivement énumérable). Dans la Théorie de la calculabilité on étudie quels langages sont décidables en utilisant diverses restrictions. Dans la Théorie de la complexité on étudie combien de ressources (temps, mémoire, processeurs, etc.) requiert un problème de décision décidable.
Les problèmes de décision sont importants car n'importe que problème général avec une réponse sur n bits peut être transformée en un problème de décision (avec une réponse oui' ou non). Résoudre le problème général ne peut pas être n fois plus dur à résoudre que le problème de désision. Il y a plusieurs façons de faire cette transformation. Par exemple si le problème général est :
Le problème de décision associé est
Les arguments de Turing suivent. Supposons que nous avons un algorithme de décision générale de premier ordre logique. La question si une machine de Turing donnée s'arrete ou non peut être formulée comme un énoncé du premier ordre, lequel serait alors résolvable par l'algorithm de décision. Mais Turing avait prouvé précédement qu'il n'y a pas d'algorithm général qui peut décider si une machine de Turing donnée s'interrompt.
Il est important de réaliser que si nous nous restraignons à une théorie spécifique de premier ordre avec des objets constants déterminés, constantes de fonctions, prédicats constants et des axiomes sujets, la vérité des énoncés dans cette théorie pourrait très bien être décidable algorithmicallement. Un exemple de cela est donné par l'Arithmetique Presburger.
Cependant, la théorie générale du premier ordre des nombres naturels exprimé dans l'arithmétique de Peano ne peut être décidé par un tel algorithme. Ceci suit aussi l'argument de Turing indiqué ci-dessus.
References:


