Navigation

Appendix A: Lambda Calculus at a glance

Lambda calculus is the basis of functional programming. It deals with the definition and evaluation of functional expressions. We take a complex expression and successively reduce (transform) it to reach a final canonical form. For the sake of brevity we shall give an incomplete, slightly inaccurate presentation of lambda calculus. The subject itself is beyond the scope of this project; a good self-sustained introduction to lambda calculus, and a nice build-up into functional programming is given in [SLPJ87].

Expressions

An expression in lambda calculus is one of the following:

  • A variable name, such as x.
  • A function definition, which is called a lambda abstraction. The syntax is: \lambda x . E where \lambda x specifies that x is the name of the function argument, and E is the function body (which can be a compound expression).
  • A function application, which is composed of two expressions. It is written E1\ E2, where E1 is a function expression (a lambda abstraction).
  • We can also define “built-in” expressions (such as a function add or a constant 4).

A variable is bound in an expression if it appears as a function argument, and the expression is inside the function definition. For example x is bound in \lambda x.x. Otherwise, a variable is free.

Functions can only take a single argument. When more are needed, we can nest functions: \lambda x.\lambda y.E takes x, and returns a function that takes y. This is known as currying (after the logician Haskell Curry). A common abbreviation is to write \lambda x\ y.E in place of the nested expression.

Reduction rules

Lambda calculus also defines rules for transforming expressions (reduction rules):

  • \alpha -conversion: Changing the name of a bound variable. For example, \lambda x . x \rightarrow \lambda y . y.
  • Substitution: If a variable x appears free in the expression E we can perform a substitution, replacing x with another expression. We denote it like this: E1[E2/x]. You can think of it as ‘dividing’ E1 by x and ‘multiplying’ by E2.
  • \beta -reduction: Function application. This rule transforms (\lambda x. E1)\ E2 into E1[E2/x], using substitution.
  • \eta -conversion: Reduces ‘redundant’ functions. An expression \lambda x.\ f\ x can be \eta-converted to f, because the two expressions are equivalent.

Note that recursion is not allowed, which seems to strictly limit the expressiveness of the language. Fortunately, there turns out to be a function that we can define inside lambda calculus (the ‘Y-combinator’) that essentially allows recursion.

The aforementioned ‘canonical form’ is a unique, final minimal expression (not further reducible) that is guaranteed to exist by the Church-Rosser theorem. There is a specific reduction order that must be taken in order to reach the canonical form.

Examples of Lambda Expressions

Here are a few examples of expressions:

  • \lambda x . x is the identity function. For example, the function application (\lambda x.x)\ E evaluates to E for any E.
  • The natural numbers can be encoded in lambda calculus without built-in constants, as Church numerals (invented by the creator of lambda calculus, Alonzo Church). Some definitions:
    • zero = \lambda f\ x.\ x
    • succ = \lambda n\ f\ x.\ f\ (n\ f\ x)

Applying succ\ zero gives the following transformations:

succ\ zero &= (\lambda n\ f\ x.\ f\ (n\ f\ x))\ zero \\ &= \{ \beta-reduction:\ substitute\ zero\ in\ place\ of\ n\} \\ &= (\lambda f\ x.\ f\ (zero\ f\ x)) \\ &= (\lambda f\ x.\ f\ ((\lambda f\ x.\ x)\ f\ x)) \\ &= \{ \beta-reduction \} \\ &= (\lambda f\ x.\ f\ x)

Thus, we have:

  • 1 = succ\ zero = \lambda f\ x.\ f x
  • 2 = succ\ 1 = \lambda f\ x.\ f (f x)
  • 3 = succ\ 2 = \lambda f\ x.\ f (f (f x))
  • etc.

Church took the next step to also define functions for addition, multiplication, subtraction, exponentiation, etc.

Table Of Contents

Previous topic

Work plan

Next topic

FRP Resources

Navigation

© Copyright 2009, Noam Lewis. Created using Sphinx 0.6.3.