The λ calculus (lambda calculus) is a formal mathematical system
devised by Alonzo Church to investigate
functions, function application and recursion.
It has influenced many programming languages but
none more so than the functional programming languages.
Lisp was the first of these although only the "pure" Lisp sublanguage
can be called a true functional language.
Haskell, Miranda and ML are more recent examples.
The syntax of the λ calculus is short and simple. There are clauses for variable identifiers, function abstraction, function application and subexpressions. This simplicity provides great power, an example of `less is more'.
A function abstraction is an expression for a function.
The identifier is the name of the parameter; it is said to be bound.
An unbound identifier is free.
The function itself has no name.
Application is left associative:
It is convenient, but not essential, to add an option for constants.
The clause for constants can be omitted because constants can be defined with what is left but this is inconvenient and does not aid our purpose. (But see [ints], [bool] and [list] if interested.) The constants certainly include true, false, integers, some functions such as plus, minus, and a conditional function (if). Just what the set of constants contains is not crucial; it is a parameter of the λ calculus rather than a central part of it, and the set can be varied from application to application.
The previous grammar forces the use of prefix notation. It costs nothing to extend the grammar to include prefix and infix operators. The gain is purely in convenience not in power or difficulty of implementation.
This section considers list processing applications which require a list constructor, often called cons, and written as an infix operator `::'. The constant `nil' represents the empty list. Unary operators `hd' (head) and `tl' (tail) dismantle a list and `null' tests for the empty list. Conventionally a list is terminated by nil, but this is not essential.
Note that the conditional expression evaluates either its true or its false branch but not both, thus the expression below evaluates to 1 and is not in error. A strict function evaluates all of its arguments; the conditional is therefore a non-strict function.
The process of evaluating a λ expression is called reduction. Each operator must have an evaluation rule but the interesting case is the application of functions.
The actual parameter f is substituted for the formal parameter x throughout the function body, e[f/x]. This is called beta-reduction. A precise definition of substitution is given shortly.
The actual parameter 7 is substituted for n. The modified body is then evaluated.
The choice of a variable name is not important. A name can be changed provided this is done "systematically". This is called alpha-conversion.
Renaming can be used to prevent name clashes, e.g.,
We can now define substitution properly in terms of the original simple grammar. The most difficult case involves substitution in functions. There could be a name clash and the rule for functions effectively defines the scope rule of λ calculus in avoiding this problem. It is essentially the same as the scope rule in Pascal or other block-structured programming languages - this is where those programming languages got the idea.
There may be a choice of two or more applications in an expression. The strategy for determining which application to carry out next is called an evaluation rule. A familiar evaluation rule is variously known as strict evaluation or call by value. It requires the evaluation of an actual parameter before it is passed to, or substituted in, a function. It corresponds to passing parameters by value in a programming language such as Pascal. A second rule is known as normal-order evaluation or as call by name. It specifies that the left-most, outer-most application of an expression be carried out at each step. An actual parameter is not evaluated before being passed to a function. This corresponds to passing parameters by name, as in Algol-60.
In the example, normal-order evaluation terminates but strict evaluation does not.
The Church-Rosser theorem states firstly that if any evaluation rule terminates when applied to a particular expression then normal-order evaluation also terminates. Secondly, if any two evaluation rules terminate then they give the same result, up to alpha-conversion. Thus, normal-order evaluation is the most general evaluation rule of all. A functional programming language having the effect of normal-order evaluation is often called lazy. There is an efficient implementation of normal-order evaluation called call by need which can be used in functional languages. The idea is to pass an actual parameter to a function in unevaluated form. If the function needs to evaluate the parameter, it does so but it also overwrites the parameter so that it need not be reevaluated later. A small interpreter using this technique is described later.
It is a great "programming" convenience to be able to make local declarations or definitions. The extended syntax is easy.
Note that this form is not intended to allow explicitly recursive definitions. Declarations can be removed systematically, perhaps by a compiler, using the following transformation.
This shows that declarations are only a convenient shorthand. They do not add to the power of λ calculus.
Recursive or self-referential definitions are not needed to write a recursive function in λ calculus! The function Y gives the effect of recursion. Y is known as the paradoxical operator or as the fixed-point operator.
For example, a factorial program can be written with no recursive declarations, in fact with no declarations at all. First note that YF=F(YF); YF is a fixed-point of F.
Using this observation it is possible to evaluate factorial(3) as follows.
The existence of Y means that recursive declarations can be introduced for free. Any such declaration can be converted to a non-recursive one by the use of Y and can then be removed as before.
The complete grammar of a small functional programming language follows. It allows the manipulation of integer, boolean, character, empty, list and function values. In programming language terms, type-checking is done at run-time when a program is executed. Note that most modern functional languages have static (compile-time) type checkers.
The empty value `( )' is principally used as a parameter to functions with no "proper" value, as in C. It is an unnecessary value in a lazy language and is only included for use with a strict version of the interpreter which accepts the same syntax.
The functional language is quite powerful enough to perform any computation. This section gives examples; they are principally numerical but only because such examples are easily stated and have short solutions.
The factorial function can also be evaluated using the paradoxical operator, Y, as described earlier.
Recursion is usually seen in function definitions. Recursive data-structures can also be defined in (lazy) functional languages. The Hamming numbers are defined to be all products of 2, 3 and 5 only, all numbers of the form:
The sequence begins 1, 2, 3, 4, 5, 6, 8, 9, 10, 12,
The Hamming program (below) defines a list which begins with the first
If you take a Hamming number and multiply it by 2, 3 or 5
you get another Hamming number.
A moment's thought reveals that all Hamming numbers,
except 1, can be obtained in this way.
The program therefore continues by merging the results
of multiplying the members of the list by 2, 3
The merge and multiply functions are quite conventional. The program below never terminates but continues to print Hamming numbers until it runs out of space or is killed. If some finite part of the list were printed then such a program would terminate normally.
The merge and multiplication functions can be thought of as processes communicating by streams (lists) of values. The initial value `1' has to be injected to start the calculation. Many operating systems and other useful programs have similar structures where graphs of processes communicate through streams.
A popular functional programming example is the sieve of Eratosthenes. This particular version prints primes up to a limit and stops.
The function call `from 2' produces the infinite list [2, 3, 4, ...]. Sieve takes the first value off the input list, which it knows must be prime, and returns this as the start of its output list. It then removes (filters) multiples of p from the rest (tl) of the input list and sieves the result. This is just the algorithm of Eratosthenese expressed in FP. Its behaviour can be visualized as an expanding network of processes:
A more unusual primes program is an extension of the Hamming numbers program. The set of primes is the complement of the set of composite numbers in the integers. A composite number is a product of at least two primes. This can be used to define two mutually recursive lists - primes and composites. It is necessary to specify the first prime, 2. The first composite is therefore 4. This means the second prime is 3, the second composite 6, the third prime 5 and so on.
In case the reader is sceptical about the viability of this program, the start of its output follows.
-- LA 9/2007