CS 461
Lambda Calculus 6:
Church Encoding 3 and List in Racket
Yanling Wang
Computer Science and Engineering Penn State University
Carnegie Mellon
1
How to encode things in 𝝀-Calculus
¢ Booleans (lecture 18/19) § True, False
§ Boolean operations: and, or, …
§ if expression: if condition then-expr else-expr
¢ Natural Numbers (lecture 18/19)
§ Natural numbers 0, 1, 2, …
§ Operations on natural numbers, +, -, *, /
¢ Structures
§ Pair, and left/right selection (lecture 19) § List (lecture 20)
¢ Recursive functions (lecture 20)
Carnegie Mellon
2
Encoding: Pair and selection
PAIR ≜ λ𝑥𝑦.λ𝑓.𝑓𝑥𝑦 LEFT ≜ λ𝑝.𝑝λ𝑥𝑦.𝑥
RIGHT ≜ λ𝑝.𝑝λ𝑥𝑦.𝑦
Carnegie Mellon
3
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
4
List
¢ ‘() or null or empty are an empty list with no elements.
¢ Otherwise, non-empty lists are a pair
§ It is a pair of an element (list head) and another list (list tail)
§ (cons 1 null) -> ‘(1)
§ (cons 1 ‘(2 3 4)) -> ‘(1 2 3 4)
¢ Any thing we want to do with a list, we need to deal with: § what do we do with an empty list? (null case)
§ what do we do with a non-empty list?
§ In particular, how do we use head/tail to solve the problem?
Carnegie Mellon
5
List
¢ Some sample list implementations in Racket § length
§ append § map
Carnegie Mellon
6
Encoding: List
NULL ≜ FALSE ≜ λ𝑥 𝑦.𝑦 CONS ≜ PAIR≜λ𝑥𝑦.λ𝑓.𝑓𝑥𝑦
CAR ≜LEFT≜λ𝑝.𝑝λ𝑥𝑦.𝑥 CDR ≜RIGHT≜λ𝑝.𝑝λ𝑥𝑦.𝑦
NULL? ≜λ𝑙.𝑙(λh𝑡.λ𝑑.FALSE)TRUE LISTFUNCTION ≜ λ𝑙. 𝑙 (λh 𝑡. λ𝑑. tht) tnull
Carnegie Mellon
7
Evaluation examples
NULL ≜ FALSE ≜ λ𝑥 𝑦.𝑦
NULL? ≜λ𝑙.𝑙(λh𝑡.λ𝑑.FALSE)TRUE NULL? NULL
Carnegie Mellon
8
Evaluation examples
CONS ≜ PAIR≜λ𝑥𝑦.λ𝑓.𝑓𝑥𝑦 NULL? ≜λ𝑙.𝑙(λh𝑡.λ𝑑.FALSE)TRUE NULL? (CONS TRUE NULL)
Carnegie Mellon
9
Encoding: infinte evaluation
(λ𝑥. 𝑥 𝑥)(λ𝑥. 𝑥 𝑥)
Carnegie Mellon
10
Encoding: Recursion
FACT ≜ λn. if n = 0 then 1 else n × FACT (n − 1)
FACTʹ ≜ λf.λn.if n = 0 then 1 else n×(f f (n−1)) FACT ≜ FACTʹ FACTʹ
Carnegie Mellon
11