more fix

src/app.tex

@@ -2,7 +2,7 @@
 
   \subsection{Un petit langage de formules propositionnelles}
 
-    Puisque les diagrammes de décision binaires représentent des formules propositionnelles, il est naturel de vouloir créer un langage pour les formules propositionnelles\ldots On se donne le type de syntaxe abstraite suivant:
+    Puisque les diagrammes de décision binaires représentent des formules propositionnelles, il est naturel de vouloir créer un langage pour les formules propositionnelles. On se donne le type de syntaxe abstraite suivant:
 
       \inputminted[bgcolor=darkBackground]{ocaml}{ml/expr_lang.ml}
 

src/bdd.tex

@@ -71,7 +71,7 @@
         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 forme 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$.
+      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
@@ -111,6 +111,6 @@
               \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}
-      \subsubsection{Lemme de canonicité}
-      Pour tout 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.
+    %\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.

src/implem.tex

@@ -43,21 +43,24 @@
 
   \inputminted[bgcolor=darkBackground]{ocaml}{ml/naive_defop.ml}
 
-  On a donc de quoi construire des diagrammes ordonnés et non-redondants. Reste à implémenter la propriété d'unicité\ldots
+  On a donc de quoi construire des diagrammes ordonnés et non-redondants. Il reste alors à implémenter la propriété d'unicité.
 
   \subsection{Implémentation du partage physique}
 
-  La démarche expliquée ici repose sur celle présentée dans \cite{ConchonFilliatre06}. Le concept principal est celui du \emph{hashconsing}.
+  La démarche expliquée ici repose sur celle présentée dans \cite{ConchonFilliatre06}. Le concept principal est celui du \emph{hashconsing}, ou partage maximal.
 
   Elle est surtout utile lorsqu'on a affaire à des structures de données récursives. Le but est d'être capable de ne jamais recréer deux fois la même valeur en mémoire, tout en préservant la sûreté des types d'OCaml et en utilisant une approche modulaire.
+
+  L'idée principale est la suivante. Lorsque l'on veut créer une valeur, on regarde si on a déjà une valeur équivalente en mémoire et si oui, on réutilise cette dernière.
+
     \subsubsection{Modèle d'exécution d'OCaml}
-  En OCaml, les valeurs sont soit des entiers, soit des pointeurs vers des entiers, c'est par exemple aussi le cas en Java. Les entiers permettant d'encoder divers types. Ainsi, contrairement à ce qui peut se faire en C, une structure ou une valeur d'un type récursif ne sont jamais copiés entièrement lors de l'appel d'une fonction, on ne passe qu'un pointeur vers notre valeur, ou bien la valeur elle-même si l'ensemble des valeurs qu'elle peut prendre peut être encodé sur un seul entier.
+  En OCaml, les valeurs sont soit des entiers, soit des pointeurs vers des entiers, c'est par exemple aussi le cas en Java. Les entiers permettent en effet d'encoder divers types. Ainsi, contrairement à ce qui peut se faire en C, une structure ou une valeur d'un type récursif ne sont jamais copiés entièrement lors de l'appel d'une fonction, on ne passe qu'un pointeur vers notre valeur, ou bien la valeur elle-même si l'ensemble des valeurs qu'elle peut prendre peut être encodé sur un seul entier.
 
   Pour notre type de diagramme de décision binaire, on peut par exemple imaginer que la valeur \texttt{False} est un entier valant $0$, \texttt{True} un entier valant $1$ et \texttt{Node (v, l, h)} un pointeur vers une structure contenant successivement un pointeur vers les trois valeurs $v$, $l$ et $h$.
 
   Pour distinguer si une valeur est un pointeur ou non, OCaml utilise une technique quelque peu particulière. En fait, les valeurs ne sont pas codées sur $32$ ou $64$ bits, mais sur $31$ ou $63$, le bit restant servant à distinguer les pointeurs.
     \subsubsection{Hashconsing basique}
-  On commence par définir une fonction \texttt{hc} qui va regarder si on a déjà construit une valeur, si oui, on renverra donc cette valeur déjà construite, sinon, on l'ajoute à la table et l'on renvoie cette valeur. L'égalité utilisée est celle par défaut, c'est-à-dire l'égalité structurelle d'OCaml, il en va de même pour la fonction de hachage, une fonction générique fournie par OCaml est utilisée.
+  On commence par définir une fonction \texttt{hc} qui va regarder si on a déjà construit une valeur. Si oui, on renverra donc cette valeur déjà construite. Sinon, on l'ajoute à la table et l'on renvoie cette valeur. L'égalité utilisée est celle par défaut, c'est-à-dire l'égalité structurelle d'OCaml, il en va de même pour la fonction de hachage, une fonction générique fournie par OCaml est utilisée.
 
   \inputminted[bgcolor=darkBackground]{ocaml}{ml/hc.ml}
 
@@ -65,13 +68,13 @@
 
   \inputminted[bgcolor=darkBackground]{ocaml}{ml/hc_node.ml}
 
