Ocaml
Évaluation des programmes
Cours Exercices
Évaluation
  1. Introduction
  2. Expressions arithmétiques
  3. Noyau ML
  4. Paires
  5. Références
  1. Expressions arithmétiques (eval, variables, eval')
  2. Règles d'erreur
  3. Paires
  4. Conditionnelle



Un peu de recul

Questions Qu'est-ce qu'un langage? Qu'est-ce qu'un langage de programmation? Sont-ils tous équivalents? Comment les comparer?

Langages de programmations

Les langages de programmation ne sont que des approximations, rigoureuses mais incomplètes, du langage mathématique. Les langages généraux (non spécialisés à certains types de problèmes), sont complets au sens de Turing. Cela veut dire qu'ils permettent d'écrire tous les algorithmes calculables. Sinon, ils ne seraient (peut-être) pas intéressants. Par conséquent, il n'est généralement  pas possible de prévoir mécaniquement de la terminaison d'un programme.

Les langages de programmation ne sont cependant pas tous équivalents, car ils diffèrent énormément par leur expressivité, c'est-à-dire leur capacité à exprimer succinctement certains algorithmes. Ce qui conduit à une recherche ---sans fin?--- de nouvelles structures de programmation, plus expressives, permettant de décrire des algorithmes de façon plus concise.

Mais l'expressivité n'est pas a rechercher à tout prix. En particulier, il faut se limiter à des constructions essentielles, simples, bien formalisés et mais aussi sûres.

En particulier, la sûreté de l'exécution ne doit évidemment pas être abandonnée au profit de l'expressivité. Pour cela, on se limite souvent à une sous-classe (décidable) des programmes qui s'évaluent normalement.

Syntaxe concrète et syntaxe abstraite

En informatique, on distingue la syntaxe concrète (phrases composée d'une suite de caractères ou de lexèmes) définissant un programme et sa syntaxe abstraite qui est une représentation informatique/mathématique de la syntaxe, en générale sous une forme arborescente.

Par exemple, la phrase let f = fun x -> x est la syntaxe concrète d'un (fragment) de programme. La syntaxe abstraite associé sera, par exemple, l'arbre

    Liaison ("f", Fonction ("x", Variable "x))
Syntaxe et sémantique

Donner la syntaxe (concrète ou abstraite) d'un langage n'est qu'un préliminaire à sa définition. Pour parler de programme il faut donner un sens aux expressions du langage, c'est-à-dire définir leur sémantique. Par exemple, cela peut se faire en décrivant le mécanisme d'évaluation des expressions.

La sémantique dénotationelle est une sémantique abstraite. C'est la donnée d'une fonction qui associe à chaque programmme un objet mathématique (sa dénotation) appartenant à un domaine sémantique (un ensemble défini pour cette occasion).

Par exemple, la sémantique des expressions arithmétiques (sans identificateurs) peut être définie en associant à chaque arbre de syntaxe abstraite représentant une expression un entier naturel correspondant à la valeur de cette expression.

La sémantique dite opérationnelle est plus concrète, en particulier les valeurs résultats de l'évaluation sont des objets syntaxiques très proche des programmes, voire un sous-ensemble des programmes. La sémantique opérationnelle n'explique donc pas ce qu'est un programme, mais elle décrit précisément comment l'évaluer.

Exemple des expressions arithmétiques

Pour simplifier on se contentera des sommes et produits:
  a ::=     Expression
    c   Constante entière
    a + a   Somme
    a * a   Produit
On peut représenter la syntaxe abstraite en Ocaml par une variante:

type exp =
Const of int
| Somme of exp * exp
| Produit of exp * exp;;
Par exemple, l'expression concrète 2 * (3 + 4) est représentée par:

let e = Produit (Const 2, Somme (Const 3, Const 4));;

Exercice 1   Écrire une fonction eval : exp -> int qui prend une expression arithmétique et retourne sa valeur.
Réponse

Ajout des variables On ajoute des identificateurs aux expressions arithmétiques
  a ::= ...
    x   Identificateur

type exp =
...
| Ident of string

let ex = Somme (Const 2, Produit (Ident "x", Const 3));;

Exercice 2   Écrire une fonction idents : exp -> string Set.t qui calcule l'ensemble des identificateurs d'une expression arithmétique.
Réponse



On peut évaluer les expressions avec identificateurs dans un environnement (liste de paires identificateurs-entiers) qui donne des valeurs aux identificateurs.


Exercice 3   Écrire une fonction eval : (string * int) list -> exp -> int qui prend un environnement, une expression et retourne le résultat de cette expression dans l'environnement.
Réponse



Les expressions du noyau de ML

Les constantes La syntaxe est définie par rapport à un ensemble de constante entières cÎ C et un ensemble de primitives données avec leur arité fn Î Fn . On notes t un tuple d'éléments de type t.

Un programme est une expression composée de l'une des formes suivantes:
  a ::=     Expression
    c   Const
    f a   Primitive
    x   Identificateur
    a a   Application
    fun  x ® a   Fonction
    let  x = a1  in  a2   Liaison
En Ocaml, on définit:

type prim = {name : string; arity : int}
let succ = {name ="succ"; arity = 1}
let plus = {name = "plus"; arity = 2}

type exp =
| Const of int
| Prim of prim * exp list
| Ident of ident
| App of exp * exp
| Fonction of ident * exp
| Liaison of ident * exp * exp
and ident = string;;
Exemple de programme:

let e1 =
Liaison ("f", Fonction ("y", Prim (plus, [ Ident "y"; Const 3 ])),
App (Ident "f", Const 2));;
Intuitivement, l'évaluation de l'expression e1 doit valoir 5? Quels sont les autres formes de valeurs possibles?

Les valeurs de ML

Ce sont les constantes entières, mais aussi les fonctions (pas ou partiellement appliquées). L'évaluation du corps d'une fonction est en effet gelé jusqu'à ce que tous les arguments soient fournis.

Cependant une fonction peut comporter des variables libres (identificateurs liés dans l'environnement d'évaluation). Traiter cette fonction comme une valeur permet de déplacer cette fonction et de l'utiliser dans un autre contexte d'évaluation. Afin de préserver la liaison (statique) des identificateurs, une fonction est évaluée en une fermeture, i.e. en couplant la fonction avec l'environnement courrant d'évaluation.


Exercice 4   On considère le programme Ocaml

Liaison
 ("f", Liaison ("x", Const 1,
Fonction ("y", Prim (plus, [Ident "x"; Ident "y"])))
Liaison ("x", Const 2, App (Ident "f", Ident "x")));;
Vérifier que cette expression n'est pas équivalente à

Liaison
  ("x", Const 2,
App (Fonction ("y", Prim (plus, [Ident "x"; Ident "y"])), Var "x"));;
obtenue en remplaçant (Ident "f") par Fonction ("y", Prim (plus, [Ident "x"; Ident "y"]))).



Formellement:
  v ::=     Valeurs
    c   Constante entière
    á fun  x ® a, rñ   Fermeture
r est un environement d'évuation, i.e. de la forme x1 |® v1, ... xk |® vk.

En OCaml:

type valeur =
Vconst of int
| Vfonction of ident * exp * env
and env = (ident * valeur) list;;

Les erreurs

Le résultat de l'évaluation peut être erroné.
  r ::=     Résultats
    v   Valeur
    Err   Erreur
Formellement un résultat est un élément d'un type à plusieurs cas. Cependant en OCaml, on traitera les erreurs comme des exceptions et on retournera une valeur dans le cas normal.

type error =
Libre of string
| Delta of prim * valeur list
| Beta of exp;;
exception Error of error;;
let error e = raise (Error e);;
L'évaluation d'un programme est paramétrée par l'évaluation des primitives. On se donne donc pour chaque primitive d'arité n une fonction d'évaluation de même arité, partiellement définie.

let delta_succ  [Vconst x] = Vconst (x + 1);;
let delta_plus [Vconst x; Vconst y] = Vconst (x + y) ;;
let delta =
[ "succ", delta_succ; "plus", delta_plus; ] ;;

Règles d'évaluations

On décrit la sémantique opérationnelle par une relation r |- a Þ r qui se lit dans l'environnement r, le programme a s'évalue en le résultat v.

Cette relation est définie par des règles d'inférences de la forme


P1        ...        Pk
C
qui signifie que la conclusion C est vrai si les prémisse P1, ... Pk sont vraies simultanément.

Const
r |- n Þ n
      
Var
r |- x Þ r(x)
      
Fun
r |- fun  x ® a Þ á fun  x ® a, rñ

App
r |- a1 Þ á fun  x ® a, r0ñ
r |- a2 Þ v        r0, x |® v |- a Þ w
r |- a1 a2 Þ w

Prim
r |- ai Þ vi        d (f, v1...vn) = w
r |- f a1 ... anÞ w
      

Règles d'erreurs

En fait, il faut compléter les règles de bonne évaluation par des règles d'erreurs.

Var-Libre
x Ï dom  r
r |- x Þ Err
      
App-Err-Left
r |- a1 Þ r        r ¬ ºá fun  x ® a, r0ñ
r |- a1 a2 Þ Err

App-Err-Right
r |- a1 Þ á fun  x ® a, r0ñ        r |- a2 Þ Err
r |- a1 a2 Þ Err

Prim-Right
r |- ai Þ Err
r |- f a Þ Err
      
Prim-Left
r |- ai Þ vi        d (f, v) undefined
r |- f a Þ Err
En fait les règles d'erreurs sont plus nombreuses que les règles de bonne évaluation. Elles décrivent à la fois comment les erreurs se déclenchent (par exemple Var-Libre) et comment elles se propagent (par exemple App-Err-Right).

Les règles d'erreur forcent également un ordre d'évaluation: ici l'ordre gauche-droite est imposé par la combinaison de App-Err-Left et App-Err-Right, puisque pour appliquer App-Err-Right il faut que la partie gauche s'évalue correctement.

Implémentation

Une fois l'ordre d'évaluation imposé (par les règles d'erreurs), la relation d'évaluation devient une fonction. On peut alors lire les règles presque comme une définition récursive par analyse de cas (filtrage) de la forme du programme.

let find x env =
try List.assoc x env with Not_found -> error (Libre x);;

let rec eval env = function Const c -> Vconst c
| Ident x as vx -> find x env
| Fonction (x, a) as f -> Vfonction (x, a, env)
| App (a1, a2) as e ->
let f = eval env a1 in let v = eval env a2 in begin match f with Vfonction (x, a, env0) -> eval ((x, v) :: env0) a
| Vconst _ -> error (Beta e)
end | Prim (f, args) as e ->
let vargs = List.map (eval env) args in begin try (List.assoc f.name delta) vargs
with x -> error (Delta (f, vargs))
end | Liaison (x, e1, e2) as e ->
eval env (App (Fonction (x, e2), e1)) ;;

let v1 = eval [] e1;;


L'évaluation d'un programme

Trois cas se présentent:

Ajout des paires

De nombreuses constructions peuvent être ajoutées en suivant le même modèle. (il faut toutefois l'enrichir).

Pour modéliser l'ajout des paires, on ajoute une notion de valeurs construites qui généralise les entiers à des constructeurs pouvant prendre des arguments.
  a ::=     Expression
    ...   comme avant, sauf
    ck a k Const
  c0 ::= 0, 1, 2, ...   Entiers
  c2 ::= (·, ·)   Paires

En Ocaml

type constr = Int of int | Constr of string
type const = {constr : constr; carity : int}
...
| Const of constructeur * exp list
Il faut aussi étendre les valeur de façon similaires:
  v ::=     Valeurs
    ...   comme avant, sauf
    ck vk   Const
  c0 ::= 0, 1, 2, ...   Entiers
  c2 ::= (_, _)   Paires
Puis ajouter les règles d'évaluation

Paire
r |- a1 Þ v1        r |- a2 Þ v2
r |- (a1, a2) Þ (v1, v2)

Exercice 5   Ajouter toutes les règles d'erreurs pour imposer une évaluation gauche-droite.
Réponse


Exercice 6   Modifier l'évaluateur pour prendre en compte les paires.
Réponse



Ajout d'une conditionnelle

  a ::=     Expression
    ...   comme avant, plus
    ifz  a0  then  a1  else a2   Conditionnelle


Ifz-True
r |- a0 Þ 0        r |- a1 Þ v
r |- ifz  a0  then  a1  else a2 Þ v
      
Ifz-False
r |- a0 Þ n        n ¹ 0        r |- a2 Þ v
r |- ifz  a0  then  a1  else a2 Þ v



Exercice 7  [Ajout d'une conditionnelle]   Compléter l'évaluateur du noyau de ML avec la contruction de test à zéro ifz  a0  then  a1  else a2.



Ajout de l'affectation

Dans le noyau précédent, une variable a une valeur donnée une fois pour toute (c'est même pour cela que nous les avons appelées identificateurs). Plusieurs évaluations de la même expression retourneront toujours la même valeur. C'est souvent un avantage (plus grande sécurité de la programmation), mais parfois un inconvénient. Par exemple comment peut-on implémenter un compteur qui retourne un nouvel entier à chaque appel?

Pour cela, il faut se donner, comme en OCaml, des objects mutables, le cas le plus simple étant la cellule de référence.

  a ::=     Expression
    ...   comme avant, sauf
    ref  a   Référence
    !a   Référence
    a := a   Référence
En OCaml,

type exp = 
...
| Ref of exp
| Deref of exp
| Assign of exp * exp
Pour décrire la sémantique avec des cellules mutables, on suit l'intuition: une cellule est une location (adresse) mémoire à laquelle on peut écrire ou lire.
  v ::=     Valeurs
    ...   comme avant, sauf
    loc  m   Location mémoire
La mémoire est une fonction qui associe des valeurs à des locations-mémoire. La relation sémantique s / r |- a Þ v / s' prend alors deux paramètres de plus, la mémoire en entrée s et la mémoire modifiée après l'évaluation de l'expression s'.

Règles pour les constructions d'affectation

Ref
s / r |- a Þ v / s'        m Ï dom (s')       
s / r |- ref  a Þ loc  m / s', m |® v

Deref
s / r |- a Þ loc  m / s'        s (m) = v
s / r |- !a Þ v / s'

Assign
s / r |- a1 Þ loc  m / s1        s1 / r |- a2 Þ v / s2        m Î dom (s2)
s / r |- a1 := a2 Þ v / (s2 \ m, m |® v)
Plus les règles d'erreurs...

Par ailleurs, il faut modifier les anciennes règles: bien qu'elles ne modifient pas la mémoire directement, elles peuvent le faire indirectement, par exemple en évaluant des sous-expressions.

Exemple de réécriture:

App
s / r |- a1 Þ á fun  x ® a, r0ñ / s1
s1 / r |- a2 Þ v / s2        s2 / r0, x |® v |- a Þ w / s3
s / r |- a1 a2 Þ w / s3
Cette ré-écriture fixe également l'ordre d'évaluation.

En ocaml

Pour la mise en oeuvre en OCaml, on pourrait suivre les règles mot à mot, mais on va plutôt profiter des références du langage hôte, ce qui revient à délocaliser la mémoire s. Aussi on ajoute simplement aux valeurs

type valeur = ... | Loc of valeur ref;;
let loc v = Loc (ref v);;
Puis on modifie la fonction d'évaluation:

type error =
 ...
| Loc of exp

let rec eval =
...
| Ref a -> loc (eval env a)
| Deref a as e ->
let v = eval env a in begin match v with Loc l -> !l | _ -> error (Loc e) end | Assign (a1, a2) ->
let v1 = eval env a1 in begin match v with Loc l -> l := eval env a2
| _ -> error (Loc e)
end ;;


Récursion

Le noyau ML défini ci-dessus ne permet pas d'écrire directement des programmes récursifs.

On peut le faire de 3 façons:

La récursion directement

On peut ajouter une nouvelle construction funrec  f x ® a qui s'évalue vers un nouveau type de valeur áfunrec  f x ® a, rñ

Fun
r |- funrec  f x ® a Þ á funrec  f x ® a, rñ

App
r |- a1 Þ v1        v1 º á funrec  f x ® a, r0ñ
r |- a2 Þ v        r0, f |® v1, x |® v |- a Þ w
r |- a1 a2 Þ w


L'opérateur de point fixe

On peut définir l'opérateur:
fix º fun  b ® (fun  f x ® b (f f) x) (fun  f x ® b (f f) x)
alors
let   rec  f = fun  x ® a1  in  a2    º    let  f = fix (fun  f x ® a1)  in  a2
Vérification: comme ce programme n'est typable qu'avec des types récursifs.
$ ocaml -rectypes

let fix b = (fun f x -> b (f f) x) (fun f x -> b (f f) x);;
let fact = fix (fun fact n -> if n > 1 then n * fact (n-1) else 1);;
fact 5 = 120;;





This document was translated from LATEX by HEVEA and HACHA.