Lambda cube

Lambda cube

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 (as in System F),
* Types depending on types, or type operators, and
* Types depending on terms, or dependent types (as in LF).All eight calculi include the most basic form of abstraction, terms depending on terms, ordinary functions as in the simply-typed lambda calculus.

All eight calculi are strongly normalizing.

The idea of the cube is due to the mathematician Henk Barendregt (1991).

ee also

* Lambda calculus
* System F
* Pure type system

References

* H.P. Barendregt, Introduction to generalized type systems, "Journal of Functional Programming", 1(2):125-154, April 1991.
* Simon Peyton Jones and Erik Meijer, 1997. [http://citeseer.ist.psu.edu/peytonjones97henk.html "Henk: A Typed Intermediate Language"]
* [http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm Barendregt's Lambda Cube]


Wikimedia Foundation. 2010.

Игры ⚽ Поможем решить контрольную работу

Look at other dictionaries:

  • Lambda cube — 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… …   Wikipédia en Français

  • Lambda calculus — In mathematical logic and computer science, lambda calculus, also written as λ calculus, is a formal system designed to investigate function definition, function application and recursion. It was introduced by Alonzo Church and Stephen Cole… …   Wikipedia

  • Cube (disambiguation) — A cube is a shape in three dimensions. It may also refer to: Contents 1 People 2 Math and science 3 Entertainment …   Wikipedia

  • Cube (homonymie) — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. Sur les autres projets Wikimedia : « Cube (homonymie) », sur le Wiktionnaire (dictionnaire universel) Sommaire …   Wikipédia en Français

  • Lambda — Pour les articles homonymes, voir Lambda (homonymie). Cet article possède des paronymes, voir : Ʌ et ∧ …   Wikipédia en Français

  • Typed lambda calculus — A typed lambda calculus is a typed formalism that uses the lambda symbol (lambda) to denote anonymous function abstraction. Typed lambda calculi are foundational programming languages and are the base of typed functional programming languages… …   Wikipedia

  • Cálculo lambda — Artículo parcialmente traducido: Contiene texto en inglés. Ayuda a terminarlo. El cálculo lambda es un sistema formal diseñado para investigar la definición de función, la noción de aplicación de funciones y la recursión. Fue introducido por… …   Wikipedia Español

  • Chebyshev cube root — In mathematics, in the theory of special functions, the Chebyshev cube root is a particular inverse function of the Chebyshev polynomial of third degree. It is analogous to the cube root function is the inverse of the third power. It can be used… …   Wikipedia

  • Dependent type — Type systems Type safety Inferred vs. Manifest Dynamic vs. Static Strong vs. Weak Nominal vs. Structural Dependent typing Duck typing Latent typing Linear typing Uniqueness typing …   Wikipedia

  • System F — System F, also known as the polymorphic lambda calculus or the second order lambda calculus, is a typed lambda calculus. It was discovered independently by the logician Jean Yves Girard and the computer scientist John C. Reynolds. System F… …   Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”