Church Numerals and Booleans¶
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)\)
Note that AND is a curried function of the two variables p and q. The following slide show indicates how TRUE AND FALSE, which is ((AND TRUE) FALSE) in curried form, is \(\beta\)-reduced.
Just as one would expect for Boolean operations, TRUE AND FALSE reduces to FALSE. You are encouraged to try similar reductions for FALSE AND TRUE, FALSE AND FALSE, TRUE AND TRUE to convince yourself that our definition of AND does exactly what it needs to do for all four possibilities.
2. Encoding If-Then-Else¶
The following problem is about a possible representation for the ternary IF/THEN/ELSE operator.
3. Encoding OR¶
The following problem is about a possible representation for the binary OR operator.
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 slide show of how the successor of THREE is reduced to FOUR.
Addition and multiplication can be encoded as curried functions:
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 slide show of how (MULT TWO THREE) is reduced to SIX.
We add a Church encoding for an operation that computes the predecessor of a Church numeral n:
PRED = \(\lambda n. \lambda f. \lambda x.(((n \; \lambda g. \lambda h.(h \; (g \; f)))\; \lambda u.x) \; \lambda u.u)\)
And finally, we add an operation to test for zero, which can be used in the if-then-else you identified in the previous practice problem (see above).
ISZERO = \(\lambda n.((n \; \lambda x.FALSE) \; TRUE)\)
Just as we did in the preceding slide shows, you should do some \(\beta\)-reductions using these defined operations to convince yourself that they work as expected.
5. Church Numerals with Addition and Multiplication¶
The following 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.
