Beta-Reducer for Lambda Calculus.
Copyright (c) 2022 Chuck Liang. Free to use under MIT license.
2

(λxλy.y x) u (λx.x)
 =>  (λy.y u) (λx.x)
 =>  (λx.x) u
 =>  u

3

K I I
= (λxλy.x) I I
 =>  (λy.I) I
= (λyλx.x) I
 =>  λx.x

S I K
= (λxλyλz.x z (y z)) I K
 =>  (λyλz.I z (y z)) K
= (λyλz.(λx.x) z (y z)) K
 =>  λz.(λx.x) z (K z)
= λz.(λx.x) z ((λxλy.x) z)
 =>  λz.z ((λxλy.x) z)
 =>  λz.z (λy.z)

S K (K I)
= (λxλyλz.x z (y z)) K (K I)
 =>  (λyλz.K z (y z)) (K I)
= (λyλz.(λxλy.x) z (y z)) (K I)
 =>  λz.(λxλy.x) z (K I z)
= λz.(λxλy.x) z ((λxλy.x) I z)
 =>  λz.(λy.z) ((λxλy.x) I z)
= λz.(λy.z) ((λxλy.x) (λx.x) z)
 =>  λz.z

S (K I)
= (λxλyλz.x z (y z)) (K I)
 =>  λyλz.K I z (y z)
= λyλz.(λxλy.x) I z (y z)
 =>  λyλz.(λy.I) z (y z)
= λyλz.(λyλx.x) z (y z)
 =>  λyλz.(λx.x) (y z)
 =>  λyλz.y z

weak S (K I)
= (λxλyλz.x z (y z)) (K I)
= (λxλyλz.x z (y z)) ((λxλy.x) I)
= (λxλyλz.x z (y z)) ((λxλy.x) (λx.x))
 =>  (λxλyλz.x z (y z)) (λyλx.x)
 =>  λyλz.(λyλx.x) z (y z)

4

PLUS
= λmλnλfλx.m f (n f x)

TIMES
= λmλnλfλx.m (n f) x

PLUS TWO ONE
= (λmλnλfλx.m f (n f x)) TWO ONE
 =>  (λnλfλx.TWO f (n f x)) ONE
= (λnλfλx.(λfλx.f (f x)) f (n f x)) ONE
 =>  λfλx.(λfλx.f (f x)) f (ONE f x)
= λfλx.(λfλx.f (f x)) f ((λfλx.f x) f x)
 =>  λfλx.(λx.f (f x)) ((λfλx.f x) f x)
 =>  λfλx.f (f ((λfλx.f x) f x))
 =>  λfλx.f (f ((λx.f x) x))
 =>  λfλx.f (f (f x))

TIMES TWO ZERO
= (λmλnλfλx.m (n f) x) TWO ZERO
 =>  (λnλfλx.TWO (n f) x) ZERO
= (λnλfλx.(λfλx.f (f x)) (n f) x) ZERO
 =>  λfλx.(λfλx.f (f x)) (ZERO f) x
= λfλx.(λfλx.f (f x)) ((λfλx.x) f) x
 =>  λfλx.(λx.(λfλx.x) f ((λfλx.x) f x)) x
 < alpha conversion of x to x1 >
 < alpha conversion of x to x2 >
 =>  λfλx.(λfλx1.x1) f ((λfλx2.x2) f x)
 =>  λfλx.(λx1.x1) ((λfλx2.x2) f x)
 =>  λfλx.(λfλx2.x2) f x
 =>  λfλx.(λx2.x2) x
 =>  λfλx.x

4 b

EXPT
= λmλn.n m

EXPT THREE TWO
= (λmλn.n m) THREE TWO
 =>  (λn.n THREE) TWO
= (λn.n (λfλx.f (f (f x)))) TWO
 =>  TWO (λfλx.f (f (f x)))
= (λfλx.f (f x)) (λfλx.f (f (f x)))
 =>  λx.(λfλx.f (f (f x))) ((λfλx.f (f (f x))) x)
 < alpha conversion of x to x1 >
 =>  λxλx1.(λfλx.f (f (f x))) x ((λfλx.f (f (f x))) x ((λfλx.f (f (f x))) x x1))
 < alpha conversion of x to x2 >
 =>  λxλx1.(λx2.x (x (x x2))) ((λfλx.f (f (f x))) x ((λfλx.f (f (f x))) x x1))
 =>  λxλx1.x (x (x ((λfλx.f (f (f x))) x ((λfλx.f (f (f x))) x x1))))
 < alpha conversion of x to x3 >
 =>  λxλx1.x (x (x ((λx3.x (x (x x3))) ((λfλx.f (f (f x))) x x1))))
 =>  λxλx1.x (x (x (x (x (x ((λfλx.f (f (f x))) x x1))))))
 < alpha conversion of x to x4 >
 =>  λxλx1.x (x (x (x (x (x ((λx4.x (x (x x4))) x1))))))
 =>  λxλx1.x (x (x (x (x (x (x (x (x x1))))))))

5

OR
= λpλq.p TRUE q

OR FALSE FALSE
= (λpλq.p TRUE q) FALSE FALSE
 =>  (λq.FALSE TRUE q) FALSE
= (λq.(λxλy.y) TRUE q) FALSE
 =>  (λxλy.y) TRUE FALSE
= (λxλy.y) (λxλy.x) FALSE
 =>  (λy.y) FALSE
= (λy.y) (λxλy.y)
 =>  λxλy.y

