A

𝜆[Link]
F L O C K of F U N C T I O N S
C O M B I N AT O R S , L A M B D A C A L C U L U S ,
& C H U R C H E N C O D I N G S in J AVA S C R I P T
 glebec
Gabriel Lebec glebec
glebec
[Link]/glebec/lambda-talk glebec
g_lebec
😭
𝜆a.a
IDENTITY
λ I := 𝜆a.a

JS I = a => a
λ I := 𝜆a.a

JS I = a => a
λ I := 𝜆a.a

JS I = a => a
λ I := 𝜆a.a

JS I = a => a
λ I := 𝜆a.a

JS I = a => a
 I := 𝜆a.a
I = a => a

λ Ix=?

JS I(x) === ?
 I := 𝜆a.a
I = a => a

λ Ix=x

JS I(x) === x
 I := 𝜆a.a
I = a => a

λ II=?

JS I(I) === ?
 I := 𝜆a.a
I = a => a

λ II=I

JS I(I) === I
id 5 == 5
𝜆?
FUNCTION
SIGNIFIER 𝜆a.a
 PA R A M E T E R VA R I A B L E

FUNCTION
SIGNIFIER 𝜆a.a
 PA R A M E T E R VA R I A B L E

FUNCTION
SIGNIFIER 𝜆a.a RETURN
EXPRESSION
 PA R A M E T E R VA R I A B L E

FUNCTION
SIGNIFIER 𝜆a.a RETURN
EXPRESSION

LAMBDA ABSTRACTION
 𝜆 - C A L C U L U S S Y N TA X

expression ::= variable identifier

| expression expression application
| 𝜆 variable . expression abstraction
| ( expression ) grouping
λ → JS
VA R I A B L E S

x x
(a) (a)
 A P P L I C AT I O N S

fa f(a)
fab f(a)(b)
(f a) b (f(a))(b)
f (a b) f(a(b))
 ABSTRACTIONS

𝜆a.b a => b

𝜆a.b x a => b(x)

𝜆a.(b x) a => (b(x))

(𝜆a.b) x (a => b)(x)

𝜆a.𝜆b.a a => b => a

𝜆a.(𝜆b.a) a => (b => a)

 β-REDUCTION

((𝜆a.a)𝜆b.𝜆c.b)(x)𝜆e.f
 β-REDUCTION

((𝜆a.a)𝜆b.𝜆c.b)(x)𝜆e.f
 β-REDUCTION

((𝜆a.a)𝜆b.𝜆c.b)(x)𝜆e.f
 β-REDUCTION

((𝜆a.a)𝜆b.𝜆c.b)(x)𝜆e.f
= (𝜆b.𝜆c.b) (x)𝜆e.f
 β-REDUCTION

((𝜆a.a)𝜆b.𝜆c.b)(x)𝜆e.f
= (𝜆b.𝜆c.b) (x)𝜆e.f
 β-REDUCTION

((𝜆a.a)𝜆b.𝜆c.b)(x)𝜆e.f
= (𝜆b.𝜆c.b) (x)𝜆e.f
 β-REDUCTION

((𝜆a.a)𝜆b.𝜆c.b)(x)𝜆e.f
= (𝜆b.𝜆c.b) (x)𝜆e.f
= (𝜆c.x) 𝜆e.f
 β-REDUCTION

((𝜆a.a)𝜆b.𝜆c.b)(x)𝜆e.f
= (𝜆b.𝜆c.b) (x)𝜆e.f
= (𝜆c.x) 𝜆e.f
 β-REDUCTION

((𝜆a.a)𝜆b.𝜆c.b)(x)𝜆e.f
= (𝜆b.𝜆c.b) (x)𝜆e.f
= (𝜆c.x) 𝜆e.f
 β-REDUCTION

((𝜆a.a)𝜆b.𝜆c.b)(x)𝜆e.f
= (𝜆b.𝜆c.b) (x)𝜆e.f
= (𝜆c.x) 𝜆e.f
= x
 β-REDUCTION*

((𝜆a.a)𝜆b.𝜆c.b)(x)𝜆e.f
= (𝜆b.𝜆c.b) (x)𝜆e.f
= (𝜆c.x) 𝜆e.f
= x
β-NORMAL FORM
*not covered: evaluation order, variable collision avoidance
𝜆[Link]
MOCKINGBIRD
λ M := 𝜆[Link]

JS M = f => f(f)
λ M := 𝜆[Link]

JS M = f => f(f)
λ M := 𝜆[Link]

JS M = f => f(f)
λ M := 𝜆[Link]

JS M = f => f(f)
 M := 𝜆[Link]

λ MI=?

JS M(I) === ?
 M := 𝜆[Link]

λ MI=II=?

JS M(I) === I(I)

&& I(I) === ?
 M := 𝜆[Link]

λ MI=II=I

JS M(I) === I(I)

&& I(I) === I
 M := 𝜆[Link]

λ MM=?

JS M(M) === ?
 M := 𝜆[Link]

λ MM=MM=?

JS M(M) === M(M) === ?

 M := 𝜆[Link]

λ MM=MM=MM=Ω

// stack overflow
JS M(M) ===
M(M) ===
M(M) ===
M(M) ===
M(M)
M(M)
===
===
M(M)
M(M)
===
===
M
M
M(M) === M(M) === M(M) === M(M) === M
M(M) === M(M) === M(M) === M(M) === M
M(M) === M(M) === M(M) === M(M) === M
 M := 𝜆[Link]

λ ω ω =ω ω =ω ω =Ω

// stack overflow
JS M(M) ===
M(M) ===
M(M) ===
M(M) ===
M(M)
M(M)
===
===
M(M)
M(M)
===
===
M
M
M(M) === M(M) === M(M) === M(M) === M
M(M) === M(M) === M(M) === M(M) === M
M(M) === M(M) === M(M) === M(M) === M
 A B S T R A C T I O N S , again

𝜆a.𝜆b.𝜆c.b a => b => c => b

= 𝜆abc.b a => b => c => b

(a, b, c) => b
 β - R E D U C T I O N , again

((𝜆a.a)𝜆bc.b)(x)𝜆e.f
 β - R E D U C T I O N , again

((𝜆a.a)𝜆bc.b)(x)𝜆e.f
= (𝜆bc.b) (x)𝜆e.f
 β - R E D U C T I O N , again

((𝜆a.a)𝜆bc.b)(x)𝜆e.f
= (𝜆bc.b) (x)𝜆e.f
 β - R E D U C T I O N , again

((𝜆a.a)𝜆bc.b)(x)𝜆e.f
= (𝜆bc.b) (x)𝜆e.f
= (𝜆c.x) 𝜆e.f
 β - R E D U C T I O N , again

((𝜆a.a)𝜆bc.b)(x)𝜆e.f
= (𝜆bc.b) (x)𝜆e.f
= (𝜆c.x) 𝜆e.f
 β - R E D U C T I O N , again

((𝜆a.a)𝜆bc.b)(x)𝜆e.f
= (𝜆bc.b) (x)𝜆e.f
= (𝜆c.x) 𝜆e.f
= x
β-NORMAL FORM
𝜆ab.a
KESTREL
λ K := 𝜆ab.a
= 𝜆a.𝜆b.a

