Le calcul lambda est un système formel de logique mathématique permettant d'exprimer des calculs basés sur l'abstraction et d'appliquer des fonctions à l'aide de liaisons et de substitutions de variables. Il s'agit d'un modèle universel qui peut être appliqué à la conception de n'importe quelle machine de Turing. Le calcul lambda a été introduit pour la première fois par Church, un célèbre mathématicien, dans les années 1930.
Le système consiste à construire des membres lambda et à effectuer des opérations de réduction sur eux.
Explications et applications
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 la première variante, les fonctions ne peuvent être utilisées que si elles sont capables de recevoir des données de ce type. Les calculs lambda typés sont plus faibles, peuvent exprimer une valeur plus petite. Mais, d'un autre côté, ils vous permettent de prouver plus de choses.
L'une des raisons pour lesquelles il existe tant de types différents est le désir des scientifiques d'en faire plus sans renoncer à la possibilité de prouver de solides théorèmes de calcul lambda.
Le système a des applications dans de nombreux domaines différents des mathématiques, de la philosophie, de la linguistique et de l'informatique. Tout d'abord, le lambda calcul est un calcul qui a joué un rôle important dans le développement de la théorie des langages de programmation. Ce sont les styles de création fonctionnelle que les systèmes mettent en œuvre. Ils sont également un sujet de recherche brûlant dans la théorie de ces catégories.
Pour les nuls
Le calcul lambda a été introduit par le mathématicien Alonzo Church dans les années 1930 dans le cadre de ses recherches sur les fondements de la science. Le système original s'est avéré logiquement incohérent en 1935 lorsque Stephen Kleen et JB Rosser ont développé le paradoxe de Kleene-Rosser.
Plus tard, en 1936, Church a isolé et publié uniquement la partie pertinente pour les calculs, ce qu'on appelle maintenant le calcul lambda non typé. En 1940, il a également introduit une théorie plus faible mais logiquement cohérente connue sous le nom de système de type premier. Dans son travail, il explique toute la théorie en termes simples, on peut donc dire que Church a publié le calcul lambda pour les nuls.
Jusqu'aux années 1960, lorsque sa relation avec les langages de programmation est devenue claire, λ n'était qu'un formalisme. Grâce aux applications de Richard Montagu et d'autres linguistes à la sémantique du langage naturel, le calcul différentiel a pris une place de choix en linguistique et en informatique.
Origine du symbole
Lambda ne représente pas un mot ou un acronyme, il provient d'une référence dans les mathématiques principales de Russell suivie de deux changements typographiques. Exemple de notation: pour une fonction f avec f (y)=2y + 1 est 2ŷ + 1. Et ici, nous utilisons un caret ("chapeau") sur y pour étiqueter la variable d'entrée.
L'église avait à l'origine l'intention d'utiliser des symboles similaires, mais les typographes n'ont pas pu placer le symbole "chapeau" au-dessus des lettres. Donc, à la place, ils l'ont imprimé à l'origine sous la forme "/\y.2y+1". Dans le prochain épisode d'édition, les dactylographes ont remplacé "/ \" par un caractère visuellement similaire.
Introduction au calcul lambda
Le système se compose d'un langage de termes, qui sont choisis par une certaine syntaxe formelle, et d'un ensemble de règles de transformation qui permettent de les manipuler. Le dernier point peut être considéré comme une théorie équationnelle ou comme une définition opérationnelle.
Toutes les fonctions du calcul lambda sont anonymes, ce qui signifie qu'elles n'ont pas de nom. Ils ne prennent qu'une seule variable d'entrée et le curry est utilisé pour implémenter des graphiques avec plusieurs variables.
Termes lambda
La syntaxe du calcul définit certaines expressions comme valides et d'autres comme invalides. Tout comme différentes chaînes de caractères sont des programmes C valides et certains ne le sont pas. L'expression réelle du calcul lambda est appelée le "terme lambda".
Les trois règles suivantes fournissent une définition inductive qui peut êtres'appliquent à la construction de tous les concepts syntaxiquement valides:
La variable x elle-même est un terme lambda valide:
- si T est LT et x n'est pas constant, alors (lambda xt) est appelé une abstraction.
- si T aussi bien que s sont des concepts, alors (TS) est appelé une application.
Rien d'autre n'est un terme lambda. Ainsi, un concept est valide si et seulement s'il peut être obtenu par l'application répétée de ces trois règles. Cependant, certaines parenthèses peuvent être omises selon d'autres critères.
Définition
Les expressions lambda consistent en:
- variables v 1, v 2, …, v n, …
- symboles d'abstraction 'λ' et point '.'
- crochets ().
L'ensemble Λ peut être défini inductivement:
- Si x est une variable, alors x ∈ Λ;
- x n'est pas constant et M ∈ Λ, alors (λx. M) ∈ Λ;
- M, N ∈ Λ, alors (MN) ∈ Λ.
Désignation
Pour garder la notation des expressions lambda épurée, les conventions suivantes sont couramment utilisées:
- Parenthèses extérieures omises: MN au lieu de (MN).
- Les applications sont supposées rester associatives: on peut écrire MNP au lieu de ((MN) P).
- Le corps de l'abstraction s'étend plus à droite: λx. MN signifie λx. (MN), pas (λx. M) N.
- La suite des abstractions est réduite: λx.λy.λz. N peut être λxyz. N.
Variables libres et liées
L'opérateur λ relie sa non-constante où qu'elle se trouve dans le corps de l'abstraction. Les variables qui entrent dans la portée sont appelées liées. Dans l'expression λ x. M, la partie λ x est souvent appelée liant. Comme s'il suggérait que les variables deviennent un groupe avec l'ajout de X x à M. Toutes les autres variables instables sont appelées libres.
Par exemple, dans l'expression λ y. x x y, y - lié non permanent et x - libre. Et il convient également de noter que la variable est regroupée par son abstraction "la plus proche". Dans l'exemple suivant, la solution du calcul lambda est représentée par une seule occurrence de x, qui est liée au second terme:
λx. y (λ x. z x)
L'ensemble des variables libres M est noté FV (M) et est défini par récurrence sur la structure des termes comme suit:
- FV (x)={x}, où x est une variable.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Une formule qui ne contient pas de variables libres est dite fermée. Les expressions lambda fermées sont également appelées combinateurs et sont équivalentes aux termes de la logique combinatoire.
Abréviation
La signification des expressions lambda est déterminée par la façon dont elles peuvent être raccourcies.
Il existe trois types de coupe:
- α-transform: modification des variables liées (alpha).
- β-réduction: appliquer des fonctions à leurs arguments (bêta).
- η-transform: couvre la notion d'extensionnalité.
Ici c'est aussinous parlons des équivalences résultantes: deux expressions sont β-équivalentes si elles peuvent être β-transformées en le même composant, et l'équivalence α / η est définie de manière similaire.
Le terme redex, abréviation de chiffre d'affaires réductible, fait référence à des sous-thèmes qui peuvent être réduits par l'une des règles. Calcul lambda pour les nuls, exemples:
(λ x. M) N est un redex bêta dans l'expression de remplacement de N par x dans M. La composante à laquelle un redex se réduit est appelée son reduct. La réduction (λ x. M) N est M [x:=N].
Si x n'est pas libre dans M, λ x. M x également em-REDEX avec régulateur M.
α-transformation
Alpha renames vous permet de changer les noms des variables liées. Par exemple, X. x peut donner λ y. y. Les termes qui ne diffèrent que par la transformation alpha sont dits α-équivalents. Souvent, lors de l'utilisation du calcul lambda, les équivalents α sont considérés comme réciproques.
Les règles exactes pour la conversion alpha ne sont pas entièrement triviales. Premièrement, avec cette abstraction, seules les variables associées au même système sont renommées. Par exemple, la transformée alpha λ x.λ x. x peut conduire à λ y.λ x. x, mais cela peut ne pas conduire à λy.λx.y Ce dernier a une signification différente de l'original. Ceci est analogue au concept de programmation d'observation variable.
Deuxièmement, une transformation alpha n'est pas possible si elle aboutirait à être capturée par une autre abstraction non permanente. Par exemple, si vous remplacez x par y dans λ x.λ y. x, alors vous pouvez obtenirλy.λy. u, ce qui n'est pas du tout le même.
Dans les langages de programmation à portée statique, la conversion alpha peut être utilisée pour simplifier la résolution des noms. En même temps, en veillant à ce que le concept de variable ne masque pas la désignation dans la zone contenante.
Dans la notation d'index de De Bruyne, deux termes équivalents alpha sont syntaxiquement identiques.
Remplacement
Les changements écrits par E [V:=R] sont le processus de substitution de toutes les occurrences libres de la variable V dans l'expression E par le chiffre d'affaires R. La substitution en termes de λ est définie par le lambda de la récursivité calcul sur la structure du concept comme suit (remarque: x et y - seules variables, et M et N - toute expression λ).
x [x:=N] ≡ N
y [x:=N] ≡ y si x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) si x ≠ y, pourvu que y ∉ FV (N).
Pour la substitution dans une abstraction lambda, il est parfois nécessaire de transformer une expression en α. Par exemple, il n'est pas vrai que (λ x. Y) [y:=x] donne (λ x. X) car le x substitué aurait dû être libre, mais a fini par être lié. Le remplacement correct dans ce cas est (λ z. X) jusqu'à α-équivalence. Notez que la substitution est définie de manière unique jusqu'à lambda.
β-réduction
La réduction bêta reflète l'idée d'appliquer une fonction. Bêta-réducteur est défini en termessubstitution: ((X V. E) E ') est E [V:=E'].
Par exemple, en supposant un codage 2, 7, ×, il y a la β-réduction suivante: ((λ n. N × 2) 7) → 7 × 2.
La réduction bêta peut être considérée comme identique au concept de réductibilité locale par déduction naturelle via l'isomorphisme de Curry-Howard.
η-transformer
Cette conversion exprime l'idée d'extensionnalité, qui dans ce contexte est que deux fonctions sont égales lorsqu'elles donnent le même résultat pour tous les arguments. Cette conversion échange entre λ x. (F x) et f chaque fois que x ne semble pas libre dans f.
Cette action peut être considérée comme identique au concept de complétude locale en déduction naturelle par l'isomorphisme de Curry-Howard.
Formes normales et fusion
Pour un calcul lambda non typé, la règle de β-réduction n'est généralement ni forte ni faible normalisante.
Néanmoins, on peut montrer que la β-réduction fusionne lorsqu'elle s'exécute avant la transformation α (c'est-à-dire que deux formes normales peuvent être considérées comme égales si une transformation α de l'une à l'autre est possible).
Par conséquent, les termes fortement normalisants et les termes faiblement ajustés ont une seule forme normale. Pour les premiers termes, toute stratégie de réduction est garantie d'aboutir à une configuration typique. Alors que pour des conditions faiblement normalisées, certaines stratégies de réduction peuvent ne pas le trouver.
Méthodes de programmation supplémentaires
Il existe de nombreux idiomes de création pour le calcul lambda. Beaucoup d'entre eux ont été développés à l'origine dans le contexte de l'utilisation de systèmes comme base de la sémantique d'un langage de programmation, les appliquant efficacement en tant que construction de bas niveau. Étant donné que certains styles incluent un calcul lambda (ou quelque chose de très similaire) en tant qu'extrait, ces techniques trouvent également une utilisation dans la création pratique, mais peuvent alors être perçues comme obscures ou étrangères.
Constantes nommées
Dans le calcul lambda, une bibliothèque prend la forme d'un ensemble de fonctions préalablement définies, où les termes ne sont que des constantes concrètes. Le calcul pur n'a pas de concept d'immuables nommés puisque tous les termes lambda atomiques sont des variables. Mais ils peuvent également être imités en prenant le mutable comme nom de la constante, en utilisant une abstraction lambda pour lier ce volatile dans le corps et en appliquant cette abstraction à la définition souhaitée. Donc, si vous utilisez f pour représenter M dans N, vous pourriez dire
(λ f. N) M.
Les auteurs introduisent souvent un concept syntaxique tel que let pour permettre aux choses d'être écrites de manière plus intuitive.
f=M à N
En chaî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 seul membre lambda, en utilisant les définitions qui constituent l'essentiel du programme.
Une limitation notable de cette let est que le nom f n'est pas défini dans M,puisque M est en dehors de la portée contraignante de l'abstraction lambda f. Cela signifie qu'un attribut de fonction récursive ne peut pas être utilisé comme M avec let. La syntaxe letrec plus avancée, qui vous permet d'écrire des définitions de fonctions récursives dans ce style, utilise en outre des combinateurs à virgule fixe à la place.
Analogues imprimés
Ce type est un formalisme typé qui utilise un symbole pour représenter 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épend du calcul en question. D'un certain point de vue, les LI typés peuvent être considérés comme des raffinements des LI non typés. Mais d'un autre côté, ils peuvent aussi être considérés comme une théorie plus fondamentale, et le calcul lambda non typé est un cas particulier avec un seul type.
Les LI typés sont le fondement des langages de programmation et l'épine dorsale des langages fonctionnels tels que ML et Haskell. Et, plus indirectement, des styles impératifs de création. Les calculs lambda typés jouent un rôle important dans le développement de systèmes de types pour les langages de programmation. Ici, la typabilité capture généralement les propriétés souhaitées du programme, par exemple, cela ne causera 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 à travers l'isomorphisme de Curry-Howard, et peuvent être considérés comme un langage interne des classes de catégories, par exemple, quiest simplement le style des fermetures cartésiennes.
