CS 461
Lambda Calculus 4: Church Encoding
Yanling Wang
Computer Science and Engineering Penn State University
Carnegie Mellon
1
Is the λ-Calculus Turing complete?
Carnegie Mellon
2
2
How to encode things in 𝝀-Calculus
¢ Booleans
§ True, False
§ Boolean operations: and, or, …
§ if expression: if condition then-expr else-expr
¢ Natural Numbers
§ Natural numbers 0, 1, 2, …
§ Operations on natural numbers, +, -, *, /
¢ Structures
§ Pair, and left/right selection § List
¢ Recursive functions
Carnegie Mellon
3
Encoding: Boolean
Booleans
Shorthand for
λ𝑥. (λ𝑦. 𝑥)
Carnegie Mellon
TRUE ≜ λ𝑥 𝑦.𝑥 FALSE ≜ λ𝑥 𝑦.𝑦 Encoding of “if”? 𝑡 when 𝑏 is TRUE
Goal: IF 𝑏 𝑡 𝑓 = 3𝑓 when 𝑏 is FALSE Definition IF ≜ λ𝑏𝑡𝑓. (𝑏𝑡𝑓)
4
4
Encoding: Boolean Booleans
TRUE ≜ λ𝑥 𝑦.𝑥 FALSE ≜ λ𝑥 𝑦.𝑦
Encoding of “and”? TRUE when 𝑏!, 𝑏” are both TRUE
Goal: AND 𝑏! 𝑏” = 3 FALSE otherwise
AND ≜ λ𝑏! 𝑏”. (𝑏! (𝑏” TRUE FALSE) FALSE) Check that AND TRUE FALSE = FALSE (Note 2)
Definition
Carnegie Mellon
5
5
Encoding: Natural Numbers Natural numbers
Churchnumerals: n ≜”λ”𝑓𝑧.𝑓^𝑛 𝑧 Note: n is the encoding of number n
0≜ λ𝑓𝑧.𝑓#𝑧=λ𝑓𝑧.𝑧
1≜ λ𝑓𝑧.𝑓!𝑧=λ𝑓𝑧.(𝑓𝑧) 2≜ λ𝑓𝑧.𝑓”𝑧=λ𝑓𝑧.(𝑓(𝑓𝑧)) …
𝑛-fold composition
Carnegie Mellon
6
6
Encoding: Natural Numbers Natural numbers
n ≜ λ𝑓𝑧.𝑓$𝑧 Encoding of “+ 1”?
SUCC 𝑛 =λ𝑓𝑧.𝑓$%!𝑧 Definition SUCC ≜ λ𝑛 𝑓 𝑧. (𝑓 (𝑛 𝑓 𝑧))
Goal:
Carnegie Mellon
7
7
Encoding: Natural Numbers Natural numbers
n ≜ λ𝑓𝑧.𝑓$𝑧 Encoding of “+”?
Goal:
Definition
PLUS 𝑛! 𝑛” =λ𝑓𝑧.𝑓$!%$” 𝑧 PLUS ≜ λ𝑛! 𝑛”. (𝑛! SUCC 𝑛2)
Carnegie Mellon
8
8
Encoding: Natural Numbers Natural numbers
n
≜ λ𝑓𝑧.𝑓$𝑧
Definition
Carnegie Mellon
PLUS ≜ λ𝑛! 𝑛”. (𝑛! SUCC 𝑛2) Check that PLUS1 2 = 3 (Note 2)
9
9
Encoding: Pair and selection
PAIR ≜ λ𝑣! 𝑣”.λ𝑓.𝑓𝑣! 𝑣” LEFT ≜ λ𝑝.𝑝λ𝑣! 𝑣”.𝑣1
RIGHT ≜ λ𝑝.𝑝λ𝑣! 𝑣”.𝑣2
Carnegie Mellon
10