Aller au contenu
Topos Uranos
Français

L’algorithme des formes normales et ses applications

Résumé

La leçon sur les formes normales a démontré que toute formule équivaut à une forme normale disjonctive et à une forme normale conjonctive ; celle-ci enseigne à les calculer sans la table et à s’en servir. Le calcul est un algorithme de réécriture en trois phases : on élimine la double implication, la disjonction exclusive, la négation conjointe et l’implication ; on porte les négations jusqu’aux variables avec De Morgan et la double négation ; et on distribue, la conjonction sur la disjonction pour la forme disjonctive et la disjonction sur la conjonction pour la forme conjonctive. On démontre sa correction, qui est une conséquence du remplacement sémantique, et sa terminaison, avec une mesure numérique qui décroît à chaque pas de chaque phase ; et on démontre aussi sa limite : la forme conjonctive d’une disjonction de nn conjonctions de deux variables a nécessairement 2n2^n clauses. On obtient ensuite les formes normales à partir de la table de vérité d’un dispositif dont on ne voit pas l’intérieur, on les simplifie en fusionnant des lignes voisines et on les convertit en circuits d’interrupteurs en série et en parallèle. Le problème d’un dispositif à quatre interrupteurs est résolu complètement, avec sa table, ses deux formes et ses circuits ; celui à cinq reste comme défi.

Objectifs d’apprentissage

  1. Appliquer l’algorithme de réécriture pour obtenir une forme normale disjonctive et une forme normale conjonctive d’une formule, en choisissant l’élimination de la double implication qui convient selon l’endroit où elle apparaît.
  2. Démontrer que l’algorithme est correct, par le remplacement sémantique, et qu’il termine, avec des mesures qui décroissent à chaque pas ; et expliquer pourquoi la forme conjonctive peut être exponentiellement plus longue que la formule de départ.
  3. Construire les formes normales d’une boîte noire à partir de sa table de vérité et les simplifier en fusionnant des lignes voisines.
  4. Représenter des circuits d’interrupteurs en série et en parallèle au moyen de formules, et concevoir et simplifier des circuits qui satisfont une spécification donnée en langage naturel.

La leçon sur les formes normales a donné deux démonstrations de leur existence. La première passe par la table de vérité, qui a 2n2^n lignes pour nn variables ; la seconde parcourt la formule à partir des variables, en suivant son unique règle de formation. Aucune des deux ne dit comment procéder devant une formule écrite avec des implications, des doubles implications et des négations imbriquées, qui est la manière dont les formules se présentent d’ordinaire. S’il en est ainsi, il manque une procédure qui travaille sur l’écriture elle-même, qui puisse s’exécuter sans réfléchir, dont on sache qu’elle termine et qui donne une formule équivalente. C’est un algorithme, et son étude est le premier objet de cette leçon ; le second est ce qu’on en fait : décrire par des formules le comportement d’un dispositif et construire un circuit qui le reproduise.

Écritures et remplacement

Rappelons que les formules du cours sont des chaînes de cercles et de disques, et que ¬\neg, ∨\vee, ∧\wedge, →\rightarrow, ↔\leftrightarrow et ⊻\veebar sont des abréviations définies à partir de la négation conjointe (leçon sur le langage de la logique propositionnelle). Quand nous écrivons ((p∨q)→(¬q∧p))((p \vee q) \rightarrow (\neg q \wedge p)), nous n’écrivons pas la chaîne, mais une écriture de celle-ci : un arbre dont les feuilles sont des variables et dont les nœuds sont les connecteurs ¬\neg, ∧\wedge, ∨\vee, →\rightarrow, ↔\leftrightarrow, ⊻\veebar et ↓\downarrow, chacun avec ses composantes. Toute écriture désigne une seule formule, celle qui résulte du dépliage de ses abréviations ; et une même formule peut avoir plusieurs écritures : la leçon sur les formes normales a observé que ¬¬φ\neg\neg\varphi et (φ∨φ)(\varphi \vee \varphi) sont la même chaîne. L’algorithme lit l’écriture, non la chaîne ; c’est pourquoi il convient de les distinguer. Comme la distinction n’importe que pour savoir où agit chaque pas, nous utiliserons les lettres φ\varphi, ψ\psi, χ\chi pour les écritures et pour les formules qu’elles désignent, et nous écrirons φ≡ψ\varphi \eqsem \psi quand les formules désignées sont sémantiquement équivalentes. Une sous-écriture d’une écriture est le sous-arbre qui pend à l’un de ses nœuds.

