Lambda-calcul
66966
30413479
2008-06-07T22:09:56Z
Zepolak
97508
Orthographe
{{Citation bloc|''La notion de λ-définissabilité fut la première de ce qui est accepté maintenant comme l'équivalent exact des descriptions mathématiques pour lesquelles des algorithmes existent.''| [[Stephen Cole Kleene|Stephen Kleene]]| in ''Origins of Recursive Function Theory'', Annals of the history of Computing, 1981, vol; 3, n°1, page 52}}
Le '''lambda-calcul''' (ou '''''λ-calcul''''') est un [[système formel]] inventé par [[Alonzo Church]] dans les [[années 1930]], qui fonde les concepts [[Application (mathématiques)|de fonction et d'application]]. Il a été le premier formalisme utilisé pour définir et [[thèse de Church | caractériser les fonctions récursive]]s et donc il a une grande importance dans la théorie de la [[calculabilité]], à l'égal des [[machine de Turing|machines de Turing]] et du [[modèle de Herbrand-Gödel]]. Il a depuis été appliqué comme [[programmation fonctionnelle | langage de programmation théorique]] et comme [[métalangage]] pour [[assistant de preuve | la démonstration formelle assistée par ordinateur]]. Le lambda-calcul peut être ou ne pas être ''typé''.
Le lambda-calcul est apparenté à la [[logique combinatoire]] de [[Haskell Curry]].
== 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égorie (linguistique)|catégories]] :
* les ''variables'' : ''x'', ''y'' ... sont des lambda-termes ;
* les ''applications'' : ''u v'' est un lambda-terme si ''u'' et ''v'' sont des lambda-termes ;
* les ''abstractions'' : ''λ x.v'' est un lambda-terme si ''x'' est une variable et ''v'' un lambda-terme.
L'''application'' peut être vue ainsi : si ''u'' est une fonction et si ''v'' est son argument, alors ''u v'' est le résultat de l'application à ''v'' de la fonction ''u''.
L'''abstraction'' ''λ x.v'' peut être interprétée comme la formalisation de la fonction qui, à ''x'', associe ''v'', où ''v'' contient en général des occurrences de ''x''.
Ainsi, la fonction<ref>Cette 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.</ref> ''f'' qui prend en paramètre le lambda-terme ''x'' et lui ajoute ''2'' (c'est-à-dire en notation mathématique courante la fonction ''f: x <math>\mapsto</math> x+2'') sera dénotée en lambda-calcul par l'expression ''λ x.x+2''. L'application de cette fonction au nombre ''3'' s'écrit ''(λ x.x+2)3'' et s'« évalue » (ou se normalise) en l'expression ''5''.
== Notations, conventions et concepts==
===Parenthésage===
Pour délimiter les applications on utilise des parenthèses, mais une utilisation trop abondante de parenthèses peut conduire à des expressions illisibles, donc pour raccourcir et clarifier les expressions, on supprime des parenthèses, ainsi <tt>x<sub>1</sub> x<sub>2</sub> ... x<sub>n</sub></tt> est équivalent à <tt>((x<sub>1</sub> x<sub>2</sub>) ... x<sub>n</sub>)</tt>
Il y a en fait deux conventions :
*'''Association à gauche''', l'expression ''((M₀ M₁) (M₂M₃))'' s'écrit ''M₀ M₁ (M₂M₃)''. Quand une application s'applique à une autre application on ne met de parenthèse que sur l'application de droite. Formellement, la [[Grammaire formelle|grammaire]] du lambda calcul parenthésé est alors
:: <math>\Lambda ::= Var | \lambda Var \Lambda | \Lambda (\Lambda)</math>
*'''Parenthésage du terme de tête''', l'expression ''((M₀ M₁) (M₂M₃)) '' s'écrit ''(M₀) M₁ (M₂) M₃''. Un terme ente parenthèses est le premier d'une suite d'applications. Ainsi les arguments d'un terme sont facilement identifiables. Formellement, la [[Grammaire formelle|grammaire]] du lambda calcul parenthésé est alors
:: <math>\Lambda ::= Var | \lambda Var \Lambda | \Lambda \Lambda | (\Lambda)</math>.
===Curryfication===
Un lambda-terme ne prend qu'un seul argument, mais [[Moses Schönfinkel|Shönfinkel]] et [[Haskell Curry | Curry]] ont introduit la [[curryfication]] et montré qu'on peut ainsi contourner cette restriction de la façon suivante : 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 la 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ée<ref>En mathématiques, les variables sont liées par ∀ ou par ∃ ou par ∫ ... ''dx''.</ref> par un λ. Une variable liée a une [[Portée (informatique)|portée]]<ref>La portée est la partie de l'expression où la variable a la même signification.</ref> 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 <math>f(x) = \int_a^b {x + y~dy}</math>, <math>x</math> est libre, mais <math>y</math> est liée (par le <math>dy</math>). Ceci est la même expression que <math>f(x) = \int_a^b {x + z~dz}</math> car <math>y</math> était un nom local, tout comme l'est z. Par contre <math>f(x) = \int_a^b {z + y~dy}</math> ne correspond pas à la même expression car le x est libre. D'ailleurs la notation <math>f(x)</math> précise que l'ensemble de ses variables (libres) est <math>\{x\}</math>.
Tout comme l'intégrale lie la variable d'intégration, le λ lie la variable qui le suit.
'''Exemples''': dans <math>\lambda x.xy</math> x est lié et y libre. On peut récrire ce terme en <math>\lambda t.ty</math>.
<math>\lambda xyzt. z(xt)ab(zsy)</math> est équivalent à <math>\lambda wjit. i(wt)ab(isj)</math>
==== Définition formelle des variables libres en lambda-calcul ====
On définit l'ensemble <tt>VL(''t'')</tt> des ''variables libres'' d'un terme ''t'' par récurrence :
* si <tt>x</tt> est une variable alors <tt>VL(x) = {x}</tt>
* si <tt>u</tt> et <tt>v</tt> sont des lambda-termes alors <tt>VL(u v) = VL(u) ∪ VL(v)</tt>
* si <tt>x</tt> est une variable et <tt>u</tt> un lambda-terme alors <tt>VL(λx.u) = VL(u) \ {x}</tt>
Si un lambda-terme n'a pas de variables libres, on dit qu'il est ''clos'' (ou fermé) on dit aussi que ce lambda-terme est un ''combinateur'' (d'après le concept apparenté de [[logique combinatoire]]).
== 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'' apparait dans ''t'' comme occurrence d'un sous terme de la forme ''λy.v'', le phénomène de capture pourrait apparaitre. 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<math>\neq</math>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'apparait ni dans ''t'' ni dans ''u''.
L'α-conversion identifie <math>\lambda</math>y.v et <math>\lambda</math>z.v[y := z]. Deux lambda-termes qui ne diffèrent que par un renommage (sans capture) de leurs variables liées sont dit ''α-convertibles''. L'α-conversion est une [[relation d'équivalence]] entre lambda-termes.
'''Exemples :'''
* (λx.xy)[y := a] = <math>\lambda</math>x.xa
* (λx.xy)[y := x] = <math>\lambda</math>z.zx (et non <math>\lambda</math> x.xx, qui est totalement différent, cf remarque ci-dessus)
'''Remarque :''' l'α-conversion doit être définie avec précaution avant la substitution. Ainsi dans le terme
λx.λy.xy λz.z, on ne pourra pas renommer brutalement x en y (on obtiendrait <math>\lambda</math>y.<math>\lambda</math>y.yy<math>\lambda</math>z.z) par contre on peut renommer x en z.
Définie ainsi la substitution est un mécanisme externe au lambda-calcul, on dit aussi qu'il fait partie de la méta-théorie. A noter que certains travaux visent à introduire la substitution comme un mécanisme interne au lambda-calcul, conduisant à ce qu'on appelle les calculs de ''substitutions explicites''.
== Réductions ==
Une manière de voir les termes du lambda-calcul consiste à les concevoir comme des arbres ayant des nœuds binaires (les applications), des nœuds unaires (les λ-abstractions) et des feuilles (les variables). Les réductions<ref>Attention « réduction » ne veut pas dire que la taille diminue !</ref> ont pour but de modifier les termes, ou les arbres si on les voit ainsi ; par exemple, la réduction de (λx.xx)(λy.y) donne (λy.y)(λy.y).
On appelle ''rédex'' un terme de la forme (<math>\lambda</math>x.u) v. On définit la ''bêta-contraction'' (ou β-contraction) de (<math>\lambda</math>x.u) v comme u[x := v]; on dit qu'un terme ''C[u]'' se réduit<ref>''C[ ]'' est appelé un ''contexte''.</ref> en ''C[u']'' si ''u'' est un redex qui se β-contracte en ''u''', on écrit alors ''C[u]''→''C[u']'', la relation → est appelée ''réduction''.
'''Exemple de réduction''' :
(<math>\lambda</math>x.xy)a donne (xy)[x := a] = ay
On note →<sup>*</sup> la fermeture réflexive transitive<ref>De nombreux auteurs notent cette relation ↠.</ref> de la relation → de réduction et =<sub>β</sub> sa fermeture réflexive symétrique et transitive (appelée ''bêta-conversion'' ou ''bêta-équivalence'').
La β-conversion permet de faire une "marche arrière" à partir d'un terme. Cela permet, par exemple, de retrouver le terme avant une β-réduction. Passer de <math>x</math> à <math>(\lambda y.y)x</math>.
On peut écrire <math> M =_{\beta}M'\mbox{ si }\exists N_{1},...,N_{p}\mbox{ tels que }M = N_{1}, M'=N_{p} \mbox{ et } N_{i} \to N_{i+1} \mbox{ ou } N_{i+1} \to N_{i}</math>
Cela signifie que dans une conversion on peut appliquer des réductions ou des relations inverses des réductions (appelées ''expansions'').
On définit également une autre opération, appelée ''êta-réduction'' (ou son inverse la ''êta-expansion''), définie ainsi : <math>\lambda</math>x.ux →<sub>η</sub> u, lorsque x n'apparaît pas libre dans u. En effet, ''ux'' s'interprète comme l'image de ''x'' par la fonction ''u''. <math>\lambda</math>x.ux s'interprète alors comme la fonction qui, à ''x'', associe l'image de ''x'' par ''u'', donc comme la fonction ''u'' elle-même.
Enfin, si on s'est donné des primitives, on peut fixer leur comportement calculatoire au moyen des règles de ''delta-réduction''.
Par exemple, si on s'est donné les entiers et + comme termes supplémentaires, les tables d'addition serviront de delta-règles. Comme les primitives sont par définition complètement étrangères au lambda-calcul, leurs règles de calcul peuvent a priori adopter
n'importe quelle forme. Toutefois, si on veut étendre les propriétés mentionnées ci-dessous au cas d'un calcul avec des primitives,
on est amené à faire quelques hypothèses sur les règles ajoutées.
== La normalisation : notion de calcul ==
Le calcul associé à un lambda-terme est la suite de réductions qu'il engendre. Le terme est la description du calcul et la ''forme normale'' du terme<ref>Le terme issu de la réduction à partir duquel on ne peut plus réduire.</ref> (si elle existe) en est le résultat.
Un lambda-terme t est dit ''en forme normale'' si aucune bêta-contraction ne peut lui être appliquée, c'est-à-dire si ''t'' ne contient aucun rédex. Ou encore, s'il n'existe aucun lambda-terme u tel que t → u.
'''''Exemple:''''' <math>\lambda x.y(\lambda z.z(yz)) </math>
On dit qu'un lambda-terme ''t'' est ''normalisable'' s'il existe un terme ''u'' tel que ''t =<sub>β</sub> u''. Un tel ''u'' est appelé la ''forme normale'' de ''t''.
On dit qu'un lambda terme ''t'' est ''fortement normalisable'' si toutes les réductions à partir de ''t'' sont ''finies''.
'''''Exemples:'''''
:*Posons <math>\Delta \equiv \lambda x.xx</math>. L'exemple par excellence de lambda-terme non fortement normalisable est obtenu en appliquant ce terme à lui même, autrement dit:
::<math> \Omega = (\lambda x.xx)(\lambda x.xx) = \Delta \Delta</math><br /> Le lambda terme <math>\Omega</math> n'est pas fortement normalisable car sa réduction boucle indéfiniment sur elle-même.
:: <math> (\lambda x.xx)(\lambda x.xx) \to (\lambda x.xx)(\lambda x.xx)</math>.
:* <math>(\lambda x.x)((\lambda y.y)z)</math> est un lambda-terme fortement normalisable.
:* <math>(\lambda x.y)(\Delta \Delta)</math> est normalisable et sa forme normale est <math>y</math>, mais il n'est pas fortement normalisable.
:* <math> (\lambda x.xxx)(\lambda x.xxx) \to (\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\to(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx) \to ...\quad\ </math> crée des termes de plus en plus grand.
Si un terme est fortement normalisable, alors il est normalisable.
'''Théorème de Church-Rosser :''' soient t et u deux termes tels que t =<sub>β</sub> u. Il existe un terme v tel que t →<sup>*</sup> v et u →<sup>*</sup> v.
'''Théorème du losange (ou de confluence) :''' soient t, u<sub>1</sub> et u<sub>2</sub> des lambda-termes tels que t →<sup>*</sup> u<sub>1</sub> et t →<sup>*</sup> u<sub>2</sub>. Alors il existe un lambda-terme v tel que u<sub>1</sub> →<sup>*</sup> v et u<sub>2</sub> →<sup>*</sup> v.
Grâce au ''Théorème de Church-Rosser '' on peut facilement montrer l'unicité de la forme normale ainsi que la cohérence du lambda-calcul (c’est-à-dire qu'il existe au moins deux termes distincts non bêta-convertibles).
== Différents lambda-calculs ==
Sur la syntaxe et la réduction du lambda-calcul on peut adapter différents calculs en restreignant plus ou moins la classe des termes. On peut ainsi distinguer deux grandes classes de lambda-calculs : le lambda-calcul non typé et les lambda-calculs typés. Les types sont des annotations des termes qui ont pour but de ne garder que les termes qui sont normalisables, éventuellement en adoptant une stratégie de réduction. On espère<ref>Espoir fondé en général, mais encore faut-il le démontrer !</ref> ainsi avoir un lambda-calcul qui satisfait les propriétés de Church-Rosser et de normalisation.
La [[correspondance de Curry-Howard]] relie un lambda calcul typé à une système de déduction naturelle. Elle énonce qu'un type correspond à une proposition et un terme correspond à une preuve, et réciproquement.
=== Le lambda-calcul non typé ===
Des codages simulent les objets usuels de l'informatique dont les entiers naturels, les fonctions récursives et les machines de Turing. Réciproquement le lambda-calcul peut être simulé par une machine de Turing. Grâce à la [[thèse de Church]] on en déduit que le lambda-calcul est un modèle universel de calcul.
==== Les booléens ====
Dans la partie Syntaxe, nous avons vu qu'il est pratique de définir des primitives. C'est ce que nous allons faire ici.
::<math>{\rm vrai} = \lambda ab.a </math>
::<math>{\rm faux} = \lambda ab.b </math>
Ceci n'est que la définition d'un codage, et l'on pourrait en définir d'autres.
Nous remarquons que :
::vrai x y →<sup>*</sup> x
et que :
::faux x y →<sup>*</sup> y
Nous pouvons alors définir un lambda-terme représentant l'alternative: ''if-then-else''. C'est une fonction à trois arguments, un booléen <math>b</math> et deux lambda termes <math>u</math> et <math>v</math>, qui retourne le premier si le booléen est vrai et le second sinon.
::<math>{\rm ifthenelse} = \lambda buv.buv</math>
Notre fonction est bien vérifiée:
::<math>{\rm ifthenelse} \; {\rm vrai} \; x \; y = \lambda buv.buv \; {\rm vrai} \; x \; y</math>
::<math>{\rm ifthenelse} \; {\rm vrai} \; x \; y \to \lambda uv.({\rm vrai} \; u \; v) \; x \; y</math>
::<math>{\rm ifthenelse} \; {\rm vrai} \; x \; y \to^{*} {\rm vrai} \; x \; y</math>
::<math>{\rm ifthenelse} \; {\rm vrai} \; x \; y \to^{*} \lambda xy.x \; x \; y</math>
::<math>{\rm ifthenelse} \; {\rm vrai} \; x \; y \to^{*} x </math>
On verra de la même manière que
::ifthenelse faux x y →<sup>*</sup> y
À partir de là nous avons aussi un lambda-terme pour les opérations booléennes classiques :
::non = λb.ifthenelse b faux vrai
::et = λab.ifthenelse a b faux (ou bien λab.ifthenelse a b a)
::ou = λab.ifthenelse a vrai b (ou bien λab.ifthenelse a a b)
==== Les entiers ====
Le codage des entiers qui suit s'appelle les ''entiers de Church'' du nom de leur concepteur. On pose :
::0 = λfx.x
::1 = λfx.f x
::2 = λfx.f (f x)
::3 = λfx.f (f (f x))
et d'une manière générale :
::n = λfx.f (f (...(f x)...)) = λfx.f<sup>n</sup>x avec f itérée n fois.
Ainsi, l'entier n est vu comme la [[fonctionnelle]], qui à au couple ≺f, x≻, associe f<sup>n</sup>(x).
===== Quelques fonctions =====
Il y a deux manières de coder la fonction ''successeur'', soit en ajoutant un f en tête, soit en queue. Au départ nous avons n = λfx.f<sup>n</sup> x et nous voulons λfx.f<sup>n+1</sup> x. Il faut pouvoir rajouter un f soit au début des f « sous » les lambdas soit à la fin.
* Si nous choisissons de le mettre en tête, il faut pouvoir entrer « sous » les lambdas. Pour cela, si n est notre entier, on forme d'abord n f x, ce qui donne f<sup>n</sup> x. En mettant un f en tête, on obtient : f (n f x) → f(f<sup>n</sup> x) = f<sup>n+1</sup> x. Il suffit alors de compléter l'entête pour reconstruire un entier de Church : λfx.f (n f x) = λfx.f<sup>n+1</sup> x (nous aurions bien sûr pu prendre d'autres noms de variables que f et x à l'étape précédente et donc nous aurions gardé ces noms ici). Enfin pour avoir la « fonction » successeur il faut bien entendu prendre un entier en paramètre, donc rajouter un lambda. Nous obtenons λnfx.f(n f x). Le lecteur pourra vérifier que (λnfx.f(n f x)) 3 = 4, avec 3 = λfx.f(f(f x))) et 4 = λfx.f(f(f(f x)))).
* Si par contre nous voulions mettre le f en queue, il suffit d'appliquer n f x non pas à x, mais à f x, à savoir n f (f x), ce qui se réduit à f<sup>n</sup> (f x) = f<sup>n+1</sup> x. On n'a plus qu'à refaire l'emballage comme dans le cas précédent et on obtient λnfx.n f (f x). La même vérification pourra être faite.
Les autres fonctions sont construites avec le même principe. Par exemple l'addition en « concaténant » les deux lambda-termes : λnpfx.n f (p f x).
Pour coder la ''multiplication'', on utilise le f pour « propager » une fonction sur tout le terme : λnpfx.(n (p f) x)
L'''exponentielle'' n'est pas triviale contrairement à ce que son écriture laisse penser, et lors de la réduction on est obligé de renommer les variables : λnp.p n
Le ''prédécesseur'' et la ''soustraction'' ne sont pas simples non plus. On en reparlera plus loin.
On peut définir le test à 0 ainsi :
if0thenelse = λnab.n (λx.b) a,
ou bien en utilisant les booléens λn.n (λx.faux) vrai.
===== Les itérateurs =====
Définissons d'abord une fonction d'itération sur les entiers : itère = λnuv.n u v
v est le cas de base et u une fonction. Si n est nul, on calcule v, sinon on calcule u<sup>n</sup>(v).
Par exemple l'addition qui provient des équations suivantes
* add(0, p) = p
* add(n+1, p) = (n+p) + 1
peut être définie comme suit. Le cas de base v est le nombre p, et la fonction u est la fonction successeur. Le lambda-terme correspondant au calcul de la somme est donc :
:add = λnp.itère n successeur p
On remarquera que add n p →<sup>*</sup> n successeur p.
==== Les couples ====
On peut coder des couples par c = λz.z a b où a est le premier élément et b le deuxième. On notera ce couple (a,b).
Pour accéder aux deux parties on utilise π<sub>1</sub> = λc.c (λab.a) et π<sub>2</sub> = λc.c (λab.b). On reconnaîtra les booléens ''vrai'' et ''faux'' dans ces expressions et on laissera le soin au lecteur de réduire π<sub>1</sub>(λz.z a b) en a.
==== Les listes ====
On peut remarquer qu'un entier est une liste dont on ne regarde pas les éléments, en ne considérant donc que la longueur. En rajoutant une information correspondant aux éléments, on peut construire les listes d'une manière analogue aux entiers : [a<sub>1</sub> ; ... ; a<sub>n</sub>] = λgy. g a<sub>1</sub> (... (g a<sub>n</sub> y)...). Ainsi :
::[] = λgy.y
::[a<sub>1</sub>] = λgy.g a<sub>1</sub> y
::[a<sub>1</sub> ; a<sub>2</sub>] = λgy.g a<sub>1</sub> (g a<sub>2</sub> y)
===== Les itérateurs sur les listes =====
De la même manière qu'on a introduit une itération sur les entiers on introduit une itération sur les listes. la fonction liste_it se définit par λlxm.l x m comme pour les entiers.
Le concept est à peu près le même mais il y a des petites nuances. Nous allons voir par un exemple.
'''exemple :'''
La longueur d'une liste est définie par
* longueur ([]) = 0
* longueur (x :: l) = 1 + longueur l
x :: l est la liste de tête x et de queue l (notation [[ML]]).
La fonction longueur appliquée sur une liste l se code par :
::λl.liste_it l (λym.add (λfx.f x) m) (λfx.x)
ou tout simplement
::λl.l (λym.add 1 m) 0
==== Les arbres binaires ====
Le principe de construction des entiers, des couples et des listes se généralise aux arbres binaires :
* constructeur de feuille : feuille = λngy.y n
* constructeur de nœud : nœud = λbcgy.g (b g y) (c g y) (avec b et c des arbres binaires)
* itérateur : arbre_it = λaxm.a x m
Un arbre est soit une feuille, soit un nœud. Dans ce modèle, aucune information n'est stockée au niveau des nœuds, les données (ou clés) sont conservées au niveau des feuilles uniquement.
On peut alors définir la fonction qui calcule le nombre de feuilles d'un arbre :
nb_feuilles = λa.arbre_it a (λbc.add b c) (λn.1), ou plus simplement: nb_feuilles = λa.a add (λn.1)
==== Le prédécesseur ====
Pour définir le prédécesseur sur les entiers de Church, il faut utiliser les couples. L'idée est de reconstruire le prédécesseur par itération :
pred = λn.π<sub>1</sub> (itère n (λc.(π<sub>2</sub> c,successeur (π<sub>2</sub> c))) (0,0)).
Puisque le prédécesseur sur les entiers naturels n'est pas défini en 0, afin de définir une fonction totale, on a ici adopté la convention qu'il vaut 0.
On vérifie par exemple que
pred 3 →<sup>*</sup> π<sub>1</sub> (itère 3 (λc.(π<sub>2</sub> c,successeur (π<sub>2</sub> c))) (0,0))
→<sup>*</sup> π<sub>1</sub> (2,3) →<sup>*</sup> 2.
On en déduit que la soustraction est définissable par :
sub = λnp.itère p pred n
avec la convention que si p est plus grand que n, alors sub n p vaut 0.
==== La récursion ====
En combinant prédécesseur et itérateur, on obtient un ''récurseur''. Celui-ci se distingue de l'itérateur par le fait que
la fonction qui est passée en argument a accès au prédécesseur.
rec = λnfx.π<sub>1</sub> (n (λc.(f (π<sub>2</sub> c) (π<sub>1</sub> c),successeur (π<sub>2</sub> c))) (x,0))
==== Combinateur de point fixe ====
Un combinateur de point fixe permet de construire pour chaque ''F'', une solution à l'équation ''X = F X'' . Ceci est pratique pour programmer des fonctions qui ne s'expriment pas simplement par itération, telle que le pgcd, et c'est surtout nécessaire pour programmer des fonctions partielles.
Le combinateur de point de fixe le plus simple, dû à Curry, est :
Y = λf.(λx.f(x x))(λx.f(x x))
On vérifie que <math>Y\ g\ =_\beta\ g(Y\ g)</math> quelque soit g. Grâce au combinateur de point fixe, on peut par exemple définir
une fonction qui prend en argument une fonction et teste si cette fonction argument renvoie vrai pour au moins un entier:
teste_annulation = λg.Y (λfn.ou (g n) (f (successeur n))) 0.
Par exemple, si on définit la suite alternée des booléens ''vrai'' et ''faux'' :
alterne = λn.itère n non faux,
alors, on vérifie que :
teste_annulation alterne →<sup>*</sup> ou (alterne 0) (Y (λfn.ou (alterne n) (f successeur n)) (successeur 0))
→<sup>*</sup> ou (alterne 1) (Y (λfn.ou (alterne n) (f successeur n)) (successeur 1))
→<sup>*</sup> vrai.
On peut aussi définir le pgcd :
pgcd = Y (λfnp.if0thenelse (sub p n) (if0thenelse (sub n p) p (f p (sub n p))) (f n (sub p n))).
==== Connexion avec les fonctions partielles récursives ====
Le récurseur et le point fixe sont des ingrédients clés permettant de montrer que toute [[fonction partielle récursive]] est définissable en λ-calcul lorsque les entiers sont interprétés par les entiers de Church. Réciproquement, les λ-termes peuvent être codés par des entiers et la réduction des λ-termes est définissable comme une fonction (partielle) récursive. Le λ-calcul est donc un modèle de la [[calculabilité]]
=== Le lambda-calcul simplement typé ===
On annote les termes par des expressions que l'on appelle des ''types'' ; pour cela on fournit un moyen de donner un type à un terme, si ce moyen réussit on dit que le terme est '''bien typé'''. Outre le fait que cela donne une indication sur ce que « fait » la fonction, par exemple, elle transforme les objets d'un certain type en des objets d'un autre type, cela permet de garantir la '''normalisation forte''', c'est-à-dire que pour tous les termes, toutes les réductions aboutissent à une forme normale (qui est unique pour chaque terme de départ). Autrement dit, tous les calculs menés dans ce contexte terminent. Les '''types simples''' sont construits comme les types des fonctions, de fonctions de fonctions, des fonctions de fonctions de fonctions vers les fonctions etc. Quoiqu'il puisse paraitre, le pouvoir expressif de ce calcul est très limité (ainsi, l'exponentielle ne peut y être définie, ni même la fonction <math>n\rightarrow 2^n</math>).
Plus formellement, les types simples sont construits de la manière suivante:
* un type de base <math>\iota</math> (si on a des primitives, on peut aussi se donner plusieurs types de bases, comme les entiers, les booléens, les caractères, etc. mais cela n'a pas d'incidence au niveau de la théorie).
* si <math>\tau_1</math> et <math>\tau_2</math> sont des types, <math>\tau_1\rightarrow\tau_2</math> est un type.
Intuitivement, le second cas représente le type des fonctions acceptant un élément de type <math>\tau_1</math> et renvoyant un élément de type
<math>\tau_2</math>.
Un contexte <math>\Gamma</math> est un ensemble de paires de la forme <math>(x,\tau)</math> où <math>x</math> est une variable et <math>\tau</math> un type. Un jugement de typage est un triplet <math>\Gamma\vdash t:\tau</math> (on dit alors que <math>t</math> est bien typé dans <math>\Gamma</math>), défini récursivement par:
* si <math>(x,\tau)\in\Gamma</math>, alors <math>\Gamma\vdash x:\tau</math>.
* si <math>\Gamma\cup (x,\tau_1)\vdash u:\tau_2</math>, alors <math>\Gamma\vdash \lambda x\!:\!\tau_1.u\,:\,\tau_1\rightarrow\tau_2</math>.
* si <math>\Gamma\vdash u:\tau_1\rightarrow\tau_2</math> et <math>\Gamma\vdash v:\tau_1</math>, alors <math>\Gamma\vdash u v:\tau_2</math>
Si on a ajouté des constantes au lambda calcul, il faut leur donner un type (via <math>\Gamma</math>).
=== Les lambda-calculs typés d'ordres supérieurs ===
Le lambda-calcul simplement typé est trop restrictif pour exprimer toutes les fonctions [[calculabilité | calculable]]s dont on a besoin en mathématiques et donc dans un programme informatique. Un moyen de dépasser l'expressivité du lambda-calcul simplement typé consiste à autoriser des variables de type et à quantifier sur elles, comme cela est fait dans le [[système F]] ou le [[calcul des constructions]]. Le [[Système T]] de [[Kurt Gödel|Gödel]] qui fusionne la [[Fonction récursive primitive|récursion primitive]] et le lambda-calcul simplement typé offre aussi, au prix d'un enrichissement, un système plus expressif. Dans ce système, on peut coder, grâce à l'ordre supérieur, de nouveaux algorithmes comme la [[fonction d'Ackermann]] qui est non primitive récursive.
== Notes ==
<references />
== Bibliographie ==
* {{en}} [[Henk Barendregt]], ''The Lambda-Calculus'', volume 103, Elsevier Science Publishing Company, Amsterdam, 1984.
* [[Jean-Louis Krivine]], ''Lambda-Calcul, types et modèles'', Masson 1991.
* {{en}} [[Steven Fortune]], [[Daniel Leivant]], [[Michael O'Donnell]], « The Expressiveness of Simple and Second-Order Type Structures » dans ''Journal of the ACM'' vol. 30 (1983), p. 151-185.
* {{en}} [[Jean-Yves Girard]], [[Paul Taylor (mathématicien)|Paul Taylor]], [[Yves Lafont]], ''[http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html Proofs and Types]'', Cambridge University Press, New York, 1989 {{ISBN|0-521-37181-3}}.
* [[Hervé Poirier]], « La Vraie Nature de l'intelligence », dans ''Science et Vie'' {{numéro}}1013 (février 2002), p. 38-57.
* [[Francis Renaud (linguiste)|Francis Renaud]], Sémantique du temps et lambda-calcul, [[Presses Universitaires de France]], 1996 {{ISBN|2-13-047709 7}}
{{Portail|informatique|logique}}
[[Catégorie:Calculabilité]]
[[Catégorie:Théorie des types]]
[[bn:ল্যাম্ডা ক্যালকুলাস]]
[[ca:Càlcul lambda]]
[[cs:Lambda kalkul]]
[[de:Lambda-Kalkül]]
[[el:Λογισμός λάμδα]]
[[en:Lambda calculus]]
[[eo:Lambda-abstraktado]]
[[es:Cálculo lambda]]
[[he:תחשיב למבדא]]
[[hr:Lambda račun]]
[[hu:Lambda-kalkulus]]
[[it:Lambda calcolo]]
[[ja:ラムダ計算]]
[[nl:Lambdacalculus]]
[[pl:Rachunek lambda]]
[[pt:Cálculo lambda]]
[[ru:Лямбда-исчисление]]
[[simple:Lambda calculus]]
[[sk:Lambda kalkul]]
[[sv:Lambdakalkyl]]
[[uk:Лямбда-числення]]
[[zh:Λ演算]]