JS K = a => b => a
λ K := 𝜆ab.a
= 𝜆a.𝜆b.a

JS K = a => b => a
λ K := 𝜆ab.a
= 𝜆a.𝜆b.a

JS K = a => b => a
λ K := 𝜆ab.a
= 𝜆a.𝜆b.a

JS K = a => b => a
 K := 𝜆ab.a
K = a => b => a

λ KMI=?

JS K(M)(I) === ?
 K := 𝜆ab.a
K = a => b => a

λ KMI=M

JS K(M)(I) === M
 K := 𝜆ab.a
K = a => b => a

λ KMI=M
KIM=?

JS K(M)(I) === M
K(I)(M) === ?
 K := 𝜆ab.a
K = a => b => a

λ KMI=M
KIM=I

JS K(M)(I) === M
K(I)(M) === I
const 7 2 == 7
 K := 𝜆ab.a
K = a => b => a

λ KIx =I

JS K(I)(x) === I
 K := 𝜆ab.a
K = a => b => a

λ KIxy=Iy=?

JS K(I)(x)(y) === I(y)

&& I(y) === ?
 K := 𝜆ab.a
K = a => b => a

λ KIxy=Iy=y

JS K(I)(x)(y) === I(y)

&& I(y) === y
 K := 𝜆ab.a
K = a => b => a

λ KIxy=Iy=y

JS K(I)(x)(y) === I(y)

&& I(y) === y
 K := 𝜆ab.a
K = a => b => a

λ KIxy=Iy=y

JS K(I)(x)(y) === I(y)

&& I(y) === y
𝜆ab.b
KITE
λ KI := 𝜆ab.b
=KI

JS KI = a => b => b
KI = K(I)
 KI := 𝜆ab.b
KI = a => b => b

λ KI M K = ?

JS KI(M)(K) === ?
 KI := 𝜆ab.b
KI = a => b => b

λ KI M K = K

JS KI(M)(K) === K
 KI := 𝜆ab.b
KI = a => b => b

λ KI M K = K
KI K M = ?

JS KI(M)(K) === K
KI(K)(M) === ?
 KI := 𝜆ab.b
KI = a => b => b

λ KI M K = K
KI K M = M

JS KI(M)(K) === K
KI(K)(M) === M
?
 SCHÖNFINKEL C U R RY S M U L LYA N

Identitätsfunktion I
 Idiot
 Ibis?

Konstante Funktion K
 Kestrel

verSchmelzungsfunktion S
 Starling

verTauschungsfunktion C
 Cardinal

Zusammensetzungsf. B Bluebird
🍛?
 T H E F O R M A L I Z AT I O N O F
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

M AT H E M AT I C A L L O G I C
 F O R M A L N O TAT I O N F O R F U N C T I O N S
1889
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

PEANO ARITHMETIC
 A X I O M AT I C L O G I C · F N N O TAT I O N
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

1891

F U N C T I O N S A S G R A P H S · C U R RY I N G
 P R I N C I P I A M AT H E M AT I C A
1910
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

R U S S E L L ’ S P A R A D O X · F N N O TAT I O N
 C O M B I N AT O RY L O G I C
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

1920

C O M B I N AT O R S · C U R RY I N G
 F U N C T I O N A L S Y S T E M O F S E T T H E O RY
1925
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

( O V E R L A P P E D W I T H C O M B I N AT O RY L O G I C )
 C O M B I N AT O RY L O G I C ( A G A I N )
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

1926

C O M B I N AT O R S · M A N Y C O N T R I B U T I O N S
 DISCOVERS SCHÖNFINKEL
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

1927

“This paper anticipates much of what I have done.”

 INCOMPLETENESS THEOREMS
1931
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

ENDING THE SEARCH FOR SUFFICIENT AXIOMS

 𝜆-CALCULUS
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

1932

A N E F F E C T I V E M O D E L O F C O M P U TAT I O N
 INCONSISTENCY OF SPECIALIZED 𝜆
1931–1936
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

CONSISTENCY OF PURE 𝜆
 S O LV E S T H E D E C I S I O N P R O B L E M
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

1936

VIA THE 𝜆-CALCULUS

 S O LV E S T H E D E C I S I O N P R O B L E M
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

1936

VIA THE TURING MACHINE

 E S TA B L I S H E S T H E C H U R C H - T U R I N G T H E S I S
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

1936

𝜆-CALCULUS TURING MACHINE

 O B TA I N S PHD UNDER CHURCH
PEANO RU S S E L L VO N N E U M A N N GÖDEL KLEENE RO S S E R

FREGE SCHÖNFINKEL C U R RY C H U RC H TURING

1936–1938

P U B L I S H E S 1 S T F I X E D - P O I N T C O M B I N AT O R
 C O M B I N AT O R S
functions with no free variables

𝜆b.b combinator
𝜆b.a not a combinator
𝜆ab.a combinator
𝜆[Link] not a combinator
𝜆abc.c(𝜆e.b) combinator
 C O M B I N AT O R S
Sym. Bird 𝜆-Calculus Use Haskell
I Idiot 𝜆a.a identity id

M Mockingbird 𝜆f.ff self-application (cannot define)

K Kestrel 𝜆ab.a first, const const

KI Kite 𝜆ab.b = KI second const id

C Cardinal 𝜆[Link] reverse arguments flip

B Bluebird 𝜆fga.f(ga) 1°-1° composition (.)

B1 Blackbird 𝜆fgab.f(gab) = BBB 1°-2° composition (.) . (.)

Th Thrush 𝜆[Link] = CI hold an argument flip id

V Vireo 𝜆[Link] = BCT hold a pair of args flip . flip id

𝜆[Link]
CARDINAL
λ C := 𝜆[Link]

JS C = f => a => b => f(b)(a)

 C := 𝜆[Link]
C = f => a => b => f(b)(a)

λ CKIM=?

JS C(K)(I)(M) === ?
 C := 𝜆[Link]
C = f => a => b => f(b)(a)

λ CKIM=M

JS C(K)(I)(M) === M
 C := 𝜆[Link]
C = f => a => b => f(b)(a)

λ CKIM=M

JS C(K)(I)(M) === M
 C := 𝜆[Link]
C = f => a => b => f(b)(a)

λ KI I M = M

JS KI(I)(M) === M
 C O M B I N AT O R S
Sym. Bird 𝜆-Calculus Use Haskell
I Idiot 𝜆a.a identity id

M Mockingbird 𝜆f.ff self-application (cannot define)

K Kestrel 𝜆ab.a first, const const

KI Kite 𝜆ab.b = KI second const id

C Cardinal 𝜆[Link] reverse arguments flip

B Bluebird 𝜆fga.f(ga) 1°-1° composition (.)

B1 Blackbird 𝜆fgab.f(gab) = BBB 1°-2° composition (.) . (.)

Th Thrush 𝜆[Link] = CI hold an argument flip id

V Vireo 𝜆[Link] = BCT hold a pair of args flip . flip id

 C O M B I N AT O R S
Sym. Bird 𝜆-Calculus Use Haskell
I Idiot 𝜆a.a identity id

