Hina

L'informatique et les mathématiques appliqués à la logique et au langage.

Page principale A propos du blog Me contacter

Découverte du lambda-calcul

Sommaire

Introduction
Base syntaxique
Abstraction & application
Base sémantique
Réduction
Conclusion
Références

Introduction

Les lambda-calculi sont une famille de systèmes formels, basés sur un modèle - le lambda-calcul - élaboré par le mathématicien Alonzo Church dans les années 1930, dans le cadre de ses travaux concernant les fondements des mathématiques.

Ici, on s'intéresse essentiellement à la version la plus simple de cette famille, c'est-à-dire celle qui en est à l'origine : le lambda-calcul (qui peut être écrit $\lambda$-calcul).

Dans cet article, je propose de découvrir les fondements du lambda-calcul sous l'angle des systèmes formels, en m'intéressant particulièrement à la réécriture comme manière de donner un sens aux phrases du langage.

Base syntaxique

Le lambda-calcul est un système formel. Grossièrement, c'est donc un langage qui permet de calculer. Pour un tel système, il est nécessaire de savoir distinguer deux aspects qui se complètent, le premier étant la syntaxe : il s'agit de la façon d'organiser les mots et les phrases du langage.

Le terme "calculer" ne fait pas précisément référence aux processus de calcul en arithmétique, par exemple, mais à un processus de transformation d'une information en une autre grâce à des règles de calcul.

En $\lambda$-calcul, la syntaxe est simple. Il existe trois sortes d'objets syntaxiques :

Les variables, qui désignent de simples valeurs nommées
Les abstractions, qui permettent de définir des fonctions : des objets qui associent un calcul à un paramètre.
Les applications, qui permettent d'exploiter les calculs donnés par les abstractions.

Ces trois objets peuvent être appelés $\lambda$-termes. À eux seuls, ils permettent d'écrire n'importe quelle phrase du lambda-calcul. On peut aussi les définir en précisant la façon de les organiser grâce à une grammaire : \begin{align} \label{eq:a} \langle \lambda \text{-term} \rangle \quad ::= & \quad \langle \text{variable} \rangle \\ | & \quad (\lambda \langle \text{variable} \rangle . \langle \lambda \text{-term} \rangle) \\ | & \quad (\langle \lambda \text{-term} \rangle \langle \lambda \text{-term} \rangle) \\ \langle \text{variable} \rangle \quad ::= & \quad x \quad | \quad y \quad | \quad z... \end{align} Comme explicité ci-dessus, un $\lambda$-terme peut avoir l'une des trois formes données, et aucune autre. Cette définition structurelle permet de raisonner sur les phrases du lambda-calcul de manière simple, en distinguant les différentes formes possibles des termes de la phrase. Plus précisément, il n'est pas rare de raisonner par induction structurelle sur chaque terme d'une phrase.

Abstraction et application

Les notions d'application et d'abstraction sont définies dans le système de Church comme des $\lambda$-termes décrits respectivement par les deuxième et troisièmes lignes de la notation BNF dans le premier paragraphe.

Une abstraction permet de définir une fonction. On peut par exemple définir la fonction qui à $x$ et $y$ associe la valeur $x + y$ de la manière suivante : \begin{equation} \lambda x.(\lambda y.x + y) \end{equation}
Une application permet d'appliquer une fonction à un argument donné. par exemple, pour sommer 1 et 2, on peut écrire : \begin{equation} ((\lambda x.(\lambda y.x + y)) \; 2) \; 1 \end{equation}
Par "appliquer une fonction à un argument donné", on sous-entend qu'il existe une méthode qui permet "d'appliquer". Ceci n'est pas évident, et il se trouve que cette méthode est décrite par la sémantique introduite dans le paragraphe précédent et expliquée dans le paragraphe suivant.

Il est essentiel de comprendre que ces deux expressions ne sont que des phrases écrites dans un langage donné, rien de plus. Par analogie, un programme écrit en python n'est rien d'autre qu'une suite de phrases et l'appel à une fonction quelconque se fait lors de l'interprétation et non lors de l'écriture. Cela fait partie de cette distinction importante que l'on doit faire entre la syntaxe et la sémantique.

Base sémantique

Le second aspect du système formel qu'il est important d'étudier est la sémantique, qui complète la syntaxe en permettant de donner une signification à chaque phrase du langage. Autrement-dit, là ou la syntaxe sert de support de l'information, la sémantique permet de manipuler l'information.

Philosophiquement, l'objectif est d'être capable d'exprimer une idée, un concept (l'abstrait) grâce à la richesse syntaxique d'un langage, et de pouvoir rendre le/la rendre exploitable par une machine, qui ne manipule que des briques élémentaires (le concret).

