Cube lambda

En logique mathématique et en théorie des types , le λ-cube (également écrit lambda cube ) est un cadre introduit par Henk Barendregt pour étudier les différentes dimensions dans lesquelles le calcul des constructions est une généralisation du λ-calcul simplement typé . Chaque dimension du cube correspond à un nouveau type de dépendance entre termes et types. Ici, « dépendance » fait référence à la capacité d'un terme ou d'un type à lier un terme ou un type. Les dimensions respectives du λ-cube correspondent à :

• axe des x ( ) : types pouvant lier des termes, correspondant aux types dépendants .
• axe y ( ) : termes pouvant lier des types, correspondant au polymorphisme .
• axe z ( ) : types pouvant lier des types, correspondant aux opérateurs de type (de liaison) .

Les différentes façons de combiner ces trois dimensions donnent les 8 sommets du cube, chacun correspondant à un type de système typé différent. Le λ-cube peut être généralisé au concept de système de types purs .

Le système le plus simple que l'on trouve dans le λ-cube est le calcul lambda simplement typé , aussi appelé λ→. Dans ce système, la seule façon de construire une abstraction est de faire dépendre un terme d'un terme , avec la règle de typage :

Dans le système F (également nommé λ2 pour le « calcul lambda typé du second ordre ») il existe un autre type d'abstraction, écrit avec un , qui permet aux termes de dépendre des types , avec la règle suivante :

Les termes commençant par a sont appelés polymorphes , car ils peuvent être appliqués à différents types pour obtenir différentes fonctions, de manière similaire aux fonctions polymorphes dans les langages de type ML . Par exemple, l'identité polymorphe

amusant 
x 
-> 
x

de OCaml a le type

' un 
-> 
' un

c'est à dire qu'il peut prendre un argument de n'importe quel type 'aet renvoyer un élément de ce type. Ce type correspond dans λ2 au type .

Dans System F, une construction est introduite pour fournir des types qui dépendent d'autres types . Cela s'appelle un constructeur de type et fournit un moyen de construire « une fonction avec un type comme valeur ». Un exemple d'un tel constructeur de type est le type d'arbres binaires avec des feuilles étiquetées par des données d'un type donné : , où « » signifie informellement « est un type ». Il s'agit d'une fonction qui prend un paramètre de type comme argument et renvoie le type de s de valeurs de type . Dans la programmation concrète, cette fonctionnalité correspond à la possibilité de définir des constructeurs de type à l'intérieur du langage, plutôt que de les considérer comme des primitives. Le constructeur de type précédent correspond approximativement à la définition suivante d'un arbre avec des feuilles étiquetées en OCaml :

type 
' un 
arbre 
= 
| 
Feuille 
de 
' un 
| 
Nœud 
de 
' un 
arbre 
* 
' un 
arbre

Ce constructeur de type peut être appliqué à d'autres types pour obtenir de nouveaux types. Par exemple, pour obtenir le type d'arbres d'entiers :

type 
int_tree 
= 
int 
arbre

Le système F n'est généralement pas utilisé seul, mais il est utile pour isoler la fonctionnalité indépendante des constructeurs de types.

Dans le système λP , également appelé λΠ, et étroitement lié au cadre logique LF , on a ce qu'on appelle des types dépendants . Ce sont des types qui sont autorisés à dépendre de termes . La règle d'introduction cruciale du système est

où représente les types valides. Le nouveau constructeur de type correspond via l' isomorphisme de Curry-Howard à un quantificateur universel, et le système λP dans son ensemble correspond à la logique du premier ordre avec implication comme connecteur uniquement. Un exemple de ces types dépendants en programmation concrète est le type de vecteurs sur une certaine longueur : la longueur est un terme dont dépend le type.

Le système Fω combine à la fois le constructeur du système F et les constructeurs de types du système F. Ainsi, le système Fω fournit à la fois des termes qui dépendent des types et des types qui dépendent des types .

Dans le calcul des constructions , noté λC dans le cube ou λPω, ces quatre caractéristiques cohabitent, de sorte que les types et les termes peuvent dépendre de types et de termes. La frontière nette qui existe dans λ→ entre termes et types est quelque peu abolie, car tous les types, à l'exception de l'universel, sont eux-mêmes des termes avec un type.

Comme pour tous les systèmes basés sur le calcul lambda simplement typé, tous les systèmes du cube sont donnés en deux étapes : d'abord, les termes bruts, accompagnés d'une notion de β-réduction , puis les règles de typage qui permettent de typer ces termes.

L'ensemble des tris est défini comme , les tris sont représentés par la lettre . Il existe également un ensemble de variables, représentées par les lettres . Les termes bruts des huit systèmes du cube sont donnés par la syntaxe suivante :

et indiquant quand n'apparaît pas libre dans .

Les environnements, comme c'est habituel dans les systèmes typés, sont donnés par

La notion de β-réduction est commune à tous les systèmes du cube. Elle s'écrit et est donnée par les règles. Sa clôture réflexive, transitive , s'écrit .

Les règles de typage suivantes sont également communes à tous les systèmes du cube :

La différence entre les systèmes réside dans les paires de tris autorisées dans les deux règles de typage suivantes :