OR FALSE TRUE
= (λpλq.p TRUE q) FALSE TRUE
 =>  (λq.FALSE TRUE q) TRUE
= (λq.(λxλy.y) TRUE q) TRUE
 =>  (λxλy.y) TRUE TRUE
= (λxλy.y) (λxλy.x) TRUE
 =>  (λy.y) TRUE
= (λy.y) (λxλy.x)
 =>  λxλy.x

OR TRUE FALSE
= (λpλq.p TRUE q) TRUE FALSE
 =>  (λq.TRUE TRUE q) FALSE
= (λq.(λxλy.x) TRUE q) FALSE
 =>  (λxλy.x) TRUE FALSE
= (λxλy.x) (λxλy.x) FALSE
 =>  (λyλxλy.x) FALSE
= (λyλxλy.x) (λxλy.y)
 =>  λxλy.x

OR TRUE TRUE
= (λpλq.p TRUE q) TRUE TRUE
 =>  (λq.TRUE TRUE q) TRUE
= (λq.(λxλy.x) TRUE q) TRUE
 =>  (λxλy.x) TRUE TRUE
= (λxλy.x) (λxλy.x) TRUE
 =>  (λyλxλy.x) TRUE
= (λyλxλy.x) (λxλy.x)
 =>  λxλy.x

6

NOT
= λp.p FALSE TRUE

NOT FALSE
= (λp.p FALSE TRUE) FALSE
 =>  FALSE FALSE TRUE
= (λxλy.y) FALSE TRUE
 =>  (λy.y) TRUE
= (λy.y) (λxλy.x)
 =>  λxλy.x

NOT TRUE
= (λp.p FALSE TRUE) TRUE
 =>  TRUE FALSE TRUE
= (λxλy.x) FALSE TRUE
 =>  (λy.FALSE) TRUE
= (λyλxλy.y) TRUE
 =>  λxλy.y

NOT (NOT TRUE)
= (λp.p FALSE TRUE) (NOT TRUE)
 =>  NOT TRUE FALSE TRUE
= (λp.p FALSE TRUE) TRUE FALSE TRUE
 =>  TRUE FALSE TRUE FALSE TRUE
= (λxλy.x) FALSE TRUE FALSE TRUE
 =>  (λy.FALSE) TRUE FALSE TRUE
= (λyλxλy.y) TRUE FALSE TRUE
 =>  (λxλy.y) FALSE TRUE
= (λxλy.y) (λxλy.y) TRUE
 =>  (λy.y) TRUE
= (λy.y) (λxλy.x)
 =>  λxλy.x

7

IF TRUE A B
= (λcλaλb.c a b) TRUE A B
 =>  (λaλb.TRUE a b) A B
= (λaλb.(λxλy.x) a b) A B
 =>  (λb.(λxλy.x) A b) B
 =>  (λxλy.x) A B
 =>  (λy.A) B
 =>  A

IF FALSE A B
= (λcλaλb.c a b) FALSE A B
 =>  (λaλb.FALSE a b) A B
= (λaλb.(λxλy.y) a b) A B
 =>  (λb.(λxλy.y) A b) B
 =>  (λxλy.y) A B
 =>  (λy.y) B
 =>  B

8

PAIR
= λaλbλc.c a b

FST
= λp.p TRUE

SND
= λp.p FALSE

M
= λc1.c1 a (λc3.c3 b c)

FST M
= (λp.p TRUE) M
 =>  M TRUE
= (λc1.c1 a (λc3.c3 b c)) TRUE
 =>  TRUE a (λc3.c3 b c)
= (λxλy.x) a (λc3.c3 b c)
 =>  (λy.a) (λc3.c3 b c)
 =>  a

SND M
= (λp.p FALSE) M
 =>  M FALSE
= (λc1.c1 a (λc3.c3 b c)) FALSE
 =>  FALSE a (λc3.c3 b c)
= (λxλy.y) a (λc3.c3 b c)
 =>  (λy.y) (λc3.c3 b c)
 =>  λc3.c3 b c

SND (SND M)
= (λp.p FALSE) (SND M)
 =>  SND M FALSE
= (λp.p FALSE) M FALSE
 =>  M FALSE FALSE
= (λc1.c1 a (λc3.c3 b c)) FALSE FALSE
 =>  FALSE a (λc3.c3 b c) FALSE
= (λxλy.y) a (λc3.c3 b c) FALSE
 =>  (λy.y) (λc3.c3 b c) FALSE
= (λy.y) (λc3.c3 b c) (λxλy.y)
 =>  (λc3.c3 b c) (λxλy.y)
 =>  (λxλy.y) b c
 =>  (λy.y) c
 =>  c

9

ISZERO
= λn.n (λz.FALSE) TRUE

ISZERO ZERO
= (λn.n (λz.FALSE) TRUE) ZERO
 =>  ZERO (λz.FALSE) TRUE
= (λfλx.x) (λz.FALSE) TRUE
 =>  (λx.x) TRUE
= (λx.x) (λxλy.x)
 =>  λxλy.x

ISZERO TWO
= (λn.n (λz.FALSE) TRUE) TWO
 =>  TWO (λz.FALSE) TRUE
= (λfλx.f (f x)) (λz.FALSE) TRUE
 =>  (λx.(λz.FALSE) ((λz.FALSE) x)) TRUE
= (λx.(λzλxλy.y) ((λz.FALSE) x)) TRUE
 =>  (λzλxλy.y) ((λz.FALSE) TRUE)
= (λzλxλy.y) ((λzλxλy.y) TRUE)
 =>  λxλy.y

10

still working on it