Utilisateur:ManiacParisien/Brouillons/Math-9
Le terme Logique pour l’informatique désigne les chevauchements et interactions entre le domaine de la logique et celui de l'informatique. Elle concerne notamment l’étude et la comparaison de l'expressivité de divers modèles. Le sujet peut être divisé en plusieurs thèmes :
- Calculabilité et définissabilité
- Complexité algorithmique
- Complexité descriptive
L'interaction entre l'informatique et la logique est basée sur les possibilités d'expression que fournit la logique pour formuler des problèmes informatiques comme la calculabilité ou la complexité. Ces moyens logiques sont nombreux, et en retour, des besoins de raffinements dans les applications informatiques ont provoqué des nouveaux développements en logique.
Calculabilité et définissabilité[modifier | modifier le code]
La théorie de la calculabilité est basée sur des concepts définis en logique, et a été étudiée par eux longtemps avant l'apparition du premier ordinateur. Plusieurs formalisations mathématiques de ce que peut être une méthode de calcul existent et on peut montrer qu'un grand nombre d'entre elles (fonctions récursives, machine de Turing, lambda-calcul, machine à compteurs, automate cellulaire, etc.) sont équivalentes, c'est-à-dire qu'elles définissent exactement les mêmes fonctions calculables. Formellement, une fonction calculable est donc une fonction calculable selon l'une de ces définitions, par exemple le lambda-calcul[1]. La thèse de Church énonce que les définitions mathématiques équivalentes ci-dessus capturent bien le concept intuitif de méthode de calcul fonctionnant en temps fini.
D'autres concepts de logique ont des influences importantes sur l'informatique. Les logiques du premier et du second ordre ont des liens très étroits avec la théorie des automates finis sur les mots, et sur les arbres. Ces logiques interviennent également sur les ensembles d'arbres et en théorie des jeux. La correspondance de Curry-Howard est à la base de la formulation théorique qui voit un programme comme une formule logique dont on peut chercher à établir qu'elle est correcte et consistente.
Les théorèmes suivants de la logique sont importants pour leur conséquences en informatique théorique.
- Le théorème de Löwenheim-Skolem (1919) est un énoncé de la logique du premier ordre. Il dit que si une théorie possède un modèle infini dénombrable, il en possède un de toute cardinalité infinie.
- Le théorème de complétude de Gödel (1929) (établi par Kurt Gödel) montre l'équivalence des démonstrations syntaxique et sémantique dans le calcul des prédicats du premier ordre.
- Le théorème d'incomplétude (1931) (établi lui aussi par Kurt Gödel) montre qu'il n'existe pas desystème logique dans lequel on peut prouver sa propre consistence.
- Le concept de la calculabilité, énoncé par David Hilbert sous le terme Entscheidungsproblem (problème de décision), et les problèmes de décidabilité, formalisés par Alan Turing et Alonzo Church en 1936 indépendamment, montrent en particulier que tout n'est pas démontrable ou calculable par ordinateur.
- L'indécidabilité du dixième problème de Hilbert est un énoncé démontré par Iouri Matiassevitch en 1970. Il dit que le problème de savoir si un polynôme en plusieurs variables à coefficients entiers s'annule en un point à coordonnées entières est indécidable.
Complexité algorithmique[modifier | modifier le code]
Complexité descriptive[modifier | modifier le code]
References[modifier | modifier le code]
- Historiquement, la première caractérisation formelle et mathématique des algorithmes (voir Origins of Recursive Function Theory in Annals of the History of Computing, Vol. 3 No. 1, janvier 1981).
Livres[modifier | modifier le code]
- Olivier Carton, Langages formels, calculabilité et complexité, [détail de l’édition] (lire en ligne)
- Jean-Michel Autebert, Calculabilité et décidabilité, Dunod, (ISBN 978-2225826320)
- Pierre Wolper, Introduction à la calculabilité : cours et exercices corrigés, Paris, Dunod, , 3e éd. (ISBN 978-2100499816).
- Mordechai Ben-Ari, Mathematical Logic for Computer Science, Springer-Verlag, , 2e éd. (ISBN 1-85233-319-7)
- George S. Huth et Mark Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2012 (8e réimpression), 2e éd. (présentation en ligne)
- George S. Boolos, John P. Burgess et Richard C. Jeffrey, Computability and Logic, Cambridge University Press, , 5e éd. (ISBN 0-521-54310-X)
- Stanley N. Burris, Logic for Mathematics and Computer Science, Prentice Hall, (ISBN 0-13-285974-2)