HOME

TheInfoList



OR:

A typed
lambda calculus Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation t ...
is a typed formalism that uses the lambda-symbol (\lambda) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered (see kinds below). 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. Typed lambda calculi are foundational
programming languages A programming language is a system of notation for writing computer program, computer programs. Most programming languages are text-based formal languages, but they may also be visual programming language, graphical. They are a kind of computer ...
and are the base of typed functional programming languages such as ML and Haskell and, more indirectly, typed imperative programming languages. Typed lambda calculi play an important role in the design of
type systems In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progra ...
for programming languages; here, typability usually captures desirable properties of the program (e.g., the program will not cause a memory access violation). Typed lambda calculi are closely related to
mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
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 The simply typed lambda calculus (\lambda^\to), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda ...
is the language of
Cartesian closed categories In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in ma ...
(CCCs).


Kinds of typed lambda calculi

Various typed lambda calculi have been studied. The
simply typed lambda calculus The simply typed lambda calculus (\lambda^\to), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda ...
has only one type constructor, the arrow \to, and its only types are basic types and
function type In computer science and mathematical logic, a function type (or arrow type or exponential) is the type of a variable or parameter to which a function has or can be assigned, or an argument or result type of a higher-order function taking or ret ...
s \sigma\to\tau. 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 In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
are definable.
System F System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphi ...
allows polymorphism by using universal quantification over all types; from a logical perspective it can describe all functions that are provably total in
second-order logic In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies ...
. Lambda calculi with dependent types are the base of intuitionistic type theory, the
calculus of constructions In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason ...
and the logical framework (LF), a pure lambda calculus with dependent types. Based on work by Berardi on
pure type system __NOTOC__ In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and ...
s,
Henk Barendregt Hendrik Pieter (Henk) Barendregt (born 18 December 1947, Amsterdam) is a Dutch logician, known for his work in lambda calculus and type theory. Life and work Barendregt studied mathematical logic at Utrecht University, obtaining his master's de ...
proposed the
Lambda cube In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ ...
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 In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, ...
'', 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 System F<:. All the systems mentioned so far, with the exception of the untyped lambda calculus, are '' strongly normalizing'': all computations terminate. Therefore, they cannot describe all Turing-computable functions.since the
halting problem In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a ...
for the latter class was proven to be undecidable
As another 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 In mathematical logic, System U and System U− are pure type systems, i.e. special forms of a typed lambda calculus with an arbitrary number of sorts, axioms and rules (or dependencies between the sorts). They were both proved inconsistent by Jea ...
. 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 " Programming language for Computable Functions" (PCF), are not normalizing, but they are not intended to be interpreted as a logic. Indeed, PCF is a prototypical, typed functional programming language, where types are used to ensure that programs are well-behaved but not necessarily that they are terminating.


Applications to programming languages

In
computer programming Computer programming is the process of performing a particular computation (or more generally, accomplishing a specific computing result), usually by designing and building an executable computer program. Programming involves tasks such as anal ...
, the routines (functions, procedures, methods) of strongly typed programming languages closely correspond to typed lambda expressions.


See also

* Kappa calculus—an analogue of typed lambda calculus which excludes higher-order functions


Notes


Further reading

* * Brandl, Helmut (2022)
Calculus of Constructions / Typed Lambda Calculus
{{DEFAULTSORT:Typed Lambda Calculus Lambda calculus Logic in computer science Theory of computation Type theory