-  Ce faisant, on peut garantir que pour deux valeurs $x$ et $y$ auquel on a appliqué le hashconsing, on a:
+  Ce faisant, on peut garantir que pour deux valeurs $x$ et $y$ auxquelles on a appliqué le hashconsing, on a:
 
     \[ x = y \Leftrightarrow x == y \]
 
   On pourrait alors maintenant remplacer l'égalité structurelle par l'égalité physique dans notre fonction \texttt{hc}, le temps de comparaison ne dépendrait alors plus de la taille de notre valeur - c'est un type récursif - mais serait constant.
 
-  OCaml permet de faire cela simplement, il suffit d'instancier un module en utilisant le foncteur de table de hachages fournit par OCaml:
+  OCaml permet de faire cela simplement, il suffit d'instancier un module en utilisant le foncteur de table de hachages fourni par OCaml:
 
     \inputminted[bgcolor=darkBackground]{ocaml}{ml/hc_phy_eq.ml}
 
@@ -96,19 +99,11 @@
 
   \inputminted[bgcolor=darkBackground]{ocaml}{ml/hc_fonct.ml}
 
-  On en profite pour attribuer au champs \texttt{tag} une valeur unique, qu'on utilisera plus tard. Il faut aussi noter qu'on n'utilise plus deux fois \texttt{v}, mais une seule: en tant que valeur associée à une clé.
-
-  On place notre type \texttt{'a hash\_consed} et notre foncteur \texttt{Make} dans un module appelé \texttt{Hashcons}.
-
-  On peut alors obtenir une version hashconsée de nos diagrammes:
+  On en profite pour attribuer au champs \texttt{tag} une valeur unique, qu'on utilisera plus tard. Il faut aussi noter qu'on n'utilise plus deux fois \texttt{v}, mais une seule: en tant que valeur associée à une clé. On place notre type \texttt{'a hash\_consed} et notre foncteur \texttt{Make} dans un module appelé \texttt{Hashcons}. On peut alors obtenir une version hashconsée de nos diagrammes:
 
   \inputminted[bgcolor=darkBackground]{ocaml}{ml/hbdd.ml}
 
-  On a utilisé le champ \texttt{tag} pour fournir une fonction de hachage en temps constant !
-
-  Désormais, le hashconsing d'un diagramme se fait en temps constant.
-
-  On peut alors redéfinir nos fonctions \texttt{view} et \texttt{hc} de la manière suivante:
+  On a utilisé le champ \texttt{tag} pour fournir une fonction de hachage en temps constant ! Désormais, le hashconsing d'un diagramme se fait en temps constant. On peut alors redéfinir nos fonctions \texttt{view} et \texttt{hc} de la manière suivante:
 
   \inputminted[bgcolor=darkBackground]{ocaml}{ml/hc_hashcons.ml}
 
@@ -116,9 +111,9 @@
 
   \subsubsection{Hashconsing avec éphéméron}
 
-    En OCaml, la mémoire n'est pas gérée par le programmeur, mais par le \emph{garbage collector}. L'un des rôles du \emph{garbage collector} est de désallouer la mémoire lorsqu'elle n'est plus utilisée. Pour cela, il peut par exemple compter le nombre de pointeurs vers une valeur afin de savoir si celle-ci est toujours utilisée. Cela a l'avantage d'éviter de faire de nombreuses erreurs: fuites mémoires, double libération de pointeurs et autres réjouissances. Cela se fait au prix d'une baisse des performances.
+    En OCaml, la mémoire n'est pas gérée par le programmeur, mais par le \emph{garbage collector}. L'un des rôles du \emph{garbage collector} est de désallouer la mémoire lorsqu'elle n'est plus utilisée. Pour cela, l'une des techniques les plus simples\footnote{Qui n'est pas celle employée par le garbage collector d'OCaml.} il peut par exemple compter le nombre de pointeurs vers une valeur afin de savoir si celle-ci est toujours utilisée. Cela a l'avantage d'éviter de faire de nombreuses erreurs: fuites mémoires, double libération de pointeurs et autres réjouissances. Cela se fait au prix d'une baisse des performances.
 
-  Il y a aussi un second inconvénient au fait de passer par un \emph{garbage collector}. Si l'on créé une table de hachage dont les clés sont des pointeurs pour par exemple implémenter la mémoïsation d'une fonction, le fait d'avoir un pointeur dans notre table empêchera le garbage collector de libérer cette valeur.
+  Il y a aussi un second inconvénient au fait de passer par un \emph{garbage collector}. Si l'on crée une table de hachage dont les clés sont des pointeurs pour par exemple implémenter la mémoïsation d'une fonction, le fait d'avoir un pointeur dans notre table empêchera le garbage collector de libérer cette valeur.
 
   Notre implémentation du hashconsing présente aussi ce problème ! Si un diagramme peut être libéré, il ne le sera pas parce qu'il est présent dans la table de hashconsing\ldots
 
