Lambda-calcul : de la définition à la logique booléenne

Deuxième partie de notre dossier consacré au lambda-calcul ! Après nous avoir présenté l’histoire du Lambda-calcul, Anatolli nous propose cette fois d’en découvrir la définition et les méthodes pour construire des programmes simples équivalents à la machine de Turing.

Dans l’article « Histoire du λ-calcul », nous avons discuté des événements historiques qui ont amené les mathématiciens à la création de la théorie de la calculabilité. Le lambda-calcul en est une part essentielle. Cependant, nous n’avons pas encore défini ce que signifie le symbole « λ », ou même le mot « calcul ».

Cette fois, avec cet article, nous souhaitons donner au lecteur le goût du λ-calcul. On présente une définition plutôt complète, puis on montre comment construire un langage de programmation élémentaire mais aussi puissant que la machine de Turing. Ce langage est connu comme le paradigme fonctionnel.

Impérative vs fonctionnelle

Quand on me parle d' »ordinateur », je pense à la machine de Turing. Réciproquement, si on me parle de « machine de Turing », j’imagine tout de suit un PC. C’est assez normal puisque la machine de Turing est un concept de langage de programmation (ou d’ordinateur) parmi les plus élémentaires, tellement élémentaire que la notion « ordinateur » et « langage de programmation » n’y sont pas discernables. La machine de Turing est faite d’un ruban contenant des instructions, des données et finalement d’un automate qui lit, efface, réécrit et déplace les données. Tout cela se traduit facilement en un programme impératif — un paradigme implémenté par plus de 9000 langages populaires. Dans ce paradigme, le processus du calcul est décrit en termes d’instructions qui modifient l’état du « calculateur ». Peu importe le langage, les programmes impératifs ont les mêmes caractéristiques :

• L’état se change par des instructions d’affectation v = E
• Les instructions sont exécutées consécutivement C1; C2; C3
• Il existe un mécanisme de branchement if, switch
• Il existe un mécanisme de boucle while, for

Remarque : Théoriquement, il est suffisant d’avoir une instruction de saut inconditionnel (goto). N’importe quelle boucle est équivalente à une combinaison de if et de goto. Mais, comme l’utilisation de goto est considérée comme une grosse bêtise de développeur, et afin de ne pas enflammer la guerre sainte, restons sur un mécanisme de boucle.

Exemple : calcul impératif d’une factorielle

res = 1;
for i = 1..n:
res = res * i;


On voit clairement que ce programme est impératif car il est composé d’instructions consécutives qui permettent la transition du calculateur de l’état initial à son état final. Une partie de l’état final (variable res) est interprétée comme le résultat du calcul.

Ce programme est très simple, mais seriez-vous capable de proposer une machine de Turing qui calcule une factorielle ? Si vous ne l’avez jamais fait à la main — amusez-vous, c’est un bon exercice de gymnastique mentale.

NB : Si vous préférez lire ou regarder comment les autres réalisent ce type de perversions mathématiques, on ne vous jugera pas…

En tout cas, l’objectif de cet article se trouve en dehors du paradigme impératif — on s’intéresse au paradigme fonctionnel qui présente un programme comme une fonction au lieu d’une liste d’instructions consécutives à exécuter. L’avantage de cette approche est que les effets de bord sont complètement interdits. Par exemple, la factorielle est une fonction qui dépend de l’entrée n et le paradigme garantit que si on appelle deux fois factorielle avec le même n, on obtient le même résultat.
De plus, dans un programme fonctionnel :

• Il n’existe pas de notion d’état ni de variable
• Pas de variable — pas d’opération d’affectation
• Pas de boucle car il n’y a pas de différence entre les itérations
• L’exécution du programme est une suite de réductions (ou calculs) de son expression jusqu’à l’expression triviale qui ne contient que le résultat
• L’ordre de calcul n’est pas important car les expressions sont indépendantes

En revanche, le paradigme fonctionnel nous donne :

