Lambda Calculus: Church encoding

# Church encoding

TRUE  = T := λab. a
FALSE = F := λab. b

NOT :: Bool -> Bool
bcs :: Bool -> Bool -> Bool

NOT := λ p   t f . p f t

# p and q are Booleans, so they must both be T for AND to be T.
# t arg repr true arg and f false, so we can explicitly pass them in
AND := λ p q t f . p (q t f) f

theme

λ p q t f . p (q t f) f

λ a b . a

// Church encoding
λab. a


TRUE = λab. a

FALSE := λab. b

NOT :: Bool -> Bool
bcs :: Bool -> Bool -> Bool

NOT := λ p   t f . p f t

# p and q are Booleans, so they must both be T for AND to be T.
# t arg repr true arg and f false, so we can explicitly pass them in
AND := λ p q t f . p (q t f) f