Church Booleans

In the simple untyped λ-calculus we can only deal with abstractions, applications and variables. So in order to do boolean manipulation, we need represent booleans. This Alonzo Church already had done for us. Let's have a look at Church encoding and Church booleans.

We define literals as $$true = \lambda t .\ \lambda f. t$$ and $$false = \lambda t .\ \lambda f. f$$ And with these in mind we can construct a test $$test = \lambda l .\ \lambda m .\ \lambda n.\ l\ m\ n$$ We can try reducing on $test\ true\ yes\ no$

test true yes no => (\lambda l . \lambda m . \lambda n . l m n) true yes no => (true yes no) => (\lambda t . \lambda f . t) yes no => yes

We can do the same for $test\ false\ yes\ no$

test false yes no => (\lambda l . \lambda m . \lambda n . l m n) false yes no => (\lambda t . \lambda f . f) yes no => no

$test$ doesn't do much by itself. The whole testing process is encoded in $true$ and $false$. However we can extend with boolean operators: $$and = \lambda b .\ \lambda c.\ b\ c\ false$$ Now we can try to reduce $and\ true\ false$

and true false => (\lambda b. \lambda c. b c false) true false => true false false => (\lambda t. \lambda f. t) false false => false

We have the same result for $and\ false\ true$ and $and\ false\ false$. However $and\ true\ true$ evaluates to true, and the behavior is as expected. Disjunction can be defined as $$\lambda b .\ \lambda c .\ b\ true\ c$$ Here observe that $true\ false$ evaluates to $false$ for any second argument. We can define negation as $$\lambda b.\ b\ false\ true$$

If you want to play around with the above definitions, you can do so here:

// literals let true = \ t . \ f . t; let false = \ t . \ f . f; // operators let and = \ b . \ c . b c false; let or = \ b . \ c . b true c; let not = \ b . b false true; let imp = \ b . \ c . or (not b) c; // conditional let test = \ l . \ m . \ n . l m n; // evaluation test (imp false true) yes no

...