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. 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.
Introduction
Le lambda-calcul pose comme primitive la notion de fonction. Si est une expression, représente la fonction définie par l'équation , et si et sont deux expressions, désigne l'application de à . Enfin, le lambda-calcul possède une notion dite de réduction qui correspond à effectuer une étape de calcul.
Par analogie, pourrait désigner la fonction qui renvoie le carré de son argument, et est la suite des étapes de calcul pour calculer cette fonction en . 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 : présente la propriété que , donc que le calcul de ne termine pas, et de plus, si est un terme, il existe un terme tel que . Pour reprendre l'analogie précédente, pour , un tel vérifierait , 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.
Syntaxe 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 ce système.
Types On suppose donné un ensemble de variables de types, qu'on note par des lettres grecques Les types du lambda-calcul simplement typé sont désignés par les lettres et sont formés par :
les variables de types ; si et sont des types, est le type des fonctions de vers . Termes Les variables seront notées par des lettres minuscules tandis que les termes seront notés Les termes sont formés ainsi :
Les variables sont des termes ; Si est un type et un terme, est un terme qui représente la fonction qui à de type associe l'expression . On peut voir ça comme l'abstraction de dans l'expression ; Si et sont des termes, est un terme qui correspond à l'application de la fonction à l'expression . De plus, on considèrera que l'application est associative à gauche, c'est-à-dire qu'on notera pour .
Règles de typage On introduit la notation , où est une liste de paires de la forme où est une variable et un type, est un terme et un type. Elle se lit « dans le contexte , le terme a pour type ». Par exemple, se lit « si est une variable de type , la fonction qui à de type associe la valeur est une fonction qui envoie les éléments de dans ».
Une règle de la forme doit se comprendre comme « si , ..., alors ». En particulier, signifie que est toujours vrai.
Le lambda-calcul présenté ici correspond, sous la correspondance de Curry-Howard, à la logique minimale.
Typage à la Church et typage à la Curry La présentation ici donnée correspond au typage à la Church, 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, 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 . Par exemple, avec un typage à la Church, a pour type , tandis qu'avec un typage à la Curry, a tous les types de la forme . 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.
Réduction Tout comme le lambda-calcul non typé, le lambda-calcul simplement typé identifie les termes 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, qui correspond à une opération de réécriture représentant une étape de calcul :
si n'est pas libre dans ;
Une des règles est étiquetée , elle correspond à une règle de calcul. La réduction associée est nommée . L'autre est étiquetée , elle correspond à une simplifications : si , et se « comportent » pareil. On nomme cette réduction . On note si ou : c'est la .
Enfin, si est une réduction, est sa clôture réflexive et transitive et sa clôture réflexive, symétrique et transitive, c'est-à-dire que s'il existe tels que et s'il existe tels que , et pour tout entre et , ou .
Préservation du typage La possède la propriété de préservation du typage () : si et alors .
Normalisation forte Un terme est dit en forme normale s'il ne peut pas se réduire d'avantage. La possède la propriété de normalisation forte, c'est-à-dire que tous les termes sont fortement normalisables : il n'y a pas de suite infinie de réductions 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 et que est en forme normale pour , on dit que est une normale de . Comme l’énonce le paragraphe suivant, cette forme est unique pour la et la .
Confluence Une réduction est dite confluente si pour tous termes , et tels que et , il existe un terme tel que et . La et la sont confluentes.
La confluence assure l'unicité de la forme normale pour la réduction : en effet, supposons et avec et en forme normale. Si alors puisque ne peut pas se réduire. De même, si alors . Donc .
Cela signifie qu'en partant d'un terme donné, l'ordre des 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 , alors atteint une forme normale en une étape en réduisant d'abord le premier rédex, tandis que 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 après les ou bien faire les après les : si , alors le réduit dans la deuxième réduction était déjà présent dans , et si est en normale, il existe un terme (non nécessairement unique) en normale tel que .
Types produits On peut étendre la présentation précédente du lambda-calcul avec un typé unité et des produits de types, on le note alors . On ajoute alors aux types un type unité , qui possède un unique élément, et et sont des types, on ajoute le type qui représente le produit des types et , dont les éléments sont des paires composées d'un élément de et d'un de .
De plus, on étend la syntaxe des termes :
L'unique terme du type unité, se note ; Si et sont des termes, le terme , représente la paire dont la première composante est et la deuxième ; Si est un terme et , la projection de la paire se note .
Les règles de typages correspondantes sont :
On peut également ajouter des règles de calcul sur les produits, à savoir : ; . Il est aussi possible d'ajouter des règles à ce lambda-calcul : ; si est de type . Mais celles-ci ne se comportent pas aussi bien que dans le cas sans type unité. En effet, si la reste confluente, la ne l'est plus, comme le montre l'exemple suivant, où :
mais et 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 et à être fortement normalisantes.
Types sommes 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. Pour cela, on ajoute à la syntaxe le type , et si et sont deux types, aussi. Le type peut être vu comme des couples avec dans ou dans et une étiquette indiquant la provenance de : ou . Ce système se note .
De plus, on ajoute à la syntaxe les termes suivants :
Si est un type et un terme, est un terme, qui sera de type . En effet, si possède un élément, tous les autres types aussi. Si et sont des types, et un terme, et sont des termes correspondant aux injections respectives de et dans . Si et sont des types, , et des termes, alors est un terme qui correspond à un filtrage par motif. Ces nouveaux termes se typent comme suit :
On peut également ajouter des règles de réduction, mais il faut ajouter un nouveau type de règles : les conversions commutatives, notées . Elles permettent d'identifier deux termes qui devraient désigner la même preuve, mais sont différents.
Les deux règles correspondent au calcul du filtrage : si provient de , on renvoie où est remplacé par , et on fait de même avec et si provient de :
. Les cinq règles suivantes correspondent aux conversions commutatives pour :
Si et sont de type , . Ces cinq règles correspondent aux conversions commutatives pour la somme :
. Enfin, on peut aussi définir des règles : la première règle correspond à , la deuxième à la somme. ; .
Les réductions et préservent le typage et sont fortement normalisantes. De plus, est confluente.
Correspondance de Curry-Howard
Les règles de typage du lambda-calcul simplement typé correspondent, une pour une, aux règles règles du fragment conjonctif et implicatif règles du fragment disjonctif d'introductions et d'éliminations de la déduction naturelle pour la logique intuitionniste. Cela permet d'établir une correspondance formelle entre preuves et programmes. Par exemple, les règles de l'implication en déduction naturelle sont :
où signifie que l'on « charge » l'hypothèse , 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.
En déduction naturelle, il existe une notion de simplification des preuves, appelée élimination des coupures pour le fragment conjonctif et implicatif pour le fragment disjonctif conversions commutatives pour le fragment disjonctif. 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 pour le fragment conjonctif et implicatif, permettant de faire le lien entre un calcul et une simplification de preuves. Ainsi, les résultats précédents sont aussi valides pour la déduction naturelle pour le fragment disjonctif.
Par exemple, si est de type et de type , la règle du lambda-calcul simplement typé correspond exactement, dans la déduction naturelle, à la règle :
Sémantique 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é.
Catégorie cartésienne fermée On peut interpréter un jugement de typage du lambda-calcul simplement typé avec les produits dans une catégorie cartésienne fermée. 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.