Une identité sur les formules

Les deux fonctions, écrites sur les quatre constructeurs :


type formule = Var of string | Non of formule
             | Et of formule * formule | Ou of formule * formule

let rec occ_var = function
  | Var _ -> 1 | Non f -> occ_var f
  | Et (a,b) | Ou (a,b) -> occ_var a + occ_var b

let rec binaires = function
  | Var _ -> 0 | Non f -> binaires f
  | Et (a,b) | Ou (a,b) -> 1 + binaires a + binaires b

Démonstration

Par induction structurelle sur $φ$ . Quatre constructeurs, donc quatre cas — et le match du code les énumère déjà.

Cas $φ = Var (p)$ (assertion). $v = 1$ , $b = 0$ , et $1 = 0 + 1$ .

Cas $φ = \neg ψ$ . La négation n'est pas binaire et n'apporte aucune variable : $v (φ) = v (ψ)$ et $b (φ) = b (ψ)$ . L'hypothèse d'induction sur $ψ$ donne le résultat, inchangé.

Cas $φ = ψ_{1} \land ψ_{2}$ . Alors $v (φ) = v (ψ_{1}) + v (ψ_{2})$ et $b (φ) = 1 + b (ψ_{1}) + b (ψ_{2})$ . Par hypothèse d'induction sur chacun des deux arguments :

$v (φ) = (b (ψ_{1}) + 1) + (b (ψ_{2}) + 1) = (1 + b (ψ_{1}) + b (ψ_{2})) + 1 = b (φ) + 1.$

Cas $φ = ψ_{1} \lor ψ_{2}$ . Identique au précédent : seul le nom du constructeur change.

Vérification. Identité testée sur $20000$ formules tirées au hasard jusqu'à la profondeur $5$ : vraie sur toutes. Sur l'exemple $(p \lor \neg q) \land \neg (q \land r)$ , on mesure $v = 4$ et $b = 3$ .

Ce que l'identité dit vraiment. Une formule est un arbre binaire déguisé (chapitre chap:arbres) : ses feuilles sont les occurrences de variables, ses nœuds à deux fils les connecteurs binaires. L'identité $v = b + 1$ est donc exactement celle du cours, $f (a) = d (a) + 1$ , transportée sur un autre type inductif. On ne l'a pas redémontrée : on a redémontré la même chose. C'est ce qu'annonçait le chapitre — un principe, et des objets qui changent.

Une conséquence pratique. Elle donne une vérification à coût nul pour tout analyseur syntaxique : si l'arbre construit à partir d'un texte ne satisfait pas $v = b + 1$ , l'analyseur est fautif. Un invariant qui se teste en $Θ (n)$ et qui ne peut pas mentir vaut mieux qu'une relecture.

Énoncé

Corrigé

Exercices semblables