Table of Contents
LANGAGES ET TRADUCTEURS – Chapitre 2 Jean-François Monin, 2021
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 Coq
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 Coq 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 :
⊗
/ \
⊕ 3
/ \
1 2
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 Coq. 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 Coq
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 Coq, 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 Coq
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.