Previous Next Contents

5  Digressions

Les sections suivantes sont techniques et demandent quelques connaissances en théorie de la complexité et en théorie des treillis. Le lecteur peu curieux pourra les laisser de côté en première lecture.



5.1  Pouvoir d'expression de la logique propositionnelle classique

Discutons du pouvoir d'expression de la logique propositionnelle classique.

Tout d'abord, la logique propositionnelle est un formalisme que l'on peut coder sous forme de matériel : on peut construire des circuits en reliant des portes les unes aux autres, chaque porte réalisant un connecteur logique. (Par exemple, une porte NAND est un bout de circuit à deux entrées et une sortie; dans les réalisations positives de la logique, lorsque la tension des deux entrées est au niveau bas, représentant F, la sortie est haute, et si une entrée est haute, alors la sortie est basse.) Elle ne peut pas décrire des circuits avec des connexions cycliques (comme l'on fait usuellement pour créer des dispositifs instables comme des horloges), mais presque tous les circuits dans un ordinateur contemporain sont des superpositions de portes logiques. En simplifiant, un ordinateur réel est une grosse formule propositionnelle codée sous forme de matériel, plus une horloge (qui envoie des suites de T et F à une vitesse prédéfinie) et des composants d'interface. En somme, la logique propositionnelle est essentiellement suffisamment expressive pour décrire n'importe quel ordinateur réel.

Cet argument est légèrement trompeur, non seulement parce que la formule propositionnelle représentant un ordinateur est gigantesque, mais aussi parce que les ordinateurs réels sont des approximations de ce que nous aimerions qu'un ordinateur soit. Un ordinateur idéal aurait une quantité de mémoire infinie, et en effet la mémoire virtuelle et les appareils de stockage secondaire sont des moyens pour approcher les ordinateurs de cet idéal.

Il y a plusieurs modèles mathématiques des ordinateurs idéaux, et clairement, plus simples ils sont, plus faciles ils seront à manipuler. Un des modèles d'ordinateur idéal les plus simples est la machine de Turing. En quelques mots, une machine de Turing est une machine d'états finis (un automate, avec un nombre fini d'états et de transitions entre ces états), plus une tête de lecture/écriture voyageant sur une bande infiniment longue. La bande est une suite linéaire de symboles pris dans un alphabet à au moins deux lettres, et s'étend à l'infini dans les deux directions. La machine de Turing calcule en lisant la lettre sous la tête de lecture/écriture, l'utilise pour décider d'une transition à suivre depuis son état courant jusqu'à l'état suivant, d'une lettre à écrire à la place de la lettre lue, et de la direction du mouvement de la tête (une case en avant ou une case en arrière). La machine procède ainsi jusqu'à ce qu'elle atteigne une case spéciale appelée état final. Les machines de Turing représentent des fonctions partielles des mots vers les mots : écrivez le mot de départ sur la bande, entre des délimiteurs spéciaux, le premier délimiteur se situant juste sous la tête; lancer la machine de Turing, et si elle termine, lire le mot écrit sur la bande à la fin de l'exécution.

Les machines de Turing sont universelles, en ce sens que l'ensemble des fonctions qu'elles calculent est exactement l'ensemble de toutes les fonctions calculables. En pratique, on est plus intéressé par savoir quelles fonctions peuvent être calculées sur un ordinateur idéalisé en un temps réaliste, autrement dit quelles fonctions sont tractables. Des recherches ont montré qu'un critère suffisamment bon pour définir un ``temps réaliste'' était un ``temps majoré par un polynôme de degré bas en la taille de l'argument d'entrée''. En particulier, si la borne supérieure des temps nécessaires à la résolution d'un problème est une exponentielle de la taille de l'entrée, on considère le problème comme intractable. Un résultat fondamental est qu'un problème est tractable sur une machine de Turing si et seulement si il est tractable sur la plupart des autres ordinateurs idéalisés, y compris notre ordinateur avec une mémoire infinie (voir plus haut). L'étude de la tractabilité et de l'intractabilité des problèmes est le sujet de la théorie abstraite de la complexité [GJ79].

Le pouvoir expressif de la logique propositionnelle est alors capturée par le théorème suivant, dû à Stephen Cook en 1971. Supposons que nos machines de Turing ont deux états finaux ``oui'' et ``non''; nous lui soumettrons des questions de la forme ``la formule F est-elle satisfiable ?'', et nous lirons la réponse dans l'état dans lequel la machine termine. De plus, les machines de Turing peuvent fonctionner soit de façon déterministe (la donnée de l'état courant et de la lettre lue détermine complètement l'état suivant, la lettre à écrire et la direction du mouvement) ou de façon non déterministe (l'état courant et la lettre lue déterminent plusieurs actions possibles différentes). Une machine de Turing déterministe accepte son argument d'entrée si elle termine dans l'état ``oui''; une machine de Turing non déterministe accepte son entrée s'il existe un chemin d'exécution qui termine dans l'état ``oui''. Remarquer que l'on définit les problèmes de décision comme étant des fonctions à valeurs booléennes :


Théorème 41  [Cook]  Soit SATle problème de décision suivant :

ENTRÉE : une formule propositionnelle F,

QUESTION : F est-elle satisfiable ?

De façon équivalente, SAT est une fonction qui associe vrai à F si et seulement si F est satisfiable.

Soit NP la classe des problèmes de décision f tels que f(x) est vrai si et seulement si il existe une machine de Turing non déterministe qui accepte l'entrée x en temps polynomial en la taille de x. (En bref, NP est la classe des problèmes résolubles ``en temps polynomial non déterministe''.)

Alors SAT est NP-complet, c'est-à-dire :


Ce théorème peut être lu de deux façons. La première est que NP est (probablement, cela n'a été ni prouvé ni contredit) beaucoup plus grande que la classe P des problèmes tractables. En particulier, NP contient de nombreux problèmes que l'on ne sait pas, à l'heure actuelle, résoudre en un temps moins qu'exponentiel en général. Le fait que SAT soit NP-difficile (la deuxième condition dans la définition ci-dessus de la NP-complétude) signifie que SAT est au moins aussi difficile que tous ces problèmes.

La deuxième lecture du théorème est la suivante. Étant donnée la représentation d'une machine de Turing non déterministe M avec son argument d'entrée déjà codé sur sa bande, nous voulons savoir si M accepte son argument. Nous pourrions exécuter M pour le découvrir, mais la preuve du théorème de Cook construit en fait une formule propositionnelle F qui est satisfiable si et seulement si M accepte. En somme, le problème de la satisfiabilité en logique propositionnelle a exactement le même pouvoir d'expression que les machines de Turing non déterministes en temps polynomial.

Ceci nous permet de quantifier le pouvoir d'expression de la logique propositionnelle de façon plus précise : NP est très certainement plus expressive que P (autrement dit, nous pouvons exprimer des problèmes, et même des problèmes non tractables en logique propositionnelle); d'un autre côté, NP est aussi très certainement beaucoup plus petite que DEXPTIME, la classe de tous les problèmes que l'on peut résoudre en temps exponentiel d'un polynôme de la taille de l'entrée sur une machine déterministe (et donc, il y a de nombreux problèmes intractables, solubles en temps exponentiel comme SAT, mais qui ne peuvent très certainement pas être exprimés comme la satisfiabilité d'une formule propositionnelle fabricable en temps polynomial).



5.2  Algèbres booléennes

Au lieu d'utiliser des systèmes de déduction pour déterminer si une formule propositionnelle est valide (ou satisfiable), il est parfois pratique d'utiliser une théorie équationnelle de l'équivalence logique, et d'essayer de dériver T en remplaçant les équivalents dans cette théorie.

Le langage des formules à équivalence propositionnelle classique près est en fait celui des algèbres booléennes. D'abord, nous définisson les treillis booléens :


Définition 42  Un treillis est un ensemble non vide L muni d'un ordre partiel £ tel que tout sous-ensemble fini S de L a une borne supérieure Ú S et une borne inférieure Ù S.

Nous notons T=ÙØ (le plus grand élément de L), F=ÚØ (le plus petit élément de L), aÙ b au lieu de Ù{a,b}, aÚ b au lieu de Ú{a,b}.

Nous disons que L est un treillis distributif si et seulement si Ù distribue par rapport à Ú, et Ú distribue par rapport à Ù, c'est-à-dire aÚ(bÙ c)=(aÚ b)Ù(aÚ c) et aÙ(bÚ c)=(aÙ b)Ù(aÙ c).

Nous disons qu'un treillis distributif est un treillis booléen s'il est muni d'une opération de complémentation ¬ telle que aÚ¬ a=T, aÙ¬ a=F, et ¬¬ a=a.


Johnstone ([Joh92], p.7) résume élégamment l'essence des algèbres booléennes en disant que, en somme, leurs axiomes sont ``tout ce que vous pouvez dire d'un ensemble à deux éléments [dans le langage de l'algèbre universelle]''. En effet :


Définition 43  Une algèbre booléenne est un ensemble non vide A contenant deux éléments T, F, et muni d'opérations Ù, Ú, ¬ obéissant aux équations suivantes :


Tout treillis booléen définit clairement une algèbre booléenne. Réciproquement, toute algèbre booléenne décrit un treillis booléen si l'on définit a£ b comme ¬ aÚ b=T (ou de façon équivalente, aÙ b=a, ou encore aÚ b=b).

Le résultat de complétude (que nous ne prouverons pas) est qu'une formule F est valide si et seulement si l'on peut transformer F en T en un nombre fini d'étapes de réécriture utilisant les équations ci-dessus.

Comme les algèbres booléennes sont équivalentes aux treillis booléens, nous pouvons aussi prouver des formules en appliquant les lois des treillis booléens à la place. Ceci fournit parfois des preuves plus courtes à la main. À notre connaissance, ceci n'a pas été approfondi dans le domaine de la démonstration automatique.

Une autre idée est d'utiliser des anneaux booléens au lieu d'algèbres booléennes. Ceci revient à axiomatiser Ù, Å (le ou exclusif, c'est-à-dire la négation de Û), T (vrai) et F (faux), et à les utiliser au lieu de Ù, Ú et ¬. Les axiomes peuvent alors être orientés sous forme de règles de réécriture [Hsi85], modulo associativité et commutativité de Ù et Å. Les règles de traduction sont : Et les règles de simplification sont : La forme normale qui en résulte (modulo associativité et commutativité de Ù et Å) est appelée forme normale de Reed-Muller de la formule. Comme pour les BDD, elle est canonique, et peut être construite depuis le bas, comme suit.

On code la forme normale de Reed-Muller d'une formule sous forme d'un ensemble d'ensembles de variables. (Si on se donne un ordre sur les variables, on peut représenter un ensemble de variables sous forme d'une liste ordonnée de ces variables sans duplication, et un ensemble d'ensembles de variables sous forme d'une liste de ces listes, ordonnée lexicographiquement par exemple.) Les ensembles internes de variables sont vus comme des conjonctions de leurs variables, et l'ensemble externe est vu comme le ou exclusif de ses éléments.

F est alors l'ensemble vide Ø, et T est le singleton {Ø}. Une variable A est codée sous forme de {{A}}. Le ou exclusif FÅF' de deux formes de Reed-Muller F et F' est calculé comme la différence symétrique (F\F') È (F'\F) des deux ensembles. La conjonction FÙF' de deux formes de Reed-Muller F et F' est la différence symétrique de tous les {a È a'}, où aÎF et a'ÎF'. Notons finalement que la forme normale de Reed-Muller peut se coder sous une forme très proche des BDD, en utilisant les ZBDD (zero-suppressed BDD) de Shin-Ichi Minato [Min93], qui sont des représentations compactes d'ensembles d'ensembles.



5.3  Logique propositionnelle quantifiée

Il est parfois intéressant d'ajouter des quantificateurs au langage de la logique propositionnelle. Ceci n'ajoute pas de pouvoir d'expression, mais peut raccourcir de façon significative certaines formules propositionnelles.

Si F est une formule, et A est une variable propositionnelle, alors nous définissons " A·F (``pour tout A, F'') comme F[T/A] Ù F[F/A], où T et F sont deux constantes nouvelles telles que [T]r=T et [F]r=F, comme dans les BDD. De même, $ A· F (``il existe A tel que F'') se définit comme F[T/A]ÚF[F/A].

Nous pourrions aussi bien définir " A·F et $ A·F directement en leur donnant une sémantique (dérivée des formules ci-dessus), et en étendant les systèmes de déduction pour traiter les nouveaux opérateurs. Par exemple, nous pourrions étendre LK0 en ajoutant les règles de déduction suivantes :



et ceci produirait exactement la même logique.

La logique propositionnelle quantifiée se code facilement dans les BDD : remplacer A par T (resp. F) revient à remplacer tous les sous-BDD de la forme A ¾® F+; F- par F+ (resp. F-), et à réduire le BDD. On code alors " et $ en prenant la conjonction ou la disjonction des BDD résultants.

L'utilisation de la logique propositionnelle quantifiée est commune en vérification de matériel, par exemple. Elle est en fait un ingrédient essentiel de la définition des procédures de vérification de modèle (``model-checking'' en anglais), que nous examinerons plus tard.

Noter que nous ne sommes pas limités à une seule alternance de quantificateurs, et que nous pouvons exprimer des propositions de la forme Q1 A1·... Qn An·F, où les Qi sont soit " soit $. Si nous devions exprimer les quantifications sous forme de conjonctions ou de disjonctions, ceci expanserait la formule F exponentiellement en général, ce qui veut dire qu'il serait déjà infaisable d'écrire la formule sans utiliser de quantificateurs. Sur les BDD, on peut le faire en général, parce que dans les bons cas, le partage et la réduction contribuent à faire que le BDD reste suffisamment petit, bien que ce ne soit pas toujours le cas.

En ce qui concerne la notion de pouvoir d'expression esquissée en section 5.1, la logique propositionnelle quantifiée est aussi expressive que les machines de Turing en espace polynomial. Plus précisément, vérifier une formule propositionnelle quantifiée est un problème PSPACE-complet, où PSPACE est la classe des problèmes de décision que l'on peut vérifier en temps fini sur une machine de Turing (déterministe ou non, ici cela n'a pas d'importance) en espace polynomial (c'est-à-dire en n'utilisant qu'un nombre polynomial de cases sur la bande). Il y a (très probablement) beaucoup plus de problèmes dans PSPACE que dans NP, ce qui suggère que les problèmes PSPACE-complets présentent davantage de difficultés que les problèmes de NP. Cependant, PSPACE est encore à l'intérieur de DEXPTIME, ce qui veut dire que nous pouvons encore les résoudre en temps exponentiel.

Previous Next Contents