Probleme – Un évaluateur d'expressions arithmétiques

1. Le type, et sa taille.

type expr =
  | Const of int
  | Var
  | Plus of expr * expr
  | Fois of expr * expr

(* taille e : nombre de noeuds de e. Precondition : aucune. *)
let rec taille e =
  match e with
  | Const _ | Var -> 1
  | Plus (a, b) | Fois (a, b) -> 1 + taille a + taille b

Quatre lignes suffisent à décrire un ensemble infini d'objets, et le filtrage rend la fonction exhaustive par construction — le compilateur crierait si l'on ajoutait un constructeur sans revenir ici. Noter le regroupement | Const _ | Var ->, autorisé « [si les motifs] comportent exactement les mêmes variables » : ici, aucune.

2. L'évaluation.

(* evalue e v : valeur de e lorsque Var vaut v.
   Precondition  : aucune.
   Postcondition : le resultat est la valeur entiere de e en v, au
                   debordement des int pres. *)
let rec evalue e v =
  match e with
  | Const c -> c
  | Var -> v
  | Plus (a, b) -> evalue a v + evalue b v
  | Fois (a, b) -> evalue a v * evalue b v

Terminaison. Le variant n'est pas un entier de boucle mais la taille de l'argument : chaque appel récursif porte sur un sous-arbre strictement plus petit, et la taille est un entier positif. Une suite d'appels ne peut donc pas être infinie. C'est la forme que prend le variant en récursion structurelle, et le chapitre chap:induction en fait un principe.

Complexité. Chaque nœud est visité une fois : $\Theta (t)$ où $t$ est la taille, et $\Theta (h)$ en espace de pile, $h$ étant la hauteur.

3. La simplification.

(* simplifie e : une expression EQUIVALENTE a e (meme valeur pour toute
   valeur de Var), sans sous-terme de la forme x + 0, 0 + x, x * 1,
   1 * x, x * 0 ni 0 * x. *)
let rec simplifie e =
  match e with
  | Const _ | Var -> e
  | Plus (a, b) ->
      (match simplifie a, simplifie b with
       | Const 0, s | s, Const 0 -> s
       | Const p, Const q -> Const (p + q)
       | sa, sb -> Plus (sa, sb))
  | Fois (a, b) ->
      (match simplifie a, simplifie b with
       | Const 0, _ | _, Const 0 -> Const 0
       | Const 1, s | s, Const 1 -> s
       | Const p, Const q -> Const (p * q)
       | sa, sb -> Fois (sa, sb))

Équivalence. Par induction sur la taille. Les feuilles sont rendues telles quelles. Pour Plus (a, b), l'hypothèse d'induction donne simplifie a équivalent à a et de même pour b ; les trois cas de la seconde analyse sont alors trois identités de l'arithmétique : $0+s=s$, $p+q$ est la constante voulue, et le dernier cas ne change rien. Idem pour le produit avec $0\times s=0$ et $1\times s=s$. Donc simplifie e et e ont la même valeur pour toute valeur de la variable.

Vérification par la mesure. Sur $e=(x+0)\times (1\times x)+0\times x$ :

e            = (((x + 0) * (1 * x)) + (0 * x))     taille 11
simplifie e  = (x * x)                             taille 3
v = 0 : evalue e = 0,  evalue (simplifie e) = 0
v = 1 : evalue e = 1,  evalue (simplifie e) = 1
v = 2 : evalue e = 4,  evalue (simplifie e) = 4
v = 3 : evalue e = 9,  evalue (simplifie e) = 9
v = 4 : evalue e = 16, evalue (simplifie e) = 16

Onze nœuds ramenés à trois, et cinq points de contrôle où les deux expressions coïncident. Attention à ce que cette table prouve : elle ne démontre rien — c'est l'induction qui le fait —, elle attrape les fautes de transcription. C'est très exactement la répartition des rôles du chapitre chap:discipline.

4. Pourquoi les sous-arbres d'abord. Parce qu'une simplification en crée d'autres. Sur $f=(0+1)\times x$ :

f            = ((0 + 1) * x)
simplifie f  = x

La racine est un produit dont aucun facteur n'est visiblement $0$ ni $1$ : une analyse de la seule racine ne trouverait rien. C'est la simplification du sous-arbre gauche, $0+1\to 1$, qui fait apparaître le $\times 1$. En simplifiant les enfants d'abord — un parcours en profondeur, suffixe —, chaque nœud est examiné une fois avec ses enfants déjà réduits.

Cela ne garantit pas encore une forme minimale : le résultat d'un nœud peut ouvrir une simplification chez son parent, ce que ce parcours attrape, mais pas chez un ancêtre plus lointain via une réécriture nouvelle. Une simplification complète s'obtiendrait en itérant simplifie jusqu'à point fixe, la taille servant de variant : elle ne croît jamais, et décroît strictement tant qu'une règle s'applique.