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. λ-calculus also provides the meta-language for formal definitions in denotational semantics. It has a good claim to be the prototype programming language.

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'.

<Exp>	::=	<identifier>	|
		( <Exp> )	|
		<Exp> <Exp>	|	--application
		λ<identifier>.<Exp>		--abstraction

— Syntax of the λ-calculus —

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: f x y=(f x)y.

It is convenient, but not essential, to add an option for constants.

<Exp>	::=	<identifier>	|
		<constant>	|
		( <Exp> )	|
		<Exp> <Exp>	|	--application
		λ<identifier>.<Exp>		--abstraction

— Syntax of the λ-calculus with 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.

<Exp> ::= ... as before ... |
          <unopr> <Exp> |
          <Exp> <binopr> <Exp> |
          if <Exp> then <Exp> else <Exp>

— Extended Grammar to include Operators —

Lists.

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.

hd (a::b) = a  |
hd x      = error

tl (a::b) = b  |
tl x      = error

null (a::b) = false |
null nil  = true    |
null x    = error

if  true then a else b = a    |
if false then a else b = b    |
if     x then a else b = error

— List and Conditional Operators —

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.

hd (if true then 1::2::nil else nil) --> 1

Evaluation.

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.

(λ x.e)f --> e[f/x]

 

— Application; Beta-Reduction —

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.

E.g.,

    (λ n. n*2+3) 7
--> (n*2+3)[7/n]
--> 7*2+3
--> 14+3
--> 17

— A Function Application —

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.

(λ x.e) = (λ y.e[y/x]), provided y not free in e

 

— Name Changing; Alpha-Conversion —

Renaming can be used to prevent name clashes, e.g.,

   λ x. (λ x. x)
=  λ x. (λ y. y)

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.

x, y, y' :ident; c :constant; e, e', a :Exp

 

x[a/x] --> a

y[a/x] --> y, if y!=x

 

c[a/x] --> c

 

(λ y.e)[a/x]

--> λ y.e, if y=x

--> λ y'.(e[y'/y][a/x]), if y!=x, x free in e, y free in a, new y'

--> λ y.(e[a/x]), otherwise

 

(e e')[a/x] --> (e[a/x])(e'[a/x])

 

(e)[a/x] --> (e[a/x])

 

— Definition of Substitution —

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.

e.g.,

(λ x. 7) ((λ x. x x)(λ y. y y))

either

--> 7 normal-order terminates

or

--> (λ x. 7) ((λ y. y y)(λ y. y y)) strict

--> ... loops

 

— Order of Evaluation —

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.

<Exp> ::= ... as before ... |
          let <decs> in <Exp>

<Decs> ::= <Dec>, <Decs> | <Dec>

<Dec>  ::= <ident> = <Exp>

— Extended Grammar including Declarations —

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.

let x=e in f  -->  (λ x.f)e

let x=e, y=f in g
--> (λ xy. (λ x. λ y. g) (hd xy) (tl xy)) (e::f)

— Removing Declarations —

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.

Y = λ G. (λ g. G(g g)) (λ g. G(g g))

 

— The Paradoxical Operator, Y —

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.

    Y F
=   (λ G. (λ g.G(g g)) (λ g.G(g g))) F
--> (λ g. F(g g)) (λ g. F(g g))
--> F( (λ g. F(g g)) (λ g. F(g g)) )
=   F( Y F )

Using this observation it is possible to evaluate factorial(3) as follows.

let F = λ f. λ n. if n=0 then 1 else n*f(n-1)
in  Y F 3

--> Y (λ f. λ n. if n=0 then 1 else n*f(n-1)) 3

--> F(Y F) 3

=   (λ f.λ n.if n=0 then 1 else n*f(n-1)) (Y F) 3

--> (λ n. if n=0 then 1 else n*(Y F)(n-1)) 3    [*]
--> if 3=0 then 1 else 3*( (Y F 2) )

--> 3*( Y F 2 )
 ...
--> 6

[*] normal order

— Evaluation of factorial(3) —

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.

<Exp> ::= ... as before ... |
          let [rec] <decs> in <Exp>

— Extended Grammar for Recursive Declarations —

let rec x=e in f  -->  let x=Y(λ x.e) in f

let rec x=e, y=f in g
--> let rec xy= let x=hd xy, y=tl xy
                in e::f
    in let x=hd xy, y=tl xy
       in g

— Removing Recursive Declarations —

A Functional Programming Language.

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.

<program> ::= <Exp>

<Exp> ::= <ident> | <numeral> |
          '<letter>' | () | true | false | nil |
          ( <Exp> ) |
          <unopr> <Exp> | <Exp> <binopr> <Exp> |
          if <Exp> then <Exp> else <Exp> |
          λ <param> . <Exp> |  <Exp> <Exp> |
          let [rec] <decs> in <Exp>