• La récursion à la place des boucles.
• Les fonctions d’ordre supérieur, c’est-à-dire les fonctions qui prennent en entrée et renvoient d’autres fonctions.
• Le filtrage par motif.

Bien sûr, il est possible de répliquer que l’ensemble de ces propriétés sont présentes dans la plupart des langages modernes. En réalité, les langages modernes sont multi-paradigmes — ils prennent le meilleur de toutes les conceptions. En revanche, le langage machine restent un langage purement impératif. De plus, en programmation fonctionnelle, toutes les fonctions sont pures, elles ne dépendent que de leurs paramètres d’entrée.

Dans la suite, nous allons définir un autre langage primitif — le λ-calcul qui induit la programmation fonctionnelle de la même façon que la machine de Turing induit la programmation impérative. Notre objectif est de réécrire en fonctionnel (et de comprendre !) un programme de calcul de la factorielle d’un nombre entier. Pour cela, nous passerons par toutes les étapes nécessaires :

• La grammaire du langage (application et abstraction)
• Les règles d’exécution (-equivalence et -réduction)
• Le codage des booléens et des nombres (nombres de Church)
• La récursion à la place de boucles

Dernière avertissement avant de plonger dans le monde des formules ! La construction complète est technique et longue, donc nous allons sauter certains détails sans pitié. Notre objectif est de donner une idée sur la façon dont les primitives de la programmation impérative peuvent être exprimées en termes de -calcul. Dans tous les cas, n’utilisez pas cet article comme la seule source si vous avez un examen sur le -calcul. Au moins, vous êtes avertis !

• Si vous avez un examen dans une semaine, prenez n’importe quel livre tiré de la bibliographie en fin d’article
• Si vous avez un examen demain et que vous ne comprenez rien, lisez au moins ça : Alligator Eggs!

 

Que signifie λ ?

Définition

Un λ-terme ou λ-expression est une expression qui satisfait la grammaire suivante :

où est l’ensemble des chaînes sur l’alphabet fixe .

La première règle définie des identifiants — variables et fonctions. La deuxième est l’application d’un terme à un autre. La troisième définie une abstraction. Cette grammaire vous semble claire ? Alors vous pouvez passer directement à la β-réduction. Sinon, essayons de rajouter du sens à cet abracadabra.

Quelques explications supplémentaires

1. Identifiant. Initialement, est considéré comme identifiant toute chaîne qui ne contient aucun des trois caractères spéciaux : , et (espace). Ainsi, , , , et sont des identifiants.

2. Application. La notion signifie qu’un terme est appliqué au terme . Du point de vue du codeur, on peut dire qu’un algorithme est appliqué à l’entrée . Mais, comme nous construisons un système formel, nous pouvons aller plus loin, par exemple : une auto-application est aussi un λ-terme correct.

3. Abstraction. Soit un λ-terme qui contient à l’intérieur (on écrit ). Dans ce cas, la notion signifie une fonction qui mappe à .

Remarque importante ! Le ou est un pseudonyme pour un λ-terme. Dans la suite de l’article, certains termes seront souvent remplacés par leurs « pseudonymes » pour simplifier les expressions. Ces pseudonymes seront surlignés en gras.

Autre moyen d’aborder l’abstraction — c’est un constructeur de fonction anonyme. Imaginons une fonction . Dans la notation du λ-calcul, correspond à . L’avantage d’une telle écriture est de mettre clairement en avant le fait que la fonction dépend de mais il n’y a pas d’ambiguïté entre la fonction et sa valeur en . Finalement, pour une valeur , on écrit :

Cela est une application : s’applique à . Par la suite, sera omis et simplement écrit . Ainsi, une λ-abstraction est un moyen de créer une fonction anonyme en partant d’une expression .

Les trois règles ci-dessus sont les seules opérations autorisées pour construire les expressions en λ-calcul. Il est important de répéter que l’univers du λ-calcul ne « sait » rien faire d’autre que construire des phrases intégrant ces trois règles : ni nombre, ni opération arithmétique — rien.