M Mockingbird 𝜆f.ff self-application (cannot define)

K Kestrel 𝜆ab.a first, const const

KI Kite 𝜆ab.b = KI = CK second const id

C Cardinal 𝜆[Link] reverse arguments flip

B Bluebird 𝜆fga.f(ga) 1°-1° composition (.)

B1 Blackbird 𝜆fgab.f(gab) = BBB 1°-2° composition (.) . (.)

Th Thrush 𝜆[Link] = CI hold an argument flip id

V Vireo 𝜆[Link] = BCT hold a pair of args flip . flip id

flip const 1 8 == 8
 𝜆-CALCULUS TURING MACHINE
abstract symbol rewriting hypothetical device
functional computation state-based computation

(𝜆[Link])𝜆a.a
real computers
machine code
assembly languages
higher-level machine-centric languages
higher-level abstract stateful languages
purely functional programming languages
𝜆 TM
E V E RY T H I N G

CAN BE
FUNCTIONS
 …
T R U E FA L S E N O T A N D O R B E Q
λ
JS const result = bool ? exp1 : exp2
λ
JS const result = bool ? exp1 : exp2
// true
λ
JS const result = bool ? exp1 : exp2
// false
λ result := ?

JS const result = bool ? exp1 : exp2

λ result := bool ? exp1 : exp2

JS const result = bool ? exp1 : exp2

λ result := bool exp1 exp2

JS const result = bool ? exp1 : exp2

λ result := func exp1 exp2

JS const result = bool (exp1) (exp2)

λ result := func exp1 exp2

JS const result = bool

// true
(exp1) (exp2)
λ result := func exp1 exp2

JS const result = bool (exp1) (exp2)

// false
 TRUE

λ result := func exp1 exp2

FALSE

JS const result = bool (exp1) (exp2)

 K

λ result := func exp1 exp2

KI

JS const result = bool (exp1) (exp2)

CHURCH ENCODINGS: BOOLEANS

λ TRUE := K
FALSE := KI = C K

JS const T = K
const F = KI
λ !p

JS !p
λ NOT p

JS not(p)
 F
λ NOT p
T

F
JS not(p)
T
 F
λ NOT T
T

F
JS not(T)
T
 F
λ NOT F
T

F
JS not(F)
T
λ p F T

JS p (F) (T)
 K KI
λ T F T

K KI
JS T (F) (T)
 KI K
λ F F T

KI K
JS F (F) (T)
λ NOT := 𝜆[Link]

JS const not = p => p(F)(T)

 CHURCH ENCODINGS: BOOLEANS
Sym. Name 𝜆-Calculus Use

T TRUE 𝜆ab.a = K encoding for true

F FALSE 𝜆ab.b = KI = CK encoding for false

NOT 𝜆[Link] negation

AND 𝜆[Link] or 𝜆[Link] conjunction

OR 𝜆[Link] or 𝜆[Link] disjunction

BEQ 𝜆pq.p q (NOT q) equality

 NOT T = F
λ NOT F = T

JS not(T) === F
not(F) === T
 𝜆ab.a 𝜆ba.a
NOT K = KI
λ NOT (KI) = K
𝜆ba.a 𝜆ab.a

JS not(K) === KI
not(KI) === K
 C K = KI
λ C (KI) = K

JS C(K) (chirp)(tweet) === tweet

C(KI)(chirp)(tweet) === chirp
 CT=F
λ CF=T

JS C(T) (chirp)(tweet) === tweet

C(F) (chirp)(tweet) === chirp
 CHURCH ENCODINGS: BOOLEANS
Sym. Name 𝜆-Calculus Use

T TRUE 𝜆ab.a = K encoding for true

F FALSE 𝜆ab.b = KI = CK encoding for false

NOT 𝜆[Link] negation

AND 𝜆[Link] or 𝜆[Link] conjunction

OR 𝜆[Link] or 𝜆[Link] disjunction

BEQ 𝜆pq.p q (NOT q) equality

 CHURCH ENCODINGS: BOOLEANS
Sym. Name 𝜆-Calculus Use

T TRUE 𝜆ab.a = K encoding for true

F FALSE 𝜆ab.b = KI = CK encoding for false

NOT 𝜆[Link] or C negation

AND 𝜆[Link] or 𝜆[Link] conjunction

OR 𝜆[Link] or 𝜆[Link] disjunction

BEQ 𝜆pq.p q (NOT q) equality

λ AND := ?

JS const and = ?
λ AND := 𝜆pq.?

JS const and = p => q => ?

λ AND := 𝜆pq.p?¿

JS const and = p => q => p(?)(¿)

 F
λ AND := 𝜆pq.p?¿

F
JS const and = p => q => p(?)(¿)
λ AND := 𝜆pq.p?F

JS const and = p => q => p(?)(F)

 T
λ AND := 𝜆pq.p?F

T
JS const and = p => q => p(?)(F)
λ AND := 𝜆[Link]

JS const and = p => q => p(q)(F)

𝜆[Link] F
 q
𝜆pq.p
F
 q
𝜆pq.p
p
𝜆[Link] p
 CHURCH ENCODINGS: BOOLEANS
Sym. Name 𝜆-Calculus Use

T TRUE 𝜆ab.a = K encoding for true

F FALSE 𝜆ab.b = KI = CK encoding for false

NOT 𝜆[Link] or C negation

AND 𝜆[Link] or 𝜆[Link] conjunction

OR 𝜆[Link] or 𝜆[Link] disjunction

BEQ 𝜆pq.p q (NOT q) equality

λ OR := ?

JS const or = ?
λ OR := 𝜆pq.…

JS const or = p => q => …

λ OR := 𝜆pq.p?¿

JS const or = p => q => p(?)(¿)

λ OR := 𝜆[Link]¿

JS const or = p => q => p(T)(¿)

λ OR := 𝜆[Link]

JS const or = p => q => p(T)(q)

λ OR := 𝜆[Link]

JS const or = p => q => p(p)(q)

 CHURCH ENCODINGS: BOOLEANS
Sym. Name 𝜆-Calculus Use

T TRUE 𝜆ab.a = K encoding for true

F FALSE 𝜆ab.b = KI = CK encoding for false

NOT 𝜆[Link] or C negation

AND 𝜆[Link] or 𝜆[Link] conjunction

OR 𝜆[Link] or 𝜆[Link] disjunction

BEQ 𝜆pq.p q (NOT q) equality

𝜆[Link]
( 𝜆[Link] )xy = ?
( 𝜆[Link] )xy = xxy
( 𝜆[Link] )xy = xxy
( ? )xy = xxy
( 𝜆[Link] )xy = xxy
( ? )xy = xxy
( 𝜆[Link] )xy = xxy
M xy = xxy
( 𝜆[Link] )xy = xxy
M xy = xxy
 CHURCH ENCODINGS: BOOLEANS
Sym. Name 𝜆-Calculus Use

T TRUE 𝜆ab.a = K encoding for true

F FALSE 𝜆ab.b = KI = CK encoding for false

NOT 𝜆[Link] or C negation

AND 𝜆[Link] or 𝜆[Link] conjunction

OR 𝜆[Link] or 𝜆[Link] disjunction

