CS 461
Lambda Calculus 2:
Yanling Wang
Computer Science and Engineering Penn State University
Carnegie Mellon
1
The λ-Calculus Alonzo Church, 1930s
A pure λ-term is defined inductively as follows: • Any variable 𝑥 is a λ-term
• If 𝑡 is a λ-term, so is λ𝑥. 𝑡 (abstraction)
• If 𝑡!, 𝑡” are λ-terms, so is 𝑡!𝑡” (application)
Carnegie Mellon
Analogy in C:
Abstraction: int f (int x) {return x+1} Application: f(2)
2
λ-Term Examples Identity function: λ𝑥. 𝑥
Application: (λ𝑥. 𝑥) 𝑦 [apply identity function to parameter 𝑦]
How to parse a λ-term
1. λ binding extends to the rightmost part
λ𝑥.𝑥 λ𝑦.𝑦 𝑧 is parsed as λ𝑥.(𝑥 (λ𝑦.(𝑦 𝑧)))
2. Applicationsareleft-associative
𝑡! 𝑡” 𝑡# is parsed as (𝑡! 𝑡”) 𝑡#
Carnegie Mellon
3
λ-Term Examples How to parse a λ-term
1. λ binding extends to the rightmost part
λ𝑥.𝑥 λ𝑦.𝑦 𝑧 is parsed as λ𝑥.(𝑥 (λ𝑦.(𝑦 𝑧))) 2. Applicationsareleft-associative
𝑡! 𝑡” 𝑡# is parsed as (𝑡! 𝑡”) 𝑡# Another example: 𝑥 λ𝑥.𝑦 𝑥 λ 𝑧.𝑥 𝑦
Carnegie Mellon
4
Number of Parameters
In the pure λ-calculus, λ only bind one parameter
For convenience, we write
λ𝑥𝑦.𝑡 asashorthandforλ𝑥.(λ𝑦.𝑡)
This process of removing parameters is called currying, which we will cover later in this course.
Carnegie Mellon
5
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
6
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}
7
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
8
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
9
Examples
Systematically, we define free variables as follows:
¢ FV 𝑥 = {𝑥}
¢FV𝑡!𝑡” =FV𝑡! ∪FV(𝑡”) ¢ FV 𝜆𝑥.𝑡 =FV 𝑡 − 𝑥
FV((λ𝑥. 𝑥) 𝑥)
FV(λy. (λ𝑥. (𝑥 𝑦)) 𝑥)
Carnegie Mellon
10