Le type du cours ne permet pas d'écrire substituer

let rec quine f =
  match variables f with
  | [] -> evalue (fun _ -> false) f
  | p :: _ -> quine (substituer f p true) || quine (substituer f p false)

1. C'est impossible, et c'est l'exercice.

let rec substituer f p b =
  match f with
  | Var q -> if q = p then ??? else Var q      (* et on écrit quoi ? *)
  | ...

Il faudrait rendre la formule constante $\mathtt{b}$. Or le type formule du cours n'a que cinq constructeurs — Var, Non, Et, Ou, Implique — et aucune feuille constante. Toute feuille est une variable.

Le même défaut se lit dans la ligne suivante : le cas [] -> evalue (fun _ -> false) f traite « la formule n'a plus aucune variable ». Avec ce type-là, ce cas est inatteignable : toute formule a au moins une feuille, donc au moins une variable. Un cas de filtrage qui ne peut jamais se produire est le signe d'un type incomplet.

On pourrait croire s'en tirer en substituant une tautologie, par exemple $r\vee \neg r$. C'est pire : la formule contiendrait alors la variable $r$, que quine substituerait à son tour, produisant une nouvelle occurrence de $r$ — et l'algorithme ne terminerait pas.

2. La correction est d'ajouter les deux constantes, ce que le programme autorise explicitement (« on peut être amené à ajouter à la syntaxe une formule tautologique et une formule antilogique ; elles sont notées $\top$ et $\perp$ »).

type formule =
  | Vrai | Faux                       (* LES DEUX FEUILLES QUI MANQUAIENT *)
  | Var of string
  | Non of formule
  | Et of formule * formule
  | Ou of formule * formule
  | Implique of formule * formule

(* f où chaque occurrence de p est remplacée par la constante b.
   Précondition : aucune. Postcondition : p n'apparaît plus dans le résultat,
   et pour toute valuation v, [[substituer f p b]]_v = [[f]]_(v avec p := b). *)
let rec substituer f p b =
  match f with
  | Vrai | Faux -> f
  | Var q -> if q = p then (if b then Vrai else Faux) else Var q
  | Non g -> Non (substituer g p b)
  | Et (g, h) -> Et (substituer g p b, substituer h p b)
  | Ou (g, h) -> Ou (substituer g p b, substituer h p b)
  | Implique (g, h) -> Implique (substituer g p b, substituer h p b)

Terminaison de substituer : appel récursif sur un sous-arbre strict, donc induction structurelle (chapitre chap:induction). Complexité : $\Theta (|f|)$ — un passage, un nœud reconstruit à chaque nœud lu.

Terminaison de quine : le variant est le nombre de variables distinctes de la formule. La postcondition ci-dessus garantit qu'après substituer f p b la variable $p$ a disparu, et qu'aucune n'est apparue : le variant décroît strictement de $1$ à chaque appel, et il est positif. La récursion a donc profondeur $n$, et l'arbre d'appels compte au plus $2^{n+1}-1$ nœuds : c'est le $O(2^n\cdot |f|)$ annoncé par le cours.

Mesure — la version sans simplification, sur $(p\wedge \neg p)\wedge (x_{12}\vee \cdots \vee z)$, soit $14$ variables : $32767$ appels, c'est-à-dire $2^{15}-1$, l'arbre binaire complet. Avec la simplification du problème 20.2 : $3$ appels. Le facteur $10000$ ne vient d'aucun changement d'algorithme — seulement de ce que substituer rend, ou non, une formule déjà réduite.