Typed lambda calculus


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 such as ML and Haskell and, more indirectly, typed imperative programming languages. They are closely related to mathematical logic and proof theory via the Curry-Howard isomorphism and they can be considered as the internal language of classes of categories, e.g. the simply typed lambda calculus is the language of Cartesian closed categories (CCCs).

From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus but from another point of view, they can also be considered the more fundamental theory and untyped lambda calculus a special case with only one type.

Various typed lambda calculi have been studied: The types of the simply typed lambda calculus are only base types (or type variables) and function types sigma o au. System T extends the simply typed lambda calculus with a type of natural numbers and higher order primitive recursion; in this system all functions provably recursive in Peano arithmetic are definable. System F allows polymorphism by using universal quantification over all types; from a logical perspective it can describe all functions which are provably total in second-order logic. Lambda calculi with dependent types are the base of intuitionistic type theory, the calculus of constructions and the logical framework (LF), a pure lambda calculus with dependent types. Based on work by Berardi, Barendregt proposed the Lambda cube to systematize the relations of pure typed lambda calculi (including simply typed lambda calculus, System F, LF and the calculus of constructions).

Some typed lambda calculi introduce a notion of "subtyping", i.e. if A is a subtype of B, then all terms of type A also have type B. Typed lambda calculi with subtyping are the simply typed lambda calculus with conjunctive types and F^leq (F-sub).

All the systems mentioned so far, with the exception of the untyped lambda calculus, are "strongly normalizing": all computations terminate. As a consequence they are consistent as a logic, i.e. there are uninhabited types. There exist, however, typed lambda calculi that are not strongly normalizing. For example the dependently typed lambda calculus with a type of all types (Type : Type) is not normalizing due to Girard's paradox. This system is also the simplest Pure type system, a formalism which generalizes the Lambda cube. Systems with explicit recursion combinators, such as Plotkin's PCF, are not normalizing, but they are not intended to be interpreted as a logic. Indeed, PCF (for Programming language for Computable Functions) is a prototypical, typed functional programming language, where types are used to ensure that programs are well-behaved but not necessarily terminating.

Typed lambda calculi play an important role in the design of new type systems for programming languages; here typability usually captures desirable properties of the program, e.g. the program will not cause a memory access violation.

In programming, the routines (functions, procedures, methods) of strongly-typed programming languages closely correspond to typed lambda expressions. Eiffel has a notion of "inline agent" that makes it possible to define and manipulate typed lambda expressions directly, through such expressions as agent (p: PERSON): STRING do Result := p.spouse.name end, denoting an object that represents a function which returns a person's spouse's name.

French computer scientist Gérard Huet gave an algorithm for unification in typed lambda calculus in 1973. [ [http://mathgate.info/cebrown/notes/huet75.php "A Unification Algorithm for Typed Lambda-Calculus", Gerard P. Huet, Theoretical Computer Science 1 (1975), 27-57] ]

References

* Henk Barendregt, [ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps Lambda Calculi with Types] , Handbook of Logic in Computer Science, Volume II, Oxford University Press.


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Simply typed lambda calculus — The simply typed lambda calculus (lambda^ o) is a typed interpretation of the lambda calculus with only one type combinator: o (function type). It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus… …   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

  • Normalization property (lambda-calculus) — In mathematical logic and theoretical computer science, a rewrite system has the strong normalization property (in short: the normalization property) if every term is strongly normalizing ; that is, if every sequence of rewrites eventually… …   Wikipedia

  • Calculus of constructions — The calculus of constructions (CoC) is a higher order typed lambda calculus, initially developed by Thierry Coquand, where types are first class values. It is thus possible, within the CoC, to define functions from, say, integers to types, types… …   Wikipedia

  • 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-Kalkül — Der Lambda Kalkül ist eine formale Sprache zur Untersuchung von Funktionen. Sie beschreibt Funktionsdefinitionen, das Definieren formaler Parameter sowie das Auswerten und Einsetzen aktueller Parameter. Inhaltsverzeichnis 1 Geschichte 2 Der… …   Deutsch Wikipedia

  • Lambda-Ausdruck — Der Lambda Kalkül ist eine formale Sprache zur Untersuchung von Funktionen, die Funktionsdefinitionen, das Definieren formaler, sowie das Auswerten und Einsetzen aktueller Parameter regelt. Inhaltsverzeichnis 1 Geschichte 2 Der untypisierte… …   Deutsch Wikipedia

  • Lambda-Notation — Der Lambda Kalkül ist eine formale Sprache zur Untersuchung von Funktionen, die Funktionsdefinitionen, das Definieren formaler, sowie das Auswerten und Einsetzen aktueller Parameter regelt. Inhaltsverzeichnis 1 Geschichte 2 Der untypisierte… …   Deutsch 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

  • SKI combinator calculus — is a computational system that is a reduced, untyped version of Lambda calculus. All operations in Lambda calculus are expressed in SKI as binary trees whose leaves are one of the three symbols S, K, and I (called combinators). In fact, the… …   Wikipedia


Share the article and excerpts

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

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.