This article may be too technical for most readers to understand.(November 2014) |
Lambda calculus is a formal mathematical system based on lambda abstraction and function application. Two definitions of the language are given here: a standard definition, and a definition using mathematical formulas.
This formal definition was given by Alonzo Church.
Lambda expressions are composed of
The set of lambda expressions, , can be defined inductively:
Instances of rule 2 are known as abstractions and instances of rule 3 are known as applications. [1]
To keep the notation of lambda expressions uncluttered, the following conventions are usually applied.
The abstraction operator, , is said to bind its variable wherever it occurs in the body of the abstraction. Variables that fall within the scope of an abstraction are said to be bound. All other variables are called free. For example, in the following expression is a bound variable and is free: . Also note that a variable is bound by its "nearest" abstraction. In the following example the single occurrence of in the expression is bound by the second lambda:
The set of free variables of a lambda expression, , is denoted as and is defined by recursion on the structure of the terms, as follows:
An expression that contains no free variables is said to be closed. Closed lambda expressions are also known as combinators and are equivalent to terms in combinatory logic.
The meaning of lambda expressions is defined by how expressions can be reduced. [6]
There are three kinds of reduction:
We also speak of the resulting equivalences: two expressions are β-equivalent, if they can be β-converted into the same expression, and α/η-equivalence are defined similarly.
The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules. For example, is a β-redex in expressing the substitution of for in ; if is not free in , is an η-redex. The expression to which a redex reduces is called its reduct; using the previous example, the reducts of these expressions are respectively and .
Alpha-conversion, sometimes known as alpha-renaming, [7] allows bound variable names to be changed. For example, alpha-conversion of might yield . Terms that differ only by alpha-conversion are called α-equivalent. Frequently in uses of lambda calculus, α-equivalent terms are considered to be equivalent.
The precise rules for alpha-conversion are not completely trivial. First, when alpha-converting an abstraction, the only variable occurrences that are renamed are those that are bound by the same abstraction. For example, an alpha-conversion of could result in , but it could not result in . The latter has a different meaning from the original.
Second, alpha-conversion is not possible if it would result in a variable getting captured by a different abstraction. For example, if we replace with in , we get , which is not at all the same.
In programming languages with static scope, alpha-conversion can be used to make name resolution simpler by ensuring that no variable name masks a name in a containing scope (see alpha renaming to make name resolution trivial).
Substitution, written , is the process of replacing all free occurrences of the variable in the expression with expression . Substitution on terms of the lambda calculus is defined by recursion on the structure of terms, as follows (note: x and y are only variables while M and N are any λ expression).
To substitute into a lambda abstraction, it is sometimes necessary to α-convert the expression. For example, it is not correct for to result in , because the substituted was supposed to be free but ended up being bound. The correct substitution in this case is , up to α-equivalence. Notice that substitution is defined uniquely up to α-equivalence.
β-reduction captures the idea of function application. β-reduction is defined in terms of substitution: the β-reduction of is .
For example, assuming some encoding of , we have the following β-reduction: .
η-reduction expresses the idea of extensionality, which in this context is that two functions are the same if and only if they give the same result for all arguments. η-reduction converts between and whenever does not appear free in .
The purpose of β-reduction is to calculate a value. A value in lambda calculus is a function. So β-reduction continues until the expression looks like a function abstraction.
A lambda expression that cannot be reduced further, by either β-redex, or η-redex is in normal form. Note that alpha-conversion may convert functions. All normal forms that can be converted into each other by α-conversion are defined to be equal. See the main article on Beta normal form for details.
Normal Form Type | Definition. |
---|---|
Normal Form | No β- or η-reductions are possible. |
Head Normal Form | In the form of a lambda abstraction whose body is not reducible. |
Weak Head Normal Form | In the form of a lambda abstraction. |
Lambda Calculus has a simple syntax. A lambda calculus program has the syntax of an expression where,
Name | BNF | Description |
---|---|---|
Abstraction | <expression>::= λ <variable-list> . <expression> | Anonymous function definition. |
Application term | <expression>::=<application-term> | |
Application | <application-term>::=<application-term><item> | A function call. |
Item | <application-term>::=<item> | |
Variable | <item>::=<variable> | E.g. x, y, fact, sum, ... |
Grouping | <item>::= ( <expression> ) | Bracketed expression. |
The variable list is defined as,
<variable-list>::=<variable> | <variable>, <variable-list>
A variable as used by computer scientists has the syntax,
<variable>::=<alpha><extension><extension>::=<extension>::=<extension-char><extension><extension-char>::=<alpha> | <digit> | _
Mathematicians will sometimes restrict a variable to be a single alphabetic character. When using this convention the comma is omitted from the variable list.
A lambda abstraction has a lower precedence than an application, so;
Applications are left associative;
An abstraction with multiple parameters is equivalent to multiple abstractions of one parameter.
where,
The problem of how variables may be renamed is difficult. This definition avoids the problem by substituting all names with canonical names, which are constructed based on the position of the definition of the name in the expression. The approach is analogous to what a compiler does, but has been adapted to work within the constraints of mathematics.
The execution of a lambda expression proceeds using the following reductions and transformations,
where,
Execution is performing β-reductions and η-reductions on subexpressions in the canonym of a lambda expression until the result is a lambda function (abstraction) in the normal form.
All α-conversions of a λ-expression are considered to be equivalent.
Canonym is a function that takes a lambda expression and renames all names canonically, based on their positions in the expression. This might be implemented as,
Where, N is the string "N", F is the string "F", S is the string "S", + is concatenation, and "name" converts a string into a name
Map from one value to another if the value is in the map. O is the empty map.
If L is a lambda expression, x is a name, and y is a lambda expression; means substitute x by y in L. The rules are,
Note that rule 1 must be modified if it is to be used on non canonically renamed lambda expressions. See Changes to the substitution operator.
The set of free variables of a lambda expression, M, is denoted as FV(M). This is the set of variable names that have instances not bound (used) in a lambda abstraction, within the lambda expression. They are the variable names that may be bound to formal parameter variables from outside the lambda expression.
The set of bound variables of a lambda expression, M, is denoted as BV(M). This is the set of variable names that have instances bound (used) in a lambda abstraction, within the lambda expression.
The rules for the two sets are given below. [5]
- Free Variable Set | Comment | - Bound Variable Set | Comment |
---|---|---|---|
where x is a variable | where x is a variable | ||
Free variables of M excluding x | Bound variables of M plus x. | ||
Combine the free variables from the function and the parameter | Combine the bound variables from the function and the parameter |
Usage;
This mathematical definition is structured so that it represents the result, and not the way it gets calculated. However the result may be different between lazy and eager evaluation. This difference is described in the evaluation formulas.
The definitions given here assume that the first definition that matches the lambda expression will be used. This convention is used to make the definition more readable. Otherwise some if conditions would be required to make the definition precise.
Running or evaluating a lambda expression L is,
where Q is a name prefix possibly an empty string and eval is defined by,
Then the evaluation strategy may be chosen as either,
The result may be different depending on the strategy used. Eager evaluation will apply all reductions possible, leaving the result in normal form, while lazy evaluation will omit some reductions in parameters, leaving the result in "weak head normal form".
All reductions that can be applied have been applied. This is the result obtained from applying eager evaluation.
In all other cases,
Reductions to the function (the head) have been applied, but not all reductions to the parameter have been applied. This is the result obtained from applying lazy evaluation.
In all other cases,
The standard definition of lambda calculus uses some definitions which may be considered as theorems, which can be proved based on the definition as mathematical formulas.
The canonical naming definition deals with the problem of variable identity by constructing a unique name for each variable based on the position of the lambda abstraction for the variable name in the expression.
This definition introduces the rules used in the standard definition and relates explains them in terms of the canonical renaming definition.
The lambda abstraction operator, λ, takes a formal parameter variable and a body expression. When evaluated the formal parameter variable is identified with the value of the actual parameter.
Variables in a lambda expression may either be "bound" or "free". Bound variables are variable names that are already attached to formal parameter variables in the expression.
The formal parameter variable is said to bind the variable name wherever it occurs free in the body. Variable (names) that have already been matched to formal parameter variable are said to be bound. All other variables in the expression are called free.
For example, in the following expression y is a bound variable and x is free: . Also note that a variable is bound by its "nearest" lambda abstraction. In the following example the single occurrence of x in the expression is bound by the second lambda:
In the definition of the Substitution Operator the rule,
must be replaced with,
This is to stop bound variables with the same name being substituted. This would not have occurred in a canonically renamed lambda expression.
For example the previous rules would have wrongly translated,
The new rules block this substitution so that it remains as,
The meaning of lambda expressions is defined by how expressions can be transformed or reduced. [6]
There are three kinds of transformation:
We also speak of the resulting equivalences: two expressions are β-equivalent, if they can be β-converted into the same expression, and α/η-equivalence are defined similarly.
The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules.
Alpha-conversion, sometimes known as alpha-renaming, [7] allows bound variable names to be changed. For example, alpha-conversion of might give . Terms that differ only by alpha-conversion are called α-equivalent.
In an α-conversion, names may be substituted for new names if the new name is not free in the body, as this would lead to the capture of free variables.
Note that the substitution will not recurse into the body of lambda expressions with formal parameter because of the change to the substitution operator described above.
See example;
α-conversion | λ-expression | Canonically named | Comment |
---|---|---|---|
Original expressions. | |||
correctly rename y to k, (because k is not used in the body) | No change to canonical renamed expression. | ||
naively rename y to z, (wrong because z free in ) | is captured. |
β-reduction captures the idea of function application (also called a function call), and implements the substitution of the actual parameter expression for the formal parameter variable. β-reduction is defined in terms of substitution.
If no variable names are free in the actual parameter and bound in the body, β-reduction may be performed on the lambda abstraction without canonical renaming.
Alpha renaming may be used on to rename names that are free in but bound in , to meet the pre-condition for this transformation.
See example;
β-reduction | λ-expression | Canonically named | Comment | ||||
---|---|---|---|---|---|---|---|
Original expressions. | |||||||
Naive beta 1, |
| x (P) and y (PN) have been captured in the substitution. | |||||
Alpha rename inner, x → a, y → b | |||||||
Beta 2, |
| x and y not captured. |
In this example,
η-reduction expresses the idea of extensionality, which in this context is that two functions are the same if and only if they give the same result for all arguments.
η-reduction may be used without change on lambda expressions that are not canonically renamed.
The problem with using an η-redex when f has free variables is shown in this example,
Reduction | Lambda expression | β-reduction |
---|---|---|
Naive η-reduction |
This improper use of η-reduction changes the meaning by leaving x in unsubstituted.
Lambda 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 that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics.
In probability theory and statistics, the negative binomial distribution is a discrete probability distribution that models the number of failures in a sequence of independent and identically distributed Bernoulli trials before a specified (non-random) number of successes occurs. For example, we can define rolling a 6 on a dice as a success, and rolling any other number as a failure, and ask how many failure rolls will occur before we see the third success. In such a case, the probability distribution of the number of failures that appear will be a negative binomial distribution.
In probability theory and statistics, the exponential distribution or negative exponential distribution is the probability distribution of the time between events in a Poisson point process, i.e., a process in which events occur continuously and independently at a constant average rate. It is a particular case of the gamma distribution. It is the continuous analogue of the geometric distribution, and it has the key property of being memoryless. In addition to being used for the analysis of Poisson point processes it is found in various other contexts.
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators, which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.
In mathematics and computer science in general, a fixed point of a function is a value that is mapped to itself by the function.
In probability theory and statistics, the gamma distribution is a two-parameter family of continuous probability distributions. The exponential distribution, Erlang distribution, and chi-squared distribution are special cases of the gamma distribution. There are two equivalent parameterizations in common use:
In mathematics, the Hodge star operator or Hodge star is a linear map defined on the exterior algebra of a finite-dimensional oriented vector space endowed with a nondegenerate symmetric bilinear form. Applying the operator to an element of the algebra produces the Hodge dual of the element. This map was introduced by W. V. D. Hodge.
In mathematical logic and type theory, the λ-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 λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to:
In probability theory, a compound Poisson distribution is the probability distribution of the sum of a number of independent identically-distributed random variables, where the number of terms to be added is itself a Poisson-distributed variable. The result can be either a continuous or a discrete distribution.
In probability and statistics, the Dirichlet distribution (after Peter Gustav Lejeune Dirichlet), often denoted , is a family of continuous multivariate probability distributions parameterized by a vector of positive reals. It is a multivariate generalization of the beta distribution, hence its alternative name of multivariate beta distribution (MBD). Dirichlet distributions are commonly used as prior distributions in Bayesian statistics, and in fact, the Dirichlet distribution is the conjugate prior of the categorical distribution and multinomial distribution.
Variational Bayesian methods are a family of techniques for approximating intractable integrals arising in Bayesian inference and machine learning. They are typically used in complex statistical models consisting of observed variables as well as unknown parameters and latent variables, with various sorts of relationships among the three types of random variables, as might be described by a graphical model. As typical in Bayesian inference, the parameters and latent variables are grouped together as "unobserved variables". Variational Bayesian methods are primarily used for two purposes:
Lambda lifting is a meta-process that restructures a computer program so that functions are defined independently of each other in a global scope. An individual "lift" transforms a local function into a global function. It is a two step process, consisting of;
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way.
A ratio distribution is a probability distribution constructed as the distribution of the ratio of random variables having two other known distributions. Given two random variables X and Y, the distribution of the random variable Z that is formed as the ratio Z = X/Y is a ratio distribution.
In mathematics, the spectral theory of ordinary differential equations is the part of spectral theory concerned with the determination of the spectrum and eigenfunction expansion associated with a linear ordinary differential equation. In his dissertation, Hermann Weyl generalized the classical Sturm–Liouville theory on a finite closed interval to second order differential operators with singularities at the endpoints of the interval, possibly semi-infinite or infinite. Unlike the classical case, the spectrum may no longer consist of just a countable set of eigenvalues, but may also contain a continuous part. In this case the eigenfunction expansion involves an integral over the continuous part with respect to a spectral measure, given by the Titchmarsh–Kodaira formula. The theory was put in its final simplified form for singular differential equations of even degree by Kodaira and others, using von Neumann's spectral theorem. It has had important applications in quantum mechanics, operator theory and harmonic analysis on semisimple Lie groups.
In probability theory and statistics, the Poisson distribution is a discrete probability distribution that expresses the probability of a given number of events occurring in a fixed interval of time or space if these events occur with a known constant mean rate and independently of the time since the last event. It is named after French mathematician Siméon Denis Poisson. The Poisson distribution can also be used for the number of events in other specified interval types such as distance, area, or volume. It plays an important role for discrete-stable distributions.
In computer science, a "let" expression associates a function definition with a restricted scope.
In rewriting, a reduction strategy or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation. Some authors use the term to refer to an evaluation strategy.
Deductive lambda calculus considers what happens when lambda terms are regarded as mathematical expressions. One interpretation of the untyped lambda calculus is as a programming language where evaluation proceeds by performing reductions on an expression until it is in normal form. In this interpretation, if the expression never reduces to normal form then the program never terminates, and the value is undefined. Considered as a mathematical deductive system, each reduction would not alter the value of the expression. The expression would equal the reduction of the expression.
In statistics, the variance function is a smooth function that depicts the variance of a random quantity as a function of its mean. The variance function is a measure of heteroscedasticity and plays a large role in many settings of statistical modelling. It is a main ingredient in the generalized linear model framework and a tool used in non-parametric regression, semiparametric regression and functional data analysis. In parametric modeling, variance functions take on a parametric form and explicitly describe the relationship between the variance and the mean of a random quantity. In a non-parametric setting, the variance function is assumed to be a smooth function.