Introduction

Mais qu'est-ce donc, le $\lambda$-calcul ?

Le $\lambda$-calcul est un langage de programmation théorique, à la base de tous les langages de programmation fonctionnels que vous pouvez connaître. Je pense notamment à Lisp, Scheme, OCaml, Haskell... et bien d'autres ! Les concepts du $\lambda$-calcul sont même appliqués à la plupart des langages orientés objet ou impératifs que nous connaissons tous. Aujourd'hui, les $\lambda$-expressions sont implémentées (plus ou moins bien, j'en conviens) en C++, en Java; en Javascript, et même avec Python. Surtout, n'allez pas dire que ces langages sont fonctionnels, certains puristes vous feraient pendre pour de tels propos.

Petit point histoire, le $\lambda$-calcul a été inventé par Alonzo Church, mathématicien et logicien américain a qui l'on doit (presque) tout en matière d'informatique aujourd'hui. Cette invention remonte environ à 1930, donc bien avant que nous commencions à faire mumuse avec les premiers ordinateurs.

Nous allons tenter ensemble de vulgariser les concepts de base du $\lambda$-calcul, afin d'avoir au moins une petite idée de son utilité et de son importance dans toutes les avancées en matière de programmation. Qui dit vulgarisation dit simplification, et même approximation. Si un logicien puriste passe par là, merci d'en tenir compte avant de me lyncher. Par ailleurs, n'hésitez à me contacter si vous souhaitez discuter d'un point particulier ou me faire part d'une erreur rédhibitoire de ma part.

Syntaxe des $\lambda$-termes

Avant de définir de manière rigoureuse ce qu'est un $\lambda$-terme, observons directement à quoi ressemble une expression simple :

Hein, mais qu'elle est cette diablerie ?

Oui, le symbole $x$, tout seul, est une expression valide dans le $\lambda$-calcul. On peut voir cela comme une expression atomique, une sorte de boîte noire. Laissons cette expression de côté et passons à la suivante :

Décortiquons ensemble cette expression :

• Le symbole $\lambda$ signifie que nous définissons une fonction. Afin de faire l'analogie avec ce qui est connu, c'est l'équivalent du mot-clé function en JavaScript.

• Le $x$ entre le symbole $\lambda$ et le "." est le nom du paramètre de notre fonction.

• Certains aiment voir ce "." comme la flèche -> ou => de la notation de fonction fléchée avec OCaml ou Javascript. On peut voir aussi le "." comme le mot-clé return dans une fonction.

• Ce qu'il y a après le ".", ici un autre symbole $x$, c'est le résultat de notre fonction, ce qu'elle nous renvoie.

Ainsi, si nous utilisons le JavaScript afin de "traduire" cette $\lambda$-expression, on obtient :

Avec la notation fléchée, très pratique pour représenter les $\lambda$-termes

1(x) => x;

Avec la notation classique :

1function(x) {
2    return x
3}

Étant donné la forte proximité de la syntaxe des fonctions fléchées en JavaScript avec celle du $\lambda$-calcul, on utilisera celle-ci à partir de maintenant, lorsqu'on essaiera de traduire une $\lambda$-expression en code.

Donc, très simplement, on s'aperçoit que la $\lambda$-expression $\lambda x.x$ représente la fonction identité, qui, à un paramètre $x$, associe $x$, lui-même. Plutôt simple, non ?

Bien, passons à une autre expression :

Ici, le terme $x$ suivi du terme $y$ intuite une application de fonction. Plus exactement, c'est l'application d'une fonction $x$, avec $y$ passé en paramètre. Pour y voir un peu plus clair, on écrirait en JavaScript :

1x(y);

Maintenant, afin de mélanger un peu toutes les $\lambda$-expressions précédentes, essayons de déduire le sens de celle-ci (sans regarder la réponse plus bas bien entendu 😉) :

Si nous traduisons cette expression en code, de manière analogue à précédemment, on obtient :

1(x) => (y) => x(y);

En français, on dirait :

"Une fonction qui prend en paramètre un argument x et qui renvoie une fonction qui prend en paramètre un argument y et qui renvoie x appliqué à y".

Pensez à réciter ce que sont les $\lambda$-expressions en langage naturel, c'est un moyen de comprendre rapidement une expression.

Maintenant, je pense que vous êtes fin prêts à gober la définition (inductive) exacte de l'ensemble des $\lambda$-termes qui est :

C'est tout. Ces trois règles de construction, à elles seules, définissent toutes les $\lambda$-expressions qu'il est possible d'écrire dans le $\lambda$-calcul, tel qu'il a été initialement défini.

Allez, une petite dernière pour la route, plus compliquée cette fois, manière de voir si on a attrapé le truc :

Alors, tout d'abord, nous pouvons nous demander : "Est-ce une expression valide dans le $\lambda$-calcul " ? Voyons-si la syntaxe est valide :

Tout d'abord, si on pose :

Alors, on a notre règle 3 définie plus haut qui est respectée pour l'instant ☑️. Maintenant, la sous-expression $M =(\lambda x . \lambda y . x y)$ est-elle valide ?

Si on pose :

Alors, on a $M = \lambda y . O$, et on reconnait une cette fois notre règle 2 ☑️. Au passage, on reconnait une expression déjà vue plus haut. Il reste à vérifier que la sous- expression $O$ est aussi valide. Si nous posons :

Alors on reconnait une application de fonction avec la règle 3, et, de même, on constate que $P$ et $Q$ sont également des expressions valides à l'aide de la règle 1 ☑️.

Bon, on en a fini avec $M$. Voyons maintenant si $N = (\lambda x . x) \; z$ est une expression valide :

On commence à avoir l'habitude, si on pose :

En utilisant la règle 3 on reconnait encore une application de fonction ☑️. Au passage, on s'aperçoit rapidement que la sous-expression $S$ vérifie la règle 1 ☑️. Il ne nous reste plus qu'à vérifier si $R = \lambda x . x$ est une expression valide, ce qui est le cas, car nous reconnaissons la fonction identité vue auparavant, la règle 2 est satisfaite, et toute notre expression est donc valide ☑️. s Ouf! 😅 . Rassurez-vous, inutile de décortiquer chaque expression de la sorte. Ici, nous le faisons une fois pour être sûr de la compréhension des règles, mais ça vient assez rapidement de constater, en un coup d'œil, s'il y a un problème de syntaxe dans une $\lambda$-expression.

Maintenant, la traduction en Javascript :

1((x) => (y) => x(y))((x) => x)(y);

Oui, je vous assure que ce code javascript est complètement valide ! Même si peu lisible, c'est vrai.

Au passage, on remarque que les règles de construction du $\lambda$-calcul font que nos fonctions ne peuvent prendre qu'un seul argument et sont contraintes de renvoyer une valeur. Nous verrons dans le prochain chapitre que, par la curryfication, ça n'est pas du tout un problème. Pour ceux d'entre vous qui êtes déjà familiers avec les concepts de programmation fonctionnelle, ce comportement est une base des langages fonctionnels dits purs.

C'est tout pour ce premier chapitre !

"Mais attends, on n'a rien calculé du tout là ?" . En effet, le concept du $\lambda$-calcul demandant un certain niveau d'abstraction, je préfère prendre le temps et donc, ce premier article est consacré à l'apprentissage de la syntaxe seule du $\lambda$-calcul, et de l'intuition qu'il y a derrière en matière de sémantique.

Cependant, peut-être avez-vous remarqué que la dernière expression que nous avons vue est "calculable", alors vous pouvez toujours essayer de la réduire, si vous avez une intuition de la manière de faire ! N'hésitez pas à me contacter si vous souhaitez discuter du résultat.

Le prochain chapitre sera consacré au calcul des $\lambda$-expressions, processus que l'on appelle une $\beta-reduction$ dans le jargon.

À bientôt !