Barendregt (cube de).
n.m.
[Barendregt et Hemerik 90, Barendregt 91]
Métaphore qui présente dans un cadre unique plusieurs
-calculs*
typés.
La remarque essentielle est qu'on peut étendre le
-calcul simplement typé*
selon trois dimensions indépendantes.
On obtient donc sept nouveaux systèmes en étendant le
-calcul
simplement typé selon une dimension
(3 systèmes),
deux dimensions
(3 autres systèmes)
et selon les trois dimensions à la fois
(1 système).
Pour comprendre les trois extensions possibles il faut se rappeler que les
-termes simplement typés ne peuvent être appliqués qu'à des
termes [Church 40],
et que cela constitue les seules applications possibles.
Les trois extensions indépendantes consistent à appliquer des
termes à des types, des types à des types et des types à des termes.
La première extension modélise le polymorphisme paramétrique où une fonction
peut recevoir un type en paramètre et produire un résultat dont le type en
dépend [Girard 72, Reynolds 74].
La seconde extension modélise le calcul de type.
Elle permet de définir les constructeurs de type dans le langage plutôt que
de les considérer comme prédéfinis dans une signature initiale.
Enfin,
la troisième extension modélise des types qui dépendent de valeurs,
par exemple
le type des listes d'une longueur donnée ou
le type des tableaux d'un nombre donné d'éléments.
Ces extensions correspondent à de vrais problèmes de programmation. Par exemple, les procédures des bibliothèques mathématiques ont souvent des paramètres pour indiquer la forme ou les dimensions d'autres paramètres qui sont des tableaux. Ces procédures sont écrites en Fortran ou en C, mais aucun de ces langages de programmation n'est prévu pour vérifier la cohérence de ce genre de paramétrage, alors qu'il est convenablement décrit par les types dépendants de termes.
Les huit systèmes du cube de Barendregt sont :
Les langages polymorphes à la
(quantification prénexe* des variables de type)
sont situés entre
et
.
On ne parle ici que du système de type,
car la présence d'une constante interprétée comme un combinateur de point-fixe
fait sortir ces langages du cube.
En particulier,
ces langages n'ont pas la propriété de
normalisation forte*,
mais c'est intentionnel.
Tous ces systèmes ont la propriété de normalisation forte et celle de Church-Rosser*.
Figure 1: Faces du cube de Barendregt. Découper et assembler comme un cube.
On exploite souvent cette métaphore en dessinant un cube étiqueté par des
noms de -calculs et des commentaires
(voir au-dessus et figure 1).
Les notations
désignent les capacités ajoutées ou retranchées pour appartenir
à telle face ou suivre telle arête.
Le signe
désigne la sorte des termes
et
désigne celle des types.
Une paire
spécifie la capacité de former des fonctions
des
dans les
.
La paire
désigne la capacité d'abstraire des termes dans
les termes,
et donc d'appliquer des termes à des termes.
C'est la capacité de base, que tous les systèmes possèdent.
La paire
désigne la capacité d'abstraire des types
dans les termes,
et donc d'appliquer des termes à des types.
Considérés comme des formules (
Curry-Howard*),
les types de ces termes sont qualifiés de «non-prédicatifs» car ils
contiennent des quantifications sur tous le domaine de formule,
sans restriction.
La paire
désigne la capacité d'abstraire des termes
dans les types,
et donc de former des types dépendants de termes.
Toujours en considérant les types comme des formules,
cette capacité fait des types les formules d'un «calcul de prédicat».
Enfin,
la paire
désigne la capacité d'abstraire des types dans les types,
et donc d'appliquer des types à des types.
Cela fait des types des formules «d'ordre supérieur».
Figure 2: Sommets du cube de Barendregt. Découper et assembler comme un octaèdre.
Figure 3: Arêtes du cube de Barendregt. Découper et assembler comme un dodécaèdre.
Cet usage de la métaphore
est assez problématique car un cube laisse une surface nulle (les sommets)
pour les objets qui sont ici les plus concrets (les systèmes),
et la plus grande surface (les faces) pour des familles de quatre systèmes.
Le dual du cube, un octaèdre, permet de consacrer le plus de surface aux objets
qui sont les plus concrets
(voir figure 2).
C'est donc lui qu'il faut choisir pour combiner la métaphore du cube et un
commentaire extensif des «sommets».
On peut aussi mettre les arêtes en valeur en construisant un dodécaèdre
(voir figure 3).
Dans cette figure,
chaque face est étiquetée par une paire et deux noms de
systèmes,
l'un écrit sous la paire, l'autre au-dessus.
Cela représente l'arête qui va du système du bas au système du haut en ajoutant
la capacité
.
But.
n.m.
Selon les contextes,
un but est un corps de clause* (
Prolog),
un littéral* (Prolog),
ou une formule à prouver.