Outline
● Lambda calculus recap
● Programming in lambda calculus
○ Church Booleans ○ Church Pairs
○ Church Numerals
○ Enriching the calculus
○ Recursion
Lambda calculus recap
Church booleans
tru := λt. λf. t fls := λt. λf. f test := λl. λm. λn. l m n
Church booleans
tru := λt. λf. t fls := λt. λf. f test := λl. λm. λn. l m n
Church Booleans: exercises
tru := λt. λf. t fls := λt. λf. f test := λl. λm. λn. l m n
Exercise 1.1. Implement logical or and and functions.
Church numerals: increment
c0 := λs. λz. z c1 := λs. λz. s z c2 := λs. λz. s (s z) c3 := λs. λz. s (s (s z)) inc := λn. λs. λz. s (n s z)
Exercise 1.2. Find another way to implement inc.
Church numerals: addition and multiplication
c0 := λs. λz. z c1 := λs. λz. s z c2 := λs. λz. s (s z) c3 := λs. λz. s (s (s z))
plus := λm. λn. λs. λz. m s (n s z) times := λm. λn. m (plus n) c0
Exercise 1.3. Implement times without using plus.
Exercise 1.4. Define a term for raising one number to the power of another.
Exercise 1.5. Define a term that checks whether a given term is zero.
Church numerals: subtraction
zz = pair c0 c0 ss = λp. pair (snd p) (plus c1 (snd p)) prd = λm. fst (m ss zz)
Exercise 1.6. Use prd to define subtraction.
Exercise 1.7. Approximate time complexity of prd.
Exercise 1.8. Write function equal that tests whether two numbers are equal.
Exercise 1.8*. See [TaPL, Exercise 5.2.8].
Enriching the calculus
Enriching the calculus
Recursion
fix := λf. (λx. f (λy. x x y)) (λx. f (λy. x x y)) g := λ fct. λn. if realeq n c0 then c1
else (times n (fct (prd n))) factorial := fix g
Exercise 1.9. Write down evaluation of factorial c3.
Exercise 1.10. Why did we use a primitive if in the definition of g, instead of the Church-boolean test function on Church booleans? Show how to define the factorial function in terms of test rather than if.
Exercise 1.11*. Use fix and the encoding of lists from Exercise 1.8 to write a function that sums lists of Church numerals.
Homework
1. Install DrRacket https://download.racket-lang.org
2. Read Quick: An Introduction to Racket with Pictures https://docs.racket-lang.org/quick/index.html
3. Read about Racket Essentials 2.1–2.2 https://docs.racket-lang.org/guide/to-scheme.html
4. Test yourself by implementing a program that renders a rainbow:
