Langages et Traducteurs – Chapitre 2 - Arbres

Les données sur lesquelles on travaillera seront organisées en arbre.

Pour information, on peut formaliser cette notion au moyen des mathématiques usuelles en théorie des ensembles. Ce ne sont rien d'autre, au final, que des encodages fabriqués à partir d'entiers et de suites d'entiers.

Pour des informaticiens, l'intuition obtenue en dessinant des arbres est suffisante : on sait comment représenter de telles structures en mémoire au moyen de cellules chaînées par des pointeurs. Plus spécifiquement, on se focalise sur le cas ou ces chaînages ne comportent pas de cycles. Programmer avec des arbres revient alors à programmer avec des structures chaînées sans se préoccuper de considérations liées à la gestion mémoire (allocation et désallocation) qui sont traitées automatiquement par les couches basses.

La structure des arbres considérés est définie par un type inductif

1 Exemples intuitifs

1.1 Listes d'entiers

(2020 : déjà vu en PF) La liste des 3 premiers entiers consécutifs se dessine :

 Cons                    ::
 /  \                   /  \
1   Cons               1    ::
    /  \                   /  \
   2   Cons               2    ::
       /  \                   /  \
      3    Nil               3    []

Définition du type correspondant

1.1.1 En OCaml

type listN = Nil  |  Cons of int * listN

Notation linéaire : Cons (1, (Cons (2, (Cons (3, Nil)))))

ou 1 :: 2 :: 3 :: []

1.1.2 En Rocq

Inductive listN : Set :=
  | Nil : listN
  | Cons : nat -> listN  -> listN
.

(Cons 1 (Cons 2 (Cons 3 Nil)))

Différences avec OCaml :

les noms des constructeurs peuvent ne pas commencer par une majuscule

Inductive listN = nil : listN | cons : nat -> listN -> listN

chaque constructeur est traité comme une fonction et les arguments sont pris un à un (ils sont pris en bloc en OCaml) Notation linéaire : Cons 1 (Cons 2 (Cons 3 Nil)) ;
déclaration du type de listN (les types aussi ont un type) ; en Rocq il y a un type prédéfini pour abriter des types comme listN, qui s'appelle Set ; on y reviendra plus tard, il suffit à ce stade de savoir l'indiquer dans la déclaration de listN ;
ponctuation.

1.2 AST (Abstract Syntactic Trees) d'expressions arithmétiques

(2020 : vu au TD1)

Ce qui s'écrit usuellement (1 + 2) * 3 peut se dessiner :

Ou encore, en étiquetant les nœuds par Apl et Amu au lieu de, respectivement, ⊕ et ⊗ :

     Amu
    /   \
 Apl     3
 / \
1   2

Pour plus de rigueur et de précision, on ajoute une étiquette aux feuilles qui portent un entier, ce qui donne :

      Amu
     /   \
  Apl    Cst
  / \     |
Cst Cst   3
 |   |
 1   2

La dernière version permet de voir aexp comme un type somme que l'on peut définir en OCaml on en Rocq. Inconvénient : les dessins sont un peu plus gros. Avantage : une distinction claire entre les types. On n'a plus de confusion entre le type des entiers et le type des AST d'expressions arithmétiques, ce qui simplifie le cadre conceptuel.

Définition du type correspondant

1.2.1 En OCaml

type aexp = Cst of int  |  Apl of aexp * aexp  |  Amu of aexp * aexp

Notation linéaire : Amu (Apl (Cst (1), Cst (2)), Cst (3))

1.2.2 En Rocq

Inductive aexp : Set := 
  | Cst : nat -> aexp
  | Apl : aexp -> aexp -> aexp
  | Amu : aexp -> aexp -> aexp
.

Notation linéaire : Amu (Apl (Cst 1) (Cst 2)) (Cst 3)

2 Grammaires d'arbres

Une façon de déclarer les arbres est la suivante, en s'inspirant du formalisme des grammaires hors-contexte définies sur des séquences linéaires plates.

2.1 AST (Abstract Syntactic Trees) d'expressions arithmétiques

aexp ::=  Cst   |      Apl       |      Amu
           |           / \              / \
          nat      aexp   aexp      aexp   aexp

2.2 Listes d'entiers

listN ::=  Nil   |     Cons
                       /  \
                     nat  listN

Ou bien, avec la notation vue ci-dessus au moyen de caractères spéciaux à la place de Nil et Cons :

listN ::=  []    |      ::
                       /  \
                     nat  listN

3 Calculs récursifs sur des arbres

Pour calculer une valeur à partir d'un arbre, on donne des équations lues de gauche à droite pour chacune des alternatives.

Exemple vu au TD 1 : nombre de feuilles d'un AST

Exemple : longueur d'une liste d'entiers

longueur []   =   0

              ::
longueur     /  \      =   1 + longueur l
            n    l

Notation linéaire : longueur ( n :: l ) = 1 + longueur l

En OCaml ou en Rocq, ces équations sont programmées par des expressions de filtrage.

3.1 En OCaml

let rec nbf = fun e ->
  match e with
  | Cst (n) -> 1
  | Apl (e1, e2) -> nbf e1  +  nbf e2
  | Amu (e1, e2) -> nbf e1  +  nbf e2

3.2 En Rocq

Fixpoint nbf := fun e =>
  match e with
  | Cst n => 1
  | Apl e1 e2 => nbf e1  +  nbf e2
  | Amu e1 e2 => nbf e1  +  nbf e2
  end.

∼∼∼

Made with Org-mode