Plan des 4 prochains cours
-
Environnements
- Fonctionnalité
- Application de fonction
- Récursivité
- Traits impératifs
-
Mémoire, références
- Exceptions
- Correction de programmes
- 1
- Renaud.Rioboo@lip6.fr
Évaluation
Espace d'expressions |
Espace de valeurs |
1+2 |
3 |
if true then 1 else 2 |
1 |
let y = 1 in y+1 |
2 |
function x -> x + 1 |
«x ~> x+1 , E » |
let y = 1 in function x -> x + y |
«x ~> x+y , E1 » |
Une expression Caml-Light prend une valeur dans un environnement. C'est l'évaluation.
Un identificateur est un nom2.
Un environnement permet d'associer
une valeur à un identificateur. Une liaison est l'association d'un
identificateur à une valeur.
Dans un environnement il peut y avoir plusieurs liaisons pour un même
identificateur, c'est le masquage.
L'environnement global est l'environnement dans lequel le programme se
trouve.
- 2
- que l'on utilise souvent dans une
fonction ou pour pour éviter des recalculs
Portée dynamique/statique
-
En portée dynamique la valeur d'un identificateur se trouve dans
l'environnement global (interprétation)
let x = 1 |
E = ë (x=1) <| E û |
let f = function y -> x + y |
E = ë (f=F) <| E û |
f 1 |
2 |
let x = 2 |
E = ë (x=2) <| E û |
f 1 |
3 |
-
En portée statique (ou lexicale) la valeur d'un identificateur se
trouve dans l'environnement de définition (compilation)
let x = 1 |
E1 = ë (x=1) <| E0 û |
let f = function y -> x + y |
E2 = ë (f=F) <| E1 û |
f 1 |
2 |
let x = `a` |
E3 = ë (x=`a`) <| E2 û |
f 1 |
2 |
Interaction avec le système de fichiers
Eg = Eu |><| Em |><| Eb
Une compilation (camlc -c) produit :
-
un fichier .zo de code et
- un fichier .zi d'interface obtenu à partir d'un fichier de
description d'interface.
La directive #open mod permet de rendre visible les identificateurs décrits dans mod.zi sans avoir à les nommer par
mod__ident.
L'interprète possède
-
une fonction load (
: string -> unit
) qui
permet de charger un module source (.ml) en mémoire.
-
une fonction load_object (
: string -> unit
) qui
permet de charger un module source (.zo) en mémoire.
En mode compilé il faut inclure le fichier .zo dans la ligne de commande
camlc -o bar foo.zo bar.ml
MATHS |
INFORMATIQUE |
variable |
paramètre formel |
paramètre |
variable libre |
argument |
paramètre effectif |
fonction |
fonction partiellement définie |
application |
fonction |
calculer f(exp) |
appliquer f à exp |
f(exp) |
f exp |
Les fonctions sont des valeurs Caml-Light que l'on nomme des fermetures.
En Caml-Light elles sont caractérisées par :
-
un nom de variable, c'est le paramètre formel (nom),
-
une expression définissant la valeur de la fonction en tout point que
l'on nomme le corps de la fonction (corps),
- un environnement de définition de la fonction (Env) :
On les note : «nom ~> corps , Env »
Appel par Nom
let deux =
(print_string "1+1" ; 1 + 1)
in
deux + deux ;;
-
liaison de deux à
(print_string "1+1" ; 1 + 1)
puis évaluation de deux + deux
-
substitution de deux à sa ``valeur'' soit :
(print_string "1+1" ; 1 + 1) +
(print_string "1+1" ; 1 + 1)
- affichage de "1+1" calcul de 1 + 1 = 2
- affichage de "1+1" calcul de 1 + 1 = 2
- calcul de 2 + 2 = 4
Les identificateurs sont remplacés par des expressions qui sont réévaluées.
Appel par Valeur
let deux =
(print_string "1+1" ; 1 + 1)
in
deux + deux ;;
-
calcul de la valeur de
(print_string "1+1" ; 1 + 1)
- affichage de "1+1" retour de 2
-
liaison de deux à sa valeur 2
-
calcul de deux + deux soit 2+2
- retour de 4
Les identificateurs sont remplacés par des valeurs et ne sont pas réévalués.
La liaison
Permet de nommer des valeurs.
-
Définitive : on modifie l'environnement global
let x = 1 ;;
-
évaluation de 1.
- modification de l'env global
E = ë (x=1) <| E û
-
Temporaire : on créée un nouvel environnement pour évaluer une
expression (portée lexicale) :
let x = 1 in x+1;;
-
évaluation de 1.
- création d'un nouvel environnement
E1 = ë (x=1) <| E û
- évaluation de x+1 dans E1
L'environnement global n'est pas modifié !
Liaison Caml-Light
La liaison permet de déstructurer
des valeurs :
type point = {abs : int ; ord : int} ;;
let ({abs = x ; ord = y} as un_point) =
{abs = 10 ; ord = 20 } ;;
Introduit 3 nouveaux noms :
-
x:int = 10, y:int = 20
- un_point:point= {abs= 10 ; ord= 20}
il n'y a pas de calcul dans les parties gauches d'un let, ce sont des motifs lexicaux.
let projection_verticale = function
{abs = x ; ord = y} as a_point ->
if (y = 0) then a_point
else {abs = x ; ord = 0};;
Ici lorsque y=0 le point n'est pas dupliqué.
Le motif _ permet de déstructurer sans nommer.
let abscisse = function {abs = x} -> x ;;
Fonctions : Exemple
type fonctions_booleenes =
Fbool of bool -> bool ;;
let vrai = Fbool (function _ -> true)
and faux = Fbool (function _ -> false);;
let ou =
function (Fbool f1) ->
function (Fbool f2) ->
Fbool (function x -> (f1 x) || (f2 x))
let applique =
function Fbool f1 ->
function x -> f1 x ;;
let est_vrai = ou vrai vrai ;;
applique est_vrai true = applique vrai true ;;
applique est_vrai false = applique vrai false;;
Application
Appliquer une fonction f à une valeur x c'est calculer la valeur de
f(x).
Il faut évaluer l'expression constituant le corps de la fonction
dans l'environnement de définition de la fonction augmenté de la liaison où
le paramètre formel est lié à la valeur d'appel (le paramètre effectif).
Soient Fe et xe deux expressions Caml-Light, la valeur de l'application Fe(xe) dans l'environnement E est la valeur de l'application
F(x) où F est la valeur de Fe dans E et x est la valeur de xe
dans E.
Si F = «p ~> Ep , Ed », alors F(x) vaut la même valeur que
let
p =
x in
Ep dans l'environnement Ed.
C'est aussi la même valeur que Ep dans l'environnement
ë (p=x) <| Ed û
Fonctions à plusieurs arguments
Deux choix ?
ce n'est pas équivalent
Fonctions
La construction
fun x1 ...xn -> E
est équivalente à
function x1 -> ...function xn ->
E
L'écriture
let F x1 ...xn = E
est équivalente à
let F = fun x1 ...xn -> E
La forme où fun ou function est explicite permet de définir un
environnement local à la fonction :
let incremente_compteur =
let compteur = ref(0) in
function n ->
begin
compteur := !compteur + n ;
!compteur
end ;;
Le filtrage
|
| F -> E |
= |
ì í î |
| F1 -> E1 |
... |
| Fn -> En |
|
|
|
-
Les Fi sont des motifs lexicaux.
- Les Ei sont des expressions qui
sont évaluées dans l'environnement de définition de la fonction augmenté des
liaisons produites pendant le filtrage.
-
Chaque clause de filtrage | Fi ® Ei
va :
-
permettre de sélectionner un sous-ensemble de valeurs du type
sv que doit avoir l'argument V.
- permettre de produire un environnement dans lequel va s'évaluer
l'expression Ei qui définit le corps de la clause comme dans :
let Fi = V in Ei
À l'appel, le paramètre effectif est ``superposé'' avec les
filtres Fi dans l'ordre du texte.
La construction match V with | F ® E
est équivalente à (function | F ® E) V.
On peut ajouter des conditions a une clause de filtrage Fi qui
a alors la forme :
| Fi when Ci ->
Ei
Où Ci est une expression qui doit être de type bool. Elle est
calculée dans l'environnement d'exécution du corps de la clause :
Si v est le paramètre effectif, et si E est l'environnement de définition
de la fonction, Ei et Ci s'évaluent dans E augmenté des
liaisons produites pendant le filtrage.
cette construction est à éviter
La récursivité
Dans le corps d'un let les identificateurs (noms de
fonctions) sont cherchés dans
l'environnement courant.
La construction
let rec
introduit un identificateur récursif.
Soit Ec
l'environnement courant, la déclaration
let rec foo = expr
créée une valeur Vfoo qui est le
résultat de l'évaluation de l'expression expr dans l'environnement
Efoo = ë (foo=Vfoo) <| Ec û
qui devient l'environnement courant.
let rec fib = function
| 0 -> 0
| 1 -> 1
| n -> fib(n-1) + fib(n-2)
;;
Récursion
Lors de l'appel d'une fonction récursive, il faut empiler les
environnements :
-
Soit Efib l'environnement de définition de fib.
-
fib(3) Þ évaluation de
E3 = fib(n-1) + fib(n-2)
dans E3 =
ë (n=3) <| Efib û,
calcul de fib(2) en suspens et :
-
calcul de fib(1) soit 1
- reprise du calcul de fib(2)Þ
E2 = fib(n-1) + fib(n-2)
dans E2 = ë (n=2) <| Efib û Þ
-
calcul de fib(0) soit 0
- puis de fib(1) soit 1
-
La valeur de E2 dans E2 est donc 1,
- on en déduit la valeur de
E3 dans E3 soit 2.
Les types sommes
La déclaration
type foo = C | C1 of t1 | C2 of t2
introduit des
Sont récursifs :
type somme_formelle =
| Variable
| Entier of int
| Somme of somme_formelle*somme_formelle
;;
let rec eval = function
| (Variable , valeur ) -> valeur
| (Entier n , _ ) -> n
| (Somme (e1,e2) , valeur) ->
eval(e1,valeur) + eval(e2,valeur)
;;
Ensuite :
eval(Somme(Variable,Entier 2) , 4)
Ordre supérieur
Sommer tous les éléments d'une liste ?
let rec somme = function
| [] -> 0
| h::r -> h + (somme r)
Ici 0:int et (prefix +):int -> int -> int. On généralise (zero: a et plus: b->a->a) :
let rec somme_abs =
function zero -> function plus ->
function
| [] -> zero
| h::r ->
(plus h (somme_abs zero plus r))
let somme =
function l -> somme_abs 0 (prefix +) l
Pour toute fonction F (monomorphe) on a :
function
x ->
F(x) = F
let somme = somme_abs 0 (prefix +) ;;
let mult = somme_abs 1 (prefix *) ;;
Récursion terminale
L'enveloppe d'un appel récursifs est l'ensemble des calculs qui doivent
d'effectuer après cet appel.
Lors d'un appel récursif, les différents environnements doivent être conservés
car d'autres calculs doivent s'exécuter après :
let rec foo = function
| 0 -> 0
| n -> foo(n-1) + n
Un appel récursif est terminal s'il n'y a pas d'autres calculs à
effectuer ensuite. C'est à dire si le résultat de la fonction est lui même un
appel récursif.
let rec foo_bis = function
| (0,res) -> res
| (n,r_p) -> foo((n-1) , r_p + n)
Et " x foo
(x) = foo_bis
(x,0).
La donnée des paramètres n et rp suffit à déterminer la valeur de la
fonction. Il n'y a plus besoin de stocker les environnements !
Lorsqu'un appel récursif est enveloppé par
une opération associative on peut rajouter un paramètre pour
obtenir un appel terminal.
let rec foo = function arg ->
if (arg = arg_0)
then val_0
else op(foo(g(arg)), f(arg))
où f et g ne contiennent pas foo, devient lorsque op
est associative :
let rec foo = function (arg,accu)
if (arg = arg_0)
then op(accu,val_0)
else foo(g(arg) , op(accu, f(arg)))
Dichotomie
Calcul de
an = {
(an/2)2 si n est pair |
a(an/2)2 si n est impair |
.
let rec pow = function a -> function n ->
if ((n mod 2) = 0) then
if (n = 0) then 1 else
let res = pow a (n / 2) in
res * res
else
if (n = 1) then a else
let res = pow a (n / 2) in
a * res * res
On peut généraliser 0, 1, * :
let rec dich = fun zero un op a n ->
if ((n mod 2) = 0) then
if (n = 0) then zero else
let res = dich zero un op a (n/2) in
op res res
else
if (n = 1) then un else
let res = dich zero un op a (n/2) in
op a (op res res)
Évaluation des arguments
Pour des raisons d'efficacité
Caml-Light évalue les arguments d'une application du dernier au premier :
let foo = fun x y -> !x + !y ;;
let essai = ref 0 in
foo
(essai := 1 ; essai)
(essai := 2 ; essai);;
Ainsi lorsqu'une application est totale il n'y a pas besoin de créer les
fermetures intermédiaires :
F x1 x2 ... xn = F1 x2 ... xn=Fn-1 xn
Les exceptions
Caml-Light offre un mécanisme d'erreurs simple grâce au type exn.
exception Foo ;; exception Bar of int;;
Les exceptions sont des valeurs :
let to_foo = function
| Bar _ -> Foo
| x -> x
;;
marquées exceptionnelles par :
raise
I (déclencher ou lever une exception).
On peut récupérer une exception :
try E with | F ® EI
let v = 1 in
try (let v = 2 in raise Foo)
with
| Foo -> v
;;
Soit E l'environnement courant.
-
Si l'évaluation de E dans E ne
déclenche pas d'exception c'est une valeur V (de type sv) qui est le
résultat.
- Sinon, soit I l'exception déclenchée, le résultat de
l'évaluation est alors le même que celui de match
I with | F ® EI dans l'environnement E.
En particulier les motifs des clauses Fi doivent être des exceptions
et les corps des clauses
EIi doivent avoir des types compatibles avec sv.
Le filtrage n'a pas besoin d'être exhaustif, on peut récupérer n'importe
quelle exception.
c'est à éviter
Une exception marquée n'est plus une valeur :
let foo = function x ->
try (x+1) with Foo -> -1
;;
foo (raise Foo);;
Traits impératifs
Les références Caml-Light correspondent aux variables des langages
impératifs. Ce sont des ``boites'' dans lesquelles on peut ``mettre'' des
valeurs de type fixé.
Caml-Light |
C |
let r = ref 1 |
int r = 1 |
On distingue la référence de son contenu |
r := !r + 1 |
r = r + 1 |
On a alors un modèle dynamique de mémoire analogue aux environnements
mais dont les ``clés'' sont des références.
L'affectation
(prefix :=): a ref -> a -> unit
modifie la valeur associée à la clé, la création
ref :a-> a ref
-
rajoute une nouvelle référence dans l'environnement,
-
créée une entrée associée à cette valeur dans la mémoire.
Soit M l'état mémoire d'un programme et E l'environnement courant ,
la déclaration
let r = ref v introduit un nouvel environnement
E' = ë (r=vr) <| E û et un nouvel état mémoire
M' = é (vr¬v)<| M ù.
Si r est le nom d'une référence vr :
-
on consulte le contenu de r par !r :
M |> vr
- l'instruction
r := v' ne modifie pas
l'environnement courant mais affecte la mémoire :
é (M|> vr)¬v ù
Il n'y a pas de masquage dans la mémoire :
é (M'|> vr)¬v' ù |
= |
é (é (vr¬v)<| M ù|> vr)¬v' ù |
= |
é (vr¬v')<| M ù |
L'état d'un programme est
alors donné par le couple environnement mémoire.
Les vecteurs, enregistrements dont les champs sont déclarés mutables
suivent le même modèle.
let foo =
let c = ref 0 in
function () ->
begin c := c+1 ; !c end
incrémente un compteur local à la fonction à chaque appel.
let foo = function () ->
let c = ref 0 in
begin c := c+1 ; !c end
Crée un nouveau compteur à chaque appel.
Que fait ? function c -> begin c := c+1 ; c end
La séquence, les boucles
begin |
begin |
E1; (:unit) |
E1; (:unit) |
... |
... |
En-1; (:unit) |
En-1; (:unit) |
En; (:unit) |
En(:sn) |
end |
end |
:unit = () |
:sn= En |
let _ = E1 in |
let _ = ...in |
let _ = En-1 in |
En |
La boucle for i = im to iM do E done introduit un nouvel identificateur i:int.
let i = "i" ;;
for i = 1 to 9 do print_int i done ;;
i;;
Impératif/Fonctionnel
let fact = function n ->
let res = ref 1 in
begin
for i = 1 to n do
res := !res * i
done ;
!res
end;;
|
let rec fact = function
| 0 -> 1
| n -> n * (fact (n-1));;
Consommation de pile !
let fact =
let rec fact_a =
function r -> function
| 0 -> r
| n -> fac_a (n*r) (n-1)
in function n -> fact_a 1 n
;;
|
let fib = function n ->
let f_0 = ref(0)
and f_1 = ref(1)
and temp = ref(0) in
begin
for i = 1 to n do
temp := !f_0;
f_0 := !f_1;
f_1 := !temp + !f_1
done;
!f_0
end
|
let fib =
let rec fib_aux = function
| 0 -> (0, 1)
| n ->
let (f_0,f_1) =
fib_aux(n - 1)
in (f_1, f_0 + f_1)
in function n -> fst(fib_aux n)
|
Correction de programmes
-
Terminaison de fonctions récursives
let rec ack = fun n m ->
if (n = 0) then m + 1 else
if (m = 1)
then ack (n - 1) 1
else ack (n - 1) (ack n (m - 1))
-
Correction de programmes
let min_list = function
| [] -> failwith "Liste vide"
| h::t -> it_list min h t
Équivalent à
let min_list =
let rec aux = function m -> function
| [] -> m
| h::t ->
if (h < m)
then aux h t
else aux m t
in function
| [] -> failwith "Liste vide"
| h::t -> aux h t
Terminaison
Mathématique |
Caml-Light |
Ensemble inductif |
type récursif |
fonction récursive |
fonction récursive |
type arbre_bin =
| Feuille of int
| Noeud of (arbre_bin * arbre_bin)
let rec it_arbre = fun op -> function
| Feuille n -> n
| Noeud (fg,fd) ->
op (it_arbre op fg) (it_arbre op fd)
deux cas :
-
l'arbre est une feuille et
it_arbre(F,Feuille n) vaut n
- on suppose que it_arbre(F , A1) et it_arbre(F,A2)
valent a1 et a2. La valeur de it_arbre(F,Noeud (A1,A2))
est alors F(a1,a2).
Correction
let rec append = function
| [] -> function l -> l
| h::t -> function l -> h::(append t l)
A-t-on l'associativité :
append l1 (append l2 l3) =
append (append l1 l2) l3
-
si l1 est vide,
append l1 (append l2 l3) = append l2 l3 et
append (append l1 l2) l3 = append l2 l3
- sinon l1 = h1::l1' et
append l1 (append l2 l3) = |
h1::(append l1' (append l2 l3)) |
append (append l1 l2) l3 = |
append (h1::(append l1' l2)) l3 = |
h1::(append (append l1' l2) l3 ) |
On conclut par induction en utilisant le résultat sur l1', l2 et l3.
Exemple : le pgcd
let rec gcd = fun n m ->
if (m = 0)
then n
else gcd m (n mod m)
Termine pour m et n positifs ?
-
supposons m < n. Si m=0 le résultat est correct. Sinon 0 £
(n mod m) < m et :
n mod m < m
et le couple (n,m) décroit strictement pour l'ordre produit.
- si m ³ n alors m < (n mod m) 3
et on utilise le point précédent.
Tout diviseur commun à n et m divise le pgcd :
- 3
- sauf si m=n=0
Ce document a été traduit de LATEX par HEVEA.