Church Encoding - Church Booleans

Church booleans are the Church encoding of the boolean values true and false. Some programming languages use these as an implementation model for boolean arithmetic; examples are Smalltalk and Pico. The boolean values are represented as functions of two values that evaluate to one or the other of their arguments.

Formal definition in lambda calculus:

true ≡ λa.λb. a

false ≡ λa.λb. b

Note that this definition allows predicates (i.e. functions returning logical values) to directly act as if-clauses, e.g. if predicate is a unary predicate,

predicate x then-clause else-clause

evaluates to then-clause if predicate x evaluates to true, and to else-clause if predicate x evaluates to false.

Functions of boolean arithmetic can be derived for Church booleans:

and ≡ λm.λn. m n m

or ≡ λm.λn. m m n

not₁ ≡ λm.λa.λb. m b a

not₂ ≡ λm. m (λa.λb. b) (λa.λb. a)

xor ≡ λa.λb. a (not₂ b) b

if ≡ λm.λa.λb. m a b

Some examples:

and true false ≡ (λm.λn. m n m) (λa.λb. a) (λa.λb. b) ≡ (λa.λb. a) (λa.λb. b) (λa.λb. a) ≡ (λa.λb. b) ≡ false

or true false ≡ (λm.λn. m m n) (λa.λb. a) (λa.λb. b) ≡ (λa.λb. a) (λa.λb. a) (λa.λb. b) ≡ (λa.λb. a) ≡ true

not₁ true ≡ (λm.λa.λb. m b a) (λa.λb. a) ≡ (λa.λb. (λa.λb. a) b a) ≡ (λa.λb. (λb.b) a) ≡ (λa.λb. b) ≡ false

not₂ true ≡ (λm. m (λa.λb. b) (λa.λb. a)) (λa.λb. a) ≡ (λa.λb. a) (λa.λb. b) (λa.λb. a) ≡ (λb. (λa.λb. b)) (λa.λb. a) ≡ λ1.λb. b ≡ false