﻿ Introduction to the Lambda calculus
• # Introduction to the Lambda calculus

In this article we introduce the basic formalism underlying functional programming, 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”.  