Booleans & Pairs
Advanced Logic Data
No booleans either — so they get built too. The idea: true and false are choosers. A boolean is a function of two options that returns one of them.
The choosers
TRUE = λx.λy.x returns the first option
FALSE = λx.λy.y returns the second option
IF = λb.λt.λe.b t e hand the choices to the boolean
IF TRUE a b unfolds to TRUE a b →
a. The boolean is the if-statement — no
if keyword required.
The connectives
NOT = λb.λx.λy.b y x swap the options
AND = λa.λb.a b a if a is TRUE answer b, else a (=FALSE)
OR = λa.λb.a a b if a is TRUE answer a, else b
Pairs: data at last
PAIR = λx.λy.λf.f x y "store x and y, hand both to f"
FST = λp.p TRUE feed the pair a first-chooser
SND = λp.p FALSE feed it a second-chooser
A pair is a function waiting for a chooser. The two values sit inside until you pass in TRUE or FALSE to fish one out:
Quietly enormous
With booleans and pairs you have
if, logic gates, and a
data structure — enough to start building lists. All from the one
substitution rule. This is the moment the λ-calculus stops looking
like a toy and starts looking like a computer.
Practice
IF FALSE x y → ___
λx.λy.y encodes…
SND (PAIR a b) → ___
A Church boolean is best described as…
Next: recursion · Back: Church numerals