Utilisateur:David.Monniaux/lambda-calcul
Un article de Wikipédia, l'encyclopédie libre.
Le lambda-calcul ou λ-calcul est une théorie mathématique du calcul, modélisant les notions d'abstraction de fonction et d'application de fonction à un paramètre.
Son nom provient de l'utilisation de la lettre λ comme symbole dénotant l'abstraction fonctionnelle, dans la présentation la plus courante du λ-calcul.
Le λ-calcul, pur ou typé, est la base théorique des langages de programmation dits fonctionnels.
Sommaire |
[modifier] λ-calcul pur
[modifier] Syntaxe
Le λ-calcul opère sur des termes, c'est-à-dire des objets définis par une certaine syntaxe. On se donne préalablement un ensemble V de noms de variables (cet ensemble, en fait, importe peu, comme on le verra par la suite).
Un terme du λ-calcul pur est :
- soit un nom de variable v dans V ;
- soit une λ-abstraction λv.t où v est un nom de variable et t est un terme
- soit une application (t u) où t et u sont des termes.
Il n'y a aucune contrainte supplémentaire de bonne formation.
Les variables libres d'un λ-terme sont les variables v utilisées dans le terme sans être à l'intérieur d'une abstraction λv. Formellement parlant, l'ensemble VL(t) des variables libres est défini par induction sur la structure syntaxique des termes :
- VL(v) = {v}
- VL(v.t) = VL(t) \ {v}
- VL(t u) = VL(t) ∪ VL(u)
Un terme sans variables libres est dit terme clos, et parfois combinateur. À l'opposé, les variables v situées à l'intérieur d'une abstraction λv sont dites variables liées.
Le nom attribué aux variables liées a peu d'importance, de même qu'en mathématiques la fonction dénotée par x↦x+1 et la fonction dénotée par y↦y+1 sont identiques. On formalise cela par la notion d'α-conversion : deux termes sont dits α-équivalents si l'on obtient l'un par renommage « sans capture » de l'autre. Par exemple, λa.a et λb.b sont α-équivalents ; par contre, λa.(λb.(a b)) et λa.(λa.(a a)) ne sont pas équivalents, car il y a eu capture.
On raisonnera uniquement sur des classes d'équivalence des λ-termes par α-équivalence. Quand la définition de certaines opérations risquerait de provoquer des captures, on se placera dans une situation α-équivalente où la capture ne se produit pas. En raison de tous ces problèmes de capture et de nommage, on pourra vouloir se passer des noms de variables ; il existe une présentation des termes clos du λ-calcul à l'aide d'indices de de Bruijn qui évite toute utilisation de noms de variables.
[modifier] β-réduction
Une expression de la forme ((λt.u) v) est, intuitivement, l'application d'un paramètre à une fonction. On nomme ce type d'expression β-rédex. La β-réduction va constituer en l'élimination des β-rédex. Pour la définir, nous aurons d'abord besoin de la notion de substitution, notée t[u/v], d'une variable v par un terme u à l'intérieur d'un terme t. On la définit par induction sur la structure de t :
- v[u/v] ≝ u
- w[u/v] ≝ w si w est une variable différente de v
- (λv.t)[u/v] ≝ λv.t
- (λw.t)[u/v] ≝ λv.(t[u/v]) si w est une variable différente de v
- (t1 t2)[u/v] ≝ (t1[u/v] t2[u/v])
[modifier] Références
- H.P. Barendregt, The Lambda-Calculus: its syntax and semantics (λ-calcul pur)
- J.Y. Girard, Proofs and Types (Système F)
Catégorie:Informatique théorique Catégorie:Programmation informatique
