λ-calculus
Chapter 11.7
What can be done by a computer?
§ Algorithm formalization – 1930s § Church, Turing, Kleene, Post, etc. § Church’s thesis:
All intuitive computing models are equally powerful.
§ Turing machine
§ automaton with an unbounded tape § imperative programming
§ Church’s λ-calculus
§ computes by substituting parameters into expressions § functional programming
§ Logic: Horn clauses
§ collection of axioms to solve a goal § logic programming
2
λ-calculus
§ λ-calculus
§ Church (1941) – to study computations with functions
§ Everything is a function!
§ λ-expressions – defined recursively: § name: x, y, z, u, v, …
§abstraction: λx.M
§ function with parameter x and body M
§ applications: M N – function M applied to N
§ Examples
§ (λ x.x*x) – a function that maps x to x*x
§ (λ x.x*x) 4 – the same function applied to 4
3
λ-calculus
§ Syntactic rules
§ application is left-associative xyz means (xy)z
§ application has higher precedence than abstraction λx.A B means λx.(A B) (not (λx.A) B)
§ consecutive abstractions:
λx1x2…xn.e means λx1.(λx2.(…(λxn.e)…))
§ Example:
λxyz.x z (y z) = (λx.(λy.(λz.((x z) (y z)))))
4
λ-calculus
§ Context-free grammars (CFG) § CFG for λ-expressions
expr → name | (λname.expr)| (expr expr)
§ CFG for λ-expressions with minimum parentheses expr → name | λname.expr | func arg
func → name |(λname.expr)| func arg
arg → name | (λname.expr)|(func arg)
5
λ-calculus
§ Examples
square = λx.times x x
identity = λx.x
const7 = λx.7
hypot = λx.λy.sqrt (plus (square x) (square y))
6
Free and bound variables
§ λx.M – is a binding of the variable (or name) x
§ lexical scope
§ x is said to be bound in λx.M
§ all x in λx.M are bound within the scope of this binding
§ x is free in M if it is not bound
§ free(M) – the set of free variables in M § free(x) = {x}
§ free(M N) = free(M) ∪ free(N) § free(λx.M) = free(M ) − {x}
§ bound(M) – the set of variables which are not free § any occurrence of a variable is free or bound; not both
7
Free and bound variables
§ Example § x is free
§ y, z are bound λy.λz.x z (y z)
8
Computing with pure λ-terms
§ Computing idea:
§ reduce the terms into as simple a form as possible § (λx.M) N =β {N/x}M – substitute N for x in M
§ the right-hand side is expected to be simpler
§ Example:
(λxy.x) u v =β (λy.u) v =β u
9
Substitution
§ {N/x}M – substitution of term N for variable x in M
§ Substitution rules (informal): § (i) if free(N) ∩ bound(M) = ∅
then just replace all free occurrences of x in M
§ (ii) otherwise, rename with fresh variables until (i) applies
10
Substitution
§ Substitution rules (formal):
§ In variables: the same or different variable § {N/x}x = N
§ {N/x}y = y, y ≠ x
§ In applications – the substitution distributes
§ {N/x}(P Q) = {N/x}P {N/x}Q
§ In abstractions – several cases § no free x:
{N/x}(λx.P) = λx.P
§ no interaction – y is not free in N:
{N/x}(λy.P) = λy.{N/x}P, y ≠ x, y ∉ free(N)
§ renaming – y is free in N; y is renamed to z in P:
{N/x}(λy.P) = λz.{N/x}{z/y}P,
y ≠ x, y ∈ free(N), z ∉ free(N) ∪ free(P)
11
Computing with pure λ-terms
§ Rewriting rules
§ α-conversion – renaming the formal parameters
λx.M ⟹α λy.{y/x}M, y ∉ free(M)
§ β-reduction – applying an abstraction to an argument (λx.M) N ⟹β {N/x} M
12
Equality of pure λ-terms
§ Example
(λxyz.x z (y z)) (λx.x) (λx.x)
⟹α (λxyz.x z (y z)) (λu.u) (λx.x) ⟹α (λxyz.x z (y z)) (λu.u) (λv.v) ⟹β (λyz.(λu.u) z (y z)) (λv.v) ⟹β (λyz.z (y z)) (λv.v)
⟹β λz.z ((λv.v) z)
⟹β λz.z z
13
Equality of pure λ-terms
§ Example
(λfgh.f g (h h)) (λxy.x) h (λx.x x) ⟹β (λgh.(λxy.x) g (h h)) h (λx.x x) ⟹α (λgk.(λxy.x) g (k k)) h (λx.x x) ⟹β (λk.(λxy.x) h (k k)) (λx.x x) ⟹β (λxy.x) h ((λx.x x) (λx.x x)) ⟹β (λy.h) ((λx.x x) (λx.x x))
⟹β h
14
Computing with pure λ-terms
§ Rewriting rules
§ Reduction: any sequence of ⟹α , ⟹β
§ Normal form: term that cannot be β-reduced § β-normal form
§ Example of normal form
λx.x x – cannot be reduced
15
Computing with pure λ-terms
§ There may be several ways to reduce to a normal form § Example: any path below is such a reduction
(λxyz.x z (y z)) (λx.x) (λx.x) (λyz.(λx.x) z (y z)) (λx.x)
(λyz.z (y z)) (λx.x) λz.(λx.x) z ((λx.x) z)
λz.z ((λx.x) z)
λz.(λx.x) z z
λz.z z
16
⟹β
⟹β
⟹β ⟹β
⟹β ⟹β
⟹β ⟹β
Computing with pure λ-terms
§ Nonterminating reductions
§ Never reach a normal form § Example
(λx.x x) (λx.x x) ⟹β (λx.x x) (λx.x x)
17
Computing with pure λ-terms
§ Theorem (Church-Roser, 1936) For all pure λ-terms M, P, Q, if
M ⟹β* P and M ⟹β*Q, then there exists a term R such that
P⟹β*RandQ⟹β* R.
§ In particular, the normal form, when exists, is unique.
18
Computing with pure λ-terms
§ Reduction strategies
§ Call-by-value reduction (applicative order)
§ parameters are evaluated first, then passed
§ might not reach a normal form even if there is one § leftmost innermost lambda that can be applied
§ Example
(λy.h) ((λx.x x) (λx.x x))
⟹β (λy.h) ((λx.x x) (λx.x x)) ⟹β (λy.h) ((λx.x x) (λx.x x)) ⟹β …
19
Computing with pure λ-terms
§ Reduction strategies
§ Call-by-name reduction (normal order)
§ parameters are passed unevaluated
§ leftmost outermost lambda that can be applied
§ Example
(λy.h) ((λx.x x) (λx.x x)) ⟹β h
§ Theorem (Church-Roser, 1936)
Normal order reduction reaches a normal form if there is one.
§ Functional languages use also call-by-value because it can be implemented efficiently and it might reach the normal form faster than call-by-name.
20
λ-calculus can model everything
§ Boolean values
§ True: T ≡ λx.λy.x
§ interpretation: of a pair of values, choose the first § False: F ≡ λx.λy.y
§ interpretation: of a pair of values, choose the second § Properties:
((T P) Q) ⟹β (((λx.λy.x) P) Q) ⟹β ((λy.P) Q) ⟹β P ((F P) Q) ⟹β (((λx.λy.y) P) Q) ⟹β ((λy.y) Q) ⟹β Q
21
λ-calculus can model everything
§ Boolean functions
§ not ≡ λx.((x F) T)
§ and ≡ λx.λy.((x y) F) § or ≡ λx.λy.((x T) y)
§ Interpretation is consistent with predicate logic: notT⟹β (λx.((xF)T))T⟹β ((TF)T) ⟹β F notF⟹β (λx.((xF)T))F⟹β ((FF)T) ⟹β T
22
λ-calculus can model everything
§ Integers
0 ≡ λf.λc.c
1 ≡ λf.λc.(f c)
2 ≡ λf.λc.(f (f c))
3 ≡ λf.λc.(f (f (f c)))
…
N ≡ λf.λc.(f (f …(f c))…)
N
§ Interpretation:
§ c is the zero element
§ f is the successor function
23
{
λ-calculus can model everything
§ Integers (cont’d)
§ Example calculations:
(N a) = (λf.λc.(f …(f c))…)) a ⟹β λc.(a…(a c)…)
N
((N a) b) = (a (a…(a b))…) N
N
24
{{ {
λ-calculus can model everything
§ Integer operations
§ Addition: + ≡ λM.λN.λa.λb.((M a)((N a) b))
[M + N] = λa.λb.((M a) ((N a) b)) ⟹β* λa.λb.(a (a…(a b))…) M+N
§ Multiplication: × ≡ λM.λN.λa.(M (N a))
[M × N] = λa.(M (N a)) ⟹β* λa.λb.(a (a…(a b))…)
M×N § Exponentiation: ∧ ≡ λM.λN.(N M)
[MN] = (N M) ⟹β* λa.λb.(a (a…(a b))…)
MN
§ This way we can develop all computable math. functions.
25
{
{
{
λ-calculus can model everything
§ Control flow
§ if ≡ λc.λt.λe.c t e
§ Interpretation: c = condition, t = then, e = else
§ifT34 = (λc.λt.λe.cte)(λx.λy.x)34 ⟹β* (λt.λe.t)34
⟹β* 3
§ifF34 = (λc.λt.λe.cte)(λx.λy.y)34
⟹β* (λt.λe.e)34 ⟹β* 4
26
λ-calculus can model everything
§ Recursion
§ gcd = λa.λb.(if (equal a b) a (if (greater a b) (gcd (minus
a b) b) (gcd (minus b a) a)))
§ This is not a definition because gcd appears in both sides
§ If we substitute this, the definition only gets bigger
§ To obtain a real definition, we rewrite using β-abstraction:
gcd = (λg.λa.λb.(if (equal a b) a (if (greater a b) (g (minus a b) b) (g (minus b a) a)))) gcd
§ we obtain the equation gcd = f gcd, where
f = λg.λa.λb.(if (equal a b) a (if (greater a b) (g (minus a b) b) (g (minus b a) a)))
§ gcd is a fixed point of f
27
λ-calculus can model everything
§ Define the fixed point combinator: Y ≡ λh.(λx.h (x x)) (λx.h (x x))
§Yf is a fixed point of f
§ if the normal order evaluation of Y f terminates then f (Y f)
and Y f will reduce to the same normal form § We get then a good definition for gcd:
gcd ≡ Y f = (λh.(λx.h (x x)) (λx.h (x x))) (λg.λa.λb.(if (equal a b) a (if (greatera b) (g (minusa b) b) (g (minusb a) a))) )
28
λ-calculus can model everything
§ Example
gcd 2 4
≡ Yf 2 4
≡ ((λh.(λx.h (x x)) (λx.h (x x))) f ) 2 4 ⟹β ((λx.f (x x)) (λx.f (x x))) 2 4
≡ (f ((λx.f (x x)) (λx.f (x x)))) 2 4
⟹β (f (k k)) 2 4
≡ ((λg.λa.λb.(if (= a b) a (if (> a b) (g (− a b) b) (g (− b a) a))))(k k)) 2 4 ⟹β (λa.λb.(if (= a b) a (if (> a b) ((k k) (− a b) b) ((k k)(− b a) a)))) 2 4 ⟹β* if (= 2 4) 2 (if (> 2 4) ((k k) (− 2 4) 4) ((k k) (− 4 2) 2))
≡ (λc.λt.λe.c t e) (= 2 4 ) 2 (if (> 2 4) ((k k) (− 2 4) 4) ((k k) (− 4 2) 2))
denote k ≡ λx.f (x x)
29
λ-calculus can model everything
≡ (λc.λt.λe.c t e) (= 2 4 ) 2 (if (> 2 4) ((k k) (− 2 4) 4) ((k k) (− 4 2) 2)) ⟹β* (= 2 4) 2 (if (> 2 4) ((k k) (− 2 4) 4) ((k k) (− 4 2) 2))
⟹δ F 2 (if (> 2 4) ((k k) (− 2 4) 4) ((k k) (− 4 2) 2))
≡ (λx.λy.y) 2 (if (> 2 4) ((k k) (− 2 4) 4) ((k k) (− 4 2) 2))
⟹β* if (> 2 4) ((k k) (− 2 4) 4) ((k k) (− 4 2) 2) ⟹β …
⟹β (k k) (− 4 2) 2
≡ ((λx.f (x x)) k) (− 4 2) 2
⟹β (f (k k))(− 4 2) 2
≡ ((λg.λa.λb.(if (= a b) a (if (> a b) (g (− a b) b) (g (− b a) a)))) (k k))(− 4 2) 2 ⟹β (λa.λb.(if (= a b) a (if (> a b) ((k k) (− a b) b) ((k k) (− b a) a))))(− 4 2) 2
30
λ-calculus can model everything
⟹β (λa.λb.(if (= a b) a (if (> a b) ((k k) (− a b) b) ((k k) (− b a) a))))(− 4 2) 2 ⟹β* if (= (− 4 2) 2) (− 4 2) (if (> (− 4 2) 2) ((k k) (− (− 4 2) 2) 2) ((k k) (− 2
(− 4 2)) (− 4 2)))
≡ (λc.λt.λe.c t e) (= (− 4 2) 2) (− 4 2) (if (> (− 4 2) 2) ((k k) (− (− 4 2) 2) 2) ((k
k) (− 2 (− 4 2)) (− 4 2)))
⟹β* (= (− 4 2) 2) (− 4 2) (if (> (− 4 2) 2) ((k k) (− (− 4 2) 2) 2) ((k k) (− 2 (− 4
2)) (− 4 2)))
⟹δ (= 2 2)(− 4 2) (if (> (− 4 2) 2) ((k k)(− (− 4 2) 2) 2) ((k k) (− 2 (− 4 2)) (− 4 2)))
⟹δ T (− 4 2) (if (> (− 4 2) 2) ((k k) (− (− 4 2) 2) 2) ((k k) (− 2 (− 4 2)) (− 4 2))) ≡ (λx.λy.x) (− 4 2) (if (> (− 4 2) 2) ((k k)(− (− 4 2) 2) 2) ((k k) (− 2 (− 4 2)) (− 4
2)))
⟹β* (− 4 2) ⟹δ 2
31
λ-calculus can model everything
§ Structures §select_first≡ λx.λy.x §select_second≡ λx.λy.y
§ cons ≡ λa.λd.λx.x a d
§car ≡ λl.lselect_first §cdr ≡ λl.lselect_second §null?≡ λl.l(λx.λy.F)
32
λ-calculus can model everything
car (cons A B)
≡ (λl.l select_first) (cons A B) ⟹β (cons A B) select_first
≡ ((λa.λd.λx.x a d) A B) select_first ⟹β* (λx.x A B) select_first
⟹β select_first A B
≡ (λx.λy.x) A B
⟹β* A
33
λ-calculus can model everything
cdr (cons A B)
≡ (λl.l select_second) (cons A B) ⟹β (cons A B) select_second
≡ ((λa.λd.λx.x a d) A B) select_second ⟹β* (λx.x A B) select_second
⟹β select_second A B
≡ (λx.λy.x) A B
⟹β* B
34
λ-calculus can model everything
null? (cons A B)
≡ (λl.l (λx.λy.select_second)) (cons A B) ⟹β (cons A B) (λx.λy.select_second)
≡ ((λa.λd.λx.x a d) A B) (λx.λy.select_second) ⟹β* (λx.x A B) (λx.λy.select_second)
⟹β (λx.λy.select_second) A B
⟹β* select_second
≡F
35