• Dan Deavours

Sponsored Links

  • FileName: lambda.pdf [preview-online]
    • Abstract: Dan DeavoursLambda CalculusPage 1 Dan DeavoursLambda Calculus• λ calculus is regarded as the theoretical foundation of functional programminglanguages

Download the ebook

Dan Deavours
Lambda Calculus
Page 1
Dan Deavours
Lambda Calculus
• λ calculus is regarded as the theoretical foundation of functional programming
• Like DFA or Turing machines is a model of computation, so is λ calculus.
• Developed in the 1930s
• Everything is a function. Arguments, return “values,” numbers, everything!
• If you’ve never seen it before, be prepared to be dazzled (or perplexed).
Page 2
Dan Deavours
Procedural Aabstraction
If you haven’t noticed before, functions are really a convenient form of abstraction.
d −ex
E.g., dx f (x), where f (x) = ex is a nice way of writing lim∆→0 e ∆ .
E.g., Fact(7) = 7 · 6 · 5 · 4 · 3 · 2 · 1.
How do you describe Fact(n)?
Page 3
Dan Deavours
Functional Description

 1 n=0
Fact(n) =
 n · Fact(n − 1) otherwise
In English, “Fact(n) := if n = 0 then 1 else n · Fact(n − 1).”
In pseudo-λ calculus:
Fact = λn. if n = 0 then 1 else n · Fact(n − 1)
Read: λn. · · · “the function that, for each n, yields · · ·.”
Page 4
Dan Deavours
What then does Fact(0) mean?
The function λn. if n = 0 then 1 else n · Fact(n − 1) applied to the argument 0
I.e., the value that results when the bound variable n in the function body “if n = 0
then 1 else . . .” is replaced by 0.
I.e., “if 0 = 0 then 1 else . . .”
I.e., 1.
Page 5
Dan Deavours
L, M, N ::= X V ariable
MN Application
λx.M Abstraction
Notation: application is left associative.
I.e., L M N = (L M )N .
Abstraction bodies extend as far right as possible.
I.e., λx.λy.x y x = λx.(λy.((x y)x)).
Don’t worry; when it’s not clear, we use lots of parentheses.
Page 6
Dan Deavours
For some λ expression λx.M , we say that x is bound in the body M .
How do you compute with λ calculus? Beta reductions!
(λx.M )N −→[N/x]M
Note: This is exactly what you “normally” do with functions anyway!
An expression can be reduced by replacing some subexpression of th eform
(λx.M )N , called a redex, by the result of substituting the argument N for the
bound variable x in the body M .
E.g., (λx. x y)(u v)−→u v y.
E.g., (λx.λy.x)z w−→(λy. z)w−→z.
We can write (λx.λy.x)z w−→∗ z.
Page 7
Dan Deavours
This gives us an interesting way to compare two programs.
We say that M and N are beta-convertible, written M =β N , if they are identical, if
one reduces to the other, or both reduce to some third expression L.
(Formally the beta-conversion relation =β is the reflexive, symmetric, transitive
closeure of beta-reduction.)
E.g., (λx.x)z =β (λx.λy.x)zw because
Page 8
Dan Deavours
We need to be very careful with the substitution [N/x]M .
We say that a variable x is free in an expression M if x appears at some position in
M where it is not bound by an enclosing lambda-abstraction on x.
E.g., x is free in xy and λy.xy, but not free in λx.x or λz.λx.λy.xyz.
FV(x) = {x}
FV(M N ) = FV(M ) ∪ FV(N )
FV(λx.M ) = FV(M ) \ {x}
Consider λx.x and λy.y . Intuitively, they are the same function, i.e., the function
that, when applied to N , returns N .
λx.M = λy.([y/x]M ) if y ∈ FV(M )
This rule is called the renaming of bound variables, or alpha conversion.
Page 9
Dan Deavours
Substitution Rules
Now, we can define substitution.
[N/x]x = N
I.e., substituting N for x in the expression consisting only of x itself yields N .
[N/x]z = z
I.e., to substitute N for x in the expression consisting only of some different variable
z yields z.
[N/x](L M ) = ([N/x]L)([N/x]M )
I.e., to substitute N for x in an application L M , we substitute in M and L
[N/x](λz.M ) = λz.([N/x]M ) if z = x and z ∈ FV(N )
To substitute N for x in a lambda abstraction M , we substitute in the body of M
only when:
1. z is not the same as x, or
2. z is not one of the free variables of N .
Page 10
Dan Deavours
Substitution exception 1
For exception 1, consider (λx.λx.x)y−→λx.y?
(λx.λx.x)y −→ [y/x]λx.x “beta − reduction
= λx.[y/x]x illegal
= λx.y
Page 11
Dan Deavours
Substitution exception 2
For exception 2, consider:
(λx.λy.x)y −→ [y/x]λx.λy.x “beta − reduction
= λy.y illegal
Thus, technically speaking, the substition [N/x]M may be undefined for some N , x,
and M , but it is always possible to change the names of the bound variables in N
and/or M so that the substion makes sense. E.g.,
(λx.λx.x)y −→ [y/x](λx.x)
= [y/x](λz.z)
= λz.z
= λx.x
Page 12
Dan Deavours
Everything (Part 1)
L, M, N ::= x variable
MN application
λx.M abstraction
Free variables:
FV(x) = {x}
FV(M N ) = FV(M ) ∪ FV(N )
FV(λx.M ) = FV(M ) \ {x}
[N/x] x = N
[N/x] z = z if z = x
[N/x] (L M ) = ([N/x]L)([N/x]M )
[N/x] (λz.M ) = λz.([N/x]M ) if z = x and z ∈ FV(N )
Page 13
Dan Deavours
Everything (Part 2)
Renaming of bound variables
λx.M = λy.([y/x]M ) if y ∈ FV(M )
Operational Semantics:
(λx.M )N −→[N/x]M functional application (“beta − reduction )
Page 14
Dan Deavours
Don’t be fooled. The simple syntax of lambda calculus is remarkably powerful.
It may seem at first that there are a number of deficiencies:
• No numbers
• Only single arguments
• Conditionals
• Booleans
• Iteration
Take heart! They’re there.
Page 15
Dan Deavours
Multiple arguments
Multiple arguments can be performed using a “trick” known as higher-order
functions, i.e., functions that return functions. (Not surprising in lambda calculus,
given that everything is a function.)
E.g., suppose we want a function F to take two parameters.
F = λ(x, y).M illegal, but intuitively desirable
Instead, we write
F = λx.λy.M
You would use F L M .
Read: F is a function that, given a value N for x, yields a function that, given a
valueL for y, yields the result.
To “execute” F:
FNL = (λx.λy.M )N L
−→ (λy.[N/x]M )L
−→ [L/y][N/x]M
Page 16
Dan Deavours
Transformation of multiple parameter functions into higher order functions is called
Currying, after Curry. It was actually invented by Sch¨nfinkel, but somehow the term
Sch¨nfinkeling hasn’t caught on.
Page 17
Dan Deavours
Boolean values are, naturally, functions. The defnitions aren’t particularly useful
(and somewhat trivial); it’s how they’re used that lets them be booleans.
True = λt.λf.t
False = λt.λf.f
Neither of these functions have free variables, and thus are called combinators.
Combinators are inert with respect to substitution, i.e., [N/x]True = True.
The (important) implication of this is that the only way to interact with combinators
(booleans in particular) is through applying them to expressions.
Thus, we can write an if-the-else statement as follows:
If = λl.λm.λn.l m n
Page 18
Dan Deavours
A bit more iffy
Note: If L M N simply means L M N . In that sense, it is a trivial definition.
If True M N = (λl.λm.λn.l m n)True M N
−→ (λm.λn.True m n)M N
−→ (λn.True M n)N
−→ True M N
= (λt.λf.t)M N
−→ (λf.M )N
−→ M
Page 19
Dan Deavours
Boolean Operators
Boolean operators, such as AND, OR, XOR, NOT, etc. can be formed similarly.
And = λb. λc. b c False
And True X = X
And False X = False
Not = λb. b False True
Page 20
Dan Deavours
Two “objects” can be encoded into a pair.
Pair = λf. λs. λb. b f s
To get each object back out,
Fst = λp. p T rue
Snd = λp. p F alse
Note notation: p is for pair, b is for boolean, f first, s second.
Pair M N is a function that, when applied to a boolean b, applies b to M and N .
Page 21
Dan Deavours
Fst(P air M N ) = Fst((λf. λs. λb. b f s)M N )
−→ Fst((λs. λb. b M s)N )
−→ Fst(λb. b M N )
= (λb. b M N )True
−→ (λb. b M N )True
−→ True M N
−→∗ M
Page 22
Dan Deavours
Natural numbers can be encoded using Church Numerals, written C0 , C1 , C2 , . . ..
Naturally, numbers are functions.
C0 = λz. λs. z
C1 = λz. λs. s z
C2 = λz. λs. s (s z)
C3 = λz. λs. s (s (s z))
Cn = λz. λs. s(. . . (s z) . . .)
n times
Each number n is represented by a combinator Cn , a function that takes two
arguments: z (zero) and s (successor), and applies s n-times to z. Note that since
numbers are really functions, numbers can “do stuff.”
Page 23
Dan Deavours
Plus = λm. λn. λz. λs. m (n z s) s
Plus is a function that takes two arguments (numbers) m and n, and yields a
function that takes two arguments: z and s, i.e., a number.
Notice that m is a number, i.e., a function that takes z and s. The z is (n z s), i.e.,
the number n. Then apply s m-times more.
Page 24
Dan Deavours
Times = λm. λn. m C0 (Plus n)
Here, the “successor” function is (Plus n), and the “zero” function is really zero,
i.e., C0 . Apply (Plus n) m-times to C0 .
Page 25
Dan Deavours
Test for zero
Testing for zero is an important (critical) function for computational completeness.
Strategy: give a number a z that is True and a s that, when applied to z one or
more times, yields False.
IsZero = λm .m True(λx. False)
Here, z = True, s = λx. False.
IsZeroC0 = (λm. mTrue (λx. False)) C0
−→ C0 True (λx. False)
= (λz. λs. z)True (λx. False)
−→ λs. True(λx. False)
−→ True
Page 26
Dan Deavours
Test for zero
Another example:
IsZero C1 = (λm. m True) (λx. F alse)) C1
−→ C1 True(λx. False)
= (λz. λs. s z)True (λx. False)
−→ (λs. s True)(λx. False)
−→ (λx. False) True
−→ False
Page 27
Dan Deavours
Subtraction (is hard)
First, we will define
Pred C0 = C0 ,
Pred Ci+1 = Ci
Let Z = Pair C0 C0
Let S = λp. P air(Snd p) (Plus (Snd p) C1 )
Pred = λm. Fst (m Z S)
• Pred takes a number m and applies S m-times to Z.
• S takes a pair (Ci , Cj ) and returns the pair (Cj , Cj+1 ).
• Applying S m-times to Z yields (C0 , C0 ) if m = 0, or (Cm−1 , Cm ) if m > 0.
• Fst of (Cm−1 , Cm )−→∗ Cm−1 .
Page 28
Dan Deavours
To perform recursive definitions (calculations), it is useful to define the so-called Y
Y = λf. (λx. f (x x))(λx. f (xx))
This may look odd, but it has the very interesting (and important) property that
Y F =β F (Y F ), for any F !
YF = (λf. (λx. f (x x))(λx. f (x x)))F
−→ (λx. F (x x))(λx. F (x x))
−→ F ((λx. F (x x))(λx. F (x x)))
←− F ((λf. (λx. f (x x))(λx. f (x x)))F )
= F (Y F )
Page 29
Dan Deavours
You can define the factorial function recursively:
if n = 0 then 1
else n · ( if n − 1 = 0 then 1
else (n − 1) · ( if n − 2 = 0 then 1
else (n − 2) · . . .))
F = YG
=β G(Y G)
=β G(G(Y G))
=β ...
Page 30
Dan Deavours
More on Factorial
Fact = λf. λn. If (IsZero n) C1 (Times n(f (Pred n)))
Factorial = Y Fact
Ok, but how do you know it works? What is 2!?
Page 31
Dan Deavours
Factorial Example
Factorial C2 = Y Fact C2
=β Fact(Y Fact) C2
=β (λFact. λn. If (IsZero n) C1 (Times n (Fact (Pred n))))(Y Fact)C2
=β (λn. If (IsZero n) C1 (Times n (Y Fact (Pred n)))) C2
=β If (IsZero C2 ) C1 (Times C2 (Y Fact (Pred C2 )))
=β If False C1 (Times C2 (Y Fact C1 ))
=β Times C2 (Y Fact C1 )
=β Times C2 (Factorial C1 )
Page 32
Dan Deavours
Other Useful Combinators
I = λx. x
K = λx. λy. x
S = λx. λy. λz. (x z) (y z)
I is the identity combinator.
K takes two arguments and throws away the second.
S “distributes” its third argument to both its first and second.
Astonishing Fact: For any combinator N , there exists a combinator M such that
N =β M , and M can be writtten using only I, K, and S.
I.e., I, K, and S contain the full power of lambda-abstraction
E.g., False = K I.
Page 33
Dan Deavours
Not all expressions are reducable, and some depend on the strategy for reduction.
Ω = (λx. x x) (λx. x x)
Is similar to
10 GOTO 10
Page 34

Use: 0.2087