Entscheidungsproblem -Entscheidungsproblem

En mathématiques et en informatique , l' Entscheidungsproblem ( prononcé [ɛntˈʃaɪ̯dʊŋspʁoˌbleːm] , en allemand pour "problème de décision") est un défi posé par David Hilbert et Wilhelm Ackermann en 1928. Le problème demande un algorithme qui considère, en entrée, un énoncé et des réponses "Oui" ou "Non" selon que l'énoncé est universellement valable , c'est-à-dire valable dans toute structure satisfaisant aux axiomes.

Théorème de complétude

Par le théorème de complétude de la logique du premier ordre , une déclaration est universellement valable si et seulement si elle peut être déduite des axiomes, donc le Entscheidungsproblem peut également être considéré comme demandant un algorithme pour décider si une déclaration donnée est prouvable à partir des axiomes en utilisant les règles de la logique .

En 1936, Alonzo Church et Alan Turing ont publié des articles indépendants montrant qu'une solution générale au problème d' Entscheidungs est impossible, en supposant que la notion intuitive de " effectivement calculable " est capturée par les fonctions calculables par une machine de Turing (ou de manière équivalente, par celles exprimables dans le calcul lambda ). Cette hypothèse est maintenant connue sous le nom de thèse Church-Turing .

Historique du problème

L'origine du problème d'Entscheidungs remonte à Gottfried Leibniz , qui au XVIIe siècle, après avoir construit une machine à calculer mécanique à succès , rêvait de construire une machine capable de manipuler des symboles afin de déterminer les valeurs de vérité des énoncés mathématiques. Il s'est rendu compte que la première étape devrait être un langage formel propre , et une grande partie de son travail ultérieur a été dirigé vers cet objectif. En 1928, David Hilbert et Wilhelm Ackermann posèrent la question sous la forme décrite ci-dessus.

Dans la continuité de son « programme », Hilbert posa trois questions lors d'une conférence internationale en 1928, dont la troisième devint connue sous le nom de « Hilbert's Entscheidungsproblem ». En 1929, Moses Schönfinkel a publié un article sur des cas particuliers du problème de décision, qui a été préparé par Paul Bernays .

Jusqu'en 1930, Hilbert croyait qu'il n'y aurait pas de problème insoluble.

Réponse négative

Avant de pouvoir répondre à la question, la notion d'« algorithme » devait être formellement définie. Cela a été fait par Alonzo Church en 1935 avec le concept de "calculabilité effective" basé sur son λ-calcul et par Alan Turing l'année suivante avec son concept de machines de Turing . Turing a immédiatement reconnu que ce sont des modèles de calcul équivalents .

La réponse négative au problème d'Entscheidungs a ensuite été donnée par Alonzo Church en 1935-36 ( théorème de Church ) et indépendamment peu de temps après par Alan Turing en 1936 ( preuve de Turing ). Church a prouvé qu'il n'y a pas de fonction calculable qui décide pour deux expressions de λ-calcul données si elles sont équivalentes ou non. Il s'est fortement appuyé sur les travaux antérieurs de Stephen Kleene . Turing a réduit la question de l'existence d'une « méthode générale » qui décide si une machine de Turing donnée s'arrête ou non (le problème de l' arrêt ) à la question de l'existence d'un « algorithme » ou d'une « méthode générale » capable de résoudre le problème d' Entscheidungs . Si « algorithme » est compris comme étant équivalent à une machine de Turing, et avec la réponse à cette dernière question négative (en général), la question sur l'existence d'un algorithme pour le problème d'Entscheidungs doit également être négative (en général). Dans son article de 1936, Turing dit : " Correspondant à chaque machine informatique 'it', nous construisons une formule 'Un(it)' et nous montrons que, s'il existe une méthode générale pour déterminer si 'Un(it)' est prouvable, alors il existe une méthode générale pour déterminer si 'il' imprime jamais 0" .

Le travail de Church et de Turing a été fortement influencé par les travaux antérieurs de Kurt Gödel sur son théorème d'incomplétude , en particulier par la méthode consistant à attribuer des nombres (une numérotation de Gödel ) à des formules logiques afin de réduire la logique à l'arithmétique.

Le problème Entscheidungs est lié au dixième problème de Hilbert , qui demande un algorithme pour décider si les équations diophantiennes ont une solution. L'inexistence d'un tel algorithme, établi par Yuri Matiyasevich en 1970, implique également une réponse négative au problème Entscheidungs.

Certaines théories du premier ordre sont décidables algorithmiquement ; les exemples de ceci incluent l'arithmétique de Presburger , les vrais champs fermés et les systèmes de type statique de beaucoup de langages de programmation . La théorie générale du premier ordre des nombres naturels exprimée dans les axiomes de Peano ne peut cependant pas être décidée avec un algorithme.

Procédures de décision pratiques

Disposer de procédures de décision pratiques pour des classes de formules logiques est d'un intérêt considérable pour la vérification de programme et la vérification de circuit. Les formules logiques pures booléennes sont généralement décidées à l'aide de techniques de résolution SAT basées sur l' algorithme DPLL . Formules conjonctives sur l' arithmétique rationnelle ou réelle linéaire peut être décidé en utilisant l' algorithme simplex , les formules en arithmétique linéaire en nombres entiers ( arithmétique Presburger ) peuvent être décidées en utilisant l'algorithme de Cooper ou William Pugh de test de Omega . Les formules avec négations, conjonctions et disjonctions combinent les difficultés du test de satisfiabilité avec celles de la décision des conjonctions ; elles sont généralement décidées de nos jours en utilisant des techniques de résolution SMT , qui combinent la résolution SAT avec des procédures de décision pour les conjonctions et les techniques de propagation. L'arithmétique polynomiale réelle, également connue sous le nom de théorie des champs réels fermés , est décidable ; c'est le théorème de Tarski-Seidenberg , qui a été implémenté dans les ordinateurs en utilisant la décomposition algébrique cylindrique .

Voir également

Remarques

Les références

Liens externes