Lambda Calculus
I saw this mentioned when reading about functional programming and want to learn more about it.
References
Notes
Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. Untyped lambda calculus is a universal machine, a model of computation that can be used to simulate any Turing machine (and vice versa).
Lambda calculus consists of constructing lambda terms and performing reduction operations on them. A term is defined as any valid lambda calculus expression. In the simplest form of lambda calculus, terms are built using only the following rules:
- : A variable is a character or string representing a parameter
- (): A lambda abstraction is a function definition, taking as input the bound variable (between the and thee punctum/dot .) and returning the body
- (): An application, applying a function to an argument . Both and are lambda terms.
The reduction operations include:
- (: -conversion, renaming the bound variables in the expression. Used to avoid name collisions.
- : -reduction, replacing the bound variables with the argument expression in the body of the abstraction
Lambda calculus is Turing complete, that is, it is a 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 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 primary subject of this article, in the sense that typed lambda calculi can express less than the untyped calculus can, On the other hand, typed lambda calculi allow more things to be proven.
Lambda calculus has many applications in many different areas in mathematics, philosophy, linguistics, and computer science. Lambda calculus has played an important role in the development of the theory of programming languages. Functional programming languages implement lambda calculus. Lambda calculus is also a current research topic in category theory.
Lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.
Computable functions are a fundamental concept within computer science and mathematics. The lambda calculus provides simple semantics for computation which are useful for formally studying properties of computation. The first simplification is that lambda calculus treats functions anonymously
: it does not given them explicit names.
Named Function:
Anonymous Function:
( A tuple of x and y is mapped to )
Lambda calculus only uses functions of a single input. An ordinary function that requires two inputs, for instance the function, can be reworked into an equivalent function that accepts a single input, and as output returns another function, that in turn accepts a single input.
can be reworked into . This method is known as currying, transforms a function that takes multiple arguments into a chain of functions each with a single argument.
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. All lambda functions are anonymous and take one input variable - multiple inputs can be handled with currying.
The syntax of the lambda calculus defines some expressions as valid lambda calculus expressions and some as invalid, just as some strings of characters are valid computer programs and some are not. A valid lambda calculus expression is called a lambda term.
The following three rules give an inductive definition that can be applied to build all syntactically valid lambda terms:
- variable is itself a valid lambda term
- if is a lambda term, and is a variable, then is a lambda term (called an abstraction)
- if and are lambda terms, then is a lambda term (called an application)
Nothing else is a lambda term. That is, a lambda term is valid if and only if it can be obtained by repeated application of these three rules.
In lambda calculus, functions are taken to be first class values
, so functions may be used as inputs, or be returned as outputs from other functions. A basic from of equivalence, definable on lambda terms, is alpha equivalence. It captures the intuition that the particular choice of bound variable, in an abstraction does not usually matter. For instance, and are alpha-equivalent lambda terms, and they both represent the same function (identity function). The terms and are not alpha-equivalent, because they are not bound in abstraction.
The free variables of a term are those variables not bound by an abstraction. The set of free variables of an expression is defined inductively:
- The free variables of are just
- The set of free variables of is the set of free variables of , but with removed
- The set of free variables of is the union of the set of free variables of and the set of free variables of
Comments
You have to be logged in to add a comment
User Comments
There are currently no comments for this article.