Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church dans les années 1930. Ce système fonde les concepts de fonction et d'application qui forment un cadre pour manipuler des expressions appelées λ-expressions. La lettre grecque λ est utilisée pour lier une variable. Par exemple, si est une λ-expression, alors représente la fonction qui à x associe .
Le λ-calcul a été le premier formalisme pour définir et caractériser les fonctions récursives. Il revêt donc une grande importance dans la théorie de la calculabilité, au même titre que les machines de Turing et le modèle de Herbrand-Gödel. Dit autrement, le lambda-calcul est Turing-complet. Depuis, il a été appliqué comme langage de programmation théorique et comme métalangage pour la démonstration formelle assistée par ordinateur. Le lambda-calcul peut être typé ou non.
Le lambda-calcul est apparenté à la logique combinatoire de Haskell Curry et se généralise dans les calculs de substitutions explicites.
Histoire Le λ-calcul est introduit par Alonzo Church dans les années 1932-1933 dans le cadre d'une théorie logique visant à fonder les mathématiques sur la notion de fonction (mathématiques), plutôt que sur celle d'ensemble, comme c'est le cas pour les théories de Zermelo ou de Zermelo-Fraenkel. Dans ce contexte, une fonction est à comprendre comme un procédé qui permet d'aller de l'argument à la valeur prise pour celui-ci, procédé donné par la définition de la fonction, ce qui est la conception originelle de fonction. Alors que dans une théorie ensembliste, une fonction est donnée par son graphe, l'ensemble des couples associant argument et valeur. Cette théorie s'avère incohérente, comme le montrent, en 1935, Stephen C. Kleene et John Barkley Rosser.
Cependant ce résultat d'incohérence n'affecte pas la partie de la théorie qui ne traite que des fonctions, ce qu'on entend depuis par λ-calcul, et qui s'avère utile pour formaliser et analyser la calculabilité effective. En 1936, Church l'utilise pour définir les fonctions de ℕ dans ℕ λ-définissables, montre que cette notion équivaut à celle de fonction récursive générale introduite par Kurt Gödel à partir d'une idée due à Jacques Herbrand (les fonctions récursives générales sont les fonctions calculables par un système formel d'équations dit de Herbrand-Gödel), et propose que ces deux formalisations équivalentes capturent celle intuitive de calculabilité effective, c'est la thèse de Church,. En 1936, indépendamment Alan Turing propose son propre modèle de calculabilité, les Machines de Turing, et montre en 1937 l'équivalence avec la λ-définissabilité ce qui renforce la thèse de ChurchDans leurs articles de 1936, Church et Turing utilisent chacun leur caractérisation pour montrer l'indécidabilité du problème de la décision (Entscheidungsproblem) en logique du premier ordre, il n'existe pas de procédé effectif, qui permet de déterminer si un énoncé de la logique du premier ordre est ou non démontrable, répondant ainsi à la négative une question posée en 1928 par David Hilbert et Wilhelm Ackermann ()..
Origine du λ Alonzo Church connaissait la relation entre son calcul et celui des Principia Mathematica de Russell et Whitehead. Or ceux-ci utilisent la notation pour noter l'abstraction, mais Church utilisa à la place la notation qui devint par la suite .. Peano a lui aussi défini l'abstraction dans son Formulaire de mathématiques., il utilise notamment la notation, pour noter la fonction telle que page 58..
Présentation informelle
En lambda-calcul, tout est fonction L'idée de base du lambda-calcul est que tout est fonction, comme en théorie des ensembles, tout est ensemble. Une fonction est exprimée par une λ-expression qui peut contenir des variables représentant des fonctions qui ne sont pas encore définies.
Application Il existe une opération fondamentale dans le lambda-calcul, appelée application. L'application consiste à appliquer une fonction à un argument , c'est-à-dire à évaluer la fonction avec comme argument l'expression . On note l'application à . Si l'expression (qui décrit une fonction) est appliquée à l'expression (qui décrit également une fonction), cela se note , et correspond à l'évaluation de la fonction avec comme argument l'expression .
Comment « fabriquer » des fonctions ? On peut aussi fabriquer des fonctions en disant que si est une expressionqui peut éventuellement contenir la variable ., on crée la fonction qui à fait correspondre l'expression . On écrit cette nouvelle fonctionce que les mathématiciens auraient écrit ..
Le nom de la variable n'est pas plus important qu'il ne l'est dans une expression comme qui est équivalente à . Autrement dit si est l'expression dans laquelle toutes les occurrences de ont été renommées en , on considérera que les expressions et sont équivalentes.
En utilisant les outils dont on vient de se doter, on obtient, par applications et abstractions, des fonctions assez compliquées que l'on peut vouloir simplifier ou évaluer. Simplifier une application de la forme (λx.E) P revient à la transformer en une variante de l'expression E dans laquelle toute occurrence libre de x est remplacée par P. Cette forme de simplification s'appelle une contraction (ou une β-contraction si l'on veut rappeler que l'on applique la règle β du lambda-calcul).
Quelques fonctions Sur cette base, on peut construire quelques fonctions intéressantes, comme la fonction identité , qui est la fonction qui à fait correspondre , autrement dit la fonction . On peut aussi construire la fonction constante égale à , à savoir .
De là on peut construire la fonction qui fabrique les fonctions constantes, pourvu qu'on lui donne la constante comme paramètre, autrement dit la fonction , c'est-à-dire la fonction qui à fait correspondre la fonction constamment égale à .
On peut aussi par exemple construire une fonction qui permute l'utilisation des paramètres d'une autre fonction, plus précisément si est une expression, on voudrait que fonctionne comme . La fonction est la fonction . Si on applique la fonction à on obtient que l'on peut simplifier en .
Jusqu'à maintenant nous avons été assez informelsEn particulier, nous avons édulcoré le problème du remplacement d'une variable par un terme qui pose des problèmes délicats.. L'idée du lambda-calcul consiste à fournir un langage précis pour décrire les fonctions et les simplifier.
Syntaxe Le lambda calcul définit des entités syntaxiques que l'on appelle des lambda-termes (ou parfois aussi des lambda expressions) et qui se rangent en trois catégories : les variables : sont des lambda-termes ; les applications : est un lambda-terme si et sont des lambda-termes ; les abstractions : est un lambda-terme si est une variable et un lambda-terme.
L’application peut être vue ainsi : si est une fonction et si est son argument, alors est le résultat de l'application à de la fonction .
L’abstraction peut être interprétée comme la formalisation de la fonction qui, à , associe , où contient en général des occurrences de .
Ainsi, la fonctionCette explication semble introduire des constantes entières et des opérations, comme et , mais il n'en est rien, car ces concepts peuvent être décrits par des lambda termes spécifiques dont ils ne sont que des abréviations. qui prend en paramètre le lambda-terme et lui ajoute 2 (c'est-à-dire en notation mathématique courante la fonction ) sera dénotée en lambda-calcul par l'expression . L'application de cette fonction au nombre 3 s'écrit et s'« évalue » (ou se normalise) en l'expression .
Notations, conventions et concepts Parenthésage Pour délimiter les applications, on utilise des parenthèses, mais par souci de clarté, on omet certaines parenthèses. Par exemple, on écrit x1 x2 ... xn pour ((x1 x2) ... xn).
Il y a en fait deux conventions : Association à gauche, l'expression ((M0 M1) (M2M3)) s'écrit M0 M1 (M2M3). Quand une application s'applique à une autre application, on ne met de parenthèse que sur l'application de droite. Formellement, la grammaire du lambda calcul parenthésé est alors :
Parenthésage du terme de tête, l'expression ((M0 M1) (M2M3)) s'écrit (M0)M1 (M2)M3. Un terme entre parenthèses est le premier d'une suite d'applications. Ainsi les arguments d'un terme sont facilement identifiables. Formellement, la grammaire du lambda-calcul parenthésé est alors :
Curryfication Shönfinkel et Curry ont introduit la curryfication : c'est un procédé pour représenter une fonction à plusieurs arguments. Par exemple, la fonction qui au couple (x, y) associe u est considérée comme une fonction qui, à x, associe une fonction qui, à y, associe u. Elle est donc notée : λx.(λy.u). Cela s'écrit aussi λx.λy.u ou λxλy.u ou tout simplement λxy.u. Par exemple, la fonction qui, au couple (x, y) associe x+y sera notée λx.λy.x+y ou plus simplement λxy.x+y.
Variables libres et variables liées Dans les expressions mathématiques en général et dans le lambda calcul en particulier, il y a deux catégories de variables : les variables libres et les variables liées (ou muettes). En lambda-calcul, une variable est liéeEn mathématiques, les variables sont liées par ∀ ou par ∃ ou par ∫ ... dx. par un λ. Une variable liée a une portéeLa portée est la partie de l'expression où la variable a la même signification. et cette portée est locale. De plus, on peut renommer une variable liée sans changer la signification globale de l'expression entière où elle figure. Une variable qui n'est pas liée est dite libre.
Variables liées en mathématiques Par exemple dans l'expression , la variable est libre, mais la variable est liée (par le ). Cette expression est « la même » que car était un nom local, tout comme l'est . Par contre ne correspond pas à la même expression car le est libre.
Tout comme l'intégrale lie la variable d'intégration, le lie la variable qui le suit.
Exemples: Dans , la variable est liée et la variable est libre. Ce terme est α-équivalent au terme .
est α-équivalent à .
est α-équivalent à .
Définition formelle des variables libres en lambda-calcul
On définit l'ensemble VL(t) des variables libres d'un terme t par récurrence : si x est une variable alors VL(x) = {x} si u et v sont des lambda-termes alors VL(u v) = VL(u) ∪ VL(v) si x est une variable et u un lambda-terme alors VL(λx.u) = VL(u) {x}
Terme clos et terme ouvert Un terme qui ne contient aucune variable libre est dit clos (ou fermé). On dit aussi que ce lambda-terme est un combinateur (d'après le concept apparenté de logique combinatoire).
Un terme qui n'est pas clos est dit ouvert.
Substitution et α-conversion
L'outil le plus important pour le lambda-calcul est la substitution qui permet de remplacer, dans un terme, une variable par un terme. Ce mécanisme est à la base de la réduction qui est le mécanisme fondamental de l'évaluation des expressions, donc du « calcul » des lambda-termes.
La substitution dans un lambda terme t d'une variable x par un terme u est notée t[x := u]. Il faut prendre quelques précautions pour définir correctement la substitution afin d'éviter le phénomène de capture de variable qui pourrait, si l'on n'y prend pas garde, rendre liée une variable qui était libre avant que la substitution n'ait lieu.
Par exemple, si u contient la variable libre y et si x apparaît dans t comme occurrence d'un sous terme de la forme λy.v, le phénomène de capture pourrait apparaître. L'opération t[x := u] s'appelle la substitution dans t de x par u et se définit par récurrence sur t :
si t est une variable alors t[x := u]=u si x=t et t sinon si t = v w alors t[x := u] = v[x := u]w[x := u] si t = λy.v alors t[x := u] = λy.(v[x := u]) si x ≠ y et t sinon Remarque : dans le dernier cas on fera attention à ce que y ne soit pas une variable libre de u. En effet, elle serait alors « capturée » par le lambda externe. Si c'est le cas, on renomme y et toutes ses occurrences dans v par une variable z qui n'apparaît ni dans t ni dans u.