Un pas de l’algorithme remplace une sous-écriture par une autre. L’instrument qui garantit que ce changement n’altère pas le sens est le théorème de remplacement sémantique de la leçon sur la conséquence et l’équivalence sémantiques ; mais ce théorème remplace une occurrence dans la chaîne, et une sous-écriture peut correspondre à plusieurs occurrences dans la chaîne, parce que chaque abréviation copie ses composantes : dans (φ∨ψ)=((φ↓ψ)↓(φ↓ψ))(\varphi \vee \psi) = ((\varphi \downarrow \psi) \downarrow (\varphi \downarrow \psi)), la composante φ\varphi figure deux fois. Le lemme suivant adapte le remplacement aux écritures.

LemmeRemplacement dans une écriture

Soient χ\chi une écriture, θ\theta l’une de ses sous-écritures et θ′\theta' une écriture avec θ≡θ′\theta \eqsem \theta'. Si χ′\chi' résulte du remplacement, dans χ\chi, de cette sous-écriture par θ′\theta', alors χ≡χ′\chi \eqsem \chi'.

Démonstration

  1. χ′=θ′≡θ=χ\chi' = \theta' \eqsem \theta = \chi

    Par récurrence sur la profondeur du nœud auquel pend θ\theta, c’est-à-dire le nombre de connecteurs de χ\chi qui se trouvent au-dessus de lui. Si la profondeur est 00, la sous-écriture est l’écriture entière.

  2. χ=c(χ1,χ2),χ′=c(χ1′,χ2),χ1′≡χ1\dato{hi}{\chi = c(\chi_1, \chi_2), \qquad \chi' = c(\resaltar{\chi_1'}, \chi_2), \qquad \chi_1' \eqsem \chi_1}

    Si elle est supérieure à 00, la racine de χ\chi est un connecteur cc de composantes χ1\chi_1 (et χ2\chi_2, si cc est binaire), et θ\theta pend à l’une d’elles, disons χ1\chi_1, à une profondeur moindre. Par l’hypothèse de récurrence, le changement à l’intérieur de χ1\chi_1 donne une écriture équivalente.

  3. v(χ′)=Fc(v(χ1′),v(χ2))=Fc(v(χ1),v(χ2))=v(χ)v(\chi') = F_c\left( v(\chi_1'), v(\chi_2) \right) = F_c\left( v(\chi_1), v(\chi_2) \right) = v(\chi)

    Par le théorème des valeurs des connecteurs dérivés (leçon sur la sémantique de la logique propositionnelle) et par la clause de la négation conjointe, la valeur de c(χ1,χ2)c(\chi_1, \chi_2) dans une valuation est une fonction des valeurs de χ1\chi_1 et de χ2\chi_2, et celles-ci ne changent pas. D’où χ\chi et χ′\chi' ont la même valeur dans toute valuation.

Ici FcF_c est la fonction de vérité du connecteur : F¬(a)=1−aF_\neg(a) = 1 - a, F∧(a,b)=abF_\wedge(a, b) = ab, et ainsi de suite pour les autres. On obtient le même résultat à partir du théorème de remplacement sémantique en l’appliquant une fois pour chaque copie de θ\theta dans la chaîne et en enchaînant les équivalences par transitivité ; la démonstration par l’écriture est plus brève parce qu’elle compte les connecteurs écrits et non les copies.