Planche 1
Cours 1
Langages fonctionnels
Jean-Jacques.Levy@inria.fr
http://jeanjacqueslevy.net
secrétariat de l'enseignement:
Catherine Bensoussan
cb@lix.polytechnique.fr
Aile 00, LIX
tel: 34 67
http://w3.edu.polytechnique.fr/informatique/
Planche 2
Plan du cours
- quatre paradigmes de langages de programmation
- fonctionnel (ML, Haskell)
- impératif (Pascal, C, Java, et un peu ML)
- logique (Prolog)
- orienté-objet (Java, Ocaml)
- Principes généraux des langages de programmation
- Sémantique (opérationnelle, plutôt que dénotationnelle)
- Vérification de programmes
(en 8 leçons!)
On supposera connue la notion de syntaxe abstraite
Planche 3
Références
-
The Lambda Calculus, Its Syntax and Semantics, H. Barendregt,
North-Holland, 1981.
- Theories of Programming Languages, J. Reynolds, Cambridge
University Press, 1998.
- Foundations for Programming Languages, J. Mitchell, MIT Press, 1996.
- Essentials of Programming Languages, D. Friedman, M. Wand,
C.Haynes, McGraw-Hill, 1992
- Semantics of Programming Languages, C. Gunter, MIT Press, 1992.
Conférences
-
ACM Conference on Principles of Programming Languages (POPL)
- IEEE Conference on Logic in Computer Science (LICS)
Planche 4
Plan
-
Lambda-calcul non typé
- Variables libres -- liées
- Substitution de variables libres
- Réductions
- Confluence
- Stratégies de réduction
- Evaluateurs formels
Planche 5
Programmation fonctionnelle
- Simple, concis et esthétique
- Notation mathématique
- Fonctions = citoyens de 1ère classe
- Fonctions + structures de données = langage puissant
- Transparence référentielle (indépendance du contexte)
- Parallélisation
Planche 6
La lambda notation --- Church [30]
Supposons que l'on dispose d'une fonction integrale telle que
integrale(a,b,f) vaut òab f(x) dx
Soit f la fonction x |® x2 + 1. On veut calculer ò01
f(x) dx.
Avec la lambda notation, on peut écrire
f º l x. x × x + 1
et calculer integrale(0,1,f)
ou plus simplement écrire
integrale(0,1, l x. x × x + 1)
Planche 7
La lambda notation -- bis
Considérons g(y) = (x+y) × (x-y) et f(x) = ò0x g(y) dy
Essayons de calculer ò01 f(x) dx = ò01 ò0x (x+y)
× (x-y) dx dy
On écrira
integrale (0,1, l x. integrale (0, x, l y. (x+y) × (x-y)))
Remarque
On a utilisé
-
notation anonyme pour les fonctions
- fonction argument d'une autre fonction
- fonction résultat d'une autre fonction
Planche 8
La lambda notation et les langages de programmation
C'est le coeur de la notation pour des langages comme Lisp, Scheme,
ML ou Haskell.
En Lisp/Scheme:
(defun integrale (a b f) ... )
(integrale 0 1 (lambda (x) (integrale 0 x (lambda (y) (+ x y)))))
En ML:
let integrale a b f = ... ;;
(integrale 0 1 (function x -> (integrale 0 x (function y -> x+y)))) ;;
Beaucoup de la problématique de la l-notation se retrouve dans
tous les langages de programmation.
Planche 9
Variables liées -- Variables libres
Le nom des variables liées n'a pas d'importance.
l x. x × x + 1 est la même fonction que l x'. x' × x' + 1
De même pour
l y. (x+y) × (x-y)) et l y'. (x+y') × (x-y'))
Mais pas identique à
l x. (x+x) × (x-x)) !!
On dit que x (resp. y) est libre (resp. lié) dans l y. (x+y)
× (x-y))
On peut donc renommer une variable liée à condition de ne pas capturer
de variable libre [une variable liée est souvent appelée variable
muette en math.]
Planche 10
Renommage des paramètres d'une fonction
Les paramètres dans les fonctions de Pascal, Java, ML, etc. sont aussi
des variables liées. On peut leur donner un nom arbitraire
let g y = (x + y) * (x - y) ;;
est identique à
let g' y' = (x + y') * (x - y') ;;
mais n'est pas équivalent à
let h x = (x + x) * (x - x) ;;
Idem en Java pour le nom du paramètre y dans
static int g (int y) { return (x + y) * (x - y); }
Planche 11
PCF -- petit langage fonctionnel [Plotkin 74]
Termes
| M, N, P |
::= |
x |
|
variable |
| |
| |
l x.M |
|
abstraction |
| |
| |
MN |
|
application |
| |
| |
|
|
constante entière |
| |
| |
M Ä N |
|
Ä Î {+,-,×,÷ } |
| |
| |
ifz M then N then N' |
|
conditionnelle |
| |
| |
µ x.M |
|
définition récursive |
Exemples
l x. x× x + 1
l x.l y. (x+y) × (x-y)
l f.l x. f(f x)
(l f.l x. f(f x)) (l x. x+1)
(µ f.l x. ifz x then 1 else x × f(x-1)) 5
Planche 12
Syntaxe abstraite de PCF
type nom = string;;
type term =
Lambda of nom * term
| Application of term * term
| Variable of nom
| Entier of int
| Ifz of term * term * term
| Plus of term * term
| Times of term * term
| Div of term * term
| Minus of term * term
| Mu of nom * term ;;
Cf. http://logical.inria.fr/~dowek/Cours/lp1.html
Planche 13
Convention
On a tendance à supprimer les parenthèses à gauche des
applications. Donc M1 M2 ··· Mn désignera
(···(M1 M2) ··· Mn).
Variables libres
| FV(x) = {x} |
|
FV(l x.M)=FV(µ x.M)= FV(M) - {x} |
|
|
|
FV (MN) = FV(M Ä N) = FV(M) È FV(N) |
| FV(ifz M then N else N') = FV(M) È FV(N) È FV(N') |
Variables liées
| BV(x) = Ø |
|
BV(l x.M)=BV(µ x.M)= BV(M) È {x} |
|
|
|
BV (MN) = BV(M Ä N) = BV(M) È BV(N) |
| BV(ifz M then N else N') = BV(M) È BV(N) È BV(N') |
Planche 14
Substitution
| x [x \ P] = P |
| y [x \ P] = y |
| (l x.M) [x \ P] = l x.M |
| (l y.M) [x \ P] = l y'.M[y \ y'][x \ P] |
(y'¹ x et y'ÏFV(P) È FV(M)) |
| (M M') [x \ P] = M [x \ P] M'[x \ P] |
|
|
| (M Ä M') [x \ P] = M [x \ P] Ä M'[x \ P] |
| (ifz M else N else N') [x \ P] =
ifz M[x \ P] then N[x \ P] else N'[x \ P] |
| (µ x.M) [x \ P] = µ x.M |
| (µ y.M) [x \ P] = µ y'.M[y \ y'][x \ P] |
(y' ¹ x et y'ÏFV(P) È FV(M)) |
Exemples
(x+y) [y \ x] = x + x
(l x. x+y) [y \ x] = l x'. x'+x
(ifz y then x+y else z) [y \ x] =
ifz x then x+x else z
(µ x. x+y) [y \ x] = µ x'. x'+x
Planche 15
Règles de réductions
| a |
l x. M º l x'. M[x \ x'] |
(x' ÏFV(M)) |
| b |
(l x.M) N ® M [x \ N] |
| op |
|
(m Ä n ³ 0) |
| cond1 |
|
| cond2 |
|
| µ |
µ x.M ® M [x \ µ x. M] |
Remarques
-
la règle a est une relation d'équivalence, et non une
réduction. L'égalité des termes est souvent considérée à
a-équivalence près.
- la règle b représente l'application d'un argument à une
fonction
Planche 16
Exemples de réductions
(l x.l y.x+y) 2 3 ® (l y.2+y)3 ® 2 + 3 ® 5
(l f.l x. f (f x))(l x.x+1) 3 ® (l x.(l x.x+1)((l x.x+1)x)) 3 ®
(l x.x+1)((l x.x+1) 3) ® (l x.x+1)(3+1) ® (l x.x+1)4 ® 4+1
® 5
|
(µ f.l x. ifz x then 1 else x × f(x-1)) 3 ® |
|
(l x. ifz x then 1 else x × (µ f.l x. ifz x then 1 else x × f(x-1))(x-1)) 3 ® |
|
ifz 3 then 1 else 3 × (µ f.l x. ifz x then 1 else x × f(x-1))(3-1)® |
|
3 × (µ f.l x. ifz x then 1 else x × f(x-1))(3-1)® |
|
3 × (µ f.l x. ifz x then 1 else x × f(x-1))2® ··· |
|
3 × 2 × 1 × ifz 0 then 1 else 0 × (µ
f.l x. ifz x then 1 else x × f(x-1))(0-1)® |
|
3 × 2 × 1 × 1 ® ··· 6 |
Planche 17
Stratégies de réduction
Plusieurs sous-termes réductibles (redex = reductible
expressions) peuvent se trouver dans un même terme.
Théorème [Church-Rosser] Si M ®* N et M ®*
N', il existe toujours un P tel que N ®* P et N' ®*
P.
On dit aussi que le système de réduction est confluent.
La démonstration est compliquée.
Ce théorème assure l'unicité du résultat (forme normale) d'un calcul.
Planche 18
Appel par nom
L'ordre d'évaluation peut influer sur la terminaison. Par exemple
(l x. 1)(µ x. x) ® (l x. 1) (µ x. x) ® ···
mais pourtant
(l x. 1)(µ x. x) ® 1
Théorème [Curry] Si M a une forme normale, la
réduction normale (qui réduit toujours le redex le plus externe et le
plus à gauche) atteint cette forme normale.
La démonstration est aussi compliquée.
Réduction normale = appel par nom dans langages de programmation
Planche 19
Appel par valeur
Valeurs
| V,V' |
::= |
x |
|
variable |
| |
| |
l x.M |
|
abstraction |
| |
| |
|
|
constante entière |
La stratégie de réduction par appel par valeur consiste à:
-
pour une application: à trouver la valeur de l'argument de gauche
d'une application, puis celle de l'argument de droite, puis à
appliquer la règle b
- pour un opérateur arithmétique: à trouver la valeur des
arguments avant de calculer la valeur finale
- pour une conditionnelle: à trouver la valeur du prédicat puis à
appliquer la bonne règle Cond1 ou Cond2.
Planche 20
Sémantique opérationnelle bigstep de l'appel par valeur
On peut définir rigoureusement l'appel par valeur pour PCF avec des
règles d'inférence.
| |- l x.M = l x.M |
| |- M[x \ µ x.M] = V |
|
|
|- µ x.M = V |
|
| |- M = l x.P
|- N = V'
|- P [x \ V'] = V |
|
|
|- MN = V |
|
|
|
| |- M = m
|- N = n
m Ä n ³ 0 |
|
|
|- M Ä N = mÄ n |
|
| |- M = 0
|- M = V |
|
|
|- ifz M then N then N' = V |
|
| |- M = n+1
|- N = V' |
|
|
|- ifz M then N then N' = V' |
|
Planche 21
Sémantique opérationnelle bigstep de l'appel par nom
En changeant légèrement la sémantique, on obtient l'appel par nom
| |- l x.M = l x.M |
| |- M[x \ µ x.M] = V |
|
|
|- µ x.M = V |
|
| |- M = l x.P
|- P [x \ N] = V |
|
|
|- MN = V |
|
|
|
| |- M = m
|- N = n
m Ä n ³ 0 |
|
|
|- M Ä N = mÄ n |
|
| |- M = 0
|- M = V |
|
|
|- ifz M then N then N' = V |
|
| |- M = n+1
|- N = V' |
|
|
|- ifz M then N then N' = V' |
|
Remarquons qu'alors on peut aussi faire plus fort en évaluant les
opérateurs arithmétiques par nom avec des règles comme 0 × M
® 0, etc.
Planche 22
Le lambda calcul pur [Church 30]
Termes
| M, N, P |
::= |
x |
|
variable |
| |
| |
l x.M |
|
abstraction |
| |
| |
MN |
|
application |
Découverte de Church: suffisant pour calculer toutes les fonctions
calculables Þ thèse de Church sur le modèle unique de la
calculabilité.
Exemples
(l x. xx)(l x.x y) ® (l x. xy)(l x.x y) ® (l x. xy)y ® yy
(l x.xx) (l x.xx) ® (l x.xx) (l x.xx) ® ···
(l x.xxx) (l x.xxx) ® (l x.xxx) (l x.xxx)(l x.xxx) ® ···
µ x. M = (l y. (l x.M)(y y))(l y. (l x.M)(y y)) ®* M[x \ µ x.M]
Y = l f. (l y. f(yy))(l y. f(yy)) et µ x. M » Y(l x.M)
Planche 23
Arithmétique -- entiers de Church
| vrai = l x.l y. x |
| faux = l x.l y. y |
| á M,N ñ = l z.zMN |
| (M)0 = Mvrai |
| (M)1 = Mfaux |
|
|
|
|
| zero = l x.xvrai |
| ifz P then M else N = (zero P) M N |
| µ x. M = (l y. (l x.M)(y y))(l y. (l x.M)(y y)) |
Church avait un calcul plus compliqué avec les entiers de
Church n = l f.l x. fn(x). Certaines fonctions (par
exemple le prédécesseur) sont plus longues à coder.
Programmer avec les entiers de Church est stupide. Nous ne les
mentionnons que pour leur application à l'expressibilité du lambda
calcul pur.
Planche 24
Encore plus fort
On peut montrer que les lambda termes K = l x.l y.x et S = l x.l y.l z.xz(yz)
sont suffisants pour exprimer toutes les lambda expressions (logique
combinatoire de [Curry]).
Mieux on peut tout exprimer à partir de la seule expression
X = l x.xKSK [Bohm].
Par exemple
K = (XX)X
S = X(XX)
I = l x.x = SKK = X(XX) ((XX)X)((XX)X)
On peut donc ne vivre qu'avec des X.
Exercice 1 Dans le lambda calcul pur, donner une
expression de l x.x+1, l x.x-1, l x.l y.x+y, l x.l y.x × y. Et
avec les entiers de Church?
Planche 25
Evaluateur de PCF
Deux techniques possibles
- évaluer le programme source avec les techniques développées
auparavant
- en appel par nom ou par valeur
- faire la différence sur quelques exemples
Les langages comme Haskell font de l'appel par nom (en ne recalculant
pas deux fois la valeur d'un argument de fonction).
[appel par nécessité]
Les langages comme ML, Pascal, C, ou Java font de l'appel par valeur.
Planche 26
En TD
-
on donnera un analyseur syntaxique pour PCF
- écrire un évaluateur symbolique de PCF
- donner une définition rigoureuse smallstep de l'appel par
nom et de l'appel par valeur.
La prochaine fois
-
interpréteurs (avec environnements)
- types dans les lambda termes
- polymorphisme
- unification et inférence de type
This document was translated from LATEX by HEVEA.