Calcul lambda - Lambda calculus

Le calcul lambda (également écrit sous le nom de λ-calcul ) est un système formel en logique mathématique pour exprimer le calcul basé sur l' abstraction de fonction et l' application utilisant la liaison et la substitution de variables . C'est un modèle de calcul universel qui peut être utilisé pour simuler n'importe quelle machine de Turing . Il a été introduit par le mathématicien Alonzo Church dans les années 1930 dans le cadre de ses recherches sur les fondements des mathématiques .

Le calcul lambda consiste à construire des termes lambda et à effectuer des opérations de réduction sur eux. Dans la forme la plus simple du calcul lambda, les termes sont construits en utilisant uniquement les règles suivantes :

produisant des expressions telles que : (λ x .λ y .(λ z .(λ x . zx ) (λ y . zy )) ( xy )). Les parenthèses peuvent être supprimées si l'expression n'est pas ambiguë. Pour certaines applications, des termes pour les constantes et opérations logiques et mathématiques peuvent être inclus.

Les opérations de réduction comprennent :

Si l' indexation De Bruijn est utilisée, la α-conversion n'est plus nécessaire car il n'y aura pas de collisions de noms. Si l' application répétée des étapes de réduction finit par se terminer, alors par le théorème de Church-Rosser, il produira une forme β-normale .

Les noms de variables ne sont pas nécessaires si vous utilisez une fonction lambda universelle, telle que Iota et Jot , qui peut créer n'importe quel comportement de fonction en l'appelant sur elle-même dans diverses combinaisons.

Explication et applications

Le calcul lambda est complet de Turing , c'est-à-dire qu'il s'agit d'un modèle de calcul universel qui peut être utilisé pour simuler n'importe quelle machine de Turing . Son homonyme, la lettre grecque lambda (λ), est utilisée dans les expressions lambda et les termes lambda pour désigner la liaison d' une variable dans une fonction .

Le calcul lambda peut être non typé ou typé . Dans le calcul lambda typé, les fonctions ne peuvent être appliquées que si elles sont capables d'accepter le "type" de données de l'entrée donnée. Les calculs lambda typés sont plus faibles que le calcul lambda non typé, qui est le sujet principal de cet article, dans le sens où les calculs lambda typés peuvent exprimer moins que les calculs non typés, mais en revanche les calculs lambda typés permettent de prouver plus de choses ; dans le calcul lambda simplement typé, c'est, par exemple, un théorème selon lequel chaque stratégie d'évaluation se termine pour chaque terme lambda simplement typé, alors que l'évaluation des termes lambda non typés n'a pas besoin de se terminer. L'une des raisons pour lesquelles il existe de nombreux calculs lambda typés différents est le désir d'en faire plus (de ce que le calcul non typé peut faire) sans abandonner la possibilité de prouver des théorèmes solides sur le calcul.

Le calcul lambda a des applications dans de nombreux domaines différents des mathématiques , de la philosophie , de la linguistique et de l' informatique . Le lambda calcul a joué un rôle important dans le développement de la théorie des langages de programmation . Les langages de programmation fonctionnels implémentent le calcul lambda. Le lambda calcul est également un sujet de recherche actuel en théorie des catégories .

Histoire

Le calcul lambda a été introduit par le mathématicien Alonzo Church dans les années 1930 dans le cadre d'une enquête sur les fondements des mathématiques . Le système original s'est avéré logiquement incohérent en 1935 lorsque Stephen Kleene et JB Rosser ont développé le paradoxe de Kleene-Rosser .

Par la suite, en 1936, Church n'a isolé et publié que la partie relative au calcul, ce qu'on appelle maintenant le calcul lambda non typé. En 1940, il a également introduit un système de calcul plus faible, mais logiquement cohérent, connu sous le nom de calcul lambda simplement typé .

Jusqu'aux années 1960 où sa relation avec les langages de programmation a été clarifiée, le lambda calcul n'était qu'un formalisme. Grâce aux applications de Richard Montague et d'autres linguistes dans la sémantique du langage naturel, le calcul lambda a commencé à jouir d'une place respectable à la fois en linguistique et en informatique.

Origine du symbole lambda

Il existe une certaine incertitude quant à la raison de l'utilisation par Church de la lettre grecque lambda (λ) comme notation pour l'abstraction de fonction dans le calcul lambda, peut-être en partie en raison d'explications contradictoires de Church lui-même. Selon Cardone et Hindley (2006) :

Au fait, pourquoi Church a-t-elle choisi la notation « λ » ? Dans [une lettre non publiée de 1964 à Harald Dickson], il déclara clairement que cela provenait de la notation " " utilisée pour l'abstraction de classe par Whitehead et Russell , en modifiant d'abord " " en " ∧ " pour distinguer l'abstraction de fonction de l'abstraction de classe, puis remplacez « ∧ » par « λ » pour faciliter l'impression. ${\displaystyle {\hat {x}}}$${\displaystyle {\hat {x}}}$${\style d'affichage x}$

Cette origine a également été rapportée dans [Rosser, 1984, p.338]. D'un autre côté, dans ses dernières années, Church a dit à deux enquêteurs que le choix était plus accidentel : un symbole était nécessaire et λ venait d'être choisi.

Dana Scott a également abordé cette question dans diverses conférences publiques. Scott raconte qu'il a posé une fois une question sur l'origine du symbole lambda au gendre de Church, John Addison, qui a ensuite écrit une carte postale à son beau-père :

Cher professeur Church,

Russell avait l' opérateur iota , Hilbert avait l' opérateur epsilon . Pourquoi avoir choisi lambda pour votre opérateur ?

Selon Scott, toute la réponse de Church a consisté à renvoyer la carte postale avec l'annotation suivante : « eeny, meeny, miny, moe ».

Description informelle

Motivation

Les fonctions calculables sont un concept fondamental en informatique et en mathématiques. Le calcul lambda fournit une sémantique simple pour le calcul, permettant d'étudier formellement les propriétés du calcul. Le calcul lambda intègre deux simplifications qui rendent cette sémantique simple. La première simplification est que le lambda calcul traite les fonctions "de manière anonyme", sans leur donner de noms explicites. Par exemple, la fonction

${\displaystyle \operatorname {square\_sum} (x,y)=x^{2}+y^{2}}$

peut être réécrit sous forme anonyme comme

${\displaystyle (x,y)\mapsto x^{2}+y^{2}}$

(qui se lit comme "un tuple de x et y est mappé sur "). De même, la fonction ${\styletexte x^{2}+y^{2}}$

${\displaystyle \operatorname {id} (x)=x}$

peut être réécrit sous forme anonyme comme

${\displaystyle x\mapsto x}$

où l'entrée est simplement mappée sur elle-même.

La deuxième simplification est que le calcul lambda n'utilise que des fonctions d'une seule entrée. Une fonction ordinaire qui nécessite deux entrées, par exemple la fonction, peut être retravaillée en une fonction équivalente qui accepte une seule entrée, et en tant que sortie renvoie une autre fonction, qui à son tour accepte une seule entrée. Par exemple, ${\textstyle \operatorname {square\_sum} }$

${\displaystyle (x,y)\mapsto x^{2}+y^{2}}$

peut être retravaillé en

${\displaystyle x\mapsto (y\mapsto x^{2}+y^{2})}$

Cette méthode, connue sous le nom de currying , transforme une fonction qui prend plusieurs arguments en une chaîne de fonctions chacune avec un seul argument.

Application de fonction de la fonction aux arguments (5, 2), donne immédiatement ${\textstyle \operatorname {square\_sum} }$

${\textstyle ((x,y)\mapsto x^{2}+y^{2})(5,2)}$

