Boolean values can be defined in the
λ calculus, although they are often "built into"
programming languages based on λ 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
{ Define Boolean From Scratch. }
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.