CS 461
Lambda Calculus 1:
Yanling Wang
Computer Science and Engineering Penn State University
Carnegie Mellon
1
Midterm Rules ¢ See document.
Carnegie Mellon
2
Plan for next week
¢ Only one very short/low weight assignment as hw5.
¢ Monday we will review homework problems / sample exam. No new lecture.
Carnegie Mellon
3
Functional Language
Output = 𝑓 (Input)
Functional: program is a mathematical function
Carnegie Mellon
4
History
What is computation?
¢ Combinatory logic (1920’s) (Moses Ilyich Schönfinkel and
Haskell Brooks Curry)
¢ Lambda calculus (1930’s) (Alonzo Church) ¢ Turing machine (1930’s) (Alan Turing) ¢…
First electronic general-purpose computer ¢ ENIAC (1946)
Carnegie Mellon
5
Mathematical Function
A mathematical function is a mapping of members of one set, called the domain set, to another set, called the range set (image).
Carnegie Mellon
Notations:
Domain Range
+: Z,Z ⟼Z isNegtive: Z ⟼ {True, False}
Function application
+12 = 3 (same as 1+2=3) isNegtive 1 = False
Infix form
6
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)
7
λ-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
8
λ-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
9
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
10