Par exemple, l’identifiant seul n’a pas le sens d’une « somme ». Il s’agit juste d’une chaîne de caractères, un objet atomique de la théorie. En ce sens, on ne peut pas « calculer » le « résultat » de l’abstraction — ce n’est qu’une construction formelle.

β-réduction

Définition. La β-équivalence est définie de manière suivante :

 

Une fois de plus, si cette définition vous semble claire, vous pouvez avancer jusqu’à la partie Variables libres et liées.
Sinon, voici une traduction de la langue Klingon.
Soit, dans la formule ci-dessus,

Dans ce cas, il est possible de « calculer » l’application en remplaçant toutes les occurrences de dans par et en enlevant λ :

 

Remarque : Ne considérez pas comme la fonction qui prend en entrée deux paramètres et . C’est une formule formelle et , ainsi que sont trois λ-termes qui ont les mêmes « droits ».

Mais que signifie « calculer » pour un λ-terme ? On dit que les termes et sont β-équivalents (pour cela on utilise un symbole « « ). L’opération qui vise à supprimer λ en remplaçant un terme par son β-équivalent, s’appelle une β-réduction. En ce sens, « calculer » signifie appliquer les β-réductions pour rendre un λ-terme initial le plus simple possible.

Remarquons aussi que nous avons besoin de parenthèses car nous ne savons pas jusqu’à quel terme s’applique l’abstraction. Pour minimiser le nombre de parenthèses par la suite, nous fixerons les règles suivantes sur les priorités entre les opérations :

• L’application est gauche-associative, c.-à-d.
• L’abstraction est droite-associative, c.-à-d.
• L’abstraction s’applique à tout ce qu’elle arrive à « toucher », c.-à-d.

α-équivalence : variables libres et liées

Considérons un terme qui contient un identifiant . Dans le terme , la variable est liée par une λ-abstraction. Si une variable n’est pas liée, on dit qu’elle est libre. Pour une définition totalement correcte, il manque quelques détails (essayez de la construire par vous-même) mais la notion est assez simple et intuitive.

Exemple : Dans le terme ci-dessous, les variables et sont liées, et sont libres :

Maintenant, considerons deux termes et . Si on applique chacun des deux termes à un terme quelconque , on obtient le même résultat :

Cela signifie que les deux termes — qui diffèrent uniquement par leurs variables liées — fonctionnent de la même façon. On dit que ces termes sont α-équivalents :

On suppose que les termes -équivalents sont égaux. C’est la deuxième et derniere règle du λ-calcul.

Un peu de sens

Сette section vise à établir des liens entre la définition formelle du λ-calcul et les lambda-fonctions qu’on peut trouver dans la plupart des langages de programmation.
Ce qu’il faut retenir : ces deux notions sont très différentes ! Les intuitions issues de l’une des deux notions sont souvent des obstacles à la compréhension de la deuxième notion.

Pour ne pas confondre, on utilise le symbole λ uniquement pour le λ-calcul de Church.

En programmation, il est souvent nécessaire de passer en paramètre une fonction : clé pour un tri, opération à appliquer à l’ensemble des éléments d’une collection, etc. Dans ce cas, si la fonction est simple et/ou n’est pas réutilisée, aucun nom ne lui est attribué et on utilise un lambda. En d’autres termes, les deux phrases sont synonymes et la version avec une lambda-fonction est bien plus courte :

• Soit la fonction . Considérons

Dans la théorie du λ-calcul, notre intérêt est différent. On « oublie » qu’une fonction est une règle qui mappe à . À la place, on considère une fonction uniquement comme une formule formelle — une phrase construite en respectant une certaine grammaire (celle que nous venons de décrire ci-dessous). Une formule formelle ne doit pas forcement être calculable, par exemple :

