Lambda cube
- 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 dépendre que d'un autre terme. Chaque axe représente une nouvelle forme d'abstraction :
- Terme dépendant de type : le polymorphisme.
- Type dépendant de type : présence d'opérateurs de types.
- Type dépendant de terme.
Notes et références
Wikimedia Foundation.
2010.
Contenu soumis à la licence CC-BY-SA. Source : Article Lambda cube de Wikipédia en français (auteurs)
Regardez d'autres dictionnaires:
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… … Wikipedia
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