La correspondance entre les systèmes et les paires autorisées dans les règles est la suivante :

Chaque direction du cube correspond à une paire (à l'exclusion de la paire partagée par tous les systèmes), et à son tour chaque paire correspond à une possibilité de dépendance entre termes et types :

Une dérivation typique qui peut être obtenue est ou avec le raccourci fléché ressemblant étroitement à l'identité (de type ) du λ→ habituel. Notez que tous les types utilisés doivent apparaître dans le contexte, car la seule dérivation qui peut être effectuée dans un contexte vide est .

La puissance de calcul est assez faible, elle correspond aux polynômes étendus (polynômes accompagnés d'un opérateur conditionnel).

Dans λ2, de tels termes peuvent être obtenus comme avec . Si on lit comme une quantification universelle, via l'isomorphisme de Curry-Howard, cela peut être vu comme une preuve du principe d'explosion. En général, λ2 ajoute la possibilité d'avoir des types imprédicatifs tels que , c'est-à-dire des termes quantifiant sur tous les types y compris eux-mêmes. Le polymorphisme permet aussi la construction de fonctions qui n'étaient pas constructibles dans λ→. Plus précisément, les fonctions définissables dans λ2 sont celles prouvablement totales dans l'arithmétique de Peano du second ordre . En particulier, toutes les fonctions récursives primitives sont définissables.

Dans λP, la possibilité d'avoir des types dépendants de termes signifie que l'on peut exprimer des prédicats logiques. Par exemple, ce qui suit est dérivable : ce qui correspond, via l'isomorphisme de Curry-Howard, à une preuve de . Du point de vue du calcul, cependant, avoir des types dépendants n'améliore pas la puissance de calcul, mais seulement la possibilité d'exprimer des propriétés de type plus précises.

La règle de conversion est fortement nécessaire lorsqu'il s'agit de types dépendants, car elle permet d'effectuer des calculs sur les termes du type. Par exemple, si l'on a et , il faut appliquer la règle de conversion pour obtenir de pouvoir taper .

Dans λω, l'opérateur suivant est définissable, c'est-à-dire . La dérivation peut déjà être obtenue dans λ2, cependant le polymorphe ne peut être défini que si la règle est également présente.

D'un point de vue informatique, λω est extrêmement fort et a été considéré comme une base pour les langages de programmation.

Le calcul des constructions possède à la fois l'expressivité des prédicats de λP et la puissance de calcul de λω, c'est pourquoi λC est également appelé λPω, il est donc très puissant, à la fois du côté logique et du côté calculatoire.

Le système Automath est similaire à λ2 d'un point de vue logique. Les langages de type ML , d'un point de vue typage, se situent quelque part entre λ→ et λ2, car ils admettent un type restreint de types polymorphes, c'est-à-dire les types sous forme normale prenex. Cependant, comme ils disposent de certains opérateurs de récursivité, leur puissance de calcul est supérieure à celle de λ2. Le système Coq est basé sur une extension de λC avec une hiérarchie linéaire d'univers, plutôt qu'un seul non typable , et la capacité de construire des types inductifs.

Les systèmes de types purs peuvent être considérés comme une généralisation du cube, avec un ensemble arbitraire de tris, d'axiomes, de produits et de règles d'abstraction. Inversement, les systèmes du lambda cube peuvent être exprimés comme des systèmes de types purs avec deux tris , le seul axiome et un ensemble de règles telles que .

Via l'isomorphisme de Curry-Howard, il existe une correspondance bijective entre les systèmes du cube lambda et les systèmes logiques, à savoir :

Toutes les logiques sont implicatives (c'est-à-dire que les seuls connecteurs sont et ), cependant on peut définir d'autres connecteurs tels que ou de manière imprédicative dans les logiques du second ordre et d'ordre supérieur. Dans les logiques faibles d'ordre supérieur, il existe des variables pour les prédicats d'ordre supérieur, mais aucune quantification sur celles-ci ne peut être effectuée.

Tous les systèmes du cube bénéficient

• la propriété de Church-Rosser : si et alors il existe tel que et ;
• la propriété de réduction du sujet : si et alors ;
• l'unicité des types : if et then .

Tout cela peut être prouvé sur des systèmes génériques de type pur.

Tout terme bien typé dans un système du cube est fortement normalisant, bien que cette propriété ne soit pas commune à tous les systèmes de types purs. Aucun système du cube n'est complet au sens de Turing.

Le sous-typage n'est cependant pas représenté dans le cube, même si des systèmes comme , connus sous le nom de quantification bornée d'ordre supérieur, qui combine le sous-typage et le polymorphisme, présentent un intérêt pratique et peuvent être généralisés aux opérateurs de type borné. D'autres extensions permettent de définir des objets purement fonctionnels ; ces systèmes ont généralement été développés après la publication de l'article sur le cube lambda.

L'idée du cube est due au mathématicien Henk Barendregt (1991). Le cadre des systèmes de types purs généralise le cube lambda dans le sens où tous les coins du cube, ainsi que de nombreux autres systèmes, peuvent être représentés comme des instances de ce cadre général. Ce cadre est antérieur au cube lambda de quelques années. Dans son article de 1991, Barendregt définit également les coins du cube dans ce cadre.