nLab lambda-calculus

Redirected from "typed lambda calculus".
The -calculus

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

The λ-calculus

Idea

The lambda calculus is:

It comes in both typed and untyped versions.

Concepts

Abstraction and application

The basic constructs of lambda calculus are lambda abstractions and applications. If tt is an expression of some sort involving a free variable xx (possibly vacuously), then the lambda abstraction

λx.t \lambda x. t

is intended to represent the function which takes one input and returns the result of substituting that input for xx in tt. Thus, for instance, (λx.(x+1))(\lambda x. (x+1)) is the function which adds one to its argument. Lambda expressions are often convenient, even outside lambda calculus proper, for referring to a function without giving it a name.

Application is how we “undo” abstraction, by applying a function to an argument. The application of the function ff to the argument tt is generally denoted simply by ftf t. Applications can be parenthesized, so for instance f(t)f(t) and (f)t(f)t and (ft)(f t) all denote the same thing as ftf t.

Application is generally considered to associate to the left. Thus uvwu v w denotes the application of uu to vv, followed by application of the result (assumed to again be a function) to ww. This allows the representation of functions of multiple variables in terms of functions of one variable via “currying” (named for Haskell Curry, although it was invented by Moses Schönfinkel): after being applied to the first argument, we return a function which, applied to the next argument, returns a function which, when applied to the next argument, … , returns a value. For instance, the “addition” function of two variables can be denoted (λx.(λy.x+y))(\lambda x. (\lambda y. x+y)): when applied to an argument xx, it returns a function which, when applied to an argument yy, returns x+yx+y. This is so common that it is generally abbreviated (λxy.x+y)(\lambda x y. x+y).

Evaluation and Reduction

Evaluation or reduction is the process of “computing” the “value” of a lambda term. The most basic operation is called beta reduction and consists in taking a lambda abstraction at its word about what it is supposed to do when applied to an input. For instance, the application (λx.x+1)3(\lambda x. x+1) 3 reduces to 3+13+1 (and thereby, presuming appropriate rules for ++, to 44). In general, the beta reduction of a term (λx.t)(u)(\lambda x.t)(u) is defined as the capture-avoiding substitution of uu for xx in tt,

(λx.t)(u) βt[u/x].(\lambda x.t)(u) \to_\beta t[u/x].

Terms which can be connected by a zigzag of beta reductions (in either direction) are said to be beta-equivalent.

Another basic operation often assumed in the lambda calculus is eta reduction/expansion, which consists of identifying a function, ff with the lambda abstraction (λx.fx)(\lambda x. f x) which does nothing other than apply ff to its argument. (It is called “reduction” or “expansion” depending on which “direction” it goes in, from (λx.fx)(\lambda x. f x) to ff or vice versa.)

A more basic operation than either of these, which is often not even mentioned at all, is alpha equivalence; this consists of the renaming of bound variables, e.g. (λx.fx)(λy.fy)(\lambda x. f x) \to (\lambda y. f y).

More complicated systems that build on the lambda calculus, such as various type theories, will often have other rules of evaluation as well.

In good situations, lambda calculus reduction is confluent (the Church-Rosser theorem), so that every term has at most one normal form, and two terms are equivalent precisely when they have the same normal form. A term is said to be normalizing if its reduction is also terminating—more precisely, tt is said to be weakly-normalizing if there exists a finite sequence of reductions

tt 1t 2t n t \to t_1 \to t_2 \to \dots \to t_n \nrightarrow

terminating in a normal form t nt_n, and strongly-normalizing if all sequences of reductions lead to a (by confluence, necessarily unique) normal form. In general, there exist terms which do not normalize by any reduction sequence, although simply-typed lambda calculus and many other typed variants of lambda calculus are strongly-normalizing.

Variants

Pure lambda calculus

In the untyped (or “pure”) lambda calculus, every term can be applied to any other term. As an example of the sort of freedom this allows, we can form the term u=λx.xxu = \lambda x. x x which applies its argument to itself, and then define

ω=u(u) \omega = u(u)

as the self-application of uu. Performing beta-reduction on ω\omega yields

ω βxx[u/x]=u(u)=ω βω β \omega \to_\beta x x[u/x] = u(u) = \omega \to_\beta \omega \to_\beta \dots

