λ calculus Boolean
- 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.