## Want to keep learning?

This content is taken from the The University of Glasgow's online course, Functional Programming in Haskell: Supercharge Your Coding. Join the course to learn more.
6.5

## The University of Glasgow Excerpt from "Postulates for the foundation of Logic" by A. Church, 1932

# Introduction to the Lambda calculus

### Introduction to the Lambda Calculus

• The lambda calculus was developed in the 1930s by Alonzo Church (1903–1995), one of the leading developers of mathematical logic.

• The lambda calculus was an attempt to formalise functions as a means of computing.

### Significance to computability theory

• A major (really the major) breakthrough in computability theory was the proof that the lambda calculus and the Turing machine have exactly the same computational power.

• This led to Church’s thesis — that the set of functions that are effectively computable are exactly the set computable by the Turing machine or the lambda calculus.

• The thesis was strengthened when several other mathematical computing systems (Post Correspondence Problem, and others) were also proved equivalent to lambda calculus.

• The point is that the set of effectively computable functions seems to be a fundamental reality, not just a quirk of how the {Turing machine, lambda calculus} was defined.

### Significance to programming languages

• The lambda calculus has turned out to capture two aspects of a function:

• A mathematical object (set of ordered pairs from domain and range), and

• An abstract black box machine that takes an input and produces an output.

• The lambda calculus is fundamental to denotational semantics, the mathematical theory of what computer programs mean.

• Functional programming languages were developed with the explicit goal of turning lambda calculus into a practical programming language.

• The ghc Haskell compiler operates by (1) desugaring the source program, (2) transforming the program into a version of lambda calculus called System F, and (3) translating the System F to machine language using graph reduction.

### Abstract syntax of lambda calculus

• We will work with the basic lambda calculus “enriched” with some constants and primitive functions (strictly speaking, that is not necessary).

• The language has constants, variables, applications, and functions.


exp
= const
| var
| exp exp
| \ var -> exp


### Variables

• Each occurrence of a variable in an expression is either bound or free

• In $$\backslash x \rightarrow x+1$$, the occurrence of $$x$$ in $$x+1$$ is bound by the $$\backslash x$$.

• In $$y*3$$, the occurrence or $$y$$ is free. It must be defined somewhere else, perhaps as a global definition.

• In general, an occurrence of a variable is bound if there is some enclosing lambda expression that binds it; if there is no lambda binding, then the occurrence if free.

We need to be careful: the first occurrence of $$a$$ is free but the second occurrence is bound.

       a + (\ a -> 2^a) 3  -- >   a + 2^3


Being free or bound is a property of an occurrence of a variable, not of the variable itself!

### Conversion rules

• Computing in the lambda calculus is performed using three conversion rules.

• The conversion rules allow you to replace an expression by another (“equal”) one.

• Some conversions simplify an expression; these are called reductions.

### Alpha conversion

• Alpha conversion lets you change the name of a function parameter consistently.

• But you can’t change free variables with alpha conversion!

• The detailed definition of alpha conversion is a bit tricky, because you have to be careful to be consistent and avoid “name capture”. We won’t worry about the details right now.

(\x -> x+1) 3
(\y -> y+1) 3


### Beta conversion

• Beta conversion is the “workhorse” of lambda calculus: it defines how functions work.

• To apply a lambda expression an argument, you take the body of the function, and replace each bound occurrence of the variable with the argument.

    (\x -> exp1) exp2


is evaluated as $$exp1[exp2/x]$$

Example:

    (\x -> 2*x + g x) 42


is evaluated as $$2*42 + g \;42$$

### Eta conversion

• Eta conversion says that a function is equivalent to a lambda expression that takes an argument and applies the function to the argument.
(\x -> f x)


is equivalent to $$f$$

Example (recall that $$(*3)$$ is a function that multiplies its argument by 3)

(\x -> (*3) x)


is equivalent to $$(*3)$$

Try applying both of these to 50:

(\x -> (*3) x) 50


is the same as $$(*3) \;50$$

### Removing a common trailing argument

There is a common usage of Eta conversion. Suppose we have a definition like this:

f x y = g y


This can be rewritten as follows:

f = \x -> (\y -> g y)
f = \x -> g = f x = g


Thus the following two definitions are equivalent:

    f x y = g y
f x = g


In effect, since the last argument on both sides of the equation is the same ($$y$$), it can be “factored out”.