@@ -130,12 +125,12 @@
 
   \inputminted[bgcolor=darkBackground]{ocaml}{ml/ephem.ml}
 
-  Il nous a suffit de changer $4$ lignes pour y parvenir. L'implémentation présentée dans \cite{ConchonFilliatre06} datant d'avant l'introduction des éphémérons dans OCaml, une grande quantité de code y est nécessaire pour arriver au même résultat.
+  Il nous a suffit de changer quatre lignes pour y parvenir. L'implémentation présentée dans \cite{ConchonFilliatre06} datant d'avant l'introduction des éphémérons dans OCaml, une grande quantité de code y est nécessaire pour arriver au même résultat.
 
  % =============== Mémo
  \subsection{Mémoïsation}
 
-  On a gagné de la place en mémoire, en utilisant le partage physique\ldots, mais, on peut en fait faire \emph{beaucoup} mieux, en mémoïsant nos opérations sur les diagrammes.
+  On a gagné de la place en mémoire, en utilisant le partage physique, mais, on peut en fait faire \emph{beaucoup} mieux, en mémoïsant nos opérations sur les diagrammes.
 
   Le concept de la mémoïsation est plutôt simple: avant de calculer le résultat de l'application d'une fonction à des arguments, on regarde si on a déjà appliqué la fonction à ces mêmes arguments, si oui, on utilise ces arguments, si non, on calcule le résultat et on l'ajoute à une table de hachage avec les arguments comme clé.
 
@@ -164,7 +159,7 @@
 
   Afin de pouvoir mesurer l'impact sur l'usage mémoire et le temps de calcul du hashconsing et de la mémoïsation, on a créé un foncteur \texttt{Bdd.Make} paramétré par un module contenant un module de hashconsing et un module de mémoïsation.
 
-  On peut alors lui donner des \enquote{faux} modules de mémoïsation et de hashconsing, ou bien des vrais et ainsi obtenir $4$ implémentations différentes à partir d'une seule.
+  On peut alors lui donner des \enquote{faux} modules de mémoïsation et de hashconsing, ou bien des vrais et ainsi obtenir quatre implémentations différentes à partir d'une seule.
 
   Le code ne sera pas recopié ici, mais est disponible sur le dépôt du projet.
 
@@ -188,7 +183,7 @@
   \subsubsection{\texttt{any\_sat}}
   La fonction \texttt{any\_sat} qui donne une assignation quelconque aux variables telle que la formule est vraie se fait aussi très simplement:
 
-  \inputminted[bgcolor=darkBackground]{ocaml}{ml/is_sat.ml}
+  \inputminted[bgcolor=darkBackground]{ocaml}{ml/any_sat.ml}
 
   On descend dans notre diagramme en prenant toujours la branche correspondant à l'assignation $\bot$ pour la variable courante. Si on a trouvé une assignation, alors, on l'utilise, sinon, on essaie avec l'autre branche, celle correspondant à $\top$. Si notre diagramme est réduit à $\bot$, alors on aura \texttt{None}, sinon, on aura forcément une assignation correcte.
 
@@ -204,4 +199,4 @@
   La fonction \texttt{random\_sat} est elle aussi similaire. Elle calcule la taille des deux sous-diagrammes, et va vers l'un ou l'autre de façon aléatoire avec une probabilité proportionnelle à la taille de chacun.
 
   \subsubsection{\texttt{count\_sat}}
-  Le cas de \texttt{count\_sat} est un peu plus compliqué, l'utilisateur doit saisir le nombre de variables existantes. On utilise alors le fait que les variables sont ordonnées pour calculer à chaque fois le nombre de variables qui n'apparaissent pas dans la formule, et on multiplie correctement le nombre possible de solution en faisant un peu d'arithmétique. On a ici aussi dû utiliser de la mémoïsation: en effet un sous-diagramme peut apparaître plusieurs fois dans notre parcours.
+  Le cas de \texttt{count\_sat} est un peu plus compliqué car l'utilisateur doit saisir le nombre de variables existantes. On utilise alors le fait que les variables sont ordonnées pour calculer à chaque fois le nombre de variables qui n'apparaissent pas dans la formule, et on multiplie correctement le nombre possible de solutions en faisant un peu d'arithmétique. On a ici aussi dû utiliser de la mémoïsation: en effet un sous-diagramme peut apparaître plusieurs fois dans notre parcours.

src/introduction.tex

@@ -1,3 +1,4 @@
 \section{Introduction}
 
 TODO \cite{Leroy00} \cite{Knuth11} \cite{Andersen97} \cite{Bryant86}
+TODO: lien vers le repo

src/ml/naive_neg.ml

@@ -2,4 +2,4 @@ let rec neg =
   fview (function
   | True -> false_bdd
   | False -> true_bdd
-  | Node (v, l, h) -> node var (neg low) (neg high))
+  | Node (v, l, h) -> node var (neg l) (neg h))