CS 461
Lambda Calculus 3: Substitution, ⍺ and β reductions
Yanling Wang
Computer Science and Engineering Penn State University
Carnegie Mellon
1
Syntax vs. Semantics
Syntax: the structure/form of lambda terms
Semantics: the meaning of lambda terms ¢ Lambda calculus defines computation ¢ What computation is defined by 𝑡 ?
Carnegie Mellon
2
Capture-Avoiding Substitution
In λ-calculus, computation is defined by capture- avoiding substitution
𝑡{𝑦/𝑥} means substitute all free 𝑥 in 𝑡 with 𝑦 same x?
(λ𝑥.𝑥) 𝑥 bound free
Carnegie Mellon
Analogy in C:
int x;
…
int f (int x) {return x}
3
Bound vs. Free Variables
In (λ𝑥. 𝑡), the variable 𝑥 in 𝑡 is bound to a λ A variable is free if it is not bound to any λ A variable is bound to the closest λ
Examples
(λ𝑥. 𝑥) 𝑥 applies the identity function to x (i.e., the 𝑥
after dot is bound to λ)
λ𝑥. λ𝑥. 𝑥 is a function that takes a parameter, and returns the identity function (i.e., the inner-most 𝑥 is bound to the second λ)
Carnegie Mellon
4
More Formally …
In (λ𝑥. 𝑡), all free variables 𝑥 in 𝑡 is bound to λ𝑥
A variable is free if it is not bound to any λ
Systematically, we define free variables as follows:
¢ FV 𝑥 = {𝑥}
¢FV𝑡!𝑡” =FV𝑡! ∪FV(𝑡”) ¢ FV 𝜆𝑥.𝑡 =FV 𝑡 − 𝑥
Let Var(𝑡) be all variables used in 𝑡, the bound variables in 𝑡 (written BD(𝑡)) are
BD𝑡 =Var𝑡 −FV(𝑡)
Carnegie Mellon
5
𝛼-Reduction (Informal) Identity function: λ𝑥. 𝑥
is the same as λ𝑦.𝑦 and λ𝑧.𝑧 etc.
Observation: the name of a parameter is irrelevant in λ-calculus
Carnegie Mellon
Analogy in C:
int f (int x) {return x} Is same as int f (int y) {return y} Is same as int f (int z) {return z}
6
𝛼-Reduction
Observation: the name of a parameter is irrelevant in
λ-calculus
Tophat 𝛼-Reduction 1 and 2
(λ𝑥.𝑥 𝑥) = (λ𝑦.𝑦 𝑦) ? (λ𝑥.𝑥 𝑥) = (λ𝑦.𝑥 𝑦) ? 𝑥=𝑦?
(λ𝑥. λ𝑥.𝑥)=(λ𝑦.λ𝑥.𝑦)? (λ𝑥. λ𝑦.𝑥)=(λ𝑦.λ𝒚.𝑦)?
Carnegie Mellon
7
𝛼-Reduction (formal)
λ𝑥.𝑡 = λ𝑦.𝑡{𝑦/𝑥} when 𝑦 ∉ FV(𝑡) and 𝑦 will not be
captured/bound in t
where 𝑡{𝑦/𝑥} means substitute all free 𝑥 in 𝑡 with 𝑦
(λ𝑥.𝑥 𝑥) = (λ𝑦.𝑦 𝑦) (λ𝑥.𝑥 𝑥) ≠ (λ𝑦.𝑥 𝑦)
𝑥≠𝑦
(λ𝑥. λ𝑥. 𝑥) ≠ (λ𝑦. λ𝑥. 𝑦) (λ𝑥. λ𝑦. 𝑥) ≠ (λ𝑦. λ𝒚. 𝑦)
Carnegie Mellon
8
𝛽-Reduction (Informal) Identity function: λ𝑥. 𝑥
(λ𝑥. 𝑥) 𝑦 = 𝑦
Observation: we can substitute the formal parameter with the true argument in function application
Carnegie Mellon
Analogy in C:
Abstraction: int f (int x) {return x} Application: f(y) evaluates to y
9
𝛽-Reduction
The key reduction rule in λ calculus
(λ𝑥. 𝑡!) 𝑡” = 𝑡!{𝑡”/𝑥} Capture-avoiding
substitution
• Substitution:
• Replace all free x in t1 with t2
• Capture-avoiding:
• Any free variables in FV(t2) will not be bound/captured by
any λ in t1
• If a capture would happen, use 𝛼–reduction to rename
Carnegie Mellon
those λ in t1 10
10
𝛽-Reduction Example Example 1: (λ𝑥. 𝑥 𝑥) 𝑦
Carnegie Mellon
𝛽-Reduction
(λ𝑥. 𝑡.) 𝑡/ = 𝑡.{𝑡//𝑥}
11
11
𝛽-Reduction Example Example2:(λ𝑥. λ𝑦.𝑥𝑦)𝑦
Carnegie Mellon
𝛽-Reduction
(λ𝑥. 𝑡.) 𝑡/ = 𝑡.{𝑡//𝑥}
13
13
Useful Rule
We say a term t is closed if it contains no free variable
Examples: (λ𝑥. 𝑥) (λ𝑥. λ𝑦. 𝑥 𝑦 )
Rule: for a capture avoiding substitution
𝑡!{𝑡”/𝑥}
the subtle captured-variable check is vacuously true when 𝑡” is closed
Carnegie Mellon
15
15
Evaluation
An evaluation of a λ term is a sequence 𝑡! = 𝑡” = 𝑡# = …
where each step is either an α-reduction or a 𝛽-reduction
Carnegie Mellon
16
16
Evaluation Order
No reduction order is specified in classical λ- Calculus
If evaluation terminates, any order gives same result
(λ𝑥.(λ𝑦.𝑥) 𝑧) 𝑢 (λ𝑥.(λ𝑦.𝑥) 𝑧) 𝑢 =(λ𝑦. 𝑢)𝑧 =(λ𝑥. 𝑥)𝑢
=𝑢 =𝑢
Carnegie Mellon
17
17