• est une formule formelle correcte. On peut la calculer et obtenir 6.
• est également une formule formelle correcte. Si, dans la grammaire de cette formule, correspondent à respectivement et correspond à une somme, on peut la calculer et obtenir également 6.
• est aussi une formule formelle correcte. Évidemment, elle ne peut pas être calculée dans le sens commun. Cependant si on change les règles du « jeu », on peut obtenir -1/12…
• est une formule incorrecte dans la grammaire du λ-calcul. Cette formule ne peut jamais être construite, la définition d’un λ-terme interdit implicitement deux symboles λ de suite.

Tous les λ-termes sont aussi des formules formelles : si, pendant le calcul, on tombe sur une forme , ou , et sont des identifiants simples (c.-à-d. des chaînes de caractères qui ne contiennent ni « λ », ni « . », ni espace), il ne faut pas essayer de leur donner du sens : ils ne sont ni des variables, ni des fonctions, ils n’ont pas d’arité non plus — ce sont juste les briques à partir desquelles on construit une expression.

Que peut-il se passer, si on essaie d’interpréter ces briques ?

Soit . Clairement, c’est une fonction d’identité car elle mappe à . Dans le λ-calcul, on peut l’appliquer à n’importe quel terme, y compris lui-même :

Autrement dit, nous avons prouvé que . Toutefois, cela n’a aucun sens car, en mathématiques, une fonction ne peut pas être incluse dans son propre domaine de définition ! En conclusion, l’application de λ-termes reste une opération formelle. Il est même dangereux de l’interpréter comme l’application d’une fonction classique à son argument, malgré l’aspect séduisant de cette approche. La différence, toutefois, est qu’une formule formelle ne se traduit pas obligatoirement en règle bien précise.

Prise en main : booléens et branchement

Dans le λ-calcul non typé, il n’existe qu’une seule primitive : les fonctions. Pour l’utiliser comme modèle de programmation, à nous de créer tous les objets, même les plus élémentaires tels que les nombres ou les constantes booléennes.

Commençons par les dernières. Les λ-termes et ci-dessous jouent respectivement les rôles de « vrai » et de « faux ».

• — est une fonction qui renvoie son premier argument
• — est une fonction qui renvoie son deuxième argument

Pour l’instant, ces termes ne sont que des formules formelles qui manquent de contexte. Notre contexte sera le terme de branchement :

Ici, est une condition de branchement, est une branche « then » et correspond à « else ». Donc, pour justifier que et correspondent aux constantes logiques, nous avons besoin de démontrer deux égalités :

Faisons le. Pour notre premier calcul en λ, n’oublions pas que ce calcul est une serie d’applications de règles décrites ci-dessus (-équivalence et -réduction) jusqu’à l’obtention d’un terme le plus simple possible sur lequel il est impossible d’appliquer l’une de ces deux règles.

Preuve. Calculons l’expression . Dans la série de réductions ci-dessous, nous soulignons la partie de l’expression à laquelle on applique la règle de calcul.








Q.E.D. (ou C.Q.F.D.)

Un lecteur curieux peut vérifier par lui-même que .
De plus, un vrai passionné peut essayer de trouver les bonnes expressions pour la conjonction (), la disjonction () ainsi que la négation ().

Spoiler :

 

Avec ces opérations supplémentaires, il est possible de prouver des formules plus longues (ne le faites pas chez vous — le calcul risque d’être bien plus long).

To be continued…

Dans la suite, nous allons construire une arithmétique basée uniquement sur les règles du λ-calcul. Et, cerise sur le gâteau, nous programmerons le calcul d’une factorielle en utilisant uniquement un langage de λ, comme c’était promis au début de l’article !

Réferences

• Henk Barendregt: The impact of the lambda calculus in logic and computer science. Bulletin of Symbolic Logic 3(2): 181-215 (1997)
• Henk Barendregt: Lambda Calculus. Its Syntaxin and Semantics. Studies in logic and the foundations of Mathematics, Rijksuniversiteit Utrecht, The Netherlands (1981)
• Felice Cardone, Hindley 1. Roger: History of Lambda calculus and Combinatory Logic. (2006)
• Peter Selinger: Lecture Notes on the Lambda Calculus
• Notes de cours de l’université russe IFMO