thus giving the classic example of a non-terminating program.

In pure untyped lambda calculus, we can define natural numbers using the Church numerals: the number nn is represented by the operation of nn-fold iteration. Thus for instance we have 2=λf.(λx.f(fx))2 = \lambda f. (\lambda x.f (f x)), the function which takes a function ff as input and returns a function that applies ff twice. Similarly 1=λf.(λx.fx)1 = \lambda f. (\lambda x.f x) is the identity on functions, while 0=λf.(λx.x)0 = \lambda f. (\lambda x . x) takes any function ff to the identity function (the 0th iterate of ff). We can then construct (very inefficiently) all of arithmetic, and prove that the arithmetic functions expressible by lambda terms are exactly the same as those computable by Turing machines or (total) recursive functions.

The most natural sort of model of pure lambda calculus is a reflexive object in a cartesian closed category, that is, an object UU together with a pair of maps

U a U U \array{U & \overset{a}{\underset{\ell}{\rightleftarrows}} & U^U}

representing aapplication and \ellambda, such that a=1a \circ \ell = 1 (to validate the β\beta equation). Such data thereby witnesses the exponential object U UU^U as a retract of UU. Of course there are no nontrivial such models in sets, but they do exist in other categories, such as domains. It is worth remarking that a necessary condition on such UU is that every term f:U Uf \colon U^U have a fixed-point; see fixed-point combinator.

From the point of view of type theory and in particular the “types à la Church” perspective, such a reflexive object UU can also be seen as the intrinsic type of every lambda term, and so the untyped lambda calculus is sometimes referred to (a bit cheekily) as really being “uni-typed”. On the other hand, from the “types à la Curry” perspective, it is also possible to begin with the pure lambda calculus as a foundation, and then try to ascribe individual terms more precise types. For example, the normalizing terms of pure lambda calculus can be characterized precisely as those which are typable in an intersection type? system.

Simply typed lambda calculus

In simply typed lambda calculus, each variable and term has a type, and we can only form the application ftf t if tt is of some type AA while ff is of a function type AB=B AA \to B = B^A whose domain is AA; the type of ftf t is then BB. Similarly, if xx is a variable of type AA and tt is a term of type BB involving xx, then λx.t\lambda x. t has type ABA\to B.

Without some further type and term constructors, there is not much that can be done, but if we add a natural numbers object (that is, a type NN with constants 00 of type NN and ss of type NNN\to N, along with a “definition-by-recursion” operator), then we can express many recursive functions. (We cannot by this means express all computable functions, although we can go beyond primitive recursive functions; for instance we can define the Ackermann function. One way to increase the expressiveness to all partial recursive functions is to add a fixpoint combinator, or an unbounded search operator).

Simply typed lambda calculus is the natural internal language of cartesian closed categories. This means that

  • Every cartesian closed category gives rise to a simply typed lambda calculus whose basic types are its objects, and whose basic terms are its morphisms, while

  • Every simply typed lambda calculus “generates” a cartesian closed category whose objects are its types and whose morphisms are its equivalence classes of terms.

These two operations are adjoint in an appropriate sense.

Functional programming

Most functional programming languages, such as Lisp, ML, and Haskell, are at least loosely based on lambda calculus.

References

Textbook accounts:

Introduction to simply typed λ\lambda-calculus:

The idea that untyped lambda calculus can be modeled internally to a cartesian closed category as a reflexive object (an object UU such that the exponential U UU^U is a retract of UU) was formulated explicitly by Dana Scott in

  • Dana Scott. Relating theories of the λ\lambda-calculus. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism (eds. Hindley and Seldin), Academic Press, 403–450, 1980.

This followed his earlier work constructing an explicit such model in the category of domains:

  • Dana S. Scott, Outline of a mathematical theory of computation, in: Proceedings of the Fourth Annual Princeton Conference on Information Sciences and Systems (1970) 169–176. [pdf, pdf]

  • Dana Scott, Data types as lattices. SIAM Journal of Computing 5 3 (1976) 522–587 [doi:10.1137/0205037, pdf]

Another, more recent take on pure lambda calculus as a certain kind of algebraic theory (called a “lambda theory”) can be found in

Last revised on February 28, 2023 at 14:35:20. See the history of this page for a list of all contributions to it.