BEQ 𝜆pq.p q (NOT q) equality

 CHURCH ENCODINGS: BOOLEANS
Sym. Name 𝜆-Calculus Use

T TRUE 𝜆ab.a = K encoding for true

F FALSE 𝜆ab.b = KI = CK encoding for false

NOT 𝜆[Link] or C negation

AND 𝜆[Link] or 𝜆[Link] conjunction

OR 𝜆[Link] or 𝜆[Link] = M* disjunction

BEQ 𝜆pq.p q (NOT q) equality

𝜆pq.p ( q T F )( q F T )
p => q => p(q(T)(F))(q(F)(T))
 (q T F)
𝜆pq.p
(q F T )
 T
(q )
F
𝜆pq.p
(q F)
T
 T
(q )
F
𝜆pq.p
(q F)
T
 T
(q )
F
𝜆pq.p
(q F)
T
 T
(q )
F
𝜆pq.p
(q F)
T
 T
(q )
F
𝜆pq.p
(q F)
T
 BOOLEAN EQUALITY

T
(q )
F
𝜆pq.p
(q F)
T
 q
𝜆pq.p
(q F)
T
 q
𝜆pq.p
(NOT q)
𝜆pq.p q (NOT q)
p => q => p(q)(not(q))
 CHURCH ENCODINGS: BOOLEANS
Sym. Name 𝜆-Calculus Use

T TRUE 𝜆ab.a = K encoding for true

F FALSE 𝜆ab.b = KI = CK encoding for false

NOT 𝜆[Link] or C negation

AND 𝜆[Link] or 𝜆[Link] conjunction

OR 𝜆[Link] or 𝜆[Link] = M* disjunction

BEQ 𝜆pq.p q (NOT q) equality

 ( O N E O F ) D E M O R G A N ' S L AW S

¬(P ∧ Q) = (¬P) ∨ (¬Q)

BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))
!(p && q) === (!p) || (!q)
BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

(𝜆xy.x y ((𝜆[Link]) y))


((𝜆[Link]) ((𝜆[Link]) p q))

((𝜆[Link]) ((𝜆[Link]) p) ((𝜆[Link]) q))
BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

(𝜆xy.x y ((𝜆[Link]) y))


((𝜆[Link]) ((𝜆[Link]) p q))

((𝜆[Link]) ((𝜆[Link]) p) ((𝜆[Link]) q))
BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

(𝜆xy.x y ((𝜆[Link]) y))


((𝜆[Link]) ((𝜆[Link]) p q))

((𝜆[Link]) ((𝜆[Link]) p) ((𝜆[Link]) q))
BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

(𝜆xy.x y ((𝜆[Link]) y))


((𝜆[Link]) ((𝜆[Link]) p q))

((𝜆[Link]) ((𝜆[Link]) p) ((𝜆[Link]) q))
BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

(𝜆xy.x y ((𝜆[Link]) y))


((𝜆[Link]) ((𝜆[Link]) p q))

((𝜆[Link]) ((𝜆[Link]) p) ((𝜆[Link]) q))
BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

(𝜆xy.x y ((𝜆[Link]) y))


((𝜆[Link]) ((𝜆[Link]) p q))

((𝜆[Link]) ((𝜆[Link]) p) ((𝜆[Link]) q))
BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

(𝜆xy.x y ((𝜆[Link]) y))


((𝜆[Link]) ((𝜆[Link]) p q))

((𝜆[Link]) ((𝜆[Link]) p) ((𝜆[Link]) q))
 …
ZERO ONE TWO THREE SUCC
 …
ZERO ONCE TWICE THRICE SUCC
 N1 := 𝜆[Link]
λ N2 := 𝜆fa.f(fa)
N3 := 𝜆fa.f(f(fa))

JS n1 = f => a => f(a)

n2 = f => a => f(f(a))
n3 = f => a => f(f(f(a)))
 N1 := 𝜆[Link]
N1 = f => a => f(a)

λ N1 NOT T = NOT T = ?

JS n1(not)(T) = not(T) = ?
 N1 := 𝜆[Link]
N1 = f => a => f(a)

λ N1 NOT T = NOT T = F

JS n1(not)(T) = not(T) = F
 N2 := 𝜆fa.f(fa)
N2 = f => a => f(f(a))

λ N2 NOT T = NOT (NOT T) = ?

JS n2(not)(T) = not(not(T)) = ?
 N2 := 𝜆fa.f(fa)
N2 = f => a => f(f(a))

λ N2 NOT T = NOT (NOT T) = T

JS n2(not)(T) = not(not(T)) = T
 N3 := 𝜆fa.f(f(fa))
N3 = f => a => f(f(f(a)))

λ N3NOT T =
NOT (NOT (NOT T))) = F

JS n3(not)(T) = not(not(not(T))) = F
 N0 := 𝜆fa.a
N1 :=
λ N2 :=
𝜆[Link]
𝜆fa.f(fa)
N3 := 𝜆fa.f(f(fa))
JS n0
n1
=
=
f
f
=>
=>
a
a
=>
=>
a
f(a)
n2 = f => a => f(f(a))
n3 = f => a => f(f(f(a)))
 N0 := 𝜆fa.a
N3 = f => a => a

λ N0 NOT T = ?

JS n0(not)(T) = ?
 N0 := 𝜆fa.a
N3 = f => a => a

λ N0 NOT T = T

JS n0(not)(T) = T
 CHURCH ENCODINGS: NUMERALS
Sym. Name 𝜆-Calculus Use

N0 ZERO 𝜆fa.a = F apply f no times to a

N1 ONCE 𝜆fa.f a = I* apply f once to a

N2 TWICE 𝜆fa.f (f a) apply 2-fold f to a

N3 THRICE 𝜆fa.f (f (f a)) apply 3-fold f to a

N4 FOURFOLD 𝜆fa.f (f (f (f a))) apply 4-fold f to a

N5 FIVEFOLD 𝜆fa.f (f (f (f (f a))))) apply 5-fold f to a

+1?
 PEANO NUMBERS

SUCC N1 = N2
SUCC N2 = N3
SUCC (SUCC N1) = N3
λ SUCC := 𝜆n.?
SUCC N1 = N2

JS succ = n => ?
λ SUCC := 𝜆n.?
SUCC 𝜆[Link] = 𝜆fa.f(fa)

JS succ = n => ?
λ SUCC := 𝜆nfa.f(nfa)
SUCC 𝜆[Link] = 𝜆fa.f(fa)

JS succ = n => f => a => f(n(f)(a))

λ SUCC := 𝜆nfa.f(nfa)
SUCC 𝜆[Link] = 𝜆fa.f(fa)

JS succ = n => f => a => f(n(f)(a))

λ SUCC := 𝜆nfa.f(nfa)
SUCC 𝜆[Link] = 𝜆fa.f(fa)

JS succ = n => f => a => f(n(f)(a))