${\textstyle =5^{2}+2^{2}}$

${\styletexte =29}$,

alors que l'évaluation de la version curry nécessite une étape de plus

${\textstyle {\Bigl (}{\bigl (}x\mapsto (y\mapsto x^{2}+y^{2}){\bigr )}(5){\Bigr )}(2)}$

${\textstyle =(y\mapsto 5^{2}+y^{2})(2)}$// la définition de a été utilisée dans l'expression interne. C'est comme la β-réduction.${\style d'affichage x}$${\style d'affichage 5}$

${\textstyle =5^{2}+2^{2}}$// la définition de a été utilisée avec . Encore une fois, similaire à la β-réduction.${\style d'affichage y}$${\style d'affichage 2}$

${\styletexte =29}$

pour arriver au même résultat.

Le calcul lambda

Le calcul lambda se compose d'un langage de termes lambda , qui sont définis par une certaine syntaxe formelle, et d'un ensemble de règles de transformation, qui permettent la manipulation des termes lambda. Ces règles de transformation peuvent être considérées comme une théorie équationnelle ou comme une définition opérationnelle .

Comme décrit ci-dessus, toutes les fonctions du lambda calcul sont des fonctions anonymes, sans nom. Ils n'acceptent qu'une seule variable d'entrée, le curry étant utilisé pour implémenter des fonctions à plusieurs variables.

Termes lambda

La syntaxe du calcul lambda définit certaines expressions comme des expressions de calcul lambda valides et d'autres comme invalides, tout comme certaines chaînes de caractères sont des programmes C valides et d'autres non. Une expression de calcul lambda valide est appelée "terme lambda".

Les trois règles suivantes donnent une définition inductive qui peut être appliquée pour construire tous les termes lambda syntaxiquement valides :

