Ocaml
Évaluation des programmes

Cours

Exercices

Évaluation

Introduction
Expressions arithmétiques
Noyau ML
Paires
Références

Expressions arithmétiques (eval, variables, eval')
Règles d'erreur
Paires
Conditionnelle

Un peu de recul

Questions Qu'est-ce qu'un langage? Qu'est-ce qu'un langage de programmtion? 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 pas intéressants. Par conséquent, il n'est 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é d'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 sures.

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 (bout) 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 l'é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 appartenant à un domaine sémantique (un ensemble défini pour cette occasion).

Par exemple, la sémantique des expressions arithmétiques (sans variables) 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'évalutaion sont des objets syntaxiques très proche des programmes, voir 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 comme 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 variables aux expressions arithemétiques

	a ::=	...
		x		Variable


type exp =
    ...
  | Var of string


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

Exercice 2 Écrire une fonction variables : exp -> string Set.t qui calcule l'ensemble des variables d'une expression arthmétique.

Réponse

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

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é fⁿ Î Fⁿ . 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	Variable
	a a	Application
	`fun` x ® a	Fonction
	`let` x = a₁ `in` a₂	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
  | Var of var
  | App of exp * exp 
  | Fonction of var * exp
  | Liaison of var * exp * exp
and var = string;;

Exemple de programme:


let e1 =
  Liaison
    ("f", Fonction ("y", Prim (plus, [ Var "y"; Const 3 ])), 
     App (Var "f", Const 2));;

Intuitivement l'évaluation de l'expression e1 doit valoir 3? 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 (liées 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 variables, 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, [Var "x"; Var "y"])))
  Liaison ("x", Const 2, App (Var "f", Var "x")));;

Vérifier que cette expression n'est pas équivalente à


Liaison
  ("x", Const 2,
   App (Fonction ("y", Prim (plus, [Var "x"; Var "y"])), Var "x"));;

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

Formellement:

v ::=		Valeurs
	c	Constante entière
	á `fun` x ® a, rñ	Fermeture

où r est un environement d'évuation, i.e. de la forme x₁ |® v₁, ... x_k |® v_k. En Ocaml,


type valeur =
  | Vconst of int
  | Vfonction of var * exp * env
and env = (var * 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 variante. 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

P₁ ... P_k

qui signifie que la conclusion C est vrai si les prémisse P₁, ... P_k sont vraies simultanément.

Const

r |- n Þ n

Var

r |- x Þ r(x)

Fun

r |- fun x ® a Þ á fun x ® a, rñ

App

r |- a₁ Þ á fun x ® a, r₀ñ

|- a₂ Þ v r₀, x |® v |- a Þ w

r |- a₁ a₂ Þ w

Prim

r |- a_i Þ v_i d (f, v) = w

r |- f a Þ 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 |- a₁ Þ r r ¬ ºá fun x ® a, r₀ñ

r |- a₁ a₂ Þ Err

App-Err-Right

r |- a₁ Þ á fun x ® a, r₀ñ r |- a₂ Þ Err

r |- a₁ a₂ Þ Err

Prim-Right

r |- a_i Þ Err

r |- f a Þ Err

Prim-Left

r |- a_i Þ v_i d (f, v) undefined

r |- f a Þ Err

En fait les règles d'erreurs sont plus nombreuses que les règles de bonnes évaluations. Elles décrivent à la fois comment les erreurs se déclanchent (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 appliqué 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 pattern matching (sur la forme du programme).

·	Deux conclusions de formes différentes sont deux cas différents dans la fonction `eval`.
·	Deux conclusions de la même forme (cas de l'application) corresponde à un même cas, les sous-expressions sont évaluées puis selon la forme de résultat l'une ou l'autre règle s'applique.


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

let rec eval env = function
  | Const c -> Vconst c
  | Var 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:

·	Dans le cas idéal, l'évaluation retourne une valeur.
·	L'évaluation produit une erreur.
·	L'évaluation peut aussi ``ne pas terminer''. Formellement, la seule chose que l'on peut dire est que pour un environnement r et un programme certain a il n'existe pas de réponse r telle que a r \|- a Þ r. On note alors r \|- a . Toutefois, la divergence ne correspond à la non terminaison au sens habituel que si les règles d'erreurs sont correctement définie (et comportent sufissement de cas). En effet, supprimer une règle d'erreur revient à chacun une erreur en une divergence.

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
	c^k a ^k	Const
c⁰ ::=	0, 1, 2, ...		Entiers
c² ::=	(·, ·)		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
	c^k v^k	Const
c⁰ ::=	0, 1, 2, ...	Entiers
c² ::=	(_, _)	Paires

Puis ajouter les règles d'évaluation

Paire

r |- a₁ Þ v₁ r |- a₂ Þ v₂

r |- (a₁, a₂) Þ (v₁, v₂)

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` a₀ `then` a₁ `else` a₂	Conditionnelle

Ifz-True

r |- a₀ Þ 0 r |- a₁ Þ v

r |- ifz a₀ then a₁ else a₂ Þ v

Ifz-False

r |- a₀ Þ n n ¹ 0 r |- a₂ Þ v

r |- ifz a₀ then a₁ else a₂ Þ v

Exercice 7 [Ajout d'une conditionnelle] Compléter l'évaluteur du noyau de ML avec la contruction de test à zéro ifz a₀ then a₁ else a₂.

Ajout de l'affectation

Dans le noyau précédent, une variable a une valeur donnée une fois pour toute. 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 |- a₁ Þ loc m / s₁ s₁ / r |- a₂ Þ v / s₂ m Î dom (s₂)

s / r |- a₁ := a₂ Þ v / (s₂ \ m, m |® v)

Plus les règles d'erreurs...

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

Exemple de réécriture:

App

s / r |- a₁ Þ á fun x ® a, r₀ñ / s₁

s₁ / r |- a₂ Þ v / s₂ s₂ / r₀, x |® v |- a Þ w / s₃

s / r |- a₁ a₂ Þ w / s₃

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 au 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:

·	Directement, en ajoutant une construction pour cela.
·	Indirectement, en utilisant des fonctions.
·	Indirectement, en utilisant des références.

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 |- a₁ Þ v₁ v₁ º á funrec f x ® a, r₀ñ

r |- a₂ Þ v r₀, f |® v₁, x |® v |- a Þ w

r |- a₁ a₂ Þ 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 ® a₁ in a₂ º let f = fix (fun f x ® a₁) in a₂

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 L^AT_EX by H^EV^EA and H^AC^HA.