Lambda-calcul simplement typé

Le lambda-calcul simplement typé est une variante du lambda-calcul qui se différencie de ce dernier par la présence de types. Il a été développé par Alonzo Church pour pallier l'incohérence du lambda-calcul non typé, due au paradoxe de Curry, et servir de fondements aux mathématiques.

Le lambda-calcul simplement typé partage un lien fort avec la logique propositionnelle minimale au travers de l'isomorphisme de Curry-Howard^[1]. Il peut également être vu comme une version simplifiée d'un langage de programmation fonctionnelle. De plus, toutes les fonctions définissables dans le lambda-calcul simplement typé terminent : le lambda-calcul simplement typé est fortement normalisant.

Le lambda-calcul pose comme primitive la notion de fonction. Si ${\displaystyle M}$ est une expression, ${\displaystyle \lambda x.M}$ représente la fonction ${\displaystyle f}$ définie par l'équation ${\displaystyle f(x)=M}$, et si ${\displaystyle M}$ et ${\displaystyle N}$ sont deux expressions, ${\displaystyle MN}$ désigne l'application de ${\displaystyle M}$ à ${\displaystyle N}$. Enfin, le lambda-calcul possède une notion dite de réduction qui correspond à effectuer une étape de calcul.

Par analogie, ${\displaystyle \lambda x.2x}$ pourrait désigner la fonction qui renvoie le double de son argument, et ${\displaystyle (\lambda x.2x)3\to 2\cdot 3\to 6}$ est la suite des étapes de calcul pour calculer cette fonction en ${\displaystyle 3}$. On peut définir et utiliser des types de données dans le lambda-calcul, notamment les entier naturels, les paires ou les listes. Néanmoins, tous les calculs ne terminent pas : ${\displaystyle \Omega =(\lambda x.xx)(\lambda x.xx)}$ présente la propriété que ${\displaystyle \Omega \to \Omega }$, et de plus, si ${\displaystyle F}$ est un terme, il existe un terme ${\displaystyle M}$ tel que ${\displaystyle FM\to ^{*}M}$. Pour reprendre l'analogie précédente, pour ${\displaystyle F=\lambda x.x+1}$, un tel ${\displaystyle M}$ vérifierait ${\displaystyle M=M+1}$, ce qui est impossible pour un entier naturel. L'introduction d'une discipline de types permet de résoudre ces deux problèmes, au prix d'une expressivité moindre.

Il y a deux sortes d'objets dans le lambda-calcul simplement typé : les types, qui correspondent à des types de donnée en informatique et à des propositions en logique, et les termes qui correspondent à des programmes ou à des démonstrations. On notera ${\displaystyle \lambda ^{\to }}$ ce système.

On suppose donné un ensemble de variables de types, qu'on note par des lettres grecques ${\displaystyle \alpha ,\beta ,\dots }$ Les types du lambda-calcul simplement typé sont désignés par les lettres ${\displaystyle T,U,\dots }$ et sont formés par^[2],[3] :

• les variables de types ${\displaystyle \alpha ,\beta ,\ldots }$ ;
• si ${\displaystyle T}$ et ${\displaystyle U}$ sont des types, ${\displaystyle T\to U}$ est le type des fonctions de ${\displaystyle T}$ vers ${\displaystyle U}$.

Les variables seront notées par des lettres minuscules ${\displaystyle x,y,\dots }$ tandis que les termes seront notés ${\displaystyle M,N,\dots }$ Les termes sont formés ainsi^[2],[3] :

• Les variables ${\displaystyle x,y,\ldots }$ sont des termes ;
• Si ${\displaystyle A}$ est un type et ${\displaystyle M}$ un terme, ${\displaystyle \lambda x^{A}.M}$ est un terme qui représente la fonction qui à ${\displaystyle x}$ de type ${\displaystyle A}$ associe l'expression ${\displaystyle M}$. On peut voir ça comme l'abstraction de ${\displaystyle x}$ dans l'expression ${\displaystyle M}$ ;
• Si ${\displaystyle M}$ et ${\displaystyle N}$ sont des termes, ${\displaystyle MN}$ est un terme qui correspond à l'application de la fonction ${\displaystyle M}$ à l'expression ${\displaystyle N}$.

De plus, on considèrera que l'application est associative à gauche, c'est-à-dire qu'on notera ${\displaystyle MNO}$ pour ${\displaystyle (MN)O}$.

On introduit la notation ${\displaystyle \Gamma \vdash M:A}$^[2], où ${\displaystyle \Gamma }$ est une liste de paires de la forme ${\displaystyle x:B}$ où ${\displaystyle x}$ est une variable et ${\displaystyle B}$ un type, ${\displaystyle M}$ est un terme et ${\displaystyle A}$ un type. Elle se lit « dans le contexte ${\displaystyle \Gamma }$, le terme ${\displaystyle M}$ a pour type ${\displaystyle A}$ ». Par exemple, ${\displaystyle f:A\to B\vdash \lambda y:A.fx:A\to B}$ se lit « si ${\displaystyle f}$ est une variable de type ${\displaystyle A\to B}$, la fonction qui à ${\displaystyle x}$ de type ${\displaystyle A}$ associe la valeur ${\displaystyle fx}$ est une fonction qui envoie les éléments de ${\displaystyle A}$ dans ${\displaystyle B}$ ».

Une règle de la forme ${\displaystyle {\frac {\Gamma _{1}\vdash M_{1}:A_{1}\dots \Gamma _{n}\vdash M_{n}:A_{n}}{\Gamma \vdash M:A}}}$ doit se comprendre comme « si ${\displaystyle \Gamma _{1}\vdash M_{1}:A_{1}}$, ..., ${\displaystyle \Gamma _{n}\vdash M_{n}:A_{n}}$alors ${\displaystyle \Gamma \vdash M:A}$ ». En particulier, ${\displaystyle {\frac {}{\Gamma \vdash M:A}}}$ signifie que ${\displaystyle \Gamma \vdash M:A}$ est toujours vrai.

