Lambda calculus

The lambda calculus is a formal language for the study of functions. He describes the definition of functions and bound parameters and was introduced in the 1930s by Alonzo Church and Stephen Cole Kleene. Today, he is an important construct for theoretical computer science, logic and linguistics higher level.

History

Alonzo Church used it to give 1936 both a negative answer to the decision problem as to find a foundation of a logical system, as it was based on Russell and Whitehead's Principia Mathematica. By means of the untyped lambda calculus can clearly define what is a computable function. The question of whether two lambda expressions (see below ) is equivalent, in general, can not be decided algorithmically. In its typed form of the calculus can be used to represent a higher level logic. The lambda calculus has substantially influenced the development of functional programming languages ​​, the research to type systems of programming languages ​​in general, and modern disciplines in the logic as the theory of types.

Developmental milestones were:

• After the introduction of the early discovery that everything can be expressed with the lambda calculus, which can be expressed with a Turing machine. In other words, the purpose of the concept of predictability are equally powerful.
• Konrad Zuse has incorporated into his plan calculus ideas from the lambda calculus from 1942 to 1946.
• John McCarthy had been used for the end of the fifties, thus defining the minimal features of the programming language Lisp.
• The typed versions of the lambda calculus led to modern programming languages ​​such as ML or Haskell.
• As a very fruitful idea, expressions of the typed lambda calculus for the representation of terms proved to create a logic based, so to use the lambda calculus as a meta- logic. First Church 1940 presented in his Theory of Simple Types, led both to modern theorem provers for higher order logics, and ...
• Other hand, in the 70s and 80s to logics with ever more powerful type systems, which are sure to represent itself as a lambda expression such as logical evidence.
• Based on the lambda calculus of pi-calculus by Robin Milner was developed in the 90s for the description of concurrent processes.

The untyped lambda calculus

Motivation

Let us start from a mathematical term, we can conclude form that maps to the function. It also writes. In the lambda calculus, the first thing to formalize such training function linguistically. In lambda calculus we would take the term

. Write It is said that the free variable is bound by abstraction. For comparison, consider in mind that variable binding also occur in other areas of mathematics:

• Set theory:
• Logic and
• Analysis:

You can also make abstraction for a variable that does not occur in the term: eg. This expression then designates the function of each of the maps to. More generally, the function of which is constant. If we abstract now still retroactively after, we get with a formalization of the function that assigns to each value of the function is constant. Thus, the expression represents a funktionswertige function. In the lambda calculus, but can be expressed also functions whose arguments are already functions. We assume the function that associates each function to another function, which results in such a way that is applied twice. Thus is indicated by the term, and the allocation by.

Since terms are seen as functions that you can apply it to an argument. We speak of application and writes in the lambda calculus rather instead. Parentheses can of course Terme group. The application as a connecting principle of terms is defined as left-associative, ie means. In the usual mathematical notation you would write here. Applying now an argument to a lambda term, ie, as the result calculated by the fact that in the term of each occurrence of the variable is replaced by. This derivation rule is called conversion.

It may be noticed that terms formulate more general principles of mathematics, and they do not call it that very objects of the standard mathematical universe. For example, formulated the principle of allocating the identical mapping but this is always relative to a given set as a set of definitions. A universal identity as a function is not defined in the set-theoretic formulation of mathematics. The lambda calculus in the strict sense is therefore more likely to be seen as a redesign of mathematics, in which the basic objects are understood as universal functions, in contrast to axiomatic set theory, where the basic objects are sets.

Numbers and terms as are initially not part of the pure lambda calculus. Similarly as in set theory, where one can construct numbers and arithmetic alone from the concept of set out, but it is also possible in the lambda calculus to define on the basis of abstraction and application arithmetic. Since each term is understood as a unary function in lambda calculus, an addition should be understood as the function that maps each number that ( digit ) function that returns the value added to each number. (See currying. )

Lambda terms without free variables are also called combinators. The combinatorial logic ( or combinator calculus ) can be seen as an alternative approach to the lambda calculus.

Formal definition

In its most basic, yet complete Form are in the lambda calculus three types of terms (T) here in Backus- Naur Form:

T :: = a ( variable ) | ( TT ) (Application) | λa.T (lambda, also called abstraction)

Where a is an arbitrary symbol from a least countably infinite set of variables, symbols ( short variables) is. For practical purposes, the lambda calculus is usually expanded by another variety of terms, the constant symbols.

The amount of the free variables can be defined inductively FV of the structure of the λ terms as follows:

The amount of bound variables B ( t ) of a term t is calculated inductively:

By means of the definition of free and bound variables may now about the ( free ) variable substitution ( establishment ) are inductively defined by:

Note: x ← T stands for the replacement of x by T.

Note that the substitution is only partially defined; possibly bound variables must be appropriately renamed (see α - congruence below ), so that there is never a free variable is bound in a substitute, through the setting for a variable.

