(**
Langages, sémantiques et modèles d'exécution.
Thibaut Balabonski @ Université Paris-Sud, M2 FIIL.
Cours 1, 11 septembre 2018.
Lambda-calcul et stratégies d'évaluation
Ces notes de cours sont exécutables.
Vous pouvez copier le contenu de cette page dans un
fichier .ml et tester le code.
*)
(**
λ-calcul.
Formalisme introduit par Alonzo Church dans les années 30, pour formaliser
les notions d'algorithme et de calculabilité.
L'élément de base est la fonction
Caml : fun x -> e
Maths : f(x) = e
λ-calcul : λx.e
Syntaxe
-------
Les 'termes' du λ-calcul sont formés avec trois constructions :
x :: variable
t₁ t₂ :: application d'un terme à un autre
t₁ peut être compris comme une fonction,
et t₂ comme son argument
λx.t :: fonction d'un paramètre x
Dynamique
---------
Un terme décrit un algorithme.
L'exécution de l'algorithme est modélisée par une transformation du terme.
L'unité de calcul (appelée /redex/) est l'application d'une fonction à
un argument :
(λx.t) u ⟶ ??
Ou de manière équivalente :
(fun x -> t) u ⟶ ??
let f(x) = t in f(u) ⟶ ??
Le résultat est quelque chose de semblable à t,
mais qui fait intervenir u en remplacement de x.
On note
(λx.t) u ⟶ t{x ← u}
et on parle de 'substitution' :
't dans lequel toutes les occurrences de x sont remplacées par u'
Substitution
------------
C'est le point un peu subtil du formalisme.
La substitution est définie par récurrence sur la structure des termes :
x {x ← u} = u
y {x ← u} = y si x ≠ y
(t₁ t₂) {x ← u} = t₁{x ← u} t₂{x ← u}
(λx.t) {x ← u} = ??
λ est ce qu'on appelle un 'lieur'.
Il définit une *nouvelle* variable, et délimite sa portée.
Le x dans λx.t n'existe qu'à l'intérieur de t.
( cf en maths : Σᵢ i = n(n+1)/2 )
Corollaire : on peut remplacer x par n'importe quel autre nom, tant
qu'on le fait de manière coordonnée.
En λ-calcul, on a donc équivalence entre :
λx.t
et
λy.(t{x ← y})
à condition que y n'apparaisse pas déjà dans t.
Exemple :
λx.xy est équivalent à λz.zy mais pas à λy.yy
Pour formaliser cela, on a une notion de 'variable libre' :
une variable apparaissant dans un terme sans être liée.
L'ensemble des variables libres d'un terme est définie par récurrence
sur la structure des termes :
fv(x) = { x }
fv(t₁ t₂) = fv(t₁) ∪ fv(t₂)
fv(λx.t) = fv(t) \ { x }
Exemple traître :
fv(x(λx.x)) = fv(x) ∪ fv(λx.x) = {x} ∪ (fv(x) \ {x}) = {x} ∪ ∅ = {x}
Avec la notion de variable libre on peut formaliser le 'renommage' :
λx.t == λy.t{x ← y} si y ∉ fv(t)
Ce renommage est appelé 'α-conversion' (ou 'α-renommage').
Petite note technique : les termes du λ-calcul sont généralement
considérés 'à α-équivalence près'.
On peut maintenant décrire plus précisément pour la substitution t{x ← u} :
remplacer dans t toutes les occurrences *libres* de x par u.
En particulier, x ∉ fv(λx.t), donc
(λx.t){x ← u} = λx.t
En revanche on pourrait imaginer :
(λy.t){x ← u} = λy.(t{x←u}) si x≠y
Exemple :
(λy.yx){x ← yz} = λy.(yx{x ← yz}) = λy.yyz
Problème :
la variable y est 'capturée' par le lieur λy.
La définition de la substitution est un peu plus subtile :
on veut éviter qu'une variable libre soit capturée.
On raffine donc la règle :
(λy.t){x ← u} = λy.(t{x←u}) si x≠y et y ∉ fv(u)
Exemple :
(λy.yx){x ← yz} ... pas de substitution possible !
Mais avec renommage :
(λy.yx){x ← yz} = (λw.wx){x ← yz} = λw.(wx{x ← yz}) = λw.wyz
Bilan
-----
Finalement, le λ-calcul est défini par une unique règle de calcul
(λx.t) u ⟶ t{x ← u}
appelée β-réduction.
(mais cette règle cache une notion subtile de substitution)
Cependant, avec le λ-calcul on peut coder :
- les nombres entiers
- l'arithmétique
- des structures de données
- des fonctions
- des boucles
- ...
- les machines de Turing
(wikipedia : encodage de Church)
*)
(**
Deuxième étape dans l'histoire du λ-calcul :
les fondements de la programmation fonctionnelle.
En Caml, quelle est la dynamique de
let f x = x + x in f (1 + 2)
?
1. évaluer 1 + 2 ⟶ 3
2. appliquer la fonction
3. évaluer 3 + 3 ⟶ 6
En pseudo-λ-calcul on pourrait l'écrire
(λx.x+x)(1+2) ⟶ (λx.x+x)3 ⟶ 3+3 ⟶ 6
Mais une autre possibilité serait par exemple
(λx.x+x)(1+2) ⟶ (1+2)+(1+2) ⟶ 3+(1+2) ⟶ 3+3 ⟶ 6
Chaque langage de programmation est associé à une 'stratégie d'évaluation'
qui définit l'ordre des opérations.
En Caml c'est l'appel 'par valeur' : lors de l'application d'une fonction,
on évalue toujours l'argument d'abord.
Celle de la deuxième ligne est l'appel 'par nom' : on applique déjà
la fonction, puis on évaluera l'argument à chaque fois que nécessaire.
Dans le λ-calcul, partant d'un terme, si on regarde toutes les manières
possibles d'évaluer, on va obtenir un graphe dans lequel :
- les sommets sont des termes
- les arcs correspondent à une étape de réduction
Une stratégie d'évaluation, c'est une manière de choisir un chemin dans
ce graphe.
À noter : chaque langage de programmation suit une stratégie donnée.
À noter : un programme qu'on exécute peut en général être considéré comme
'clos', c'est-à-dire qu'il ne contient pas de variable libre. Cela va
simplifier l'implémentation des substitutions.
À noter : la dynamique d'un langage de programmation fonctionnelle
vise à 'évaluer' le programme, c'est-à-dire littéralement à produire
une 'valeur', qui peut être une constante ou une fonction.
Ainsi, en Caml
fun () -> print_int 1
est une valeur, et le corps de la fonction n'est pas évalué tant que
ce terme n'est pas appliqué à un argument.
Vérification : si vous entrez ce terme dans le toplevel Caml, l'affichage
n'aura pas lieu.
Définition de la dynamique d'un langage
---------------------------------------
On peut définir la dynamique d'un langage fonctionnel au moyen d'une
'sémantique naturelle', ou 'sémantique à grands pas', qui à un terme
associe la valeur qu'il produit :
t ⟹ v
On peut utiliser des règles d'inférences basées sur la structure des
termes pour définir cette relation t ⟹ v :
-------------
λx.t ⟹ λx.t
Une fonction est en soi une valeur et est son propre résultat,
à partir de ce point on n'évalue plus.
t ⟹ λx.w w{x ← u} ⟹ v
-----------------------------
t u ⟹ v
Si l'évaluation d'un terme t donne une fonction λx.w,
alors le résultat de l'évaluation du terme t u
est le résultat qu'on obtiendrait en appliquant
la fonction λx.w à u.
Ces règles d'inférence sous entendent une stratégie d'évaluation, en
l'occurrence l'appel par nom.
On peut les traduire en code pour s'en rendre compte :
*)
(* Représentation des λ-termes. *)
type terme =
| Variable of string (* x *)
| Application of terme * terme (* t₁ t₂ *)
| Abstraction of string * terme (* λx.t *)
(* Définition simple de la substitution.
Ici on suppose qu'on ne manipule que des termes sans variables libres,
il n'y a donc pas de problèmes de capture ou de renommage. *)
let rec substitution x u = function
| Variable(y) ->
if x=y
then u (* x{x ← u} = u *)
else Variable(y) (* y{x ← u} = y si x ≠ y *)
| Application(t1, t2) -> (* (t₁ t₂){x ← u} = t₁{x ← u} t₂{x ← u} *)
Application(substitution x u t1, substitution x u t2)
| Abstraction(y, t) ->
if x=y
then Abstraction(y, t) (* (λx.t){x ← u} = λx.t *)
else Abstraction(y, substitution x u t) (* (λy.t){x ← u} = λy.(t{x←u})
si x≠y et y ∉ fv(u) *)
(* Dans ce dernier cas, si on autorisait les variables libres il faudrait
faire des vérifications, et éventuellement un renommage. *)
(* Définition d'un évaluateur, qui correspond aux règles de sémantique *)
let rec eval_call_by_name = function
| Abstraction(x, t) ->
(* -------------
λx.t ⟹ λx.t *)
Abstraction(x, t)
| Application(t, u) ->
(* t ⟹ λx.w w{x ← u} ⟹ v
-----------------------------
t u ⟹ v *)
(match eval_call_by_name t (* t ⟹ λx.w *) with
| Abstraction(x, w) ->
eval_call_by_name (substitution x u w) (* w{x ← u} ⟹ v *) )
(**
L'évaluateur fonctionne en appel par valeur : il effectue la substitution
de l'argument non évalué, puis évalue le résultat, ce qui impliquera
d'évaluer l'argument u à chaque qu'il sera nécessaire.
L'évaluateur suivant propose une version en appel par valeur :
l'argument est évalué avant d'être substitué dans le corps de la fonction.
*)
(* Évaluateur en appel par valeur *)
let rec eval_call_by_value = function
| Abstraction(x, t) ->
(* Cas de l'abstraction : rien ne change *)
Abstraction(x, t)
| Application(t, u) ->
(* Cas de l'application : on évalue d'abord le terme de gauche... *)
(match eval_call_by_value t with
| Abstraction(x, w) ->
(* Puis on évalue l'argument... *)
let v = eval_call_by_value u in
(* Et enfin on évalue le terme obtenu en substituant l'argument
déjà évalué dans le corps de la fonction. *)
eval_call_by_value (substitution x v w) )
(**
D'autres règles d'inférence correspondent à ce nouveau comportement :
------------- [inchangée]
λx.t ⟹ λx.t
t ⟹ λx.w u ⟹ v w{x ← v} ⟹ r [le terme substitué est le résultat
------------------------------------ d'une évaluation ]
t u ⟹ r
*)
(**
Évaluation paresseuse : combiner les aspects
intéressant d'appel par valeur et par nom :
- évaluer l'argument d'une fonction au plus une fois
- ne pas évaluer l'argument d'une fonction s'il n'est pas utile
Technique : mécanisme de 'suspension' (ou mémoïsation)
- La première fois qu'un argument est utilisé, on calcule sa valeur
et on la stocke en mémoire.
- Les fois suivantes, on se contente de lire la valeur déjà calculée.
Sémantique un peu plus compliquée : il va falloir représenter cette mémoire
Évaluation :
⟦Σ⟧t ⟹ ⟦Σ'⟧v
où Σ est un état de la mémoire : associe des suspensions (évaluées ou
non) aux variables.
L'évaluation d'un terme t peut modifier la mémoire : on produit un nouvel
état Σ' dans lequel de nouvelles suspensions peuvent avoir été créées, et
des suspensions déjà présentes peuvent avoir été évaluées.
-------------------
⟦Σ⟧λx.t ⟹ ⟦Σ⟧λx.t
⟦Σ⟧t ⟹ ⟦Σ'⟧λx.w ⟦Σ',x←u⟧w ⟹ ⟦Σ''⟧v
-----------------------------------------
⟦Σ⟧t u ⟹ ⟦Σ''⟧v
⟦Σ₁⟧u ⟹ ⟦Σ₁'⟧v
-------------------------------------
⟦Σ₁, x←u, Σ₂⟧x ⟹ ⟦Σ₁', x←v, Σ₂⟧v
Cette version historique est subtilement fausse, on en reparlera bientôt.
*)