<decs>  ::= <dec>,<decs> | <dec>
<dec>   ::= <ident>=<Exp>

<param> ::= () | <ident>

<unopr> ::= hd | tl | null | not | -
<binopr> ::= and | or | = | <> | < | <= | > | >= |
             + | - | * | / | ::

priorities: ::               1 cons list (right assoc)
            or               2
            and              3
            = <> < <= > >=   4 scalars only
            + -              5 (binary -)
            * /              6
            application      7
            - hd tl null not 8 (unary -)

— Grammar for a Functional Programming Language —

Programming Techniques.

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.

program: [fact.fp]

let rec fact = lambda n. if n=0 then 1 else n*fact(n-1) in fact 10 {\fB Factorial. \fP}

output area

The factorial function can also be evaluated using the paradoxical operator, Y, as described earlier.

program: [Y.fp]

let Y = lambda G. (lambda g. G(g g)) (lambda g. G(g g)) in let F = lambda f. lambda n. if n=0 then 1 else n*f(n-1) in Y F 10 {<B> Factorial via Y </B>}

output area

Circular Programs.

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:

2ⁱ×3^j×5^k, i,j,k>=0

The sequence begins 1, 2, 3, 4, 5, 6, 8, 9, 10, 12, 15, ... . Note that 7, 11, 13, 14 are not in the list.

The Hamming program (below) defines a list which begins with the first Hamming number '1':

hamm = 1 :: ...

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 and 5.

merge (mult 2 hamm) (merge .... )

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.

program: [hamm.fp]

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.

let rec merge = lambda a. lambda b. if hd a < hd b then (hd a)::(merge tl a b) else if hd b < hd a then (hd b)::(merge a tl b) else (hd a)::(merge tl a tl b), mul = lambda n. lambda l. (n* hd l)::(mul n tl l), first = lambda n. lambda l. if n <= 0 then nil else hd l :: first (n-1) tl l in let rec hamm = 1 :: (merge (mul 2 hamm) (merge (mul 3 hamm) (mul 5 hamm))) in first 10 hamm {\fB Hamming Numbers. \fP}

output area

Sieve of Eratosthenese.

A popular functional programming example is the sieve of Eratosthenes. This particular version prints primes up to a limit and stops.

program: [primes.fp]

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:

let rec first = lambda n. lambda l. if n=0 then nil else (hd l)::(first (n-1) tl l), from = lambda n. n::(from (n+1)) in let rec filter = lambda f. lambda l. {remove multiples} if null l then nil {of f from l } else if hd l/f*f = hd l then filter f tl l else hd l :: filter f tl l, sieve = lambda l. if null l then nil else let p = hd l { prime } in p :: sieve (filter p tl l) in first 10 ( sieve (from 2) ) {\fB Sieve of Eratosthenes. \fP}

output area

Composites.

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.

program: [compositeQ.fp]

In case the reader is sceptical about the viability of this program, the start of its output follows.

(2::
(3::
(5::
(7::
 ...etc...

— Output from Composites/Primes Program —

let rec merge = lambda a. lambda b. {assume a and b infinite and disjoint} let a1=hd a, b1=hd b in if a1 < b1 then a1::(merge (tl a) b) else {a1 > b1} b1::(merge a (tl b)), mult = lambda a. lambda b. (a * hd b)::(mult a tl b), remove = lambda a. lambda b. { a-b, treat lists as sets. PRE: a & b ascending } if hd a < hd b then (hd a)::(remove tl a b) else if hd a > hd b then remove a tl b else remove tl a tl b, from = lambda n. n::(from (n+1)), { n::(n+1)::(n+2):: ... } products = lambda l. { PRE: l ascending } let rec p = (hd l * hd l) :: { & elts coprime } (merge (mult hd l (merge tl l p)) (products tl l)) in p, first = lambda n. lambda l. if n <= 0 then nil else hd l :: first (n-1) tl l in let rec composites = products primes, primes = 2 :: (remove (from 3) composites) { ! } in first 10 primes {\fB Composites and Primes. \fP}

output area

Exercises.

1. Write an FP function to reverse a list.

2. Write an FP function unique L. Unique accepts an input list, possibly infinitely long. It returns a list having the same members as L but with duplicates removed. The order of first occurrence must be maintained.

   eg.  unique ( 1::2::1::4::3::2:: ... )
      = 1::2::4::3:: ...
   

3. A node in a binary tree can be represented as a triple: elt::left::right. Write a functional program to build a binary search tree from a list of elements.

4. Extend the functional language parser to permit [a, b, c, ..., x] as a shorthand for a::b::c::...::x::nil and to allow "string" as shorthand for a list of characters ['s','t','r','i','n','g'].

Also see the [examples] and the [interpreter].