(pi sinon( (Vrai alors sinon) = alors , (Faux alors sinon) = sinon )) . 
-calcul simplement typé des combinateurs Vrai et Faux.
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 :
--
-calcul simplement typé*.
La puissance de calcul y est très faible.
--
-calcul polymorphe du second ordre.
On y trouve des applications de termes à des types
et les abstractions et les constructions de type
qui vont avec [Girard 72, Reynolds 74]
(
type produit*).
La puissance de calcul dépasse celle des fonctions primitives récursives.
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.
--
-calcul peu étudié.
On peut y définir les constructeurs de type.
--
-calcul polymorphe d'ordre supérieur.
Il combine et [Girard 72].
Il n'est pas calculatoirement complet,
aucun des -calculs du cube ne l'est,
mais sa puissance de calcul est suffisamment importante pour envisager
de l'utiliser comme langage de
programmation [Pierce et al. 89].
--
-calcul à type dépendant.
On y trouve des applications de types à des termes
et les abstractions et les constructions de type qui vont avec
( type produit*).
Il s'agit essentiellement de LF
(Logical Framework [Harper et al. 87]).
Il faut noter que la dépendance de type n'augmente pas la puissance
de calcul.
Elle augmente seulement la faculté d'exprimer dans les types des propriétés
complexes.
--
-calcul polymorphe du second ordre à type dépendant.
Il combine et .
--
-calcul peu étudié.
Il combine et .
--
, et .
Une variante un peu plus puissante est à la base du système de développement
de programmes appelé Coq [Huet et al. 97].
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.