${\displaystyle (var)\;{\frac {}{\Gamma ,x:A,\Gamma '\vdash x:A}}}$
${\displaystyle (abs)\;{\frac {\Gamma ,x:A\vdash M:B}{\Gamma \vdash \lambda x^{A}.M:A\to B}}}$	${\displaystyle (app)\;{\frac {\Gamma \vdash M:A\to B\quad \Gamma \vdash N:A}{\Gamma \vdash MN:B}}}$

Le lambda-calcul présenté ici correspond, sous la correspondance de Curry-Howard, à la logique minimale.

La présentation ici donnée correspond au typage à la Church^[4], ou typage explicite, c'est-à-dire qu'un terme donné a au plus un seul type. Il existe une autre façon de présenter le lambda-calcul simplement typé, c'est le typage à la Curry^[4], ou typage implicite. Les règles de typage restent les mêmes, mais les termes sont ceux du lambda-calcul pur : notamment, l'abstraction se note ${\displaystyle \lambda x.M}$. Par exemple, avec un typage à la Church, ${\displaystyle \lambda x^{A}.x}$ a pour type ${\displaystyle A\to A}$, tandis qu'avec un typage à la Curry, ${\displaystyle \lambda x.x}$ a tous les types de la forme ${\displaystyle T\to T}$. L'opération qui consiste à trouver le type le plus général qui convient pour un lambda-terme donné, si un tel type existe, s'appelle l'inférence de types^[5].

Tout comme le lambda-calcul non typé, le lambda-calcul simplement typé identifie les termes ${\displaystyle \alpha }$-équivalents et définit la substitution de façon similaire. De même, on peut définir pour le lambda-calcul simplement typé une notion de réduction^[6], qui correspond à une opération de réécriture représentant une étape de calcul :

• ${\displaystyle (\lambda x.M)N\to _{\beta }M[x:=N]}$ ;
• ${\displaystyle \lambda x.Mx\to _{\eta }M}$ si ${\displaystyle x}$ n'est pas libre dans ${\displaystyle M}$ ;

Une des règles est étiquetée ${\displaystyle \beta }$, elle correspond à une règle de calcul. La réduction associée est nommée ${\displaystyle \beta }$-réduction. L'autre est étiquetée ${\displaystyle \eta }$, elle correspond à une simplifications : si ${\displaystyle M\to _{\eta }N}$, ${\displaystyle M}$ et ${\displaystyle N}$ se « comportent » pareil. On nomme cette réduction ${\displaystyle \eta }$-réduction. On note ${\displaystyle M\to _{\beta \eta }N}$ si ${\displaystyle M\to _{\beta }N}$ ou ${\displaystyle M\to _{\eta }N}$ : c'est la ${\displaystyle \beta \eta }$-réduction.

Enfin, si ${\displaystyle \to _{R}}$ est une réduction, ${\displaystyle \to _{R}^{*}}$ est sa clôture réflexive et transitive et ${\displaystyle =_{R}}$ sa clôture réflexive, symétrique et transitive, c'est-à-dire que ${\displaystyle M\to _{R}^{*}N}$ s'il existe ${\displaystyle M_{1},\ldots ,M_{n}}$ tels que ${\displaystyle M=M_{1}\to _{R}\ldots \to _{R}M_{n}=N}$ et ${\displaystyle M=_{R}N}$ s'il existe ${\displaystyle M_{1},\ldots ,M_{n}}$ tels que ${\displaystyle M=M_{1}}$, ${\displaystyle M_{n}=N}$ et pour tout ${\displaystyle i}$ entre ${\displaystyle 1}$ et ${\displaystyle n-1}$, ${\displaystyle M_{i}\to _{R}M_{i+1}}$ ou ${\displaystyle M_{i}\leftarrow _{R}M_{i+1}}$.

La ${\displaystyle \beta \eta }$-réduction possède la propriété de préservation du typage^[6] (en anglais : subject reduction) : si ${\displaystyle \Gamma \vdash M:T}$ et ${\displaystyle M\to _{\beta \eta }N}$ alors ${\displaystyle \Gamma \vdash N:T}$.

Un terme est dit en forme normale s'il ne peut pas se réduire d'avantage^[7]. La ${\displaystyle \beta \eta }$-réduction possède la propriété de normalisation forte^[8], c'est-à-dire que tous les termes sont fortement normalisables : il n'y a pas de suite infinie de réductions ${\displaystyle M_{0}\to M_{1}\to \dots }$ Ainsi tout terme peut, en un nombre fini (potentiellement nul) d'étapes, être réduit en une forme normale. On dit aussi que la réduction est fortement normalisante. Si ${\displaystyle M\to _{R}^{*}N}$ et que ${\displaystyle N}$ est en forme normale pour ${\displaystyle \to _{R}}$, on dit que ${\displaystyle N}$ est une ${\displaystyle R}$-forme normale de ${\displaystyle M}$. Comme l’énonce le paragraphe suivant, cette forme est unique pour la ${\displaystyle \beta \eta }$-réduction et la ${\displaystyle \beta }$-réduction.

Une réduction est dite confluente si pour tous termes ${\displaystyle M}$, ${\displaystyle N_{1}}$ et ${\displaystyle N_{2}}$ tels que ${\displaystyle M\to ^{*}N_{1}}$ et ${\displaystyle M\to ^{*}N_{2}}$, il existe un terme ${\displaystyle O}$ tel que ${\displaystyle N_{1}\to ^{*}O}$ et ${\displaystyle N_{2}\to ^{*}O}$. La ${\displaystyle \beta \eta }$-réduction et la ${\displaystyle \beta }$-réduction sont confluentes^[9].

La confluence assure l'unicité de la forme normale pour la réduction : en effet, supposons ${\displaystyle M\to ^{*}N_{1}}$ et ${\displaystyle M\to ^{*}N_{2}}$ avec ${\displaystyle N_{1}}$ et ${\displaystyle N_{2}}$ en forme normale. Si ${\displaystyle N_{1}\to ^{*}O}$ alors ${\displaystyle N_{1}=O}$ puisque ${\displaystyle N_{1}}$ ne peut pas se réduire. De même, si ${\displaystyle N_{2}\to ^{*}O}$ alors ${\displaystyle N_{2}=O}$. Donc ${\displaystyle N_{1}=N_{2}}$.

Cela signifie qu'en partant d'un terme donné, l'ordre des ${\displaystyle \beta }$-réductions n'importe pas : quel que soit l'ordre de réduction choisi, en un nombre fini d'étapes, on atteindra une forme normale qui ne dépend pas de l'ordre des réductions. En revanche, l'ordre de réduction peut avoir une influence sur le nombre de réductions. Par exemple, si ${\displaystyle y:A,t:B\vdash (\lambda x^{B}.y)((\lambda z^{B}.z)t)}$, alors ${\displaystyle (\lambda x^{B}.y)((\lambda z^{B}.z)t)\to y}$ atteint une forme normale en une étape en réduisant d'abord le premier rédex, tandis que ${\displaystyle (\lambda x^{B}.y)((\lambda z^{B}.z)t)\to (\lambda x^{B}.y)t\to y}$ atteint la même forme normale en deux étapes, en réduisant d'abord le deuxième rédex.

De plus, on peut choisir de faire les ${\displaystyle \eta }$-réductions après les ${\displaystyle \beta }$-réductions ou bien faire les ${\displaystyle \beta }$-réductions après les ${\displaystyle \eta }$-réductions : si ${\displaystyle M\to _{\eta }N\to _{\beta }O}$, alors le ${\displaystyle \beta }$-rédex réduit dans la deuxième réduction était déjà présent dans ${\displaystyle M}$, et si ${\displaystyle M}$ est en ${\displaystyle \beta }$-forme normale, il existe un terme ${\displaystyle N}$ (non nécessairement unique) en ${\displaystyle \beta \eta }$-forme normale tel que ${\displaystyle M\to _{\eta }^{*}N}$^[9].

On peut étendre la présentation précédente du lambda-calcul avec un typé unité et des produits de types^[2], on le note alors ${\displaystyle \lambda ^{\to ,\times ,1}}$. On ajoute alors aux types un type unité ${\displaystyle 1}$, qui possède un unique élément, et ${\displaystyle T}$ et ${\displaystyle U}$ sont des types, on ajoute le type ${\displaystyle T\times U}$ qui représente le produit des types ${\displaystyle T}$ et ${\displaystyle U}$, dont les éléments sont des paires composées d'un élément de ${\displaystyle T}$ et d'un de ${\displaystyle U}$.

De plus, on étend la syntaxe des termes :

• L'unique terme du type unité, se note ${\displaystyle *}$ ;
• Si ${\displaystyle M}$ et ${\displaystyle N}$ sont des termes, le terme ${\displaystyle \langle M,N\rangle }$, représente la paire dont la première composante est ${\displaystyle M}$ et la deuxième ${\displaystyle N}$ ;
• Si ${\displaystyle M}$ est un terme et ${\displaystyle i=1~{\textrm {ou}}~2}$, la ${\displaystyle i}$-ème projection de la paire ${\displaystyle M}$ se note ${\displaystyle \pi _{i}(M)}$.

Les règles de typages correspondantes sont^[2] :

${\displaystyle (pair)\;{\frac {\Gamma \vdash M:A\quad \Gamma \vdash N:B}{\Gamma \vdash \langle M,N\rangle :A\times B}}}$	${\displaystyle (\pi _{1})\;{\frac {\Gamma \vdash M:A\times B}{\Gamma \vdash \pi _{1}(M):A}}}$	${\displaystyle (\pi _{2})\;{\frac {\Gamma \vdash M:A\times B}{\Gamma \vdash \pi _{2}(M):B}}}$
${\displaystyle (*)\;{\frac {}{\Gamma \vdash *:1}}}$

On peut également ajouter des règles de calcul sur les produits^[6], à savoir :

• ${\displaystyle \pi _{1}(\langle M,N\rangle )\to _{\beta }M}$ ;
• ${\displaystyle \pi _{2}(\langle M,N\rangle )\to _{\beta }N}$.

Il est aussi possible d'ajouter des règles ${\displaystyle \eta }$ à ce lambda-calcul^[6] :

• ${\displaystyle \langle \pi _{1}x,\pi _{2}x\rangle \to _{\eta }x}$ ;
• ${\displaystyle M\to _{\eta }*}$ si ${\displaystyle M}$ est de type ${\displaystyle 1}$.

Mais celles-ci ne se comportent pas aussi bien que dans le cas sans type unité. En effet, si la ${\displaystyle \beta }$-réduction reste confluente^[9], la ${\displaystyle \beta \eta }$-réduction ne l'est plus, comme le montre l'exemple suivant^[9], où ${\displaystyle x:A\times 1}$ :

• ${\displaystyle \langle \pi _{1}x,\pi _{2}x\rangle \to _{\eta }\langle \pi _{1}x,*\rangle }$ ;
• ${\displaystyle \langle \pi _{1}x,\pi _{2}x\rangle \to _{\eta }x}$ ;
• mais ${\displaystyle \langle \pi _{1}x,*\rangle }$ et ${\displaystyle x}$ sont tous deux en forme normale, donc ils ne peuvent pas se réduire vers un terme commun.

En revanche toutes ces réductions continuent à préserver le typage^[6] et à être fortement normalisantes^[8].

On peut également introduire dans le lambda-calcul simplement typé des types représentant respectivement la proposition toujours fausse ou le type vide, ainsi que la disjonction de deux propositions ou la somme de deux types^[10],[11]. Pour cela, on ajoute à la syntaxe le type ${\displaystyle 0}$, et si ${\displaystyle T}$ et ${\displaystyle U}$ sont deux types, ${\displaystyle T+U}$ aussi. Le type ${\displaystyle T+U}$ peut être vu comme des couples ${\displaystyle (e,M)}$ avec ${\displaystyle M}$ dans ${\displaystyle T}$ ou dans ${\displaystyle U}$ et ${\displaystyle e}$ une étiquette indiquant la provenance de ${\displaystyle M}$ : ${\displaystyle T}$ ou ${\displaystyle U}$. Ce système se note ${\displaystyle \lambda ^{\to ,\times ,1,+,0}}$.

De plus, on ajoute à la syntaxe les termes suivants :

• Si ${\displaystyle T}$ est un type et ${\displaystyle M}$ un terme, ${\displaystyle \square _{T}M}$ est un terme, qui sera de type ${\displaystyle T}$. En effet, si ${\displaystyle 0}$ possède un élément, tous les autres types aussi.
• Si ${\displaystyle T}$ et ${\displaystyle U}$ sont des types, et ${\displaystyle M}$ un terme, ${\displaystyle \operatorname {inl} _{T,U}M}$ et ${\displaystyle \operatorname {inr} _{T,U}M}$ sont des termes correspondant aux injections respectives de ${\displaystyle T}$ et ${\displaystyle U}$ dans ${\displaystyle T+U}$.
• Si ${\displaystyle T}$ et ${\displaystyle U}$ sont des types, ${\displaystyle M}$, ${\displaystyle N}$ et ${\displaystyle O}$ des termes, alors ${\displaystyle \operatorname {case} M\operatorname {of} x^{T}\Rightarrow N\mid y^{U}\Rightarrow O}$ est un terme qui correspond à un filtrage par motif.

Ces nouveaux termes se typent comme suit :

${\displaystyle (\operatorname {inl} )\;{\frac {\Gamma \vdash M:T}{\Gamma \vdash \operatorname {inl} _{T,U}M:T+U}}}$	${\displaystyle (\operatorname {inr} )\;{\frac {\Gamma \vdash M:U}{\Gamma \vdash \operatorname {inr} _{T,U}M:T+U}}}$	${\displaystyle (\operatorname {case} )\;{\frac {\Gamma \vdash M:T+U\quad \Gamma ,x:T\vdash N:V\quad \Gamma ,y:U\vdash O:V}{\Gamma \vdash \operatorname {case} M\operatorname {of} x^{T}\Rightarrow N\mid y^{U}\Rightarrow O:V}}}$
${\displaystyle (\square )\;{\frac {\Gamma \vdash M:0}{\Gamma \vdash \square _{T}M:T}}}$

On peut également ajouter des règles de réduction^[11], mais il faut ajouter un nouveau type de règles : les conversions commutatives, notées ${\displaystyle \to _{cc}}$. Elles permettent d'identifier deux termes qui devraient désigner la même preuve, mais sont différents.

Les deux règles ${\displaystyle \beta }$ correspondent au calcul du filtrage : si ${\displaystyle M}$ provient de ${\displaystyle T}$, on renvoie ${\displaystyle N}$ où ${\displaystyle x}$ est remplacé par ${\displaystyle M}$, et on fait de même avec ${\displaystyle O}$ et ${\displaystyle y}$ si ${\displaystyle M}$ provient de ${\displaystyle U}$ :

• ${\displaystyle \operatorname {case} \operatorname {inl} _{T,U}M\operatorname {of} x^{T}\Rightarrow N\mid y^{U}\Rightarrow O\to _{\beta }N[x:=M]}$ ;
• ${\displaystyle \operatorname {case} \operatorname {inr} _{T,U}M\operatorname {of} x^{T}\Rightarrow N\mid y^{U}\Rightarrow O\to _{\beta }O[y:=M]}$.

Les cinq règles suivantes ${\displaystyle cc}$ correspondent aux conversions commutatives pour ${\displaystyle 0}$ :

• ${\displaystyle \pi _{1}(\square _{T\times U}M)\to _{cc}\square _{T}M}$ ;
• ${\displaystyle \pi _{2}(\square _{T\times U}M)\to _{cc}\square _{U}M}$ ;
• ${\displaystyle (\square _{T\to U}M)N\to _{cc}\square _{U}M}$ ;
• ${\displaystyle \square _{T}(\square _{0}M)\to _{cc}\square _{T}M}$ ;
• Si ${\displaystyle N}$ et ${\displaystyle O}$ sont de type ${\displaystyle V}$, ${\displaystyle \operatorname {case} \square _{T+U}M\operatorname {of} x^{T}\Rightarrow N\mid y^{U}\Rightarrow O\to _{cc}\square _{V}M}$.

Ces cinq règles ${\displaystyle cc}$ correspondent aux conversions commutatives pour la somme :

• ${\displaystyle \pi _{1}(\operatorname {case} M\operatorname {of} x^{T}\Rightarrow N\mid y^{U}\Rightarrow O)\to _{cc}\operatorname {case} M\operatorname {of} x^{T}\Rightarrow \pi _{1}(N)\mid y^{U}\Rightarrow \pi _{1}(O)}$;
• ${\displaystyle \pi _{2}(\operatorname {case} M\operatorname {of} x^{T}\Rightarrow N\mid y^{U}\Rightarrow O)\to _{cc}\operatorname {case} M\operatorname {of} x^{T}\Rightarrow \pi _{2}(N)\mid y^{U}\Rightarrow \pi _{2}(O)}$;
• ${\displaystyle (\operatorname {case} M\operatorname {of} x^{T}\Rightarrow N\mid y^{U}\Rightarrow O)P\to _{cc}\operatorname {case} M\operatorname {of} x^{T}\Rightarrow NP\mid y^{U}\Rightarrow OP}$ ;
• ${\displaystyle \square _{W}(\operatorname {case} M\operatorname {of} x^{T}\Rightarrow N\mid y^{U}\Rightarrow O)\to _{cc}\operatorname {case} M\operatorname {of} x^{T}\Rightarrow \square _{W}N\mid y^{U}\Rightarrow \square _{W}O}$ ;
• ${\displaystyle {\begin{array}{l}\operatorname {case} (\operatorname {case} M\operatorname {of} x^{T}\Rightarrow N\mid y^{U}\Rightarrow O)\\\operatorname {of} x'^{T}\Rightarrow N'\mid y'^{U}\Rightarrow O'\\\end{array}}\to _{cc}{\begin{array}{l}\operatorname {case} M\operatorname {of} \\\quad x^{T}\Rightarrow (\operatorname {case} N\operatorname {of} x'^{T}\Rightarrow N'\mid y'^{U}\Rightarrow O')\\\quad y^{U}\Rightarrow (\operatorname {case} O\operatorname {of} x'^{T}\Rightarrow N'\mid y'^{U}\Rightarrow O')\\\end{array}}}$.

Enfin, on peut aussi définir des règles ${\displaystyle \eta }$ : la première règle ${\displaystyle \eta }$ correspond à ${\displaystyle 0}$, la deuxième à la somme.

• ${\displaystyle \square _{0}M\to _{\eta }M}$ ;
• ${\displaystyle \operatorname {case} M\operatorname {of} x^{T}\Rightarrow \operatorname {inl} _{T,U}x\mid y^{U}\Rightarrow \operatorname {inr} _{T,U}\to _{\eta }M}$.

Les réductions ${\displaystyle \to _{\beta cc}}$ et ${\displaystyle \to _{\beta cc\eta }}$ préservent le typage et sont fortement normalisantes. De plus, ${\displaystyle \to _{\beta cc}}$ est confluente.

Les règles de typage du lambda-calcul simplement typé correspondent, une pour une, aux règles^[12],[13] d'introductions et d'éliminations de la déduction naturelle pour la logique intuitionniste^[14]. Cela permet d'établir une correspondance formelle entre preuves et programmes. Par exemple, les règles de l'implication en déduction naturelle sont :

${\displaystyle (I_{\to })\;{\frac {\begin{array}{c}[A]\\\vdots \\B\\\end{array}}{A\to B}}}$

${\displaystyle (E_{\to })\;{\frac {A\to B\quad A}{B}}}$

où ${\displaystyle [A]}$ signifie que l'on « charge » l'hypothèse ${\displaystyle A}$, c'est-à-dire qu'on a le droit de l'utiliser comme hypothèse uniquement au-dessus de la barre.

C'est encore plus flagrant si l'on considère la présentation de la déduction naturelle avec des séquents, qui correspond exactement aux règles du lambda-calcul dans lesquelles on a enlevé les termes et les variables pour ne garder que les types.

${\displaystyle (I_{\to })\;{\frac {\Gamma ,A\vdash B}{\Gamma \vdash A\to B}}}$

${\displaystyle (E_{\to })\;{\frac {\Gamma \vdash A\to B\quad \Gamma \vdash A}{\Gamma \vdash B}}}$

En déduction naturelle, il existe une notion de simplification des preuves, appelée élimination des coupures^{[15],[16],[17]}. Une coupure correspond à une règle d'introduction immédiatement suivie de la règle d'élimination correspondante. La procédure d'élimination des coupures correspond exactement à la relation ${\displaystyle \to _{\beta cc}}$^[18], permettant de faire le lien entre un calcul et une simplification de preuves. Ainsi, les résultats précédents — comme la confluence, la préservation du typage et la normalisation forte — sont aussi valides pour la déduction naturelle^[18],[19].

Par exemple, si ${\displaystyle t}$ est de type ${\displaystyle A}$ et ${\displaystyle u}$ de type ${\displaystyle B}$, la règle ${\displaystyle \pi _{1}(\langle t,u\rangle )\to t}$ du lambda-calcul simplement typé correspond exactement, dans la déduction naturelle, à la règle :

${\displaystyle {\begin{array}{c}\vdots \quad \vdots \\A\quad B\\\hline A\land B\\\hline A\end{array}}\to {\begin{array}{c}\vdots \\A\end{array}}}$

On peut définir différentes sémantiques pour le lambda-calcul simplement typé, qui permettent à la fois d'étudier le lambda-calcul en tant que tel, ou d'étudier d'autres objets en utilisant le lambda-calcul simplement typé.

On peut interpréter un jugement de typage du lambda-calcul simplement typé avec les produits ${\displaystyle \lambda ^{\to ,\times ,1}}$ dans une catégorie cartésienne fermée^[20]. Une catégorie cartésienne fermée est une catégorie qui possède un objet terminal, des produits et des objets exponentiels, qui représentent l'ensemble des morphismes d'un objet vers un autre. Cette correspondance entre lambda-calcul typé, déduction naturelle et catégorie cartésienne fermée est parfois connue sous le nom de correspondance de Curry-Howard-Lambek.

Plus généralement, Joachim Lambek et Dana Scott ont mis en évidence^[21],[22] l'équivalence entre lambda-théories typées, c'est-à-dire les extensions de ${\displaystyle \lambda ^{\to ,\times ,1}}$ avec éventuellement des constantes et des règles supplémentaires étendant ${\displaystyle =_{\beta \eta }}$, et catégories cartésiennes fermées.

Si ${\displaystyle \rho }$ assigne à chaque variable de type un objet d'une catégorie ${\displaystyle {\mathcal {C}}}$, on peut définir une sémantique ${\displaystyle [\![\;]\!]}$^[20] qui associe à un séquent ${\displaystyle \Gamma \vdash M:A}$ un morphisme ${\displaystyle [\![\Gamma \vdash M:A]\!]:[\![\Gamma ]\!]\to [\![A]\!]}$ : l'interprétation des types envoie le type unité ${\displaystyle 1}$ sur l'objet terminal ${\displaystyle 1}$, le produit de deux types ${\displaystyle T\times U}$ sur le produit catégorique des interprétations de chaque type ${\displaystyle [\![T]\!]\times [\![U]\!]}$ et le type ${\displaystyle T\to U}$ est envoyé sur ${\displaystyle [[\![T]\!],[\![U]\!]]}$, où ${\displaystyle [A,B]}$ désigne l'objet représentant les morphismes de ${\displaystyle A}$ vers ${\displaystyle B}$ dans la catégorie ${\displaystyle {\mathcal {C}}}$. On peut étendre cette définition à un contexte : si ${\displaystyle \Gamma =x_{1}:A_{1},\dots ,x_{n}:A_{n}}$, ${\displaystyle [\![\Gamma ]\!]=[\![A_{1}]\!]\times \dots [\![A_{n}]\!]}$. Pour les termes,

• Si ${\displaystyle x}$ est une variable et ${\displaystyle \Gamma =\Gamma ',x:A,\Gamma ''}$, ${\displaystyle [\![\Gamma \vdash x:A]\!]=\pi _{A}}$ est la projection de ${\displaystyle [\![\Gamma ]\!]}$ sur la composante représentée par ${\displaystyle x}$ ;
• ${\displaystyle \Gamma \vdash *:1}$ est envoyé sur l'unique morphisme de ${\displaystyle [\![\Gamma ]\!]}$ vers ${\displaystyle 1}$ ;
• ${\displaystyle \Gamma \vdash \langle M,N\rangle :A\times B}$ est envoyé sur ${\displaystyle \langle [\![\Gamma \vdash M:A]\!],[\![\Gamma \vdash N:B]\!]\rangle }$, qui désigne l'unique morphisme de ${\displaystyle \Gamma }$ vers ${\displaystyle [\![A]\!]\times [\![B]\!]}$ induit par ${\displaystyle [\![\Gamma \vdash M:A]\!]}$ et ${\displaystyle [\![\Gamma \vdash N:B]\!]}$ ;
• ${\displaystyle \Gamma \vdash \pi _{i}(M)}$ est envoyé sur ${\displaystyle \pi _{i}\circ [\![\Gamma \vdash M:A\times B]\!]}$, qui désigne la ${\displaystyle i}$-ème projection du morphisme ${\displaystyle [\![\Gamma \vdash M:A\times B]\!]}$ ;
• ${\displaystyle \Gamma \vdash \lambda x^{A}.M:A\to B}$ doit-être envoyé sur un morphisme ${\displaystyle [\![\Gamma ]\!]\to [[\![A]\!],[\![B]\!]]}$. Or ${\displaystyle [\![\Gamma ,x:A\vdash M:B]\!]}$ est un morphisme ${\displaystyle [\![\Gamma ]\!]\times [\![A]\!]\to [\![B]\!]}$ et dans une catégorie cartésienne fermée, pour tout morphisme ${\displaystyle f:X\times Y\to Z}$, il existe un unique morphisme ${\displaystyle f^{*}:X\to [Y,Z]}$ représentant sa version curryfiée. On définit donc ${\displaystyle [\![\Gamma \vdash \lambda x^{A}.M:A\to B]\!]=[\![\Gamma ,x:A\vdash M:B]\!]^{*}}$.
• Pour déterminer ${\displaystyle \Gamma \vdash MN:B}$, on remarque que ${\displaystyle [\![\Gamma \vdash M:A\to B]\!]}$ est un morphisme ${\displaystyle [\![\Gamma ]\!]\to [[\![A]\!],[\![B]\!]]}$, et ${\displaystyle [\![\Gamma \vdash N:A]\!]}$ est un morphisme ${\displaystyle [\![\Gamma ]\!]\to [\![A]\!]}$. Or dans une catégorie cartésienne fermée, pour toute paire d'objets ${\displaystyle X}$ et ${\displaystyle Y}$ il existe un morphisme d'évaluation ${\displaystyle \varepsilon :[X,Y]\times X\to Y}$, qui est la counité de l'adjonction entre les foncteurs ${\displaystyle \bullet \times X}$ et ${\displaystyle X\to \bullet }$. On définit donc ${\displaystyle [\![\Gamma \vdash MN:B]\!]=\varepsilon \circ \langle [\![\Gamma \vdash M:A\to B]\!],[\![\Gamma \vdash N:A]\!]\rangle }$.

Cette sémantique est correcte^[20] vis-à-vis de ${\displaystyle =_{\beta \eta }}$, c'est-à-dire que si ${\displaystyle M=_{\beta \eta }N}$ alors ${\displaystyle [\![M]\!]=[\![N]\!]}$. De plus, elle est également complète^[20], c'est-à-dire que si ${\displaystyle [\![M]\!]=[\![N]\!]}$ pour toute interprétation alors ${\displaystyle M=_{\beta \eta }N}$.

Dans cette sémantique, la substitution correspond à la composition^[23] : si ${\displaystyle \Gamma ,x:A\vdash M:B}$ et ${\displaystyle \Gamma \vdash N:A}$,

${\displaystyle [\![\Gamma \vdash M[x:=N]:B]\!]=[\![\Gamma ,x:A\vdash M]\!]\circ \langle id_{\Gamma },[\![\Gamma \vdash N:A]\!]\rangle :[\![\Gamma ]\!]\to [\![B]\!].}$

Les ensembles et les fonctions entre eux forment une catégorie cartésienne close, où l'objet terminal ${\displaystyle 1}$ est le singleton (il y n'en a qu'un seul à unique isomorphisme près), le produit ${\displaystyle A\times B}$ est le produit cartésien de ${\displaystyle A}$ et ${\displaystyle B}$ et l'objet exponentiel ${\displaystyle [A,B]}$ est l'ensemble des fonctions de ${\displaystyle A}$ dans ${\displaystyle B}$. Harvey Friedman a montré que si ${\displaystyle \rho }$ n'a pour valeurs que des ensembles infinis, la sémantique induite par ${\displaystyle \rho }$ est complète^[24],[25].

La théorie des domaines fournit un certain nombre de catégories cartésiennes fermées, comme celles des dcpo et ${\displaystyle \omega }$-cpo, ainsi que leurs versions pointées^[26]. Cette théorie a notamment permis à Dana Scott de construire un modèle non-trivial ${\displaystyle D_{\infty }}$^[27],[28] vérifiant ${\displaystyle D_{\infty }=D_{\infty }\to D_{\infty }}$, modèle qui peut servir à interpréter le lambda-calcul non typé^[29].

Les espaces cohérents (en) forment également une catégorie cartésienne fermée. Ils ont été introduit par Jean-Yves Girard^[30],[31] et c'est la découverte que le type des fonctions usuelles ${\displaystyle T\to U}$ pouvait s'écrire ${\displaystyle (!T)\multimap U}$, où ${\displaystyle \multimap }$ désigne l'implication linéaire et ${\displaystyle !}$ une opération de copie, qui lui a inspiré la logique linéaire.

Tout comme la logique intuitionniste, le lambda-calcul simplement typé ne démontre pas le tiers exclus ${\displaystyle P\lor \neg P}$, pas plus que l'élimination de la double négation ${\displaystyle \neg \neg P\to P}$ ou la loi de Pierce ${\displaystyle ((P\to Q)\to P)\to P}$. Il existe plusieurs façons d'étendre le lambda-calcul pour obtenir un système équivalent à la logique classique^[32] par la correspondance de Curry-Howard.

Une première méthode est celle de Timothy G. Griffith^[33], qui consiste à ajouter une version typée de l'opérateur ${\displaystyle {\mathcal {C}}}$ de Matthias Felleisen^[34] : si ${\displaystyle M}$ est de type ${\displaystyle \neg \neg T}$, où ${\displaystyle \neg U}$ est défini comme ${\displaystyle U\to \bot }$, ${\displaystyle {\mathcal {C}}M}$ est de type ${\displaystyle T}$. Cet opérateur peut aussi être munie de règles de réduction^[35] : ${\displaystyle {\mathcal {C}}(uv)\to {\mathcal {C}}(\lambda k.u(\lambda f.k(fv))}$ et ${\displaystyle {\mathcal {C}}(\lambda k.kM)\to M}$ si ${\displaystyle k}$ n'est pas libre dans ${\displaystyle M}$. La variable ${\displaystyle k}$ désigne ici une continuation, et ${\displaystyle {\mathcal {C}}}$ est un opérateur proche de call-with-current-continuation (en). Cet opérateur peut être traduit dans le lambda-calcul non typé avec une traduction CPS (en).

La méthode précédente se base sur la déduction naturelle intuitionniste. Michel Parigot a proposé une variante du lambda-calcul basé sur la déduction naturelle classique, dans laquelle il peut y avoir plusieurs formules à droite de ${\displaystyle \vdash }$ : le lambda-mu calcul (en)^[36]. Dans son calcul, il y a deux types de termes, les termes nommés qui correspondent aux formules à droite du ${\displaystyle \vdash }$ et les termes innomés, qui correspondent aux termes à gauche du ${\displaystyle \vdash }$. Un terme innomé peut être nommé par la construction ${\displaystyle [\alpha ]M}$. Les termes innomés sont les termes du lambda-calcul usuel et ceux de la forme ${\displaystyle \mu \alpha .M}$, qui permette d'abstraire un terme nommé ${\displaystyle \alpha }$.

Le lemme de Joyal^[37] montre qu'il n'y a pas de correspondance de Curry-Howard-Lambek pour la logique classique : il énonce que si ${\displaystyle {\mathcal {C}}}$ est une catégorie cartésienne fermée munie d'un objet dualisant, c'est-à-dire un objet ${\displaystyle \bot }$ tel que pour tout ${\displaystyle A}$, le morphisme ${\displaystyle A\to [[A,\bot ],\bot ]}$ est un isomorphisme, alors ${\displaystyle {\mathcal {C}}}$ est un préordre. Cela signifie que toutes les preuves d'une même proposition sont égales, et donc que la réduction n'a pas d'intérêt.

Il est possible, comme dans le lambda-calcul non typé, de définir les entiers comme les entiers de Church, c'est-à-dire comme le type ${\displaystyle (\alpha \to \alpha )\to (\alpha \to \alpha )}$ pour ${\displaystyle \alpha }$ un type de base. Un entier ${\displaystyle n}$ est alors représenté par ${\displaystyle {\overline {n}}=\lambda f^{\alpha \to \alpha }.\lambda x^{\alpha }.f^{n}x}$ qui compose la fonction en argument ${\displaystyle n}$ fois avec elle-même. Mais cette représentation est limitée : en effet, seuls les polynômes généralisés, c'est-à-dire les fonctions obtenues par composition de polynôme et de la fonction ${\displaystyle \operatorname {if} (n,m,i)={\begin{cases}n&{\text{si }}i=0\\m&{\text{si }}i\neq 0\\\end{cases}}}$, sont définissables avec cette présentation des entiers^[38].

Pour pallier ce problème, on peut utiliser le système T de Gödel^[39]. C'est une extension du lambda calcul simplement typé avec les produits ${\displaystyle \lambda ^{\to ,\times ,1}}$ qui possède des booléens et des entiers naturels : il y a deux constantes booléennes ${\displaystyle T}$ et ${\displaystyle F}$ et une structure conditionnelle : si ${\displaystyle M}$ est un booléen et ${\displaystyle N}$ et ${\displaystyle O}$ sont de type ${\displaystyle A}$, ${\displaystyle D_{A}MNO}$ est de type ${\displaystyle A}$. On a de plus les règles ${\displaystyle D_{A}TNO\to N}$ et ${\displaystyle D_{A}FNO\to O}$. De plus, il y a une constante ${\displaystyle 0}$ de type entier, et si ${\displaystyle M}$ est un entier, ${\displaystyle SM}$ aussi, qui représente son successeur. Enfin, pour chaque type ${\displaystyle A}$, il y a un une construction qui permet de produire une valeur par récurrence sur un entier : si ${\displaystyle M}$ est un entier, ${\displaystyle N}$ un terme de type ${\displaystyle A}$, ${\displaystyle O}$ de type ${\displaystyle A\to \mathbb {N} \to A}$, ${\displaystyle R_{A}MNO}$ est de type ${\displaystyle A}$ vérifiant pour tout ${\displaystyle M}$, ${\displaystyle N}$ et ${\displaystyle O}$, ${\displaystyle R_{A}0MN\to M}$ et ${\displaystyle R_{A}(SM)NO\to N(R_{A}MNO)O}$^[40]. Système T a notamment permis de donner une preuve de l'arithmétique de Heyting, de laquelle on peut déduire l'arithmétique de Peano^[39]. Notamment, les fonctions entre les entiers définissables dans le système T correspondent exactement aux fonctions prouvablement totales dans l'arithmétique de Peano^[41], ou, ce qui revient au même, dans l'arithmétique de Heyting^[42].

Le ${\displaystyle \lambda Y}$-calcul est une extension du lambda-calcul simplement typé avec produits ${\displaystyle \lambda ^{\to ,\times ,1}}$ avec des combinateurs de points fixes, introduit par Dana Scott^[43] et étudiée par Gordon Plotkin^[44]. On ajoute pour chaque type ${\displaystyle T}$ une constante ${\displaystyle Y_{T}}$ de type ${\displaystyle (T\to T)\to T}$ et une constante ${\displaystyle \Omega _{T}}$ de type ${\displaystyle T}$, et la règle de réduction ${\displaystyle Y_{T}M\to M(Y_{T}M)}$^[45]. Le ${\displaystyle \lambda Y}$-calcul s'interprète notamment dans la catégorie des dcpo pointés et des fonctions continues entre eux. Cette catégorie cartésienne close, chaque objet a un plus petit élément ${\displaystyle \bot }$ (qui sert à interpréter ${\displaystyle \Omega _{T}}$) et chaque fonction continue d'un dcpo dans lui-même a un plus petit point fixe : ${\displaystyle Y_{T}}$ a alors pour sémantique la fonction qui a ${\displaystyle f}$ associe son plus petit point fixe.

PCF (en)^[44],[46] est une variante du ${\displaystyle \lambda Y}$-calcul avec les types de fonctions et deux types de bases, les booléens et les entiers naturels, vu comme des domaines plats. Cela signifie que si ${\displaystyle \mathbb {N} }$ représente les entiers naturels usuels, les entiers de PCF sont ${\displaystyle \mathbb {N} _{\bot }=\mathbb {N} \cup \{\bot \}}$, avec ${\displaystyle \bot }$ le plus petit élément de ${\displaystyle \mathbb {N} _{\bot }}$, les autres éléments étant incomparables entre eux. Une valeur ${\displaystyle \bot }$ représente une valeur indéfinie. En plus des constantes ${\displaystyle Y}$ et ${\displaystyle \Omega }$ pour chaque type, PCF possède également une constante pour chaque entier et pour chaque booléen, une structure conditionnelle ${\displaystyle \operatorname {if} \dots \operatorname {then} \dots \operatorname {else} \dots }$, une fonction pour tester si un entier vaut zéro, ainsi que les fonctions successeur et prédécesseur. C'est un exemple minimal de langage de programmation fonctionnel, et il est Turing-complet^[44].

Il est possible d'étendre le lambda-calcul simplement typé pour qu'il supporte des abstractions et des instanciations de type, c'est-à-dire ajouter du polymorphisme^[47]. Le système formel obtenu se nomme le système F^[48]. Très expressif, ce système permet de définir les produits, les sommes et le quantificateur existentiel, ainsi que les types inductifs comme les entiers ou les listes. Les fonctions définissables sur les entiers dans le système F sont exactement les fonctions prouvablement totales dans l'arithmétique du second ordre^[49], ou de façon équivalente, dans l'arithmétique de Heyting du second ordre.

On peut également étendre le système de types pour obtenir des types dépendants^[50], c'est-à-dire des types qui dépendent de valeur, et des types d'ordre supérieur^[51], c'est-à-dire des types qui dépendent d'autre types, formant ainsi le lambda-cube^[52],[53]. De plus, on peut également considérer diverses théories des types possédant à la fois du polymorphisme, des types d'ordre supérieur et des types dépendants, comme par exemple la théorie des types de Martin-Löf MLTT^[54], le calcul des constructions CoC^[55],[56], ou enfin la théorie des types homotopiques HoTT^[57].

• (en) Peter Selinger, Lecture Notes on the Lambda Calculus, 2013, 2^e éd. (1^re éd. 2008), 120 p. (arXiv abs/0804.3434, lire en ligne). 
• (en) Rob Nederpelt et Herman Geuvers, Type Theory and Formal Proof : An Introduction, Cambridge University Press, 2014 (ISBN 978-1-107-03650-5, DOI 10.1017/CBO9781139567725, lire en ligne). 
• (en) Jean-Yves Girard, Paul Taylor et Yves Lafont, Proofs and Types, Cambridge University Press, 1989, 183 p. (ISBN 0-521-37181-3, lire en ligne). 
• Jean-Louis Krivine, Lambda-calcul : types et modèles, Masson, 1990, 206 p. (ISBN 978-2-225-82091-5, lire en ligne), chapitre 3, section 2.
• (en) Joachim Lambek et Dana S. Scott, Introduction to Higher-Order Categorical Logic, Cambridge University Press, 1988 (ISBN 9780521356534). .
• (en) Roberto M. Amadio et Pierre-Louis Curien, Domains and Lambda-Calculi, Cambridge University Press, coll. « Cambridge Tracts in Theoretical Computer Science », 1998, 534 p. (ISBN 978-0-521-62277-6, lire en ligne). .

• Lambda-calcul
• Correspondance de Curry-Howard

• Système F
• Catégorie cartésienne fermée

• Portail de l'informatique théorique
• Portail de la logique