L'une des sémantiques du $\lambda$-calcul est construite à partir de règles de transformation syntaxique très simples. En appliquant ces règles à une phrase, on en déduit une nouvelle phrase, plus petite, ou non, mais qui conserve l'information initialement stockée (il faut s'intéresser à la notion d'ordre dans le langage étudié pour pouvoir considérer qu'une phrase est plus petite qu'une autre). En appliquant ces règles un certain nombre de fois, on se trouve face à une phrase qui ne peut plus être réduite et qui est équivalente à la phrase initiale.

Les règles en question sont l'$\alpha$-conversion et la $\beta$-réduction.

On remarquera qu'en réalité, ces règles ne permettent pas toujours de réduire la taille des phrases transformées.

De manière informelle, les règles de réduction données permettent de simuler l'exécution d'une suite de calculs écrits en $\lambda$-calcul. Cette interprétation lie clairement le système formel aux langages de programmation fonctionnels. On pourrait imaginer que pour définir la sémantique d'un tel langage, il serait alors nécessaire de créer des règles de réduction sur sa syntaxe.

Réduction

Comme expliqué précédemment, les techniques de réductions permettent de construire une sémantique calculatoire pour le $\lambda$-calcul. La $\alpha$-conversion et l'$\beta$-réduction sont respectivement définies de la manière suivante :

L'$\alpha$-conversion consiste simplement à renommer les variables nommées dans les abstractions. Par exemple, la phrase \begin{align} (\lambda x. xx) (\lambda x. x) \end{align} après une $\alpha$-réduction devient \begin{align} (\lambda x. xx) (\lambda y. y) \end{align} Cette règle permet de démontrer des résultats sur le lambda-calcul sans devoir se soucier des conflits de nommage des variables utilisées. L'$\alpha$-conversion donne une solution efficace au problème de capture de variables.

En particulier, la démonstration de résultats sur des phrases du système se fait généralement à $\alpha$-conversion près : au lieu de considérer une phrase en particulier, on considère toutes les phrase qui lui sont égales après une certaine $\alpha$-conversion.

La $\beta$-réduction permet grossièrement d'exécuter une application, en transformant les applications en expressions dans lesquelles l'argument a été substitué. Par exemple, la phrase \begin{align} ((\lambda x. (\lambda y. x + y)) \; 1) \; 2 \end{align} après une $\beta$-réduction devient \begin{align} (\lambda y. 2 + y) \; 1 \end{align} En fait, à un niveau d'imbrication donné d'une phrase, on transforme l'écriture sous forme d'application en une écriture sous forme d'un $\lambda$-terme dans lequel toutes les occurences de l'argument dans l'abstraction sont remplacées par le $\lambda$-terme en argument : \begin{equation} (\lambda x. M) (A) \; \Longrightarrow \; M[x := A] \end{equation}

Conclusion

Dans les sciences informatiques, le système formel sert de modèle théorique aux langages de programmation fonctionnels. Plus précisément, il s'agirait de construire un modèle théorique d'un langage de programmation fonctionnel concret en se servant du $\lambda$-calcul. Cette idée nous amène intuitivement à penser qu'il est nécessaire que le $\lambda$-calcul ait la même forme logique que le langage qui nous serions amenés à étudier. Après la construction d'une telle correspondance de ces formes, on peut alors étudier le langage concret au travers de l'étude du lambda-calcul (en pratique amélioré), d'une certaine manière.

Les travaux d'Alonzo Church, d'Alan Turing et d'autres mathématiciens ont permis d'établir une thèse particulièrement puissante, puisqu'elle fait le lien entre un système formel aussi simple que le lambda-calcul avec une notion abstraite difficilement abordable et au centre de nombreux problèmes des sciences informatiques. En effet, la thèse de Church permet d'affirmer que tout ce qui est calculable peut être calculé en lambda-calcul. L'intuition de la calculabilité est totalement couverte par les possibilités données par le ce modèle de calcul. Autrement dit, chaque algorithme qui existe, chaque suite d'instructions précises peu être représentée dans ce langage. Il suffit d'une grammaire simpliste et de deux règles de transformation pour pouvoir représenter n'importe quel calcul possible.

Finalement, la simplicité du lambda-calcul, ainsi que la possibilité de calculer tout ce qui est calculable avec, font de ce système formel un véritable pilier des langages de programmation.

Références

Je me suis majoritairement inspiré du livre An introduction to Lambda Calculi for Computer Scientists de Chris Hankin et du Lecture Notes on the Lambda Calculus de Peter Sellinger pour écrire cet article.