> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/340-lambda-calculi/lambda-calculus-encodings/encodings/church-encoding3.md).

# Lambda Calculus: Church encoding

## deBruijn indices

T = λ. λ. 2 F = λ. λ. 1 NOT = λ. 1 F T AND = λ. λ. 2 1 F OR = λ. λ. 2 2 T BEQ = λ. λ. 2 (1 T F) (1 F T) PAIR = λ. λ. λ. 1 3 2 FST = λ. 1 T SND = λ. 1 F NIL = λ. T NULL = λ. 1 (λ. λ. F) DATUM = λ. FST 1 LEFT = λ. FST (SND 1) RIGHT = λ. SND (SND 1) TREE = λ. λ. λ. (PAIR 3) (PAIR 2 1) ZERO = λ. λ. 2 SUCC = λ. λ. λ. 2 (3 2 1) IS\_0 = λ. 1 (λ. F) T ADD = λ. λ. 2 SUCC 1 MUL = λ. λ. 2 (ADD 1) ZERO POW = λ. λ. 1 2

## Booleans

### Boolean constants

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

### Boolean connectives

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

NOT := λ p t f . p f t 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 -- i.e. t must be (λab.a) and f must be (λab.b) to make sense -- if p is F the f atg is immediately returned, otherwise first (q t f) -- that part tests q: if it is T thr t arg is returned else f arg AND := λ p q t f . p (q t f) f AND := λ p q . p q F ≡ λ p q . p q p -- However, since T always returns 1.arg and F second, we can write it as above

OR := λ p q t f . p t (q t f)

NOT := λ p . p F T OR := λ p q . p T q ≡ λ p q . p p q

IMP := λpq. p q T XOR := λpq. p F q

BEQ :: Bool -> Bool -> Bool BOOL\_EQ = BEQ := λpq. p (qTF) (qFT)

## Conditionals

IF :: Bool -> a -> a -> a IF := λ b t e . b t e

## Natural numbers

ZERO := λsz.z SUCC := λnsz.s(nsz)

ONE := λsz.sz ≡ SUCC ZERO TWO := λsz.s(sz) ≡ SUCC (SUCC ZERO)

// We start with zero. If our input is zero, we want to produce `T`. Otherwise, we want to produce `F`. In our function below, if the input is zero, we run the inner function zero times, which means we return the final argument (`T`). However, if the input is any number greater than zero, we run the inner function at least once; that inner function is designed to always produce `F`.

IS\_ZERO = 0? := λn. n F (NOT F)

ISZERO := λn. n (λ\_. F) T

// With K, we can redefine our isZero function more concisely.

IS\_0 := λn. n (K F) T

ADD := λab. a SUCC b ADD = (+) := λm. λn. λf. λx. m f (n f x)

MULT := λab. a ∘ b = compose = B

B := λgfx. g (f x)

// with B combinator, we can define SUCC without mentioning the final x SUCC := λnf. f ∘ (n f) ≡ λnf. B f (n f)

POW := λab.ba (Thrush)

## Pair

PAIR := λabs.sab

FST := λp.p(λab.a) SND := λp.p(λab.b)

## List

NIL := (PAIR) () ()

## Maybe

A Maybe value has two choices like Booleans, so the Church-encoded *Maybe* values will also be binary functions:

Nothing :: Maybe a Just :: a -> Maybe a

NOTHING := λn. λj. n JUST := λa. λn. λj. j a

## more

true : (λt. (λf. t)) false : (λt. (λf. f)) and : (λa. (λb. ((a b) a))) or : (λa. (λb. ((a a) b))) not : (λb. ((b false) true)) if : (λp. (λa. (λb. ((p a) b)))) pair : (λx. (λy. (λf. ((f x) y)))) cons : (λx. (λy. (λf. ((f x) y)))) first : (λp. (p true)) car : (λp. (p true)) second : (λp. (p false)) cdr : (λp. (p false)) nil : (λx. true) empty : (λx. true) null : (λp. (p (λx. (λy. false)))) isempty : (λp. (p (λx. (λy. false)))) tree : (λd. (λl. (λr. ((pair d) ((pair l) r))))) datum : (λt. (first t)) left : (λt. (first (second t))) right : (λt. (second (second t))) incr : (λn. (λf. (λy. (f ((n f) y))))) plus : (λm. (λn. ((m incr) n))) times : (λm. (λn. ((m (plus n)) zero))) iszero : (λn. ((n (λy. false)) true)) zero : (λf. (λx. x))