Lambda cube
![](http://upload.wikimedia.org/wikipedia/commons/thumb/3/33/Consistency.png/45px-Consistency.png)
Cet article est une ébauche concernant la logique.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
![](http://upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Lambda_Cube_img.svg/220px-Lambda_Cube_img.svg.png)
Initialement proposé par Henk Barendregt[1], le -cube permet de visualiser les différentes dimensions pour lesquelles le calcul des constructions apporte une généralisation par rapport au lambda-calcul simplement typé où un terme ne peut dépendre que d'un autre terme. Chaque axe représente une nouvelle forme d'abstraction :
- Terme dépendant de type : le polymorphisme (d'où le Système F);
- Type dépendant de type : présence d'opérateurs de types ;
- Type dépendant de terme.
Notes et références
- ↑ (en) [PDF] Henk Barendregt, « Introduction to generalized type systems », Journal of Functional Programming, 1 (2) : 125-154, avril 1991.
Portail de la logique
Portail de l'informatique théorique