
Boolean values can be defined in the
Lambda Calculus, although they are often "built into"
programming languages based on Lambda Calculus.
let
TRUE = lambda a. lambda b. a,
FALSE = lambda a. lambda b. b
in let
AND = lambda p. lambda q. p q FALSE,
OR = lambda p. lambda q. p TRUE q,
NOT = lambda p. lambda a. lambda b. p b a,
IF = lambda p. lambda a. lambda b. p a b,
EQ = lambda x. lambda y.
if x = y then TRUE else FALSE
in {simple test:}
IF TRUE 1 (1) ::
IF FALSE (2) 2 ::
IF (OR FALSE TRUE) 3 (3) ::
IF (AND FALSE TRUE) (4) 4 ::
IF (NOT FALSE) 5 (5) ::
IF (EQ 1 1) 6 (6) ::
IF (OR (EQ 1 2) (EQ 2 2)) 7 (7) ::
nil
{\fB Define Boolean From Scratch. \fP}

The example defines `TRUE', `FALSE', `AND', `OR', etc.
from first principles but defines `EQ' using the built in `=' which
is of course a cheat (to keep the example small). However, the section on
integers
shows how to define `ISZERO' which could
be used to define `EQ' from first principles.
Also see
[Ints]
and
[Lists].

window on the wide world:
λ ...
::  list cons 
nil  the [ ] list 
null  predicate 
hd  head (1st) 
tl  tail (rest) 


