Lambda Calculus
CSN 312 – Principles of
Programming Languages
Lambda Calculus
• Language to express function application
– Ability to define anonymous functions
– Ability to "apply" functions
• Functional programming derives from
lambda calculus
– ML
– Haskell
– F#
– Clojure
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
2
History
• Frege in 1893 studied the use of functions in logic
• Schönfinkel, in the 1920s, studied how
combinators, a specific type of function, could be
applied to formal logic
• Church introduced lambda calculus in the 1930s
• Original system was shown to be logically
inconsistent in 1935 by Kleene and Rosser
• In 1936, Church published the lambda calculus
that is relevant to computation
• Refined further
– Type systems, …
Adapted from Jesse Alama:
http://plato.stanford.edu/entries/lambda-calculus/#BriHisLCal
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
3
Syntax
• Everything in lambda calculus is an
expression (E)
E → ID
E → λ ID . E
E→EE
E → (E)
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
4
Examples
E → ID
E → λ ID . E
E→EE
E → (E)
x
λx.x
xy
λλx.y
λx.yz
foo λ bar . (foo (bar baz))
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
5
Ambiguous Syntax
• How to parse
xyz
Exp Exp
Exp z x Exp
x y y z
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
6
Ambiguous Syntax
• How to parse
λx.xy
Exp Exp
λ Exp Exp
x Exp
y
Exp Exp λ x Exp
x y x
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
7
Disambiguation Rules
• E → E E is left associative
– x y z is
• (x y) z
– w x y z is
• ((w x) y) z
• λ ID . E extends as far to the right as
possible, starting with the λ ID .
– λ x . x y is
• λ x . (x y)
– λ x . λ x . x is
• λ x. ( λ x . x)
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
8
Examples
• (λ x . y) x is the same as λ x . y x
– No!
– (λ x . y) x
• λ x . (x) y is the same as
– λ x . ((x) y)
• λa.λb.λc.abc
– λ a . (λ b . (λ c . ((a b) c)))
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
9
Semantics
• Every ID that we see in lambda calculus is
called a variable
• E → λ ID . E is called an abstraction
– The ID is the variable of the abstraction (also
metavariable)
– E is called the body of the abstraction
• E→EE
– This is called an application
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
10
Semantics
• λ ID . E defines a new anonymous function
– This is the reason why anonymous functions
are called "Lambda Expressions" in Java 8
(and other languages)
– ID is the formal parameter of the function
– Body is the body of the function
• E → E1 E2, function application, is similar
to calling function E1 and setting its formal
parameter to be E2
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
11
Example
• Assume that we have the function + defined
and the constant 1
• λx.+x1
– Represents a function that adds one to its
argument
• (λ x . + x 1) 2
– Represents calling the original function by
supplying 2 for x and it would "reduce" to (+ 2 1)
=3
• How can + function be defined if abstractions
only accept 1 parameter?
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
12
Currying
• Technique to translate the evaluation of a function
that takes multiple arguments into a sequence of
functions that each take a single argument
• Define adding two parameters together with
functions that only take one parameter:
– λ x . λ y . ((+ x) y)
– (λ x . λ y . ((+ x) y)) 1
• λ y . ((+ 1) y)
– (λ x . λ y . ((+ x) y)) 10 20
• (λ y . ((+ 10) y)) 20
• ((+ 10) 20) = 30
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
13
Free Variables
• A variable is free if it does not appear
within the body of an abstraction with a
metavariable of the same name
• x free in λ x . x y z?
• y free in λ x . x y z?
• x free in (λ x . (+ x 1)) x?
• z free in λ x . λ y . λ z . z y x?
• x free in (λ x . z foo) (λ y . y x)?
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
14
Free Variables
• x is free in E if:
–E=x
– E = λ y . E1, where y != x and x is free in E1
– E = E1 E2, where x is free in E1
– E = E1 E2, where x is free in E2 and every
occurrence of
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
15
Examples
• x free in x λ x . x ?
• x free in (λ x . x y) x ?
• x free in λ x . y x ?
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
16
Combinators
• An expression is a combinator if it does
not have any free variables
• λ x . λ y . x y x combinator?
• λ x . x combinator?
• λ z . λ x . x y z combinator?
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
17
Bound Variables
• If a variable is not free, it is bound
• Bound by what abstraction?
– What is the scope of a metavariable?
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
18
Bound Variable Rules
• If an occurrence of x is free in E, then it is bound
by λ x . in λ x . E
• If an occurrence of x is bound by a particular λ x .
in E, then x is bound by the same λ x . in λ z . E
– Even if z == x
– λx.λx. x
• Which lambda expression binds x?
• If an occurrence of x is bound by a particular λ x .
in E1, then that occurrence in E1 is tied by the
same abstraction λ x . in E1 E2 and E2 E1
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
19
Examples
• (λ x . x (λ y . x y z y) x) x y
– (λ x . x (λ y . x y z y) x) x y
• (λ x . λ y . x y) (λ z . x z)
– (λ x . λ y . x y) (λ z . x z)
• (λ x . x λ x . z x)
– (λ x . x λ x . z x)
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
20
Equivalence
• What does it mean for two functions to be
equivalent?
–λy.y =λx.x?
–λx.xy=λy.yx?
–λx.x=λx.x?
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
21
α-equivalence
• α-equivalence is when two functions vary
only by the names of the bound variables
• E1 =α E2
• We need a way to rename variables in an
expression
– Simple find and replace?
–λx.xλy.xyz
• Can we rename x to foo?
• Can we rename y to bar?
• Can we rename y to x?
• Can we rename x to z?
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
22
Renaming Operation
• E {y/x}
– x {y/x} = y
– z {y/x} = z, if x ≠ z
– (E1 E2) {y/x} = (E1 {y/x}) (E2 {y/x})
– (λ x . E) {y/x} = (λ y . E {y/x})
– (λ z . E) {y/x} = (λ z . E {y/x}), if x ≠ z
Material courtesy of Peter Selinger
http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
23
Examples
• (λ x . x) {foo/x}
• (λ foo . (x) {foo/x})
• (λ foo . (foo))
– ((λ x . x (λ y . x y z y) x) x y) {bar/x}
• (λ x . x (λ y . x y z y) x) {bar/x} (x) {bar/x} (y) {bar/x}
• (λ x . x (λ y . x y z y) x) {bar/x} (x) {bar/x} y
• (λ x . x (λ y . x y z y) x) {bar/x} bar y
• (λ bar . (x (λ y . x y z y) x) {bar/x}) bar y
• (λ bar . (bar (λ y . x y z y) {bar/x} bar)) bar y
• (λ bar . (bar (λ y . (x y z y) {bar/x} ) bar)) bar y
• (λ bar . (bar (λ y . (bar y z y)) bar)) bar y
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
24
α-equivalence
• For all expressions E and all variables y
that do not occur in E
– λ x . E =α λ y . (E {y/x})
• λy.y =λx.x?
• ((λ x . x (λ y . x y z y) x) x y) =
((λ y . y (λ z . y z w z) y) y x) ?
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
25
Substitution
• Renaming allows us to replace one variable
name with another
• However, our goal is to reduce (λ x . + x 1) 2
to (+ 1 2), which replaces x with the
expression 2
– Can we use renaming?
• We need another operator, called
substitution, to replace a variable by a
lambda expression
– E[x→N], where E and N are lambda expressions
and x is a name
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
26
Substitution
• Seems simple, right?
• (+ x 1) [x→2]
– (+ 2 1)
• (λ x . + x 1) [x→2]
– (λ x . + x 1)
• (λ x . y x) [y→ λ z . x z]
– (λ x . (λ z . x z) x)
– (λ w . (λ z . x z) w)
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
27
Substitution Operation
• E [x→N]
– x [x→N] = N
– y [x→N] = y, if x ≠ y
– (E1 E2) [x→N] = (E1 [x→N]) (E2 [x→N])
– (λ x . E) [x→N] = (λ x . E)
– (λ y . E) [x→N] = (λ y . E [x→N]) if x ≠ y and y
is not a free variable in N
– (λ y . E) [x→N] = (λ y' . E {y'/y} [x→N]) if x ≠ y,
y is a free variable in N, and y' is a fresh
variable name
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
28
Examples
• (λ x . x) [x→foo]
• (λ x . x)
– (+ 1 x) [x→2]
• (+[x→2] 1[x→2] x[x→2])
• (+ 1 2)
– (λ x . y x) [y→λ z . x z]
• (λ w . (y x){w/x} [y→λ z . x z])
• (λ w . (y w) [y→λ z . x z])
• (λ w . (y [y→λ z . x z] w [y→λ z . x z])
• (λ w . (λ z . x z) w)
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
29
Examples
• (x (λ y . x y)) [x→y z]
– (x [x→y z] (λ y . x y) [x→y z])
– ((y z) (λ y . x y) [x→y z])
– (y z) (λ q . (x y){q/y}[x→y z])
– (y z) (λ q . (x q)[x→y z])
– (y z) (λ q . ((y z) q))
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
30
Execution
• Execution will be a sequence of terms, resulting
from calling/invoking functions
• Each step in this sequence is called a β-reduction
– We can only β-reduce a β-redux (expressions in the
application form)
– (λ x . E) N
• β-reduction is defined as:
– (λ x . E) N β-reduces to
– E[x→N]
• β-normal form is an expression with no reduxes
• Full β-reduction is reducing all reduxes regardless
of where they appear
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
31
Examples
• (λ x . x) y
– x[x→y]
–y
• (λ x . x (λ x . x)) (u r)
– (x (λ x . x))[x→(u r)]
– (u r) (λ x . x)
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
32
Examples
• (λ x . y) ((λ z . z z) (λ w . w))
– (λ x . y) (z z)[z→(λ w . w)]
– (λ x . y) ((λ w . w) (λ w . w))
– (λ x . y) (w)[w→(λ w . w)]
– (λ x . y) (λ w . w)
– y[x→(λ w . w)]
–y
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
33
Examples
• (λ x . x x) (λ x . x x)
– (x x)[x→(λ x . x x)]
– (λ x . x x) (λ x . x x)
– (x x)[x→(λ x . x x)]
– (λ x . x x) (λ x . x x)
–…
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
34
Boolean Logic
• T = (λ x . λ y . x)
• F = (λ x . λ y . y)
• and = (λ a . λ b . a b F)
• and T T
– (λ a . λ b . a b (λ x . λ y . y))
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
35
and T T
• (λ a . λ b . a b (λ x . λ y . y)) (λ x . λ y . x) (λ x . λ y . x)
• (λ b . a b (λ x . λ y . y))[a →(λ x . λ y . x)] (λ x . λ y . x)
• (λ b . (λ x . λ y . x) b (λ x . λ y . y)) (λ x . λ y . x)
• ((λ x . λ y . x) b (λ x . λ y . y))[b→(λ x . λ y . x)]
• (λ x . λ y . x) (λ x . λ y . x) (λ x . λ y . y)
• (λ y . x)[x →(λ x . λ y . x)] (λ x . λ y . y)
• (λ y . (λ x . λ y . x)) (λ x . λ y . y)
• (λ x . λ y . x)[y→(λ x . λ y . y)]
• (λ x . λ y . x)
• T
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
36
and T F
• (λ a . λ b . a b F) T F
• (λ b . a b F)[a→T] F
• (λ b . T b F) F
• (T b F)[b→F]
• (T F F)
• (λ x . λ y . x) F F
• (λ y . x)[x→F] F
• (λ y . F) F
• F[y→F]
• F
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
37
and F T
• (λ a . λ b . a b F) F T
• FTF
• F
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
38
and F F
• (λ a . λ b . a b F) F F
• FFF
• F
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
39
not
• not T = F
• not F = T
• not = (λ a . a F T)
• not T
– (λ a . a F T) T
– TFT
–F
• not F
– (λ a . a F T) F
– FFT
–T
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
40
If Branches
if c then
a
else
b
• if c a b
• if T a b = a
• if F a b = b
• if = (λ a . a)
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
41
Examples
• if T a b
– (λ a . a) T a b
–Tab
–a
• if F a b
– (λ a . a) F a b
–Fab
–b
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
42
Church's Numerals
• 0=λf.λx.x
• 1=λf.λx.fx
• 2=λf.λx.ffx
• 3=λf.λx.fffx
• 4=λf.λx.ffffx
– λ f . λ x . (f (f (f (f x))))
• 4ab
–aaaab
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
43
Successor Function
• succ = λ n . λ f . λ x . f (n f x)
• 0=λf.λx.x
• succ 0
– (λ n . λ f . λ x . f (n f x)) 0
– λ f . λ x . f (0 f x)
– λ f . λ x . f ((λ f . λ x . x) f x)
– λf.λx.fx
• 1=λf.λx.fx
• succ 0 = 1
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
44
Successor Function
• succ = λ n . λ f . λ x . f (n f x)
• 1=λf.λx.fx
• succ 1
– (λ n . λ f . λ x . f (n f x)) 1
– λ f . λ x . f (1 f x)
– λ f . λ x . f ((λ f . λ x . f x) f x)
– λf.λx.ffx
• 2=λf.λx.ffx
• succ 1 = 2
• succ n = n + 1
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
45
Addition
• add 0 1 = 1
• add 1 2 = 3
• add = λ n . λ m . λ f . λ x . n f (m f x)
• add 0 1
– (λ n . λ m . λ f . λ x . n f (m f x)) 0 1
– (λ m . λ f . λ x . 0 f (m f x)) 1
– λ f . λ x . 0 f (1 f x)
– λ f . λ x . 0 f (f x)
–λf.λx.fx
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
46
Addition
• add = λ n . λ m . λ f . λ x . n f (m f x)
• add 1 2
– (λ n . λ m . λ f . λ x . n f (m f x)) 1 2
– (λ m . λ f . λ x . 1 f (m f x)) 2
– λ f . λ x . 1 f (2 f x)
– λ f . λ x . 1 f (f f x)
– λ f . λ x . (f f f x)
–3
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
47
Multiplication
• mult 01=0
• mult 12=2
• mult 2 5 = 10
• mult = λ n . λ m . m (add n) 0
• mult 01
– (λ n . λ m . m (add n) 0) 0 1
– (λ m . m (add 0) 0) 1
– 1 (add 0) 0
– add 0 0
– 0
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
48
Multiplication
• mult 1 2
– (λ n . λ m . m (add n) 0) 1 2
– (λ m . m (add 1) 0) 2
– 2 (add 1) 0
– (add 1) ((add 1) 0)
– (add 1) (add 1 0)
– (add 1) (1)
– (add 1 1)
–2
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
49
Turing Complete?
• We have Boolean logic
– Including true/false branches
• We have arithmetic
• What does it mean for lambda calculus to
be Turing complete?
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
50
Factorial
• n!
– fact(0) = 1
– fact(n) = n * fact(n-1)
int fact(int n)
{
if (n == 0)
{
return 1;
}
return n * fact(n-1);
}
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
51
Factorial
• (assuming that we have definitions of the
iszero and pred functions)
• fact = (λ n . if (iszero n) (1) (mult n (fact
(pred n)))
• However, we cannot write this function!
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
52
Y Combinator
• Y = (λ x . λ y . y (x x y)) (λ x . λ y . y (x x y))
• Y foo
– (λ x . λ y . y (x x y)) (λ x . λ y . y (x x y)) foo
– (λ y . y ((λ x . λ y . y (x x y)) (λ x . λ y . y (x x y)) y))
foo
– foo ((λ x . λ y . y (x x y)) (λ x . λ y . y (x x y)) foo)
– foo (Y foo)
– foo (foo (Y foo))
– foo (foo (foo (Y foo)))
–…
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
53
Recursion
• fact = (λ n . if (iszero n) (1) (mult n (fact (pred n)))
• fact = Y (λ f . λ n . if (iszero n) (1) (mult n (f (pred n)))
• fact 1
– Y (λ f . λ n . if (iszero n) (1) (mult n (f (pred n))) 1
– (λ f . λ n . if (iszero n) (1) (mult n (f (pred n))) (Y (λ f . λ n . if (iszero n) (1) (mult n (f
(pred n))) 1
– (λ n . if (iszero n) (1) (mult n ((Y (λ f . λ n . if (iszero n) (1) (mult n (f (pred n))) (pred n)))
1
– if (iszero 1) (1) (mult 1 ((Y (λ f . λ n . if (iszero n) (1) (mult n (f (pred n))) (pred 1))
– if F (1) (mult 1 ((Y (λ f . λ n . if (iszero n) (1) (mult n (f (pred n))) (pred 1))
– mult 1 ((Y (λ f . λ n . if (iszero n) (1) (mult n (f (pred n))) (pred 1)
– mult 1 (λ f . λ n . if (iszero n) (1) (mult n (f (pred n))) (Y (λ f . λ n . if (iszero n) (1) (mult n
(f (pred n))) (pred 1)
– mult 1 (λ n . if (iszero n) (1) (mult n ((Y (λ f . λ n . if (iszero n) (1) (mult n (f (pred n)))
(pred n))) (pred 1)
– mult 1 (λ n . if (iszero n) (1) (mult n ((Y (λ f . λ n . if (iszero n) (1) (mult n (f (pred n)))
(pred n))) 0
– mult 1 (if (iszero 0) (1) (mult 0 ((Y (λ f . λ n . if (iszero n) (1) (mult n (f (pred n))) (pred
0)))
– mult 1 if T (1) (mult 0 ((Y (λ f . λ n . if (iszero n) (1) (mult n (f (pred n))) (pred 0)))
– mult 1 1
– 1
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
54
Turing Complete
• Boolean Logic
• Arithmetic
• Loops
Slides have been taken from Adam Doupé’s course on
Principles of programming Languages
55
Fall 2015
PRINCIPLES OF
PROGRAMMING LANGUAGES
56
