英和和英

出典:『Wikipedia』 (2011/03/04 15:50 UTC 版)

英語による解説

引用

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 Fω.
• Types depending on terms, or dependent types. Imposing only this property yields λΠ, a type system closely related to LF.