ter-report/src/bdd.tex

119 lines
9.9 KiB
TeX

\section{Les diagrammes de décision binaires}
\subsection{La logique propositionnelle}
\subsubsection{Les propositions}
\paragraph{}
Une proposition est un énoncé pour lequel il fait sens de juger de la valeur de vérité. Par exemple, la phrase \enquote{\bsc{OCaml} est le plus beau langage au monde} est soit vraie, soit fausse. En revanche, pour la phrase \enquote{Ça va ?}, il n'y a aucun sens à dire qu'elle est vraie ou fausse.
\paragraph{}
On notera $\bot$ la proposition correspondant à \emph{faux} et $\top$ celle correspondant à \emph{vrai}. Une proposition est donc un élément de l'ensemble $\{\top, \bot\}$, que l'on notera $\mathbb{B}$.
\subsubsection{Les fonctions}
\paragraph{}
Dès lors, il est possible de définir des fonctions de $\mathbb{B}$ vers $\mathbb{B}$. On a par exemple la \emph{négation}, qui est la fonction qui à $\top$ associe $\bot$ et qui à $\bot$ associe $\top$. La négation d'une proposition $P$ est notée $\neg P$. Par la suite, lorsque l'on écrira $P$ sans plus de précision, $P$ sera tenue pour vraie, et lorsque l'on écrira $\neg P$, elle sera tenue pour fausse.
\paragraph{}
De façon similaire, on peut définir des fonctions de $\mathbb{B}^2$ vers $\mathbb{B}$. Soient $P$ et $Q$ deux propositions, on a notamment la conjonction de $P$ et $Q$, notée $P \land Q$ ; leur disjonction, notée $P \lor Q$ ; l'implication, notée $P \Rightarrow Q$.
\paragraph{}
$P \land Q$ vaut $\top$ si et seulement si $P$ et $Q$ valent tous les deux $\top$. $P \lor Q$ vaut $\top$ si et seulement si au moins $P$ ou $Q$ vaut $\top$. $P \Rightarrow Q$ vaut $\bot$ si et seulement si $P$ vaut $\top$ et que $Q$ vaut $\bot$.
\subsubsection{Encore ?}
\paragraph{}
On ne détaillera pas plus la logique propositionnelle, et l'on considérera par la suite que le reste est connu. Le lecteur souhaitant en savoir plus peut se tourner vers \href{https://www.lri.fr/~paulin/Logique/}{ce cours de logique pour l'informatique}.
\subsection{Représentation graphique}
\paragraph{}
% TODO
En une phrase: les diagrammes de décision binaires permettent de représenter les fonctions de $\mathbb{B}^n$ dans $\mathbb{B}$. Les diagrammes de décision binaires peuvent être représentés graphiquement, ce par quoi on commencera avant toute définition formelle, afin d'en facilitier la compréhension\ldots
\paragraph{}
Représentons tout d'abord la formule $P$:
\begin{center}
\includesvg[width=100pt]{simple_bdd_dot.svg}
\end{center}
\paragraph{}
Un diagramme de décision binaire a donc un sommet \enquote{de départ}, $P$ ici. Un sommet a soit deux arcs sortants, soit aucun. S'il en a deux, alors, il contient une \emph{variable propositionnelle} et dans ce cas, le \enquote{chemin à suivre} dépend de la valeur de vérité de la variable. Si la variable vaut $\bot$, on prend l'arc en pointillés, sinon, on prend l'autre. Si le sommet n'a aucun arc sortant, alors, il contient soit $\top$ soit $\bot$, ce qui correspond à la valeur de vérité de la formule représentée par ce diagramme dans le cas où on assigne aux variables les mêmes valeurs de vérités que celles que l'on a prises sur ce chemin.
\subsubsection{Ordre}
\paragraph{}
Prenons un autre exemple, voilà un diagramme représentant la proposition $P \lor Q$:
\begin{center}
\includesvg[width=100pt]{simple_bdd2_dot.svg}
\end{center}
\paragraph{}
Il aurait aussi été possible de la représenter par celui-ci:
\begin{center}
\includesvg[width=100pt]{simple_bdd3_dot.svg}
\end{center}
\paragraph{}
On va en fait se donner un \emph{ordre} sur les variables et dès que l'on \enquote{aura le choix} entre deux variables, on prendra la plus petite des deux selon cet ordre. Par exemple, si l'on décide d'utiliser l'ordre lexicographique, alors, on aura le premier des deux diagrammes ci-dessus.
\subsubsection{Non-redondance}
\paragraph{}
Une seconde chose à prendre en compte est le fait que l'on va éviter toute redondance dans nos diagrammes. Si deux sommets mènent au même résultat dans tous les cas, on va les fusionner. Sur notre exemple précédent, on peut par exemple fusionner les deux sommets $\top$:
\begin{center}
\includesvg[width=100pt]{simple_bdd4_dot.svg}
\end{center}
\subsubsection{Simplification}
\paragraph{}
Enfin, si les deux arcs sortants d'un sommet mènent à la même chose, on va tout simplement supprimer ce sommet. Par exemple, la proposition $P \lor \neg P$ ne sera pas représentée comme ceci:
\begin{center}
\includesvg[width=50pt]{simple_bdd5_dot.svg}
\end{center}
Mais comme cela:
\begin{center}
\includesvg[width=50pt]{simple_bdd6_dot.svg}
\end{center}
En fait, on a en quelque sorte développé la fonction, elle est \enquote{partiellement calculée}. Dans le cas d'une tautologie ou d'une contradiction, on aurait même complètement calculé la valeur de la proposition.
\subsection{Représentation formelle}
On utilise ici l'approche présentée dans \cite{Andersen97}.
\subsubsection{Opérateur \texttt{if-then-else}}
On définit l'opérateur \texttt{if-then-else}, de $\mathbb{B}^3$ vers $\mathbb{B}$, et noté $P \rightarrow Q_1, Q_2$ ainsi:
\[P \rightarrow Q_1, Q_2 = (P \land Q_1) \lor (\neg P \land Q_2)\]
Ce qui se lit: \enquote{Si $P$, alors, $Q_1$, sinon, $Q_2$.}.
\subsubsection{Forme normale \texttt{if-then-else}}
On dit qu'une formule propositionnelle est en forme normale \texttt{if-then-else} (FNI) si elle est construite uniquement à partir de l'opérateur \texttt{if-then-else} et des constantes $\top$ et $\bot$ ; et de telle sorte que le premier opérande de l'opérateur \texttt{if-then-else} est toujours une variable. On recommande la lecture de \cite{Mohring93} au lecteur curieux d'en apprendre plus à ce sujet.
\subsubsection{Expansion de \bsc{Shannon}}
On note $P[Q_1/Q_2]$ la proposition $P$ dans laquelle on a substitué toutes les occurences de $Q_1$ par $Q_2$. On a alors:
\[P = Q \rightarrow P[Q/\top], P[Q/\bot]\]
C'est ce que l'on appelle l'expansion de \bsc{Shannon} de $P$ par rapport à $Q$.
\subsubsection{Passage en FNI}
\paragraph{}
Pour n'importe quelle proposition, il est possible d'obtenir son équivalent en FNI. Il suffit pour cela d'appliquer l'expansion de Shannon de $P$ par rapport à n'importe quelle variable $Q$ de $P$, on aura alors $Q \rightarrow P[Q/\top], P[Q/\bot]$. Puis, on applique la même transformation à $P[Q/\top]$ et à $P[Q/\bot]$ et ce jusqu'à ce qu'il n'y ait plus de variables disponibles, on aura alors forcément soit $\top$ soit $\bot$.
\paragraph{}
Par exemple, la proposition $P \land Q$ peut être mise sous FNI ainsi:
% TODO: align
\[P \land Q = P \rightarrow (\top \land Q), (\bot \land Q) \]
\[= P \rightarrow (Q \rightarrow (\top \land \top), (\top \land \bot)), (Q \rightarrow (\bot \land \top), (\bot \land \bot)) \]
\[= P \rightarrow (Q \rightarrow \top, \bot), (Q \rightarrow \bot, \bot) \]
\subsubsection{Passage en graphe orienté acyclique}
À partir de maintenant, on ne poursuit non plus sur l'approche de \cite{Andersen97}, mais sur celle de \cite{Bryant86}.
\paragraph{}
Une proposition sous FNI peut être représentée comme un arbre binaire, sur notre exemple précédent, cela donnerait le résultat suivant:
\begin{center}
\includesvg[width=150pt]{simple_bdd7_dot.svg}
\end{center}
\paragraph{}
% TODO oe
On peut alors réduire l'arbre, c'est-à-dire que tout noeud ayant deux sous-arbres identiques sera supprimé:
\begin{center}
\includesvg[width=150pt]{simple_bdd8_dot.svg}
\end{center}
\paragraph{}
% TODO: déf. d'isomorphisme de graphes dans ce cas
Enfin, il est possible de passer à une représentation sous forme de graphe. Un arbre binaire n'étant qu'un cas particulier de graphe. Il est alors possible de réduire encore ce graphe en faisant en sorte de fusionner tous les sous-graphes isomorphes.
\paragraph{}
Le résultat final est un graphe orienté acyclique. La preuve d'absence de cycles se base sur le fait que chaque sommet est soit $\top$, soit $\bot$, soit étiqueté par une variable propositionnelle $x$ et possède deux arcs sortants, menant à deux sommets distincts $y$ et $y'$ tels que $x < y$ et $x < y'$. S'il existait un cycle passant par les sommets $x_1, \ldots, x_n$, on aurait alors:
\[x_1 < x_2 < \ldots < x_n < x_1\]
Ce qui est bien évidemment contradictoire.
\subsubsection{Résumé formel}
\paragraph{}
Un diagramme de décision binaire est donc un graphe orienté acyclique, donc les sommets sont soit des sommets sans arcs sortants étiquetés par $\top$ ou $\bot$, soit des sommets étiquetés par des variables propositionnelles et possédants deux arcs sortants.
\paragraph{}
Un diagramme de décision binaire est dit \emph{ordonné} si tous les chemins dans le graphes respectent un ordre donné sur l'étiquetage des sommets.
\paragraph{}
Un diagramme de décision binaire (ordonné) est dit réduit s'il respecte les deux propriétés suivantes:
\begin{description}
\item[unicité] il n'existe pas deux sommets avec la même étiquette et les mêmes successeurs
\item[non-redondance] il n'existe pas de sommet avec les mêmes deux successeurs
\end{description}
%\subsection{Propriétés}
\subsection{Lemme de canonicité}
Pour toute fonction $f : \mathbb{B}^n \rightarrow \mathbb{B}$, il existe, pour un ordre donné sur les variables propositionnelles, \emph{un unique} diagramme de décision binaire ordonné réduit.