3.8. Church Numerals and Booleans¶
3.8.1. Church Booleans¶
To turn the \(\lambda\) calculus into a "real" programming language, we need to be able to manipulate:
- boolean constants (true, false)
- logical operators (and, or, not)
- conditionals (if)
- integers (0, 1, 2, 3, etc.)
- arithmetic operators (\(+\), \(-\), etc.)
- mathematical functions (factorial, etc.)
Alonzo Church, the creator of the \(lambda\) calculus, realized this and consequently set about to make a series of encodings of lambda expressions designed to satisfy the properties we expect from the items in the preceding list. Let's first examine some of the encodings for the church boolean constants and operations.
- TRUE = \(\lambda x. \lambda y.x\)
- FALSE = \(\lambda x. \lambda y.y\)
- AND = \(\lambda p. \lambda q.((p \; q) \; FALSE)\)
The following slideshow indicates how TRUE AND FALSE is \(\beta\) reduced.
As one would expect for boolean operations, TRUE AND FALSE reduces to FALSE.
3.8.2. Encoding If-Then-Else¶
This problem is about a possible representation for the ternary IF/THEN/ELSE operator.
3.8.3. Encoding OR¶
This problem is about a possible representation for the binary OR operator.
3.8.4. Church Numerals¶
To encode the non-negative integers, Church used the following encoding:
- ZERO = \(\lambda f. \lambda\ x.x\)
- A successor function SUCC = \(\lambda n. \lambda f. \lambda x.(f \; ((n \; f) \; x))\)
- ONE = (SUCC ZERO) = \(\lambda f. \lambda\ x.(f \; x)\)
- TWO = (SUCC ONE) = \(\lambda f. \lambda\ x.(f \; (f \; x))\)
- THREE = (SUCC TWO) = \(\lambda f. \lambda\ x.(f \; (f \; (f \; x)))\)
- FOUR = (SUCC THREE) = ???
- FIVE = (SUCC FOUR) = ???
- SIX = (SUCC FIVE) = ???
- SEVEN = (SUCC SIX) = ???
- EIGHT = (SUCC SEVEN) = ???
- NINE = (SUCC EIGHT) = ???
- TEN = (SUCC NINE) = ???
To help you see how the successor function works, watch the following slideshow of how the successor of THREE is reduced to FOUR.
Addition and multiplication can be encoded as:
- PLUS = \(\lambda m. \lambda n. \lambda f. \lambda x.((n \;f) \; ((m \; f) \; x))\)
- MULT = \(\lambda m. \lambda n. \lambda f.(m \; (n \; f))\)
To see how the multiplication function works, watch the following slideshow of how (MULT TWO THREE) reduced to SIX.
An encoding for a predecessor operation:
PRED = \(\lambda n. \lambda f. \lambda x.(((n \; \lambda g. \lambda h.(h \; (g \; f))) \lambda u.x) \; \lambda u.u)\)
And an operation to test for zero in an if-then-else
ISZERO = \(\lambda n.((n \; \lambda x.FALSE) \; TRUE)\)
3.8.5. Church numerals with addition and multiplication¶
This problem will help you recognize and use the Church numerals as well as the representation of the corresponding addition and multiplication operators. To get credit for this randomized problem, you must solve it correctly three times in a row.