SUCC N2 = (𝜆nfa.f(nfa)) N2
= 𝜆fa.f(N2 f a)
= 𝜆fa.f(f(f a)
= N3
 CHURCH ARITHMETIC
Name 𝜆-Calculus Use

SUCC 𝜆nfa.f(nfa) successor of n

ADD 𝜆nk.n SUCC k = 𝜆nkf.B (n f) (k f) addition of n and k

MULT 𝜆nkf.n(kf) = B multiplication of n and k

POW 𝜆[Link] = Th raise n to the power of k

PRED 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n

PRED 𝜆[Link] (n Φ (PAIR N0 N0)) predecessor of n (easier)

SUB 𝜆nk.k PRED n subtract k from n

𝜆fga.f(ga)
BLUEBIRD
λ B := 𝜆fga.f(ga)

JS B = f => g => a => f(g(a))

 B := 𝜆fga.f(ga)
B = f => g => a => f(g(a))

λ B NOT NOT T = ?

JS B(not)(not)(T) === ?
 B := 𝜆fga.f(ga)
B = f => g => a => f(g(a))

λ B NOT NOT T = T

JS B(not)(not)(T) === T
odd = not . even
 C O M B I N AT O R S
Sym. Bird 𝜆-Calculus Use Haskell
I Idiot 𝜆a.a identity id

M Mockingbird 𝜆f.ff self-application (cannot define)

K Kestrel 𝜆ab.a true, first, const const

KI Kite 𝜆ab.b = KI = CK false, second const id

C Cardinal 𝜆[Link] reverse arguments flip

B Bluebird 𝜆fga.f(ga) 1°←1° composition (.)

B1 Blackbird 𝜆fgab.f(gab) = BBB 1°-2° composition (.) . (.)

Th Thrush 𝜆[Link] = CI hold an argument flip id

V Vireo 𝜆[Link] = BCT hold a pair of args flip . flip id

λ SUCC := 𝜆nfa.f(nfa)

JS succ = n => f => a => f(n(f)(a))

λ SUCC := 𝜆[Link](nf)

JS succ = n => f => B(f)(n(f))

 CHURCH ARITHMETIC
Name 𝜆-Calculus Use

SUCC 𝜆nf.B f (nf) = 𝜆nfa.f(nfa) successor of n

ADD 𝜆nk.n SUCC k = 𝜆nkf.B (n f) (k f) addition of n and k

MULT 𝜆nkf.n(kf) = B multiplication of n and k

POW 𝜆[Link] = Th raise n to the power of k

PRED 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n

PRED 𝜆[Link] (n Φ (PAIR N0 N0)) predecessor of n (easier)

SUB 𝜆nk.k PRED n subtract k from n

 …
A D D M U LT P O W
λ ADD := 𝜆nk.?
ADD N3 N5 = SUCC (SUCC (SUCC N5))

JS add = n => k => ?

λ ADD := 𝜆nk.?
ADD N3 N5 = (SUCC ∘ SUCC ∘ SUCC) N5

JS add = n => k => ?

λ ADD := 𝜆nk.?
ADD N3 N5 = N3 SUCC N5

JS add = n => k => ?

λ ADD := 𝜆nk.n SUCC k
ADD N3 N5 = N3 SUCC N5

JS add = n => k => n(succ)(k)

ADD N3 N5 = N3 SUCC N5
= THRICE SUCC FIVEFOLD
= SUCC (SUCC (SUCC FIVEFOLD)))
= EIGHTFOLD
 CHURCH ARITHMETIC
Name 𝜆-Calculus Use

SUCC 𝜆nf.B f (nf) = 𝜆nfa.f(nfa) successor of n

ADD 𝜆nk.n SUCC k = 𝜆nkf.B (n f) (k f) addition of n and k

MULT 𝜆nkf.n(kf) = B multiplication of n and k

POW 𝜆[Link] = Th raise n to the power of k

PRED 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n

PRED 𝜆[Link] (n Φ (PAIR N0 N0)) predecessor of n (easier)

SUB 𝜆nk.k PRED n subtract k from n

λ MULT := 𝜆nk.?
MULT N2 N3 = N6

JS mult = n => k => ?

λ MULT := 𝜆nk.?
MULT N2 N3 f a = N6 f a

JS mult = n => k => ?

λ MULT := 𝜆nk.?
MULT N2 N3 f a = (f ∘ f ∘ f ∘ f ∘ f ∘ f) a

JS mult = n => k => ?

λ MULT := 𝜆nk.?
MULT N2 N3 f a = ((f ∘ f ∘ f) ∘ (f ∘ f ∘ f)) a

JS mult = n => k => ?

λ MULT := 𝜆nk.?
MULT N2 N3 f a = ((N3 f) ∘ (N3 f)) a

JS mult = n => k => ?

λ MULT := 𝜆nk.?
MULT N2 N3 f a = N2 (N3 f) a

JS mult = n => k => ?

λ MULT := 𝜆nk.?
MULT N2 N3 f a = N2 (N3 f) a

JS mult = n => k => ?

λ MULT := 𝜆nk.?
MULT N2 N3 f = N2 (N3 f)

JS mult = n => k => ?

λ MULT := 𝜆nkf.n(kf)
MULT N2 N3 f = N2 (N3 f)

JS mult = n => k => n(k(f))

MULT N2 N3 f = N2 (N3 f)
= TWICE (THRICE f)
= (f ∘ f ∘ f) ∘ (f ∘ f ∘ f)
= SIXFOLD f
 CHURCH ARITHMETIC
Name 𝜆-Calculus Use

SUCC 𝜆nf.B f (nf) = 𝜆nfa.f(nfa) successor of n

ADD 𝜆nk.n SUCC k = 𝜆nkf.B (n f) (k f) addition of n and k

MULT 𝜆nkf.n(kf) multiplication of n and k

POW 𝜆[Link] = Th raise n to the power of k

PRED 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n

PRED 𝜆[Link] (n Φ (PAIR N0 N0)) predecessor of n (easier)

SUB 𝜆nk.k PRED n subtract k from n

λ MULT := 𝜆nkf.n(kf)
MULT N2 N3 f = N2 (N3 f)

JS mult = n => k => n(k(f))

λ MULT := 𝜆nkf.n(kf)
MULT N2 N3 f = (N2 ∘ N3) f

JS mult = n => k => n(k(f))

λ MULT := 𝜆nkf.n(kf)
MULT N2 N3 f = (N2 ∘ N3) f

JS mult = n => k => n(k(f))

λ MULT := 𝜆nkf.n(kf)
MULT N2 N3 = N2 ∘ N3

JS mult = n => k => n(k(f))

λ MULT := 𝜆nkf.n(kf)
MULT N2 N3 = B N2 N3

JS mult = n => k => n(k(f))

λ MULT := 𝜆nkf.n(kf)
MULT N2 N3 = B N2 N3

JS mult = n => k => n(k(f))

λ MULT := 𝜆nkf.n(kf)
MULT = B

JS mult = n => k => n(k(f))

MULT := B
 𝛼 - E Q U I VA L E N C E

Mult := 𝜆 n k f . n (k f)
= B = 𝜆 f g a . f (g a)
 CHURCH ARITHMETIC
Name 𝜆-Calculus Use

SUCC 𝜆nf.B f (nf) = 𝜆nfa.f(nfa) successor of n

ADD 𝜆nk.n SUCC k = 𝜆nkf.B (n f) (k f) addition of n and k

MULT 𝜆nkf.n(kf) = B multiplication of n and k

