Community hub
Recent from talks
Knowledge base stats:
Talk channels stats:
Members stats:
Lambda calculus
In mathematical logic, the lambda calculus (also written as λ-calculus) is a formal system for expressing computation based on function abstraction and application using variable binding and substitution. Untyped lambda calculus, the topic of this article, is a universal machine, a model of computation that can be used to simulate any Turing machine (and vice versa). It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics. In 1936, Church found a formulation which was logically consistent, and documented it in 1940.
The lambda calculus consists of a language of lambda terms, that are defined by a certain formal syntax, and a set of transformation rules for manipulating the lambda terms. In BNF, the syntax is where variables x,y,z range over an infinite set of names. Terms M,N,t,s,e,f range over all lambda terms. This corresponds to the following inductive definition:
A lambda term is syntactically valid if and only if it can be obtained by repeated application of these three rules. For convenience, parentheses can often be omitted when writing a lambda term—see Lambda calculus definition § Notation for details.
In the term , occurrences of x within M that are under the scope of this λ are termed bound; any occurrence of a variable not bound by an enclosing λ is free. FV(M) is the set of free variables of M. The notation denotes capture-avoiding substitution: substituting N for every free occurrence of x in M, while avoiding variable capture. This operation is defined inductively as follows:
![{\displaystyle M[x:=N]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2903f0b1ec544a7beb9cdca4dd72aed0e81e3494)
There are several notions of "equivalence" and "reduction" that make it possible to reduce lambda terms to equivalent lambda terms.
The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules. For example, (λx.M) N is a β-redex in expressing the substitution of N for x in M. The expression to which a redex reduces is called its reduct; the reduct of (λx.M) N is M[x := N].
Lambda calculus is Turing complete, that is, it is a universal model of computation that can be used to simulate any Turing machine. Its namesake, the Greek letter lambda (λ), is used in lambda expressions and lambda terms to denote binding a variable in a function.
Lambda calculus may be untyped or typed. In typed lambda calculus, functions can be applied only if they are capable of accepting the given input's "type" of data. Typed lambda calculi are strictly weaker than the untyped lambda calculus, which is the primary subject of this article, in the sense that typed lambda calculi can express less than the untyped calculus can. On the other hand, more things can be proven with typed lambda calculi. For example, in simply typed lambda calculus, it is a theorem that every evaluation strategy terminates for every simply typed lambda-term, whereas evaluation of untyped lambda-terms need not terminate (see below). One reason there are many different typed lambda calculi has been the desire to do more (of what the untyped calculus can do) without giving up on being able to prove strong theorems about the calculus.
Hub AI
Lambda calculus AI simulator
(@Lambda calculus_simulator)
Lambda calculus
In mathematical logic, the lambda calculus (also written as λ-calculus) is a formal system for expressing computation based on function abstraction and application using variable binding and substitution. Untyped lambda calculus, the topic of this article, is a universal machine, a model of computation that can be used to simulate any Turing machine (and vice versa). It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics. In 1936, Church found a formulation which was logically consistent, and documented it in 1940.
The lambda calculus consists of a language of lambda terms, that are defined by a certain formal syntax, and a set of transformation rules for manipulating the lambda terms. In BNF, the syntax is where variables x,y,z range over an infinite set of names. Terms M,N,t,s,e,f range over all lambda terms. This corresponds to the following inductive definition:
A lambda term is syntactically valid if and only if it can be obtained by repeated application of these three rules. For convenience, parentheses can often be omitted when writing a lambda term—see Lambda calculus definition § Notation for details.
In the term , occurrences of x within M that are under the scope of this λ are termed bound; any occurrence of a variable not bound by an enclosing λ is free. FV(M) is the set of free variables of M. The notation denotes capture-avoiding substitution: substituting N for every free occurrence of x in M, while avoiding variable capture. This operation is defined inductively as follows:
There are several notions of "equivalence" and "reduction" that make it possible to reduce lambda terms to equivalent lambda terms.
The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules. For example, (λx.M) N is a β-redex in expressing the substitution of N for x in M. The expression to which a redex reduces is called its reduct; the reduct of (λx.M) N is M[x := N].
Lambda calculus is Turing complete, that is, it is a universal model of computation that can be used to simulate any Turing machine. Its namesake, the Greek letter lambda (λ), is used in lambda expressions and lambda terms to denote binding a variable in a function.
Lambda calculus may be untyped or typed. In typed lambda calculus, functions can be applied only if they are capable of accepting the given input's "type" of data. Typed lambda calculi are strictly weaker than the untyped lambda calculus, which is the primary subject of this article, in the sense that typed lambda calculi can express less than the untyped calculus can. On the other hand, more things can be proven with typed lambda calculi. For example, in simply typed lambda calculus, it is a theorem that every evaluation strategy terminates for every simply typed lambda-term, whereas evaluation of untyped lambda-terms need not terminate (see below). One reason there are many different typed lambda calculi has been the desire to do more (of what the untyped calculus can do) without giving up on being able to prove strong theorems about the calculus.