Can over the set of λ -terms now matching rules ( written here ==) are defined, which summarize the formal intuition that two expressions describe the same function. These relations are detected by the so-called α - conversion, the β conversion and the η - conversion.

Matching rules

α - conversion

The α - conversion rule formalizes the idea that the names of bound variables " smoke and mirrors " are; For example, mean and λx.x λy.y same function. However, the details are not quite as simple as it first appears: A number of limitations need to be considered when bound variables are replaced by other bound variables.

Formally, the rule is as follows:

If W occurs nowhere free in E and W is not bound in E where it replaces a V. Since a congruence rule is applicable in every part of term, it allows the derivation that λ x. ( λ x. x) x = λ y. ( λ x. x) y.

β - conversion

The β - conversion rule formalizes the concept of " function application ". If they applied exclusively from left to right, one also speaks of β - reduction. Formally, they can be extended by

Describe, where all free variables in E ' in E [ V ← e '] must remain free (see constraint in the substitution definition).

A term called " β in normal form " if no β - reduction is more applicable ( not exist for all of the terms a β - normal form, see below ). A deep result of Church and Rosser on the λ - calculus states that the sequences of α - conversion and β - reduction in a sense irrelevant: if T1 and T2 derives a term to two terms, there is always a possibility T1 and T2 each derive a common term T3.

η - conversion

The η - conversion can be optionally added to the calculus. They formalized the concept of extensionality, which means that two functions are equal if and only if they give the same result for all arguments. Formally, the η - conversion is described by:

Comments

• Not for all terms, there is a β - normal form. For example, one can apply the term, although reduction, but one again obtains the same expression as the result.
• Each term, satisfies the condition of β rule is called β - reducible.
• The β - reduction is not unique in general; there may be several " starting points " ( β - redexes ) provide for the application of the β - rule because the rule application is possible in all sub- terms.
• When multiple sequences of β - reductions are possible and several of them lead to a non- β - reducible term, these terms are identical up to α - congruence.
• However, if a sequence of the β - β to a non - reducible term ( a result) leads, so does the standard reduction order, wherein the first term in the oxygen will be used first.
• In an alternative notation, the variable name with de - Bruijn indices are replaced. These indices represent the number of lambda -terms between the variable and its binding lambda expression. This display is often used in computer programs.

Other examples

• The term λx.λy. ( (xy) false) is one of many possibilities the logical function and display. For this one understands true as an abbreviation for λx.λy.x and false as an abbreviation for λx.λy.y. The term fulfills all requirements that are asked on the function and. ( ( and true) true) = ((( λx.λy. ( (xy) false) ) true) true) = ( true true ) = false ( ( λx.λy.x ) true) false = ( λy.wahr ) false = true
• ( ( and true) false) = ... = ( true false ) false = ... = ( λy.falsch ) false = false
• ( ( and false ) true) = ( true false ) false = (( λx.λy.y ) true) false = ( λy.y ) false = false
• ( ( and false ) false) = ( false false ) false = ... = ( λy.y ) false = false

Typed Lambda Calculus

The central idea of the typed lambda calculus is to consider only lambda expressions, which a type can be assigned by a system of Typinferenzregeln. The simplest type of system that was introduced by Church in his 1940 Theory of Simple Types, provides for the types that are generated by the following grammar in Backus- Naur Form:

The type I ( individuals) can be thought of as numbers, O is used for Boolean values ​​as True and False.

In addition, an environment is defined; this is a function that maps symbols variable types TT.

A triple from an environment, an expression e and a type T is written is called a type judgment.

Now, the inference relations between expressions that produce their types and type judgments:

This is the function that maps the type of the point, and otherwise the function. (In other words, the a parameter of the function is type and exactly this information is added to the environment. )

By introducing a second environment and constant symbols are treatable; Another important extension is also the category of type variables or type constructors such permit in types: as already produces very powerful functional or logical core languages.

It is decidable whether an untyped term can be typified, even when the environment is unknown (a variant with type variables and type constructors is the algorithm according to Hindley - Milner ).

The set of typable expressions is a proper subset of the untyped lambda calculus; For example, the Y- combinator could not be typed. On the other hand, is decidable for typed expressions equality between two functions modulo α and β conversions. It is known that the matching problem on lambda expressions is decidable to fourth order. The unification problem is undecidable; However, there are practically useful approximate algorithms.

Application in the semantics

The semantics is that branch of linguistics, which analyzes the meaning of natural language expressions. The formal semantics initially uses this simple means of predicate logic and set theory. This one expanded to include basics of lambda calculus to approximately represent means of lambda abstraction propositions as properties and can represent more complex noun phrases, adjective phrases, and some verb phrases. It is based around a model-theoretic semantic interpretation of intensional logic Richard Montague.

Application in computer science

The lambda calculus is the formal basis for many programming languages ​​such as Scheme or Lisp. In the programming languages ​​commonly used and well-built it is mostly used as an additional module or library. One example is Ruby.