In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions (higher order dependently-typed polymorphic lambda calculus) as its diametric opposite vertex. Each axis of the cube represents a new form of abstraction: Terms depending on types, or polymorphism.
| Property | Value |
|---|
| dbpprop:abstract
|
- In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions (higher order dependently-typed polymorphic lambda calculus) as its diametric opposite vertex. Each axis of the cube represents a new form of abstraction: Terms depending on types, or polymorphism. System F, aka second order lambda calculus, is obtained by imposing only this property. Types depending on types, or type operators. Simply typed lambda-calculus with type operators, λω, is obtained by imposing only this property. Combined with System F it yields System <math>F_\omega</math>. Types depending on terms, or dependent types. Imposing only this property yields LF. All eight calculi include the most basic form of abstraction, terms depending on terms, ordinary functions as in the simply-typed lambda calculus. The richest calculus in the cube, with all three abstractions, is the calculus of constructions. All eight calculi are strongly normalizing. Subtyping however is not represented in the cube, even though systems like <math>F^\omega_{<:}</math>, known as Higher-order bounded quantification, which combines subtyping and polymorphism are of practical interest, and can be further generalized to bounded type operators. Further extensions to <math>F^\omega_{<:}</math> allow the definition of purely functional objects; these systems were generally developed after the lambda cube paper was published. The idea of the cube is due to the mathematician Henk Barendregt (1991). The framework of pure type systems generalizes the lambda cube in the sense that all corners of the cube, as well as many other systems can be represented as instances of this general framework. This framework predates lambda cube a couple of years. In his 1991 paper, Barendregt also defines the corners of the cube in this framework.
- Ля́мбда-куб (λ-куб) задает единообразное описание восьми различных систем типизированного лямбда-исчисления с явным приписыванием типов (систем, типизированных по Чёрчу). Он организован в соответствии с возможными зависимостями между типами и термами этого исчисления и формирует естественную структуру для исчисления конструкций. Идею лямбда-куба предложил в 1991 году голландский логик и математик Хенк Барендрегт. Лямбда-куб. Стрелка вдоль каждого ребра указывает на направление включения; более простая система является частным случаем более сложной.
|
| dbpprop:hasPhotoCollection
| |
| dbpprop:reference
| |
| rdfs:comment
|
- In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions (higher order dependently-typed polymorphic lambda calculus) as its diametric opposite vertex. Each axis of the cube represents a new form of abstraction: Terms depending on types, or polymorphism.
- Ля́мбда-куб (λ-куб) задает единообразное описание восьми различных систем типизированного лямбда-исчисления с явным приписыванием типов (систем, типизированных по Чёрчу).
|
| rdfs:label
| |
| owl:sameAs
| |
| skos:subject
| |
| foaf:page
| |
| is dbpprop:redirect
of | |
![[RDF Data]](/statics/sw-cube.png)
