# 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))


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://mandober.gitbook.io/math-debrief/340-lambda-calculi/lambda-calculus-encodings/encodings/church-encoding3.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.