• une variable, , est elle-même un terme lambda valide${\style d'affichage x}$
• si est un terme lambda, et est une variable, alors (parfois écrit en ASCII comme ) est un terme lambda (appelé une abstraction ) ;${\style d'affichage t}$${\style d'affichage x}$${\style d'affichage (\lambda xt)}$${\style d'affichage ({\text{L}}xt)}$
• si et sont des termes lambda, alors est un terme lambda (appelé une application ).${\style d'affichage t}$${\style d'affichage s}$${\style d'affichage (ts)}$

Rien d'autre n'est un terme lambda. Ainsi un terme lambda est valide si et seulement si il peut être obtenu par l'application répétée de ces trois règles. Cependant, certaines parenthèses peuvent être omises selon certaines règles. Par exemple, les parenthèses les plus à l'extérieur ne sont généralement pas écrites. Voir Notation ci-dessous.

Une abstraction est une définition d'une fonction anonyme qui est capable de prendre une seule entrée et de la substituer dans l'expression . Il définit ainsi une fonction anonyme qui prend et retourne . Par exemple, est une abstraction pour la fonction utilisant le terme pour . La définition d'une fonction avec une abstraction se contente de "mettre en place" la fonction mais ne l'invoque pas. L'abstraction lie la variable dans le terme . ${\style d'affichage \lambda xt}$${\style d'affichage x}$${\style d'affichage t}$${\style d'affichage x}$${\style d'affichage t}$${\displaystyle \lambda xx^{2}+2}$${\style d'affichage f(x)=x^{2}+2}$${\style d'affichage x^{2}+2}$${\style d'affichage t}$${\style d'affichage x}$${\style d'affichage t}$

Une application représente l'application d'une fonction à une entrée , c'est-à-dire qu'elle représente l'action d'appeler la fonction sur l'entrée pour produire . ${\style d'affichage ts}$${\style d'affichage t}$${\style d'affichage s}$${\style d'affichage t}$${\style d'affichage s}$${\style d'affichage t(s)}$

Il n'y a pas de concept dans le calcul lambda de déclaration de variable. Dans une définition telle que (c'est-à-dire ), le calcul lambda traite comme une variable qui n'est pas encore définie. L'abstraction est syntaxiquement valide et représente une fonction qui ajoute son entrée au encore-inconnu . ${\style d'affichage \lambda x.x+y}$${\style d'affichage f(x)=x+y}$${\style d'affichage y}$${\style d'affichage \lambda x.x+y}$${\style d'affichage y}$

Des crochets peuvent être utilisés et peuvent être nécessaires pour lever l'ambiguïté des termes. Par exemple, et désignent des termes différents (bien qu'ils se réduisent par coïncidence à la même valeur). Ici, le premier exemple définit une fonction dont le terme lambda est le résultat de l'application de x à la fonction enfant, tandis que le deuxième exemple est l'application de la fonction la plus externe à l'entrée x, qui renvoie la fonction enfant. Par conséquent, les deux exemples évaluent la fonction d'identité . ${\displaystyle \lambda x.((\lambda xx)x)}$${\style d'affichage (\lambda x.(\lambda xx))x}$ ${\style d'affichage \lambda xx}$

Fonctions qui opèrent sur des fonctions

Dans le calcul lambda, les fonctions sont considérées comme des « valeurs de première classe », de sorte que les fonctions peuvent être utilisées comme entrées ou renvoyées comme sorties d'autres fonctions.

Par exemple, représente la fonction d'identité , et représente la fonction d'identité appliquée à . De plus, représente la fonction constante , la fonction qui renvoie toujours , quelle que soit l'entrée. Dans le lambda calcul, l'application de la fonction est considérée comme associative à gauche , ce qui signifie . ${\style d'affichage \lambda xx}$${\displaystyle x\mapsto x}$${\style d'affichage (\lambda xx)y}$${\style d'affichage y}$${\style d'affichage (\lambda xy)}$ ${\displaystyle x\mapsto y}$${\style d'affichage y}$${\displaystyle stx}$${\style d'affichage (st)x}$

Il existe plusieurs notions d'« équivalence » et de « réduction » qui permettent de « réduire » les termes lambda en termes lambda « équivalents ».

Équivalence alpha

Une forme d'équivalence de base, définissable en termes lambda, est l'équivalence alpha. Il capture l'intuition que le choix particulier d'une variable liée, dans une abstraction, n'a pas (généralement) d'importance. Par exemple, et sont des termes lambda alpha-équivalents, et ils représentent tous deux la même fonction (la fonction d'identité). Les termes et ne sont pas alpha-équivalents, car ils ne sont pas liés dans une abstraction. Dans de nombreuses présentations, il est habituel d'identifier des termes lambda alpha-équivalents. ${\style d'affichage \lambda xx}$${\displaystyle \lambda yy}$${\style d'affichage x}$${\style d'affichage y}$

Les définitions suivantes sont nécessaires pour pouvoir définir la -réduction :

Variables libres

Les variables libres d'un terme sont les variables non liées par une abstraction. L'ensemble des variables libres d'une expression est défini inductivement :

• Les variables libres de sont juste${\style d'affichage x}$${\style d'affichage x}$
• L'ensemble des variables libres de est l'ensemble des variables libres de , mais avec supprimé${\style d'affichage \lambda xt}$${\style d'affichage t}$${\style d'affichage x}$
• L'ensemble des variables libres de est l'union de l'ensemble des variables libres de et de l'ensemble des variables libres de .${\style d'affichage ts}$${\style d'affichage t}$${\style d'affichage s}$

Par exemple, le terme lambda représentant l'identité n'a pas de variables libres, mais la fonction a une seule variable libre, . ${\style d'affichage \lambda xx}$${\style d'affichage \lambda x.yx}$${\style d'affichage y}$

Substitutions évitant les captures

Supposons que , et sont des termes lambda et et sont des variables. La notation indique la substitution de for in d'une manière évitant la capture . Celui-ci est défini de telle sorte que : ${\style d'affichage t}$${\style d'affichage s}$${\style d'affichage r}$${\style d'affichage x}$${\style d'affichage y}$${\style d'affichage t[x:=r]}$${\style d'affichage r}$${\style d'affichage x}$${\style d'affichage t}$

• ${\style d'affichage x[x:=r]=r}$;
• ${\style d'affichage y[x:=r]=y}$si ;${\style d'affichage x\neq y}$
• ${\style d'affichage (ts)[x:=r]=(t[x:=r])(s[x:=r])}$;
• ${\style d'affichage (\lambda xt)[x:=r]=\lambda xt}$;
• ${\displaystyle (\lambda yt)[x:=r]=\lambda y.(t[x:=r])}$si et n'est pas dans les variables libres de . La variable est dite "fraîche" pour .${\style d'affichage x\neq y}$${\style d'affichage y}$${\style d'affichage r}$${\style d'affichage y}$${\style d'affichage r}$

Par exemple , et . ${\displaystyle (\lambda xx)[y:=y]=\lambda x.(x[y:=y])=\lambda xx}$${\displaystyle ((\lambda xy)x)[x:=y]=((\lambda xy)[x:=y])(x[x:=y])=(\lambda xy)y}$

La condition de fraîcheur (nécessitant que cela ne soit pas dans les variables libres de ) est cruciale pour s'assurer que la substitution ne change pas le sens des fonctions. Par exemple, une substitution est effectuée qui ignore la condition de fraîcheur : . Cette substitution transforme la fonction constante en identité par substitution. ${\style d'affichage y}$${\style d'affichage r}$${\style d'affichage (\lambda xy)[y:=x]=\lambda x.(y[y:=x])=\lambda xx}$${\style d'affichage \lambda xy}$${\style d'affichage \lambda xx}$

En général, le non-respect de la condition de fraîcheur peut être corrigé en renommant alpha avec une variable fraîche appropriée. Par exemple, en revenant à notre notion correcte de substitution, l'abstraction peut être renommée avec une nouvelle variable , pour obtenir , et la signification de la fonction est préservée par substitution. ${\style d'affichage (\lambda xy)[y:=x]}$${\style d'affichage z}$${\displaystyle (\lambda zy)[y:=x]=\lambda z.(y[y:=x])=\lambda zx}$

-réduction

La règle de -réduction stipule qu'une application de la forme se réduit au terme . La notation est utilisée pour indiquer que -réduit à . Par exemple, pour chaque , . Cela démontre que c'est vraiment l'identité. De même, , qui démontre qu'il s'agit d'une fonction constante. ${\style d'affichage (\lambda xt)s}$${\style d'affichage t[x:=s]}$${\displaystyle (\lambda xt)s\to t[x:=s]}$${\style d'affichage (\lambda xt)s}$${\style d'affichage t[x:=s]}$${\style d'affichage s}$${\style d'affichage (\lambda xx)s\to x[x:=s]=s}$${\style d'affichage \lambda xx}$${\displaystyle (\lambda xy)s\to y[x:=s]=y}$${\style d'affichage \lambda xy}$

Le calcul lambda peut être considéré comme une version idéalisée d'un langage de programmation fonctionnel, comme Haskell ou Standard ML . Sous cette vue, la -réduction correspond à une étape de calcul. Cette étape peut être répétée par des réductions β supplémentaires jusqu'à ce qu'il n'y ait plus d'applications à réduire. Dans le calcul lambda non typé, tel que présenté ici, ce processus de réduction peut ne pas se terminer. Par exemple, considérons le terme . Ici . C'est-à-dire que le terme se réduit à lui-même en une seule β-réduction, et donc le processus de réduction ne se terminera jamais. ${\displaystyle \Omega =(\lambda x.xx)(\lambda x.xx)}$${\style d'affichage (\lambda x.xx)(\lambda x.xx)\to (xx)[x:=\lambda x.xx]=(x[x:=\lambda x.xx])(x[x :=\lambda x.xx])=(\lambda x.xx)(\lambda x.xx)}$

Un autre aspect du calcul lambda non typé est qu'il ne fait pas de distinction entre les différents types de données. Par exemple, il peut être souhaitable d'écrire une fonction qui ne fonctionne que sur des nombres. Cependant, dans le calcul lambda non typé, il n'y a aucun moyen d'empêcher une fonction d'être appliquée à des valeurs de vérité , des chaînes ou d'autres objets non numériques.

Définition formelle

Définition

Les expressions lambda sont composées de :

• variables v ₁ , v ₂ , ...;
• les symboles d'abstraction λ (lambda) et . (point);
• parenthèses ().

L'ensemble des expressions lambda, Λ , peut être défini inductivement :

1. Si x est une variable, alors x Λ.
2. Si x est une variable et M Λ, alors (λ x . M ) Λ.
3. Si M , N Λ, alors ( MN ) Λ.

Les instances de la règle 2 sont appelées abstractions et les instances de la règle 3 sont appelées applications .

Notation

Pour ne pas encombrer la notation des expressions lambda, les conventions suivantes sont généralement appliquées :

• Les parenthèses extérieures sont supprimées : M N au lieu de ( M N ).
• Les applications sont supposées être laissées associatives : M N P peut être écrit au lieu de (( M N ) P ).
• Le corps d'une abstraction s'étend le plus à droite possible : λ x . MN signifie λ x .( MN ) et non (λ x . M ) N .
• Une suite d'abstractions est contractée : λ x .λ y .λ z . N est abrégé en λ xyz . N .

Variables libres et liées

L'opérateur d'abstraction, , est censé lier sa variable partout où elle apparaît dans le corps de l'abstraction. Les variables qui entrent dans le cadre d'une abstraction sont dites liées . Dans une expression λ x . M , la partie λ x est souvent appelée liant , pour indiquer que la variable x est liée en ajoutant λ x à M . Toutes les autres variables sont dites libres . Par exemple, dans l'expression y . xxy , y est une variable liée et x est une variable libre. Une variable est également liée par son abstraction la plus proche. Dans l'exemple suivant, l'occurrence unique de x dans l'expression est liée par le deuxième lambda : λ x . y (λ x . zx ).

L'ensemble des variables libres d'une expression lambda, M , est noté FV( M ) et est défini par récursivité sur la structure des termes, comme suit :

1. FV( x ) = { x }, où x est une variable.
2. FV(λ x . M ) = FV( M ) \ { x }.
3. FV( MN ) = FV( M ) FV( N ).

Une expression qui ne contient aucune variable libre est dite fermée . Les expressions lambda fermées sont également appelées combinateurs et sont équivalentes aux termes de la logique combinatoire .

Réduction

La signification des expressions lambda est définie par la façon dont les expressions peuvent être réduites.

Il existe trois types de réduction :

• -conversion : modification des variables liées ;
• -réduction : appliquer des fonctions à leurs arguments ;
• η-réduction : qui capte une notion d'extensionnalité.

On parle aussi des équivalences résultantes : deux expressions sont α-équivalentes , si elles peuvent être α-converties en la même expression. La -équivalence et la -équivalence sont définies de manière similaire.

Le terme redex , abréviation d' expression réductible , fait référence à des sous-termes qui peuvent être réduits par l'une des règles de réduction. Par exemple, (λ x . M ) N est un -redex pour exprimer la substitution de N pour x dans M . L'expression à laquelle se réduit un redex s'appelle son reduct ; le réduit de (λ x . M ) N est M [ x  := N ].

Si x n'est pas libre dans M , λ x . M x est aussi un -redex, avec un réducteur de M .

-conversion

La -conversion, parfois appelée -renommage, permet de changer les noms de variables liées. Par exemple, la α-conversion de λ x . x pourrait donner λ y . oui . Les termes qui ne diffèrent que par la -conversion sont appelés α-équivalent . Fréquemment, dans les utilisations du calcul lambda, les termes α-équivalents sont considérés comme équivalents.

Les règles précises pour la -conversion ne sont pas complètement triviales. Premièrement, lors de la -conversion d'une abstraction, les seules occurrences de variable qui sont renommées sont celles qui sont liées à la même abstraction. Par exemple, une α-conversion de λ x .λ x . x pourrait donner λ y .λ x . x , mais cela ne peut pas donner λ y .λ x . oui . Ce dernier a un sens différent de l'original. Ceci est analogue à la notion de programmation d' ombrage variable .

Deuxièmement, la -conversion n'est pas possible si elle entraîne la capture d'une variable par une abstraction différente. Par exemple, si nous remplaçons x par y dans λ x .λ y . x , on obtient λ y .λ y . y , ce qui n'est pas du tout le même.

Dans les langages de programmation à portée statique, la -conversion peut être utilisée pour simplifier la résolution de noms en s'assurant qu'aucun nom de variable ne masque un nom dans une portée contenante (voir α-renommer pour rendre la résolution de noms triviale ).

Dans la notation de l' indice de De Bruijn , deux termes α-équivalents quelconques sont syntaxiquement identiques.

Substitution

La substitution, notée M [ V  := N ], est le processus consistant à remplacer toutes les occurrences libres de la variable V dans l'expression M par l'expression N . La substitution sur les termes du lambda calcul est définie par récursivité sur la structure des termes, comme suit (remarque : x et y ne sont que des variables tandis que M et N sont une expression lambda quelconque) :

x [ x  := N ] = N

y [ x  : = N ] = y , si x ≠ y

( M ₁ M ₂ )[ x  := N ] = ( M ₁ [ x  := N ]) ( M ₂ [ x  := N ])

(λ x . M )[ x  := N ] = λ x . M

(λ y . M )[ x  := N ] = λ y .( M [ x  := N ]), si x ≠ y et y ∉ FV( N )

Pour substituer en une abstraction, il est parfois nécessaire de -convertir l'expression. Par exemple, il n'est pas correct que (λ x . y )[ y  := x ] donne λ x . x , car le x substitué était censé être libre mais a fini par être lié. La substitution correcte dans ce cas est λ z . x , jusqu'à -équivalence. La substitution est définie uniquement jusqu'à l'équivalence .

-réduction

La -réduction capture l'idée d'application de fonction. La -réduction est définie en termes de substitution : la -réduction de (λ V . M ) N est M [ V  := N ].

Par exemple, en supposant un codage de 2, 7, ×, nous avons la -réduction suivante : (λ n . n × 2) 7 → 7 × 2.

La β-réduction peut être considérée comme identique au concept de réductibilité locale en déduction naturelle , via l' isomorphisme de Curry-Howard .

-réduction

La -réduction exprime l'idée d' extensionnalité , qui dans ce contexte est que deux fonctions sont identiques si et seulement si elles donnent le même résultat pour tous les arguments. La η-réduction convertit entre λ x . f x et f chaque fois que x n'apparaît pas libre dans f .

La η-réduction peut être considérée comme le même que le concept de complétude locale en déduction naturelle , via l' isomorphisme de Curry-Howard .

Formes normales et confluence

Pour le calcul lambda non typé, la -réduction en tant que règle de réécriture n'est ni fortement normalisante ni faiblement normalisante .

Cependant, on peut montrer que la -réduction est confluente jusqu'à la -conversion (c'est-à-dire que nous considérons deux formes normales égales s'il est possible de -convertir l'une dans l'autre).

Par conséquent, les termes fortement normalisants et les termes faiblement normalisants ont une forme normale unique. Pour les termes fortement normalisants, toute stratégie de réduction est garantie de produire la forme normale, alors que pour les termes faiblement normalisants, certaines stratégies de réduction peuvent ne pas la trouver.

Encodage des types de données

Le lambda calcul de base peut être utilisé pour modéliser les booléens, l' arithmétique , les structures de données et la récursivité, comme illustré dans les sous-sections suivantes.

Arithmétique en lambda calcul

Il existe plusieurs manières possibles de définir les nombres naturels dans le calcul lambda, mais les plus courantes sont de loin les nombres d'église , qui peuvent être définis comme suit :

0 := f .λ x . X

1 := f .λ x . f x

2 := f .λ x . f ( f x )

3 := f .λ x . f ( f ( f x ))

etc. Ou en utilisant la syntaxe alternative présentée ci-dessus dans Notation :

0 := fx . X

1 := fx . f x

2 := fx . f ( f x )

3 := fx . f ( f ( f x ))

Un chiffre d'église est une fonction d'ordre supérieur — il prend une fonction à un seul argument f et renvoie une autre fonction à un seul argument. Le chiffre d'Église n est une fonction qui prend une fonction f comme argument et renvoie la n- ième composition de f , c'est-à-dire la fonction f composée avec elle-même n fois. Ceci est noté f ^{( n )} et est en fait la puissance n- ième de f (considéré comme un opérateur) ; f ⁽⁰⁾ est défini comme la fonction d'identité. De telles compositions répétées (d'une seule fonction f ) obéissent aux lois des exposants , c'est pourquoi ces nombres peuvent être utilisés pour l'arithmétique. (Dans le calcul lambda original de Church, le paramètre formel d'une expression lambda devait apparaître au moins une fois dans le corps de la fonction, ce qui rendait la définition ci-dessus de 0 impossible.)

Une façon de penser au chiffre de l'Église n , qui est souvent utile lors de l'analyse de programmes, consiste à utiliser une instruction « répéter n fois ». Par exemple, en utilisant les fonctions PAIR et NIL définies ci-dessous, on peut définir une fonction qui construit une liste (liée) de n éléments tous égaux à x en répétant n fois « ajouter un autre élément x » , à partir d'une liste vide. Le terme lambda est

λ n .λ x . n (PAIRE x ) NUL

En variant ce qui est répété, et en variant l'argument auquel la fonction répétée est appliquée, un grand nombre d'effets différents peuvent être obtenus.

Nous pouvons définir une fonction successeur, qui prend un chiffre d'Église n et renvoie n + 1 en ajoutant une autre application de f , où '(mf)x' signifie que la fonction 'f' est appliquée 'm' fois sur 'x' :

SUCC := n .λ f .λ x . f ( n f x )

Étant donné que la m -ième composition de f composée avec la n -ième composition de f donne la m + n -ième composition de f , l'addition peut être définie comme suit :

PLUS := m .λ n .λ f .λ x . m f ( n f x )

PLUS peut être considéré comme une fonction prenant deux nombres naturels comme arguments et renvoyant un nombre naturel ; on peut vérifier que

PLUS 2 3

et

5

sont des expressions lambda -équivalentes. Étant donné que l'ajout de m à un nombre n peut être accompli en ajoutant 1 m fois, une définition alternative est :

PLUS := m .λ n . m SUCC n 

De même, la multiplication peut être définie comme

MULT := m .λ n .λ f . m ( n f )

Alternativement

MULT := λ m .λ n . m (PLUS n ) 0

puisque multiplier m et n revient à répéter la fonction addition n m fois, puis à l'appliquer à zéro. L'exponentiation a un rendu assez simple en chiffres d'église, à savoir

POU := λ b .λ e . e b

La fonction prédécesseur définie par PRED n = n − 1 pour un entier positif n et PRED 0 = 0 est considérablement plus difficile. La formule

PRED := n .λ f .λ x . n (λ g .λ h . h ( g f )) (λ u . x ) (λ u . u )

peut être validé en montrant inductivement que si T désigne (λ g .λ h . h ( g f )) , alors T ^{( n )} (λ u . x ) = (λ h . h ( f ^{( n −1)} ( x ))) pour n > 0 . Deux autres définitions de PRED sont données ci-dessous, l'une utilisant des conditions et l'autre utilisant des paires . Avec la fonction prédécesseur, la soustraction est simple. Définir

SUB := m .λ n . n PRED m ,

SUB m n donne m − n lorsque m > n et 0 sinon.

Logique et prédicats

Par convention, les deux définitions suivantes (appelées booléennes d'Église) sont utilisées pour les valeurs booléennes VRAI et FAUX :

VRAI := λ x .λ y . X

FAUX := λ x .λ y . oui

(Notez que FAUX est équivalent au chiffre zéro de l'Église défini ci-dessus)

Ensuite, avec ces deux termes lambda, nous pouvons définir quelques opérateurs logiques (ce ne sont que des formulations possibles ; d'autres expressions sont tout aussi correctes) :

ET := p .λ q . p q p

OU := p .λ q . p p q

NON := p . p FAUX VRAI

IFTHENELSE := λ p .λ a .λ b . p a b

Nous sommes maintenant capables de calculer certaines fonctions logiques, par exemple :

ET VRAI FAUX

(λ p .λ q . p q p ) VRAI FAUX → _β VRAI FAUX VRAI

(λ x .λ y . x ) FAUX VRAI → _β FAUX

et nous voyons que AND TRUE FALSE est équivalent à FALSE .

Un prédicat est une fonction qui renvoie une valeur booléenne. Le prédicat le plus fondamental est ISZERO , qui renvoie TRUE si son argument est le chiffre Church 0 , et FALSE si son argument est un autre chiffre Church :

ISZERO := n . n (λ x .FAUX) VRAI

Le prédicat suivant teste si le premier argument est inférieur ou égal au second :

LEQ := λ m .λ n .ISZERO (SUB m n ) ,

et puisque m = n , si LEQ m n et LEQ n m , il est simple de construire un prédicat pour l'égalité numérique.

La disponibilité des prédicats et la définition ci-dessus de TRUE et FALSE facilitent l'écriture d'expressions "if-then-else" dans le calcul lambda. Par exemple, la fonction prédécesseur peut être définie comme :

PRED := n . n (λ g .λ k .ISZERO ( g 1) k (PLUS ( g k ) 1)) (λ v .0) 0

ce qui peut être vérifié en montrant inductivement que n (λ g .λ k .ISZERO ( g 1) k (PLUS ( g k ) 1)) (λ v .0) est la fonction addition n − 1 pour n > 0.

Paires

Une paire (2-tuple) peut être définie en termes de TRUE et FALSE , en utilisant l' encodage Church pour les paires . Par exemple, PAIR encapsule la paire ( x , y ), FIRST renvoie le premier élément de la paire et SECOND renvoie le second.

PAIRE := x .λ y .λ f . f x y

PREMIER := p . p VRAI

DEUXIÈME := p . p FAUX

NIL := λ x .TRUE

NULL := p . p (λ x .λ y .FAUX)

Une liste chaînée peut être définie soit comme NIL pour la liste vide, soit comme la PAIRE d'un élément et d'une liste plus petite. Le prédicat NULL teste la valeur NIL . (Alternativement, avec NIL := FALSE , la construction l (λ h .λ t .λ z .deal_with_head_ h _and_tail_ t ) (deal_with_nil) évite le besoin d'un test NULL explicite).

Comme exemple d'utilisation de paires, la fonction de décalage et d'incrémentation qui mappe ( m , n ) à ( n , n + 1) peut être définie comme

Φ := λ x .PAIR (DEUXIÈME x ) (SUCC (DEUXIÈME x ))

ce qui nous permet de donner peut-être la version la plus transparente de la fonction prédécesseur :

PRED := λ n .FIRST ( n Φ (PAIR 0 0)).

Techniques de programmation supplémentaires

Il existe un corpus considérable d' idiomes de programmation pour le calcul lambda. Beaucoup d'entre eux ont été développés à l'origine dans le contexte de l'utilisation du calcul lambda comme base de la sémantique du langage de programmation , en utilisant efficacement le calcul lambda comme langage de programmation de bas niveau . Étant donné que plusieurs langages de programmation incluent le lambda calcul (ou quelque chose de très similaire) en tant que fragment, ces techniques sont également utilisées dans la programmation pratique, mais peuvent alors être perçues comme obscures ou étrangères.

Constantes nommées

Dans le calcul lambda, une bibliothèque prendrait la forme d'une collection de fonctions préalablement définies, qui, en tant que termes lambda, ne sont que des constantes particulières. Le calcul lambda pur n'a pas de concept de constantes nommées puisque tous les termes lambda atomiques sont des variables, mais on peut émuler des constantes nommées en mettant de côté une variable comme nom de la constante, en utilisant l'abstraction pour lier cette variable dans le corps principal , et appliquer cette abstraction à la définition voulue. Ainsi, pour utiliser f pour signifier M (un terme lambda explicite) dans N (un autre terme lambda, le "programme principal"), on peut dire

(λ f . N ) M

Les auteurs introduisent souvent du sucre syntaxique , tel que let , pour permettre d' écrire ce qui précède dans l' ordre le plus intuitif

soit f = M dans N

En enchaînant de telles définitions, on peut écrire un « programme » de calcul lambda sous la forme de zéro ou plusieurs définitions de fonction, suivies d'un terme lambda utilisant ces fonctions qui constituent le corps principal du programme.

Une restriction notable de ce let est que le nom f n'est pas défini dans M , puisque M est en dehors de la portée de l' abstraction liant f ; cela signifie qu'une définition de fonction récursive ne peut pas être utilisée comme M avec let . La construction de sucre syntaxique letrec plus avancée qui permet d'écrire des définitions de fonctions récursives dans ce style naïf utilise en plus des combinateurs à virgule fixe.

Récursivité et points fixes

La récursivité est la définition d'une fonction en utilisant la fonction elle-même. Le lambda calcul ne peut pas exprimer cela aussi directement que certaines autres notations : toutes les fonctions sont anonymes dans le lambda calcul, nous ne pouvons donc pas faire référence à une valeur qui n'a pas encore été définie, à l'intérieur du terme lambda définissant cette même valeur. Cependant, la récursivité peut toujours être obtenue en faisant en sorte qu'une expression lambda se reçoive comme valeur d'argument, par exemple dans  (λ x . x x ) E .

Considérons la fonction factorielle F( n ) définie récursivement par

F( n ) = 1, si n = 0; sinon n × F( n − 1) .

Dans l'expression lambda qui doit représenter cette fonction, un paramètre (généralement le premier) sera supposé recevoir l'expression lambda elle-même comme valeur, de sorte que l'appeler - l'appliquer à un argument - équivaudra à une récursivité. Ainsi, pour obtenir la récursivité, l'argument destiné à s'auto-référencer (appelé r ici) doit toujours être passé à lui-même dans le corps de la fonction, à un point d'appel :

G := r . λ n .(1, si n = 0; sinon n × ( r r ( n −1)))

avec  r r x = F x = G r x  à tenir, donc  {{{1}}}  et

F := GG = (λ x . x x ) G

L'auto-application réalise la réplication ici, en passant l'expression lambda de la fonction à l'appel suivant en tant que valeur d'argument, la rendant disponible pour y être référencée et appelée.

Cela résout le problème mais nécessite de réécrire chaque appel récursif en tant qu'auto-application. Nous aimerions avoir une solution générique, sans avoir besoin de réécritures :

G := r . λ n .(1, si n = 0; sinon n × ( r ( n −1)))

avec  r x = F x = G r x  à tenir, donc  r = G r = : FIX G  et

F := FIX G  où  FIX g  := ( r où r = g r ) = g (FIX g )

de sorte que  FIX G = G (FIX G) = (λ n .(1, si n = 0; sinon n × ((FIX G) ( n −1))))

Étant donné un terme lambda dont le premier argument représente l'appel récursif (par exemple G ici), le combinateur à virgule fixe FIX retournera une expression lambda auto-répliquante représentant la fonction récursive (ici, F ). La fonction n'a pas besoin de se passer explicitement à elle-même à aucun moment, car l'auto-réplication est arrangée à l'avance, lors de sa création, pour être effectuée à chaque fois qu'elle est appelée. Ainsi, l'expression lambda originale (FIX G) est recréée à l'intérieur d'elle-même, au point d'appel, réalisant l' auto-référence .

En fait, il existe de nombreuses définitions possibles pour cet opérateur FIX , la plus simple d'entre elles étant :

Y  := g .(λ x . g ( x x )) (λ x . g ( x x ))

Dans le calcul lambda, Y g   est un point fixe de g , car il se développe en :

Y g

(λ h .(λ x . h ( x x )) (λ x . h ( x x ))) g

(λ x . g ( x x )) (λ x . g ( x x ))

g ((λ x . g ( x x )) (λ x . g ( x x )))

g ( Y g )

Maintenant, pour effectuer notre appel récursif à la fonction factorielle, nous appellerions simplement ( Y G) n , où n est le nombre dont nous calculons la factorielle. Étant donné n = 4, par exemple, cela donne :

( JV ) 4

G ( Y G) 4

(λ r .λ n .(1, si n = 0; sinon n × ( r ( n −1)))) ( Y G) 4

(λ n .(1, si n = 0; sinon n × (( Y G) ( n −1)))) 4

1, si 4 = 0 ; sinon 4 × (( Y G) (4−1))

4 × (G ( Y G) (4−1))

4 × ((λ n .(1, si n = 0; sinon n × (( Y G) ( n −1)))) (4−1))

4 × (1, si 3 = 0 ; sinon 3 × (( Y G) (3−1)))

4 × (3 × (G ( Y G) (3−1)))

4 × (3 × ((λ n .(1, si n = 0; sinon n × (( Y G) ( n −1)))) (3−1)))

4 × (3 × (1, si 2 = 0 ; sinon 2 × (( Y G) (2−1))))

4 × (3 × (2 × (G ( Y G) (2−1))))

4 × (3 × (2 × ((λ n .(1, si n = 0; sinon n × (( Y G) ( n −1)))) (2−1))))

4 × (3 × (2 × (1, si 1 = 0 ; sinon 1 × (( Y G) (1−1)))))

4 × (3 × (2 × (1 × (G ( Y G) (1−1)))))

4 × (3 × (2 × (1 × ((λ n .(1, si n = 0; sinon n × (( Y G) ( n −1)))) (1−1)))))

4 × (3 × (2 × (1 × (1, si 0 = 0 ; sinon 0 × (( Y G) (0−1)))))))

4 × (3 × (2 × (1 × (1))))

24

Chaque fonction définie de manière récursive peut être considérée comme un point fixe d'une fonction définie de manière appropriée se refermant sur l'appel récursif avec un argument supplémentaire et, par conséquent, en utilisant Y , chaque fonction définie de manière récursive peut être exprimée sous la forme d'une expression lambda. En particulier, nous pouvons maintenant définir proprement les prédicats de soustraction, multiplication et comparaison de nombres naturels de manière récursive.

Conditions standard

Certains termes ont des noms communément acceptés :

I  := x . X

K  := x .λ y . X

S  := x .λ y .λ z . x z ( y z )

B  := x .λ y .λ z . x ( y z )

C  := x .λ y .λ z . x z y

W  := x .λ y . x y y

U  := x . x x

ω  : = λ x . x x

Ω  : = ω ω

Y  := g .(λ x . g ( x x )) (λ x . g ( x x ))

Plusieurs d'entre eux ont des applications directes dans l' élimination de l'abstraction qui transforme les termes lambda en termes de calcul combinateur .

Élimination de l'abstraction

Si N est un terme lambda sans abstraction, mais contenant éventuellement des constantes nommées ( combinateurs ), alors il existe un terme lambda T ( x , N ) qui est équivalent à λ x . N mais manque d'abstraction (sauf dans le cadre des constantes nommées, si celles-ci sont considérées comme non atomiques). Cela peut également être considéré comme des variables d'anonymisation, car T ( x , N ) supprime toutes les occurrences de x de N , tout en permettant aux valeurs d'argument d'être substituées dans les positions où N contient un x . La fonction de conversion T peut être définie par :

T ( x , x ) := Je

T ( x , N ) := K N si x n'est pas libre dans N .

T ( x , M N ) := S T ( x , M ) T ( x , N )

Dans les deux cas, un terme de la forme T ( x , N ) P peut réduire en ayant le combinateur initial I , K ou S grab l'argument P , comme β-réduction (λ x . N ) P ferait. Je retourne cet argument. K rejette l'argument, tout comme (λ x . N ) le ferait si x n'a pas d'occurrence libre dans N . S transmet l'argument aux deux sous-termes de l'application, puis applique le résultat du premier au résultat du second.

Les combinateurs B et C sont similaires à S , mais transmettent l'argument à un seul sous-terme d'une application ( B au sous-terme "argument" et C au sous-terme "fonction"), sauvant ainsi un K suivant s'il n'y a pas d'occurrence de x dans un sous-terme. Par rapport à B et C , le combinateur S associe en fait deux fonctionnalités : réorganiser les arguments et dupliquer un argument afin qu'il puisse être utilisé à deux endroits. Le combinateur W ne fait que ce dernier, donnant le système B, C, K, W comme alternative au calcul du combinateur SKI .

Calcul lambda typé

Un lambda calcul typé est un formalisme typé qui utilise le symbole lambda ( ) pour désigner une abstraction de fonction anonyme. Dans ce contexte, les types sont généralement des objets de nature syntaxique qui sont affectés à des termes lambda ; la nature exacte d'un type dépend du calcul considéré (voir Types de calculs lambda typés ). D'un certain point de vue, les lambda calculs typés peuvent être considérés comme des raffinements du lambda calcul non typé mais d'un autre point de vue, ils peuvent également être considérés comme la théorie la plus fondamentale et le lambda calcul non typé un cas particulier avec un seul type. ${\style d'affichage \lambda }$

Les calculs lambda typés sont des langages de programmation fondamentaux et constituent la base des langages de programmation fonctionnels typés tels que ML et Haskell et, plus indirectement, des langages de programmation impératifs typés . Les calculs lambda typés jouent un rôle important dans la conception de systèmes de types pour les langages de programmation ; ici, la typabilité capture généralement les propriétés souhaitables du programme, par exemple le programme ne provoquera pas de violation d'accès à la mémoire.

Les calculs lambda typés sont étroitement liés à la logique mathématique et à la théorie de la preuve via l' isomorphisme de Curry-Howard et ils peuvent être considérés comme le langage interne des classes de catégories , par exemple le lambda calcul simplement typé est le langage des catégories fermées cartésiennes (CCC).

Stratégies de réduction

Qu'un terme se normalise ou non, et combien de travail doit être fait pour le normaliser s'il l'est, dépend dans une large mesure de la stratégie de réduction utilisée. Les stratégies courantes de réduction du calcul lambda comprennent :

Ordre normal

Le redex le plus à gauche et le plus à l'extérieur est toujours réduit en premier. C'est-à-dire que, dans la mesure du possible, les arguments sont substitués dans le corps d'une abstraction avant que les arguments ne soient réduits.

Ordre d'application

Le redex le plus à gauche et le plus à l'intérieur est toujours réduit en premier. Intuitivement, cela signifie que les arguments d'une fonction sont toujours réduits avant la fonction elle-même. L'ordre d'application tente toujours d'appliquer des fonctions aux formes normales, même lorsque cela n'est pas possible.

-réductions complètes

Tout redex peut être réduit à tout moment. Cela signifie essentiellement l'absence d'une stratégie de réduction particulière - en ce qui concerne la réductibilité, "tous les paris sont ouverts".

Les stratégies de réduction faible ne réduisent pas sous les abstractions lambda :

Appel par valeur

Un redex n'est réduit que lorsque sa partie droite est réduite à une valeur (variable ou abstraction). Seuls les redexes les plus externes sont réduits.

Appel par nom

Comme l'ordre normal, mais aucune réduction n'est effectuée à l'intérieur des abstractions. Par exemple, λ x .(λ x . x ) x est sous forme normale selon cette stratégie, bien qu'il contienne le redex (λ x . x ) x .

Les stratégies avec partage réduisent les calculs « les mêmes » en parallèle :

Réduction optimale

Comme l'ordre normal, mais les calculs qui ont la même étiquette sont réduits simultanément.

Appel par besoin

Comme appel par nom (donc faible), mais les applications de fonction qui dupliqueraient des termes nomment à la place l'argument, qui n'est ensuite réduit que "lorsque cela est nécessaire".

Calculabilité

Il n'y a pas d'algorithme qui prend en entrée deux expressions lambda et renvoie VRAI ou FAUX selon qu'une expression se réduit à l'autre. Plus précisément, aucune fonction calculable ne peut trancher la question. C'était historiquement le premier problème pour lequel l'indécidabilité pouvait être prouvée. Comme d'habitude pour une telle preuve, calculable signifie calculable par n'importe quel modèle de calcul qui est Turing complet . En fait la calculabilité peut elle-même être définie via le calcul lambda : une fonction F : N → N d'entiers naturels est une fonction calculable si et seulement s'il existe une expression lambda f telle que pour tout couple de x , y dans N , F ( x ) = y si et seulement si f x  = _β  y , où x et y sont des chiffres correspondant à l' Eglise x et y , respectivement , et = _β signifie l' équivalence avec les β-réduction. Voir la thèse de Church-Turing pour d'autres approches pour définir la calculabilité et leur équivalence.

La preuve d'incalculabilité de Church réduit d'abord le problème à déterminer si une expression lambda donnée a une forme normale . Ensuite, il suppose que ce prédicat est calculable, et peut donc être exprimé en lambda calcul. En s'appuyant sur des travaux antérieurs de Kleene et en construisant une numérotation de Gödel pour les expressions lambda, il construit une expression lambda e qui suit de près la preuve du premier théorème d'incomplétude de Gödel . Si e est appliqué à son propre nombre de Gödel, il en résulte une contradiction.

Complexité

La notion de complexité de calcul pour le lambda calcul est un peu délicate, car le coût d'une β-réduction peut varier selon la façon dont elle est implémentée. Pour être précis, il faut en quelque sorte trouver l'emplacement de toutes les occurrences de la variable liée V dans l'expression E , ce qui implique un coût en temps, ou il faut garder une trace des emplacements des variables libres d'une manière ou d'une autre, ce qui implique un coût en espace. Une recherche naïve des emplacements de V dans E est O ( n ) dans la longueur n de E . Les chaînes de directeur étaient une première approche qui échangeait ce coût de temps contre une utilisation quadratique de l'espace. Plus généralement, cela a conduit à l'étude de systèmes utilisant la substitution explicite .

En 2014, il a été montré que le nombre d'étapes de réduction prises par la réduction d'ordre normal pour réduire un terme est un modèle de coût en temps raisonnable , c'est-à-dire que la réduction peut être simulée sur une machine de Turing en temps polynomialement proportionnel au nombre d'étapes. . Il s'agissait d'un problème ouvert de longue date, en raison de l' explosion de taille , de l'existence de termes lambda dont la taille augmente de façon exponentielle pour chaque -réduction. Le résultat contourne ce problème en travaillant avec une représentation partagée compacte. Le résultat montre clairement que la quantité d'espace nécessaire pour évaluer un terme lambda n'est pas proportionnelle à la taille du terme lors de la réduction. On ne sait pas actuellement quelle serait une bonne mesure de la complexité spatiale.

Un modèle déraisonnable ne signifie pas nécessairement inefficace. La réduction optimale réduit tous les calculs avec la même étiquette en une seule étape, évitant le travail en double, mais le nombre d'étapes de β-réduction parallèles pour réduire un terme donné à la forme normale est approximativement linéaire dans la taille du terme. C'est beaucoup trop petit pour être une mesure de coût raisonnable, car toute machine de Turing peut être codée dans le calcul lambda en taille linéairement proportionnelle à la taille de la machine de Turing. Le véritable coût de la réduction des termes lambda n'est pas dû à la -réduction en soi mais plutôt à la gestion de la duplication des redexes lors de la -réduction. On ne sait pas si les implémentations de réduction optimales sont raisonnables lorsqu'elles sont mesurées par rapport à un modèle de coût raisonnable tel que le nombre d'étapes les plus à gauche jusqu'à la forme normale, mais il a été démontré pour des fragments du calcul lambda que l'algorithme de réduction optimale est efficace et a au plus un surcoût quadratique par rapport à l'extrême gauche. De plus, la mise en œuvre du prototype BOHM de la réduction optimale a surpassé à la fois Caml Light et Haskell en termes lambda purs.

Calcul lambda et langages de programmation

Comme l'a souligné l'article de Peter Landin de 1965 "A Correspondence between ALGOL 60 and Church's Lambda-notation", les langages de programmation procéduraux séquentiels peuvent être compris en termes de calcul lambda, qui fournit les mécanismes de base pour l'abstraction procédurale et la procédure (sous-programme) application.

Fonctions anonymes

Par exemple, dans Lisp, la fonction "carré" peut être exprimée comme une expression lambda comme suit :

(lambda (x) (* x x))

L'exemple ci-dessus est une expression qui évalue une fonction de première classe. Le symbole lambdacrée une fonction anonyme, étant donné une liste de noms de paramètres, (x)- juste un seul argument dans ce cas, et une expression qui est évaluée comme le corps de la fonction, (* x x). Les fonctions anonymes sont parfois appelées expressions lambda.

Par exemple, Pascal et de nombreux autres langages impératifs ont longtemps pris en charge le passage de sous-programmes en tant qu'arguments à d'autres sous-programmes via le mécanisme des pointeurs de fonction . Cependant, les pointeurs de fonction ne sont pas une condition suffisante pour que les fonctions soient des types de données de première classe , car une fonction est un type de données de première classe si et seulement si de nouvelles instances de la fonction peuvent être créées au moment de l'exécution. Et cette création de fonctions au moment de l'exécution est prise en charge dans Smalltalk , JavaScript et Wolfram Language , et plus récemment dans Scala , Eiffel ("agents"), C# ("delegates") et C++11 , entre autres.

Parallélisme et concurrence

La propriété de Church-Rosser du lambda calcul signifie que l'évaluation (β-réduction) peut être effectuée dans n'importe quel ordre , même en parallèle. Cela signifie que diverses stratégies d'évaluation non déterministes sont pertinentes. Cependant, le lambda calcul n'offre aucune construction explicite pour le parallélisme . On peut ajouter des constructions telles que Futures au calcul lambda. D'autres calculs de processus ont été développés pour décrire la communication et la concurrence.

Sémantique

Le fait que les termes du lambda calcul agissent comme des fonctions sur d'autres termes du lambda calcul, et même sur eux-mêmes, a conduit à des questions sur la sémantique du lambda calcul. Un sens raisonnable pourrait-il être attribué aux termes du calcul lambda ? La sémantique naturelle était de trouver un ensemble D isomorphe à l'espace des fonctions D → D , de fonctions sur lui-même. Cependant, pas triviale telle D peut exister, par cardinalité contraintes , car l'ensemble de toutes les fonctions de D à D a une plus grande cardinalité que D , à moins que D est un ensemble singleton .

Dans les années 1970, Dana Scott a montré que si seules les fonctions continues étaient considérées, un ensemble ou un domaine D avec la propriété requise pouvait être trouvé, fournissant ainsi un modèle pour le calcul lambda.

Ce travail a également constitué la base de la sémantique dénotationnelle des langages de programmation.

Variantes et extensions

Ces extensions sont dans le cube lambda :

• Calcul lambda typé – Calcul lambda avec variables typées (et fonctions)
• Système F - Un calcul lambda typé avec des variables de type
• Calcul des constructions - Un calcul lambda typé avec des types comme valeurs de première classe

Ces systèmes formels sont des extensions du lambda calcul qui ne sont pas dans le cube lambda :

• Calcul lambda binaire - Une version du calcul lambda avec des E/S binaires, un codage binaire des termes et une machine universelle désignée.
• Calcul lambda-mu - Une extension du calcul lambda pour traiter la logique classique

Ces systèmes formels sont des variantes du lambda calcul :

• Calcul Kappa - Un analogue de premier ordre du calcul lambda

Ces systèmes formels sont liés au calcul lambda :

• Logique combinatoire - Une notation pour la logique mathématique sans variables
• SKI combinator calculus – Un système de calcul basé sur les combinateurs S , K et I , équivalent au calcul lambda, mais réductible sans substitutions de variables

Voir également

Remarques

Les références

Lectures complémentaires

• Abelson, Harold et Gerald Jay Sussman. Structure et interprétation des programmes informatiques . La presse du MIT . ISBN  0-262-51087-1 .
• Hendrik Pieter Barendregt Introduction au Lambda Calcul .
• Henk Barendregt , L'impact du calcul Lambda en logique et en informatique . Le Bulletin de la Logique Symbolique, Volume 3, Numéro 2, Juin 1997.
• Barendregt, Hendrik Pieter , The Type Free Lambda Calculus pp1091-1132 of Handbook of Mathematical Logic , North-Holland (1977) ISBN  0-7204-2285-X
• Cardone et Hindley, 2006. Histoire du lambda-calcul et de la logique combinatoire . Dans Gabbay et Woods (éd.), Handbook of the History of Logic , vol. 5. Elsevier.
• Church, Alonzo, Un problème insoluble de la théorie des nombres élémentaires , American Journal of Mathematics , 58 (1936), pp. 345-363. Cet article contient la preuve que l'équivalence des expressions lambda n'est en général pas décidable.
• Église Alonzo, Les calculs de la conversion Lambda ( ISBN  978-0-691-08394-0 )
• Frink Jr., Orrin, Revue : Les calculs de la conversion lambda
• Kleene, Stephen, A theory of positive integers in formal logic , American Journal of Mathematics , 57 (1935), pp. 153-173 et 219-244. Contient les définitions de calcul lambda de plusieurs fonctions familières.
• Landin, Peter , Une correspondance entre ALGOL 60 et la notation Lambda de Church , Communications de l'ACM , vol. 8, non. 2 (1965), pages 89-101. Disponible sur le site de l' ACM . Un article classique soulignant l'importance du calcul lambda comme base des langages de programmation.
• Larson, Jim, Une introduction au calcul et au schéma Lambda . Une introduction douce pour les programmeurs.
• Schalk, A. et Simmons, H. (2005) Une introduction aux -calculs et à l'arithmétique avec une sélection décente d'exercices . Notes pour un cours du MSc Mathematical Logic à l'Université de Manchester.
• de Queiroz, Ruy JGB (2008). « Sur les règles de réduction, le sens en tant qu'usage et la sémantique théorique de la preuve ». Studia Logica . 90 (2) : 211-247. doi : 10.1007/s11225-008-9150-5 . S2CID  11321602 . Un article donnant un fondement formel à l'idée de « le sens-est-l'utilisation » qui, même si elle est basée sur des preuves, est différente de la sémantique de la théorie de la preuve comme dans la tradition Dummett-Prawitz puisqu'elle prend la réduction comme règles donnant un sens.
• Hankin, Chris, Une introduction aux calculs Lambda pour les informaticiens, ISBN  0954300653

Monographies/manuels pour étudiants diplômés :

• Morten Heine Sørensen, Paweł Urzyczyn, Lectures on the Curry-Howard isomorphism , Elsevier, 2006, ISBN  0-444-52077-5 est une monographie récente qui couvre les principaux sujets du calcul lambda de la variété sans type, à la plupart des lambda typés calculs , y compris des développements plus récents comme les systèmes de type pur et le cube lambda . Il ne couvre pas les extensions de sous-typage .
• Pierce, Benjamin (2002), Types et langages de programmation , MIT Press, ISBN 0-262-16209-1couvre les calculs lambda d'un point de vue de système de type pratique ; certains sujets comme les types dépendants ne sont mentionnés que, mais le sous-typage est un sujet important.

Certaines parties de cet article sont basées sur du matériel de FOLDOC , utilisé avec permission .

Liens externes

• Graham Hutton, Lambda Calculus , une courte vidéo (12 minutes) Computerphile sur le Lambda Calculus
• Helmut Brandl, Introduction étape par étape au calcul Lambda
• " Lambda-calcul " , Encyclopédie des mathématiques , EMS Press , 2001 [1994]
• Achim Jung, Une brève introduction au calcul Lambda -( PDF )
• Dana Scott, Une chronologie du calcul lambda -( PDF )
• David C. Keenan, Pour disséquer un oiseau moqueur : une notation graphique pour le calcul Lambda avec réduction animée
• Raúl Rojas, Un didacticiel d'introduction au calcul Lambda -( PDF )
• Peter Selinger, Notes de cours sur le calcul Lambda -( PDF )
• L. Allison, Quelques exemples de -calcul exécutables
• Georg P. Loczewski, Le Lambda Calcul et A++
• Bret Victor, Alligator Eggs : un jeu de réflexion basé sur le lambda calcul
• Le Lambda Calcul sur le site de Safalra
• LCI Lambda Interpreter un interpréteur de calcul pur simple mais puissant
• Liens Lambda Calculus sur Lambda-the-Ultimate
• Mike Thyer, Lambda Animator , une applet Java graphique démontrant des stratégies de réduction alternatives.
• Implémentation du calcul Lambda à l' aide de modèles C++
• Marius Buliga, Calcul lambda graphique
• Lambda Calculus comme modèle de workflow par Peter Kelly, Paul Coddington et Andrew Wendelborn ; mentionne la réduction de graphe comme moyen courant d'évaluer les expressions lambda et discute de l'applicabilité du calcul lambda pour l' informatique distribuée (en raison de lapropriété Church-Rosser , qui permet laréduction de graphe parallèle pour les expressions lambda).
• Shane Steinert-Threlkeld, " Lambda Calculi " , Internet Encyclopedia of Philosophy
• Anton Salikhmetov, Macro Lambda Calcul