INFO817 : Sémantique des langages fonctionnels et objets, preuves de programmes

Objectifs de ce cours :

Comprendre la sémantique (c'est à dire la manière dont les programmes s'évaluent) des langages fonctionnel (Lisp, SML, OCaml, Python, ...) et aussi des langages objets (OCaml, Java, C++, ...).

On commencera par parler des types de données, avant de donner la sémantique d'un langage minimaliste, mais très riche, qui permettra d'illustrer les points généraux communs à tous les langages. On essayera aussi de traiter quelques particularités de langages réellement utilisés. Enfin, on montrera comment la connaissance de la sémantique d'un langage permet de raisonner sur les programmes et donc d'obtenir des programmes sans bug.

Objectif du cours

Il s'agit d'étudier la sémantique des langages de programmation (non impératif, cf cours d'INFO 815)

Qu'est ce que le sémantique :

• Sémantique dénotationnelle : que fait le programme (quel résultat retourne la fonction...) On ne s'interesse qu'à ce qui est observable de l'extérieur
• Sémantique opérationnelle : comment le programme le fait.

Pourquoi connaître la sémantique ? La question devrait plutôt être : comment programmer sans savoir ce que fait le programme que l'on écrit ?

L'intérêt de la sémantique c'est de prendre du recul sur la programmation et l'algorithmique afin de maîtriser les concepts et faire abstraction de la syntaxe des langages.

La sémantique devient aussi indispensable dans le cadre des méthodes formelles et tout particulièrement de la preuve de programme (dans ce cas on doit écrire ce que le programme fait).

Introduction : historique et classification des langages.

Historique des langages ML voir l'arbre des langages

Un langage est défini par différent "trait" de programmation:

• fonctionnel : les fonctions sont des objets de première classe (les fonctions peuvent prendre en paramètre d'autres fonctions) et peuvent être appliqué partiellement

 Fortran :  non, C et C++ : en partie, ML et LISP : oui

• langage à GC : la libération mémoire est prise en charge par le langage

 Fortran :  non, C et C++ : oui avec lc GC de Boehm, ML et LISP : oui

• langage impératif : on peut modifier plus d'une fois le contenu d'un bloc mémoire (on n'est pas limité aux structures

de donnée persistantes) tout les langages : oui, sauf Haskell et encore, il y a les monades

• objets : notion de classes, d'objets, ...

 oui pour Java, C++, Objective-C, OCaml 

• modulaire : notion de module et parfois de foncteur

 oui pour les langages de la famille ML, oui pour modula, mais pas de foncteur 

Pour ce cours : illustration en OCaml et PML, et structure de donnée persistante uniquement.

Des types de données.

Un modèle très simple (un peu trop pour programmer directement avec)

Qu'est ce qu'une donnée :

• modèle mémoire
• modèle de graphe orientée (on distingue le rôle des pointeurs/adresses)
• arbre dans le cas des données persistentes
• arbre à branchement borné
• donnée algébrique : 3 types de noeuds ((), (x,y), L(x), R(x))

Tout programme utilisant des arbres à branchement borné peut être réecrit avec des données algébriques en perdant au plus un facteur constant en temps et en mémoire.

Type de données = ensemble de données partageant certaines propriétés.

Type de données algébrique

 0 | 1 | A $\times$ B | A + B | $\mu$ X.A(X) 

• type vide : 0 = $\emptyset$
• type avec un seul élément : 1 = {()}
• produit cartésien : A $\times$ B = {(a,b) | a $\in$ A et b $\in$ B} (A et B étant deux types)
• somme disjointe : A + B = {L(a) | a $\in$ A} $\cup$ {R(b) | b $\in$ B} (A et B étant deux types)
• type inductif : $\mu$ X.A(X) = A(0) \cup A(A(0)) \cup A(A(A(0))) \cup ... (A étant un type avec au moins un paramètre)

Une manière de voir les types inductifs est de voir que $\mu$ X.A(X) est une solution de l'équation X = A(X) sur les types.

On a d'ailleurs le théorème suivant:

Considérons $A_{1}(X_{1},...,X_{n}),...,A_{n}(X_{1},...,X_{n})$ n types algébriques avec au moins n paramètres $X_{1},...,X_{n}$. Considérons le systèmes d'équation suivant:

$\left\{{\begin{matrix}X_{1}=A_{1}(X_{1},...,X_{n})\\\vdots \\X_{n}=A_{n}(X_{1},...,X_{n})\end{matrix}}\right.$

Ce système admet toujours une unique solution que l'on peut calculer en posant

1. $X_{n}=\mu X_{n}.A_{n}(X_{1},...,X_{n})$ et en remplaçant $X_{n}$ dans les autres équations si n > 1 et ainsi de suite.

Type de données algébrique usuel :

• booléens : $\mathbb {B}$ = 1 + 1
• type à trois éléments = (1 + 1) + 1 ou 1 + (1 + 1)
• entiers en unaires : $\mathbb {N}$ = $\mu$ X.1 + X
• listes à éléments dans A : $\mathbb {L}$(A) = $\mu$ X.1 + (A $times$ X)
• entier en binaire : $\mathbb {L(B)}$
• arbre binaire : $\mu$ X.1 + (X $times$ X)

Exercices :

1. Donner un type des listes.
2. Donner un type des arbres binaires avec des données de type A au niveau des noeuds, un type des arbres binaires avec des données de type B au niveau des feuilles, un type des arbres binaires avec à la fois des données de type A au niveau des noeuds et des données de types B au niveau des feuilles.
3. Donner un type des arbres à branchement fini.
4. Donner un type des entiers binaires sans zéro inutile.

Solutions :

• Rappel sur les entiers unaire:

N sol de X=1+X µ * (1+X)=1+0 U 1+(1+0) U 1+(1+(1+0)). ={L{()}; R(L{()}); R(R(L{()}) }.

• Rappel sur les entiers binaire : liste de bool

N = 1 + ( ( 1 + 1 ) x N) N = 1 + ( N x N )

• Liste : LL(A)= 1+(A*LL(A)), liste peut être vide ou se constitue du premier élément A et de la suite de la liste.
• Arbre sans donnée : $\mathbb {A}$=1+($\mathbb {A}$*A). Arbre ou le premier élément est vide et la suite constitue sous arbres.

A0=1+(0*0)=L{()}

A1=1+(1+0*0)*(1+0*0)=R(L(),L())

$\mathbb {A}$=1+(A*($\mathbb {A}$*$\mathbb {A}$)) : arbre ou le premier élément est vide et la suite se constitue d’un element A et deux sous arbres.

• Arbre binaire avec donnée sur les nœuds $\mathbb {A}$(A) :

$\mathbb {A}$(X)=1+(($\mathbb {A}$(X)*X)*$\mathbb {A}$(X))+X*($\mathbb {A}$(X)* $\mathbb {A}$(X)).

• Arbre binaire avec donnée sur les feuilles $\mathbb {A}$’(B) :

$\mathbb {A}$’(Y)=Y+$\mathbb {A}$’’(Y)*$\mathbb {A}$(Y). L’arbre n’est pas vide.

$\mathbb {A}$’(Y)=1+$\mathbb {A}$’’(Y). arbre vide.

• Arbre binaire avec donnée sur les noeuds feuilles $\mathbb {A}$’(B) :

$\mathbb {A}$(X,Y)= Y+X *($\mathbb {A}$’(X,Y)*$\mathbb {A}$’(X,Y)).

$\mathbb {A}$(X,Y)=1+$\mathbb {A}$’(X,Y).

• Type des arbres à branchement fini.

$\mathbb {A}$F= LL(AF)

$\mathbb {A}$f=LL(Af)

=A+$\mathbb {A}$f*Af

=$\mathbb {A}$.

• type des entiers binaires sans zéro inutile

$\mathbb {N}$*=$\mathbb {N}$*+$\mathbb {N}$

RR=0.

RL=1

L=fin

Exemple : 100=RRRRRL().

Un entier $\mathbb {N}$=1+($\mathbb {N}$*$\mathbb {N}$).

• Let rec eq n m = match n with

L()à(match m with L(-)àL()| R(-)àR()) R(n’)à (match m with L(-)àR(-) | R(m’)àeqn’m’)

• Let rec append LL’=match L with

L()->L’ R(P)->R(pi1(p),append pi2(p)L’) R(a,L1)->R(a,appendL1L’)

Destructeurs des types algébriques

Les destructeurs servent à lire les données d'un type algébrique.

• x $\in$ 0 : abort(x) (cas impossible)
• x $\in$ 1 : pas de destructeur, un seul cas possible
• x $\in$ A $\times$ B : 2 projections : $\pi _{1}$(x) $\in$ A et $\pi _{2}$(x) $\in$ B
• x $\in$ A + B, ($\forall a\in$ A, c[y:=a]$\in$ C) et ($\forall b\in$ B, c'[z:=b] $\in$ C) : match x with L(y) -> c| R(z) -> c'$\in$ C
• Pour utiliser les types inductifs on définira des fonctions par récurrence. exemple :

 let rec add x y = match x with L(x') -> y | R(x') -> R(add x' y)

Il n'y a donc pas de destructeur particuler aux types inductifs.

Les fonctions

Pour programmer il nous faut des fonctions :

• A $\rightarrow$ B = {$\lambda$ x.t | t $\in$ B si on suppose x $\in$ A} : ce type désigne de type des fonctions prenant des arguments de type A et rendant un résultat de type B et $\lambda x.t$ désigne la fonction qui associe t à x. Par example $\lambda x.x$ est la fonction identité.

On a bien sûr un destructeur pour les fonctions : l'application

• t v $\in$ B si t $\in$ A $\rightarrow$ B et u $\in$ A

Il nous faut aussi des fonctions récursives et mutuellement récursives. Les définitions récursives peuvent s'écrire directement, ou avec un combinateur de point fixe Y, en remplaçant la définition récursive

$f=t$ où f apparait dans t (sinon la définition n'est pas récursive) par $f=Yf.t$

Pour les types, on a Y t $\in$ A si t $\in$ A $\rightarrow$ A

Exemples

• La fonction multiplier.

     Let rec mul n m=match n with
     L(-) | L()
     R(n’) | add(mul n’m)m

     Let rec eq n m = match n with
     L()|(match m with L(-)|L()| R(-)|R())
     R(n’) | (match m with 
     L(-)|R(-)
     | R(m’)|eqn’m’)

     Let rec append LL’= match L with
     L()|L’
     R(P)| R(pi1(p),append pi2(p)L’)
     R(a,L1)|R(a,appendL1L’) 

• entier N

  type rec nat =[End[]|
  Zero[nat] |
  one[nat]]

• Fonction successeur

Nat -> nat’=

Fun End[]| one [End[]]

| Zero[n]| one[n]

|one[n]|zero[succ n]

prédécesseur n-|n-1

val rec pred : nat’->nat

=Fun One[n]|Zero[n]

|Zero[n]|One[pred n] Fonction opposé Val opp int ->int=Fun Minus[n]|opp(pred’n) |n|succ n Hauteur d’une arbre en caml

let rec hauteur = function | Feuille -> 0 | Branche (branche, _, branche') -> 1 + max (hauteur branche) (hauteur branche') ;;

map en caml

1. List.map (fun i -> i * i) [0; 1; 2; 3; 4; 5] ;;

let apply_rev f x y = f y x;; let g x y = (x,y);; apply_rev g 64 16;; apply_rev (fun x y -> x / y) 3 18;; let rec f x = (x x);;

Sémantique dénotationnelle

Pour préciser comment s'évalue le langage, on définit une relation d'équivalence $\simeq$ comme la plus petite relation d'équivalence vérifiant :

• $\pi _{1}$(u,v) $\simeq$ u
• $\pi _{2}$(u,v) $\simeq$ v
• match L(a) with L(y) -> c | R(z) -> c' $\simeq$ c[y:=a]
• match R(b) with L(y) -> c | R(z) -> c' $\simeq$ c'[z:=b]
• $(\lambda x.t)u$ $\simeq$ t[x:=u]
• Y f.t $\simeq$ t[f := Y t]

Exercices

1. Ecrire des fonctions calculant l'addition et la multiplication pour les entiers unaires. Évaluer ces fonctions à la main sur de petits entiers.
2. Ecrire quelques fonctions sur les listes (map, append, rev, rev_append). Évaluer ces fonctions à la main sur de petites listes.

Corrections

1. addition pour les entiers unaires

• solution 1: let rec add n m = match n with L (_) -> m | R (n') -> add n'(R(m))
• solution 2: let rec add n m = match n with L (_) -> m | R (n') -> R(add n' m)
• exemple: add 2 3 = add (R R L()) (R R R L()) = add (R L()) R R R R L() = add (L()) R R R R R L() = R R R R R L() = 5

1. multiplication pour les entiers unaires

• solution 1 ( utilisant la récursivité non terminale) : let rec mul n m = match n with L (_) -> L() | R (n') -> add (mul n' m) m
• solution 2 (récursivité terminale) : let mul n m = aux n m (L())
• let rec aux n m a = match n with L() -> a | R(n') -> aux n' m (add m a)

Sémantique opérationelle

Généralités sur l'appel par nom, l'appel par valeur et l'évaluation paresseuse.

Définition d'une sémantique opérationnelle pour l'appel par valeur par contexte d'évaluation.

• Valeur : La grammaire du mini langage peut-être réécrite en distinguant deux types les valeurs des programmes qui ne sont pas des valeurs:

$V=x\mid \lambda x.T\mid LV\mid RV\mid (V,V)\mid ()$ $T=V\mid TT\mid matchTwithLx->T|Ry->T\mid \pi _{1}T\mid \pi _{2}T$

• Contexte d'évaluation
• La sémantique

Définition d'une sémantique opérationnelle pour l'appel par valeur avec une machine abstraite.

• Clôture
• Machine SECD
• Table de transition

Exercice : faire le même travail pour l'appel par nom. Pourquoi tout ceci serait plus compliqué pour l'évaluation paresseuse ?

Quelques théorèmes

• Préservation du type par réduction
• Existence d'un unificateur le plus général sur les types
• Inférence de type
• Théorème de Church-Rosser

Bibliographie

"Foundations for Programming Languages" de John C. Mitchell

"The ZINC experiment, an economical implementation of the ML language" de Xavier Leroy. Rapport technique 117, INRIA, 1990. pdf Ce rapport contient une description du compilateur ZINC, dont l'évolution a ensuite donné naissance à Caml Light puis Objective Caml. Une grande partie de ce rapport est obsolète. Néanmoins, il garde un intérêt pour la description de la machine abstraite utilisée par Caml Light et (avec quelques simplifications et améliorations supplémentaires) par Objective Caml.

Custom essays