POW 𝜆[Link] = Th raise n to the power of k

PRED 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n

PRED 𝜆[Link] (n Φ (PAIR N0 N0)) predecessor of n (easier)

SUB 𝜆nk.k PRED n subtract k from n

λ POW := 𝜆nk.?
POW N2 N3 = N8

JS pow = n => k => ?

λ POW := 𝜆nk.?
POW N2 N3 = N2 × N2 × N2

JS pow = n => k => ?

λ POW := 𝜆nk.?
POW N2 N3 = N2 ∘ N2 ∘ N2

JS pow = n => k => ?

λ POW := 𝜆nk.?
POW N2 N3 = N3 N2

JS pow = n => k => ?

λ POW := 𝜆[Link]
POW N2 N3 = N3 N2

JS pow = n => k => k(n)

POW N2 N3 = N3 N2
= THRICE TWICE
= TWICE ∘ TWICE ∘ TWICE
= EIGHTFOLD
 CHURCH ARITHMETIC
Name 𝜆-Calculus Use

SUCC 𝜆nf.B f (nf) = 𝜆nfa.f(nfa) successor of n

ADD 𝜆nk.n SUCC k = 𝜆nkf.B (n f) (k f) addition of n and k

MULT 𝜆nkf.n(kf) = B multiplication of n and k

POW 𝜆[Link] raise n to the power of k

PRED 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n

PRED 𝜆[Link] (n Φ (PAIR N0 N0)) predecessor of n (easier)

SUB 𝜆nk.k PRED n subtract k from n

𝜆[Link]
THRUSH
 C O M B I N AT O R S
Sym. Bird 𝜆-Calculus Use Haskell
I Idiot 𝜆a.a identity id

M Mockingbird 𝜆f.ff self-application (cannot define)

K Kestrel 𝜆ab.a true, first, const const

KI Kite 𝜆ab.b = KI = CK false, second const id

C Cardinal 𝜆[Link] reverse arguments flip

B Bluebird 𝜆fga.f(ga) 1°←1° composition (.)

Th Thrush 𝜆[Link] hold an argument

V Vireo 𝜆[Link] = BCT hold a pair of args flip . flip id

B1 Blackbird 𝜆fgab.f(gab) = BBB 1°←2° composition (.) . (.)

 C O M B I N AT O R S
Sym. Bird 𝜆-Calculus Use Haskell
I Idiot 𝜆a.a identity id

M Mockingbird 𝜆f.ff self-application (cannot define)

K Kestrel 𝜆ab.a true, first, const const

KI Kite 𝜆ab.b = KI = CK false, second const id

C Cardinal 𝜆[Link] reverse arguments flip

B Bluebird 𝜆fga.f(ga) 1°←1° composition (.)

Th Thrush 𝜆[Link] = CI hold an argument flip id

V Vireo 𝜆[Link] = BCT hold a pair of args flip . flip id

B1 Blackbird 𝜆fgab.f(gab) = BBB 1°←2° composition (.) . (.)

 CHURCH ARITHMETIC
Name 𝜆-Calculus Use

SUCC 𝜆nf.B f (nf) = 𝜆nfa.f(nfa) successor of n

ADD 𝜆nk.n SUCC k = 𝜆nkf.B (n f) (k f) addition of n and k

MULT 𝜆nkf.n(kf) = B multiplication of n and k

POW 𝜆[Link] raise n to the power of k

PRED 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n

PRED 𝜆[Link] (n Φ (PAIR N0 N0)) predecessor of n (easier)

SUB 𝜆nk.k PRED n subtract k from n

 CHURCH ARITHMETIC
Name 𝜆-Calculus Use

SUCC 𝜆nf.B f (nf) = 𝜆nfa.f(nfa) successor of n

ADD 𝜆nk.n SUCC k = 𝜆nkf.B (n f) (k f) addition of n and k

MULT 𝜆nkf.n(kf) = B multiplication of n and k

POW 𝜆[Link] = Th raise n to the power of k

PRED 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n

PRED 𝜆[Link] (n Φ (PAIR N0 N0)) predecessor of n (easier)

SUB 𝜆nk.k PRED n subtract k from n

…
ISZERO
IS0 N0 = T
IS0 N1 = F
IS0 N2 = F
…
λ IS0 := 𝜆n.?

JS is0 = n => ?
λ IS0 := 𝜆n.n func arg

JS is0 = n => n(func)(arg)

 N0
λ IS0 := 𝜆n.n func arg

JS is0 = n => n(func)(arg)

 N0
λ IS0 := 𝜆n.n func T

JS is0 = n => n(func)(T)

 N1
λ IS0 := 𝜆n.n func T F

JS is0 = n => n(func)(T)

 N2
λ IS0 := 𝜆n.n func T F

JS is0 = n => n(func)(T)

 N>0
λ IS0 := 𝜆n.n func T F

JS is0 = n => n(func)(T)

λ IS0 := 𝜆n.n (KF) T

JS is0 = n => n(K(F))(T)

λ IS0 := 𝜆n.n (KF) T
IS0 N3 = KF(KF(KF(T))) = F

JS is0 = n => n(K(F))(T)

λ IS0 := 𝜆n.n (KF) T
IS0 N3 = KF(KF(KF(T))) = F

JS is0 = n => n(K(F))(T)

λ IS0 := 𝜆n.n (KF) T
IS0 N3 = KF(KF(KF(T))) = F

JS is0 = n => n(K(F))(T)

CHURCH ARITHMETIC: BOOLEAN OPS
Name 𝜆-Calculus Use

IS0 𝜆n.n (K F) T test if n = 0

LEQ 𝜆nk.IS0 (SUB n k) test if n !<= k

EQ 𝜆[Link] (LEQ n k) (LEQ k n) test if n = k

GT 𝜆nk.B1 NOT LEQ test if n > k

+×^
–1?
PRED := 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0
PRED := 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0

I
N0: N0 (𝜆g.IS0 (g N1) ) (K N0) N0 N0
(B SUCC g)
(K N0)
I
N1: N1 (𝜆g.IS0 (g N1) ) (K N0) N0 N0
(B SUCC g)
I I
N2: N2 (𝜆g.IS0 (g N1) ) (K N0) N0 N1
(B SUCC g)
(SUCC ∘ I)
I
N3: N3 (𝜆g.IS0 (g N1) ) (K N0) N0 N2
(B SUCC g)
 …
PA I R F S T S N D P H I
𝜆[Link]
VIREO
λ V := 𝜆[Link]

JS V = a => b => f => f(a)(b)

 V := 𝜆[Link]
V = a => b => f => f(a)(b)

λ VIM
= (𝜆f.f I M)

JS V(I)(M)
// f => f(I)(M)
 V := 𝜆[Link]
V = a => b => f => f(a)(b)

λ VIMK
= (𝜆f.f I M) K = ?

JS V(I)(M)(K)
// (f => f(I)(M))(K) === ?
 V := 𝜆[Link]
V = a => b => f => f(a)(b)

λ VIMK
= (𝜆f.f I M) K = I

JS V(I)(M)(K)
// (f => f(I)(M))(K) === I
 V := 𝜆[Link]
