Informatique et logique (IN T10)
Le traitement de démonstrations
Une démonstration mathématique est un enchaînement de propositions
tel que chacune d'elles découle des précédentes par une règle
logique. Dans une telle démonstration, il suffit d'une erreur minime
dans une seule étape pour que la démonstration entière soit
fausse. Des programmes informatiques (les ``systèmes de traitement de
démonstrations'') permettent de vérifier, étape par étape, qu'une
démonstration est correcte et d'acquérir la certitude que ce qu'on
affirme est vrai.
Dans certains cas simples, on peut utiliser les ordinateurs non seulement
pour vérifier la correction d'une démonstration, mais également pour
trouver la démonstration elle-même. On parle alors de ``démonstration
automatique''. Même si ces programmes ne démontrent en général que des
théorèmes très simples, ils sont utiles dans de nombreux champs
d'application de l'informatique (l'interrogation de bases de données,
la conception de systèmes experts ...).
La notion de démonstration
La plupart des mathématiciens et des étudiants s'entendent
ordinairement sur ce que sont une proposition et une démonstration. Ils
ne ressentent pas le besoin, sauf dans certains cas très particuliers, de
donner une définition précise de ces notions.
Pourtant le problème de savoir ce qu'est une démonstration ne peut
plus être éludé quand les démonstrations sont manipulées par des
programmes. Les réponses apportées par la logique à ces questions
sont alors centrales. Le choix entre les différentes définitions
possibles de la notion de démonstration est essentiel.
La sécurité informatique
Quand la vie humaine est en danger (industrie ferroviaire, avionique,
...) ou quand les erreurs coûtent trop cher (banque, industrie
spatiale ...), les programmeurs et les concepteurs de circuits n'ont
pas droit à l'erreur. Quelques bugs récents (une panne qui a
privé des dizaines de milliers d'Américains de téléphone pendant
plusieurs heures, une erreur dans le circuit de multiplication d'un
microprocesseur mondialement diffusé ou l'explosion en vol d'une
fusée) ont provoqué une prise de conscience des problèmes de sécurité
informatique.
Une méthode pour développer des systèmes d'information zéro-défaut
consiste à commencer par donner une spécification du programme ou du
circuit développé. La spécification d'un programme est une définition
de la valeur calculée par ce programme en fonction de ses entrées. Un
programme
d'inversion de matrices, par exemple, se spécifie par la formule
A × B = I
où A est la matrice donnée en argument au programme et B la
matrice calculée par le programme. Cette spécification, est une
définition de la notion de matrice inverse beaucoup plus simple qu'un
programme qui peut faire plusieurs centaines de lignes.
Après avoir spécifié et écrit un programme, on doit ensuite démontrer
que le programme vérifie sa spécification. Une telle
démonstration est souvent facile, mais longue et fastidieuse. Pour
construire ces démonstrations ou vérifier leur correction, on utilise
souvent des programmes de traitement de démonstrations.
Programmation en langage mathématique
Une approche plus radicale propose de n'utiliser que des spécifications.
Ainsi on programme l'inversion de matrice en indiquant simplement la
formule A × B = I. Exécuter un programme, par exemple avec
l'entrée
consiste alors à résoudre l'équation
Résoudre une équation consiste à chercher une valeur (la solution de
l'équation) et une démonstration (que la valeur trouvée est solution
de l'équation), c'est donc un problème de démonstration automatique.
Cette approche est à la base des langages de programmation logique
(comme le langage Prolog) et plus récemment des langages de
programmation par contraintes.
Au lieu de laisser l'ordinateur se débrouiller pour trouver, à chaque
exécution, une valeur et une démonstration, on peut l'aider en
donnant, outre la spécification de la notion de matrice
inverse, une démonstration que
pour toute matrice A d'un certain ensemble, il existe une matrice
B, telle que A × B = I. Quand on exécute ce programme, par
exemple sur l'entrée
il suffit d'appliquer cette
démonstration au cas particulier
pour obtenir une
démonstration d'existence d'une matrice inverse de
De cette démonstration, on peut tirer la matrice B et la
démonstration que c'est la matrice inverse de
en appliquant une opération de transformation des démonstrations
appelée ``l'élimination des coupures'' et connue des logiciens depuis
les années trente.
Calculabilité, complexité
Toutes les sciences identifient des impossibles (la quadrature du
cercle, le mouvement perpétuel, la génération spontanée ...).
En informatique, ces impossibles prennent la forme de résultats de non
calculabilité : ``il n'y a pas de programme qui résolve tel
problème'', par exemple ``il n'y a pas de programme qui résolve le
problème de l'arrêt'', ou de bornes à la complexité des programmes
``il n'y a pas de programme qui résolve tel problème en un temps
polynomial'' ...
Par exemple, un problème ouvert, qui défie les informaticiens depuis
plusieurs dizaines d'années, et qui porte le nom barbare de ``problème P
¹ NP'', consiste à montrer qu'il n'y a pas de programme qui reconnaisse
la vérité des propositions sans quantificateurs en un temps polynomial
en fonction de la taille de la formule.
L'interaction entre la logique et les théories de la calculabilité et
de la complexité provient du fait que les problèmes de démonstration
automatique sont des exemples paradigmatiques de problèmes décidables
et de problèmes indécidables (on parle alors de ``problème de
décision''). Plus fondamentalement, la décidabilité et la complexité
d'un problème dépend souvent de la forme logique que prend son
expression.
This document was translated from LATEX by
HEVEA.