Tutte le nostre biblioteche: classicistranieri.com - classicistranieri.org - classicistranieri.eu - classicistranieri.it - classicistranieri..net - controversi.org

DOWNLOAD THIS WEB SITE!

Utilisateur:David.Monniaux/lambda-calcul - Wikipédia

Utilisateur:David.Monniaux/lambda-calcul

Un article de Wikipédia, l'encyclopédie libre.

Vous avez de nouveaux messages (diff ?).

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.tv 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)