V = a => b => f => f(a)(b)

λ V I M KI
= (𝜆f.f I M) KI = M

JS V(I)(M)(KI)
// (f => f(I)(M))(KI) === M
 C O M B I N AT O R S
Sym. Bird 𝜆-Calculus Use Haskell
I Idiot 𝜆a.a identity id

M Mockingbird 𝜆f.ff self-application (cannot define)

K Kestrel 𝜆ab.a true, first, const const

KI Kite 𝜆ab.b = KI = CK false, second const id

C Cardinal 𝜆[Link] reverse arguments flip

B Bluebird 𝜆fga.f(ga) 1°←1° composition (.)

Th Thrush 𝜆[Link] = CI hold an argument flip id

V Vireo 𝜆[Link] = BCT hold a pair of args flip . flip id

B1 Blackbird 𝜆fgab.f(gab) = BBB 1°←2° composition (.) . (.)

 C H U R C H PA I R S
Sym. Name 𝜆-Calculus Use

PAIR 𝜆[Link] = V pair two arguments

FST 𝜆[Link] extract first of pair

SND 𝜆p.p(KI) extract second of pair

Φ PHI 𝜆[Link] (SND p) (SUCC (SND p) copy 2nd to 1st, inc 2nd

SET1ST 𝜆[Link] c (SND p) set first, immutably

SET2ND 𝜆[Link] (FST p) c set second, immutably

FST := 𝜆[Link]
SND := 𝜆p.p(KI)
 C H U R C H PA I R S
Sym. Name 𝜆-Calculus Use

PAIR 𝜆[Link] = V pair two arguments

FST 𝜆[Link] extract first of pair

SND 𝜆p.p(KI) extract second of pair

Φ PHI 𝜆[Link] (SND p) (SUCC (SND p) copy 2nd to 1st, inc 2nd

SET1ST 𝜆[Link] c (SND p) set first, immutably

SET2ND 𝜆[Link] (FST p) c set second, immutably

λ PHI := 𝜆p.V (SND p) (SUCC (SND p))

JS phi = p => pair (snd(p)) (succ(snd(p)))

Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = ?
Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = ( , )
Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = (N7, )

Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = (N7, N8)

Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = (N7, N8)

Φ (N9, N2) = (N2, N3)
 C H U R C H PA I R S
Sym. Name 𝜆-Calculus Use

PAIR 𝜆[Link] = V pair two arguments

FST 𝜆[Link] extract first of pair

SND 𝜆p.p(KI) extract second of pair

Φ PHI 𝜆[Link] (SND p) (SUCC (SND p) copy 2nd to 1st, inc 2nd

SET1ST 𝜆[Link] c (SND p) set first, immutably

SET2ND 𝜆[Link] (FST p) c set second, immutably

Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = (N7, N8)

Φ (N9, N2) = (N2, N3)
Φ (N0, N0) = (N0, N1)
Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = (N7, N8)

Φ (N9, N2) = (N2, N3)
Φ (N0, N0) = (N0, N1)
Φ (N0, N1) = (N1, N2)
Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = (N7, N8)

Φ (N9, N2) = (N2, N3)
Φ (N0, N0) = (N0, N1)
Φ (N0, N1) = (N1, N2)
Φ (N1, N2) = (N2, N3)
Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = (N7, N8)

Φ (N9, N2) = (N2, N3)
Φ (N0, N0) = (N0, N1)
Φ (N0, N1) = (N1, N2)
Φ (N1, N2) = (N2, N3)
N8 Φ (N0, N0) = ?
Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = (N7, N8)

Φ (N9, N2) = (N2, N3)
Φ (N0, N0) = (N0, N1)
Φ (N0, N1) = (N1, N2)
Φ (N1, N2) = (N2, N3)
N8 Φ (N0, N0) = (N7, N8)
 Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = (N7, N8)

Φ (N9, N2) = (N2, N3)
Φ (N0, N0) = (N0, N1)
Φ (N0, N1) = (N1, N2)
Φ (N1, N2) = (N2, N3)
FST ( N8 Φ (N0, N0))= FST (N7, N8) = N7
 Φ := 𝜆[Link] (SND p) (SUCC (SND p))

Φ (M, N7) = (N7, N8)

Φ (N9, N2) = (N2, N3)
Φ (N0, N0) = (N0, N1)
Φ (N0, N1) = (N1, N2)
Φ (N1, N2) = (N2, N3)
FST ( N8 Φ (N0, N0))= FST (N7, N8) = N7
λ PRED := 𝜆[Link] (n Φ (PAIR N0 N0))

JS pred = n => fst(n(phi)(pair(n0)(n0)))

 CHURCH ARITHMETIC
Name 𝜆-Calculus Use

SUCC 𝜆nf.B f (nf) = 𝜆nfa.f(nfa) successor of n

ADD 𝜆nk.n SUCC k = 𝜆nkf.B (n f) (k f) addition of n and k

MULT 𝜆nkf.n(kf) = B multiplication of n and k

POW 𝜆[Link] = Th raise n to the power of k

PRED 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n

PRED 𝜆[Link] (n Φ (PAIR N0 N0)) predecessor of n (easier)

SUB 𝜆nk.k PRED n subtract k from n

 …
SUB LEQ EQ GT
λ SUB := 𝜆nk.k PRED n

JS sub = n => k => k(pred)(n)

 CHURCH ARITHMETIC
Name 𝜆-Calculus Use

SUCC 𝜆nf.B f (nf) = 𝜆nfa.f(nfa) successor of n

ADD 𝜆nk.n SUCC k = 𝜆nkf.B (n f) (k f) addition of n and k

MULT 𝜆nkf.n(kf) = B multiplication of n and k

POW 𝜆[Link] = Th raise n to the power of k

PRED 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n

PRED 𝜆[Link] (n Φ (PAIR N0 N0)) predecessor of n (easier)

SUB 𝜆nk.k PRED n subtract k from n

λ LEQ := 𝜆nk.IS0 (SUB n k)

JS leq = n => k => is0(sub(n)(k))

λ EQ := 𝜆[Link](LEQ n k)(LEQ k n)

JS eq = n => k => and(leq(n)(k))(leq(k)(n))

CHURCH ARITHMETIC: BOOLEAN OPS
Name 𝜆-Calculus Use

IS0 𝜆n.n (K F) T test if n = 0

LEQ 𝜆nk.IS0 (SUB n k) test if n !<= k

EQ 𝜆[Link] (LEQ n k) (LEQ k n) test if n = k

GT 𝜆nk.B1 NOT LEQ test if n > k

λ GT := 𝜆[Link] (LEQ n k)

JS eq = n => k => not(leq(n)(k))

λ GT := 𝜆[Link] (LEQ n k)

JS eq = n => k => not(leq(n)(k))

λ GT := B NOT LEQ ???

JS eq = B(not)(leq) ???
λ GT := B NOT LEQ

JS eq = B(not)(leq)
λ GT := 𝜆[Link] (LEQ n k)

JS eq = n => k => not(leq(n)(k))

𝜆fgab.f(gab)
BLACKBIRD
 B1 = 𝜆fgab.f(gab)

λ GT := B1 NOT LEQ

JS eq = B1(not)(leq)
CHURCH ARITHMETIC: BOOLEAN OPS
Name 𝜆-Calculus Use

IS0 𝜆n.n (K F) T test if n = 0

LEQ 𝜆nk.IS0 (SUB n k) test if n !<= k

EQ 𝜆[Link] (LEQ n k) (LEQ k n) test if n = k

GT 𝜆nk.B1 NOT LEQ test if n > k

 C O M B I N AT O R S
Sym. Bird 𝜆-Calculus Use Haskell
I Idiot 𝜆a.a identity id

M Mockingbird 𝜆f.ff self-application (cannot define)

K Kestrel 𝜆ab.a true, first, const const

KI Kite 𝜆ab.b = KI = CK false, second const id

C Cardinal 𝜆[Link] reverse arguments flip

B Bluebird 𝜆fga.f(ga) 1°←1° composition (.)

Th Thrush 𝜆[Link] = CI hold an argument flip id

V Vireo 𝜆[Link] = BCT hold a pair of args flip . flip id

B1 Blackbird 𝜆fgab.f(gab) 1°←2° composition

 C O M B I N AT O R S
Sym. Bird 𝜆-Calculus Use Haskell
I Idiot 𝜆a.a identity id

M Mockingbird 𝜆f.ff self-application (cannot define)

K Kestrel 𝜆ab.a true, first, const const

KI Kite 𝜆ab.b = KI = CK false, second const id

C Cardinal 𝜆[Link] reverse arguments flip

B Bluebird 𝜆fga.f(ga) 1°←1° composition (.)

Th Thrush 𝜆[Link] = CI hold an argument flip id

V Vireo 𝜆[Link] = BCT hold a pair of args flip . flip id

B1 Blackbird 𝜆fgab.f(gab) = BBB 1°←2° composition (.) . (.)

 B C K I

KI = KI=CK
B1 = BBB
Th = CI
V= B C Th = B C (C I)
 QUESTION
how many combinators

are needed to form a basis?
20? 10? 5?
S TA R L I N G · K E S T R E L

S := 𝜆[Link](bc)
K := 𝜆ab.a
 THE

SK
C O M B I N AT O R
CALCULUS
I =SKK
 I =SKK
V = (S(K((S((S(K((

S(KS))K)))S))(KK))))
((S(K(S((SK)K))))K)
seriously though,
why?
🎮
🤔
🎨
 …
ADDENDUM
 C O M B I N AT O R S
Sym. Bird 𝜆-Calculus Use Haskell
I Idiot 𝜆a.a identity id

M Mockingbird 𝜆f.ff self-application (cannot define)

K Kestrel 𝜆ab.a true, first, const const

KI Kite 𝜆ab.b = KI = CK false, second const id

C Cardinal 𝜆[Link] reverse arguments flip

B Bluebird 𝜆fga.f(ga) 1°←1° composition (.)

Th Thrush 𝜆[Link] = CI hold an argument flip id

V Vireo 𝜆[Link] = BCT hold a pair of args flip . flip id

B1 Blackbird 𝜆fgab.f(gab) = BBB 1°←2° composition (.) . (.)

 CHURCH ENCODINGS: BOOLEANS
Sym. Name 𝜆-Calculus Use

T TRUE 𝜆ab.a = K = C(KI) encoding for true

F FALSE 𝜆ab.b = KI = CK encoding for false

NOT 𝜆[Link] or C negation

AND 𝜆[Link] or 𝜆[Link] conjunction

OR 𝜆[Link] or 𝜆[Link] = M* disjunction

BEQ 𝜆pq.p q (NOT q) equality

 CHURCH ENCODINGS: NUMERALS
Sym. Name 𝜆-Calculus Use

N0 ZERO 𝜆fa.a = F apply f no times to a

N1 ONCE 𝜆fa.f a = I* apply f once to a

N2 TWICE 𝜆fa.f (f a) apply 2-fold f to a

N3 THRICE 𝜆fa.f (f (f a)) apply 3-fold f to a

N4 FOURFOLD 𝜆fa.f (f (f (f a))) apply 4-fold f to a

N5 FIVEFOLD 𝜆fa.f (f (f (f (f a))))) apply 5-fold f to a

 CHURCH ARITHMETIC
Name 𝜆-Calculus Use

SUCC 𝜆nf.B f (nf) = 𝜆nfa.f(nfa) successor of n

ADD 𝜆nk.n SUCC k = 𝜆nkf.B (n f) (k f) addition of n and k

MULT 𝜆nkf.n(kf) = B multiplication of n and k

POW 𝜆[Link] = Th raise n to the power of k

PRED 𝜆n.n (𝜆g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n

PRED 𝜆[Link] (n Φ (PAIR N0 N0)) predecessor of n (easier)

SUB 𝜆nk.k PRED n subtract k from n

CHURCH ARITHMETIC: BOOLEAN OPS
Name 𝜆-Calculus Use

IS0 𝜆n.n (K F) T test if n = 0

LEQ 𝜆nk.IS0 (SUB n k) test if n !<= k

EQ 𝜆[Link] (LEQ n k) (LEQ k n) test if n = k

GT 𝜆nk.B1 NOT LEQ test if n > k

 C H U R C H PA I R S
Sym. Name 𝜆-Calculus Use

PAIR 𝜆[Link] = V pair two arguments

FST 𝜆[Link] extract first of pair

SND 𝜆p.p(KI) extract second of pair

Φ PHI 𝜆[Link] (SND p) (SUCC (SND p) copy 2nd to 1st, inc 2nd

SET1ST 𝜆[Link] c (SND p) set first, immutably

SET2ND 𝜆[Link] (FST p) c set second, immutably

 𝜆f.M(𝜆x.f(Mx))
T H E Y F I X E D - P O I N T C O M B I N AT O R
 E VA L U AT I O N S T R AT E G I E S

CALL BY NAME C A L L B Y VA L U E
(apply to args before reduction) (reduce args before application)

(𝜆ab.b)((𝜆[Link])𝜆[Link]) x (𝜆ab.b)((𝜆[Link])𝜆[Link])x
= (𝜆b.b) x = (𝜆ab.b)((𝜆[Link])𝜆[Link])x
= x = (𝜆ab.b)((𝜆[Link])𝜆[Link])x
= (𝜆ab.b)((𝜆[Link])𝜆[Link])x
= (𝜆ab.b)((𝜆[Link])𝜆[Link])x

(AKA normal order; lazy) (AKA applicative order; strict)

 𝜆f.M(𝜆x.f(𝜆[Link]))
T H E Z F I X E D - P O I N T C O M B I N AT O R
 ADDITIONAL RESOURCES
Combinator Birds · Rathman · [Link]
To Mock a Mockingbird · Smullyan · [Link]
To Dissect a Mockingbird · Keenan · [Link]
.:.

A Tutorial Introduction to the Lambda Calculus · Rojas · [Link]
Lambda Calculus · Wikipedia · [Link]
The Lambda Calculus · Stanford · [Link]
.:.

History of Lambda-calculus and Combinatory Logic
Cardone, Hindley · [Link]
.:.

An Introduction to Functional Programming

through Lambda Calculus · Michaelson · [Link]