Le Lambda Calcul en moins de 5 (?) minutes... (QUICK DRAFT)
Introduction
Le lambda calcul est un langage de programmation fonctionnel Turing-complet. Il sert à comprendre certains fondements de la programmation.Syntaxe
Il existe plusieurs syntaxes pour ce langage. En voici une...Variable
Une variable est un mot composé de lettres. En général on limite les lettres de l'alphabet (a à z). Certaines syntaxes proposent que les noms de variables tiennent sur un seul caractère.Abstraction
\ et . permettent de définir une abstraction. Équivalents Objective Caml : mots-clef fun et -> (c'est un choix arbitraire ! Si la touche λ (il y a marqué la lettre grecque lambda, je précise pour ceux qui ne peuvent pas afficher les lettres grecques) était disponible sur le clavier de tout le monde, on utiliserait cette lettre à la place de \ ou de ,\ etc.)
exemple : \x.x
Application
( et ) Les parenthèses permettent de définir l'application. Équivalents Objective Caml : c'est la même chose. Sauf qu'en Objective Caml les parenthèses ne sont pas toujours obligatoires.exemple : (a b)
Remarque
Rappelons que cette syntaxe est une syntaxe parmi d'autres. Ensuite, notons qu'il est utile d'autoriser les parenthèses autour des définitions d'abstractions. Notons également qu'il est prudent d'imposer les parenthèses autour des applications. (tout ça dans le but de simplifier l'analyse syntaxique)
Limiter les variables à un seul caractère permet d'écrire \xzy.(x y z)
Exemples
| Lambda-Calcul | Objective Caml |
|---|---|
| \x.x | fun x -> x |
| (a b) | (a b) |
| ((\x.x) 42) | (fun x -> x) 42 |
| (\x.x 42) Attention, cette notation peut souvent signifier autre chose avec une autre syntaxe | (fun x -> x) 42 |
| (\x y z. x z y) (\x.x) (\x.(x 42)) (\y z.(y z)) | (fun x y z -> x y z) (fun x -> x) (fun x -> x 42) (fun y z -> y z) |
Structures de données
Le lambda-calcul permet de représenter des données avec des fonctions ! (il le faut bien, puisqu'il est Turing-complet)Booléens
Voici un codage possible des booléens, parmi d'autres !
| Valeur représentée | Codage |
|---|---|
| TRUE | \x y.x |
| FALSE | \x y.y |
| IFTHENELSE | \x y z.(x y z) |
| IFTHENELSE COND A B | (\x y z.(x y z)) COND A B |
Choix de codage
Le codage des booléens proposé ci-dessus est arbitraire. En BASH, le code de retour 0 signifie que l'application a bien terminé. Ce qui correspond à TRUE. En C, 0 est équivalent à FALSE, et tous les autres entiers sont équivalents à TRUE. En Lambda-Calcul, vous avez le choix puisque c'est un langage un peu "vide"... en revanche il vous permet de coder n'importe quelle donnée (mais à vous de définir la représentation et les opérations associées à ces données)Alpha conversion
Deux lambda-termes sont alpha-équivalents signifie qu'ils calculent exactement la même chose.
Par exemple :\x.x et \y.y calculent exactement la même chose.
\a.(a b) et \a.(a c) ne calculent pas forcément exactement la même chose. Il faut prouver que b et c sont pareils pour pouvoir dire que les deux termes sont alpha-équivalents
Beta réduction
La beta-reduction, c'est pour réduire (attention parfois ça agrandi...) les lambda-termes. S'il existe une beta-réduction qui permet de passer d'un terme A à un terme B, alors A et B calculent la même chose.
Par exemple :((\x.x) a) se beta-réduit en a
Aller plus loin
Pour aller plus loin, il existe de nombreuses sources plus complètes et plus techniques sur le sujet ;-)- Lambda calcul pur (M2 UPMC) :
- Lambda calcul simplement typé (M2 UPMC) :
- Le cours de Conception de langages (M2 UPMC) :
- Cours de lambda calcul par Jean Goubault-Larrecq :
- Théorie des types, par Gilles Dowek : (contient le lambda-pi calcul et le lambda-1 calcul)