CS 461
Lambda Calculus 5: Church Encoding 2
Yanling Wang
Computer Science and Engineering Penn State University
Carnegie Mellon
1
How to encode things in 𝝀-Calculus
¢ Booleans (last lecture) § True, False
§ Boolean operations: and, or, …
§ if expression: if condition then-expr else-expr
¢ Natural Numbers (last lecture and today’s lecture) § Natural numbers 0, 1, 2, …
§ Operations on natural numbers, +, -, *, /
¢ Structures (today’s lecture) § Pair, and left/right selection § List
¢ Recursive functions (next lecture)
Carnegie Mellon
2
Encoding: Natural Numbers Natural numbers
Churchnumerals: n ≜”λ”𝑓𝑧.𝑓^𝑛 𝑧 Note: n is the encoding of number n
0≜ λ𝑓𝑧.𝑓!𝑧=λ𝑓𝑧.𝑧
1≜ λ𝑓𝑧.𝑓”𝑧=λ𝑓𝑧.(𝑓𝑧) 2≜ λ𝑓𝑧.𝑓#𝑧=λ𝑓𝑧.(𝑓(𝑓𝑧)) …
𝑛-fold composition
Carnegie Mellon
3
3
Encoding: Natural Numbers Natural numbers
n ≜ λ𝑓𝑧.𝑓$𝑧 Encoding of “+ 1”?
SUCC 𝑛 =λ𝑓𝑧.𝑓$%”𝑧 Definition SUCC ≜ λ𝑛 𝑓 𝑧. (𝑓 (𝑛 𝑓 𝑧))
Goal:
Carnegie Mellon
4
4
Encoding: Natural Numbers Natural numbers
n ≜ λ𝑓𝑧.𝑓$𝑧 Encoding of “+”?
Goal:
Definition
PLUS 𝑛” 𝑛# =λ𝑓𝑧.𝑓$!%$” 𝑧 PLUS ≜ λ𝑛” 𝑛#. (𝑛” SUCC 𝑛2)
Carnegie Mellon
5
5
Encoding: Natural Numbers Natural numbers
n
≜ λ𝑓𝑧.𝑓$𝑧
Definition
Carnegie Mellon
PLUS ≜ λ𝑛” 𝑛#. (𝑛” SUCC 𝑛2) Check that PLUS1 2 = 3 (Note 2)
6
6
Pair and selection in Racket/Scheme ¢ Forming a pair:
§ (cons v1 v2)
¢ Selecting from a pair: § selecting left: (car p) § selecting right: (cdr p)
Carnegie Mellon
7
Encoding: Pair and selection
PAIR ≜ λ𝑥𝑦.λ𝑓.𝑓𝑥𝑦 LEFT ≜ λ𝑝.𝑝λ𝑥𝑦.𝑥
RIGHT ≜ λ𝑝.𝑝λ𝑥𝑦.𝑦
Carnegie Mellon
8
Encoding: Pair and selection
PAIR ≜λ𝑥𝑦.λ𝑓.𝑓𝑥𝑦 LEFT ≜ λ𝑝.𝑝λ𝑥𝑦.𝑥 RIGHT ≜ λ𝑝.𝑝λ𝑥𝑦.𝑦
Examples:
p = PAIR TRUE FALSE = (λ𝑥 𝑦. λ 𝑓. 𝑓𝑥 𝑦) TRUE FALSE LEFT p =
RIGHT p =
Carnegie Mellon
9
List and list operations in Racket/Scheme
¢ List in racket
§ null/empty/‘(): an empty list
§ null?/empty?: predicate function returns #t when list is empty and returns #f otherwise
§ (cons head tail): adding an element (head) to the beginning of a list (tail)
§ (car list): retrieve the head element of a non-empty list.
§ (cdr list): retrieve the tail list of a non-empty list.
Carnegie Mellon
10
Encoding: List
NULL ≜ FALSE ≜ λ𝑥 𝑦.𝑦 CONS ≜ PAIR≜λ𝑥𝑦.λ𝑓.𝑓𝑥𝑦
CAR ≜LEFT≜λ𝑝.𝑝λ𝑥𝑦.𝑥 CDR ≜RIGHT≜λ𝑝.𝑝λ𝑥𝑦.𝑦
NULL? ≜λ𝑙.𝑙(λh𝑡.λ𝑑.FALSE)TRUE
Carnegie Mellon
11