SK numerals

Church Numerals

C0 f x = f⁰ x = x
C1 f x = f¹ x = f x
C2 f x = f² x = f (f x)
Csucc = λn.λf.λx. f (n f x)
Cn = Cn Csucc C0
add = λm.λn.λf.λx. m f (n f x)
mul = λm.λn.λf. m (n f)
pow = λm.λn. n m
Cpred = λn.λf.λx. n(λg.λh. h(g f))(λu. x)(λu. u)
div = λn.λm.λf.λx.n(λx.λf.f x)(λd.x)(n (λt.m(λx.λf.f x)(λc.f(c t))(λx.x))x)

SK Combinatory Logic

S = λx.λy.λz. x z (y z)
K = λx.λy. x
I = S K K
F0 = K
F1 = S K
F2 = S (S K)
F3 = S ( S (S K)))
F0 = K
Fsucc = S
F0 x y = x
F(n+1) x y = S Fn x y = Fn y (x y)
F1 x y = y
F2 x y = x y
F3 x y = y (x y)
F4 x y = x y (y (x y))
F(n+2) x y = (Fn x y) (F(n+1) x y)
True = K
False = S K
Fpred = λn.λx.λy. n (K y) x
Fiszero = λn. n False I S K
F2C = λn. Fiszero n C0 (Csucc (F2C (pred n)))
Fpred F1 x y = F1 (K y) x = x
Fpred F2 x y = F2 (K y) x = K y x = y
F-1 x y = Fpred F0 x y = F0 (K y) x = K y
F-2 x y = Fpred F-1 x y = F-1 (K y) x = K x
F-3 x y = Fpred F-2 x y = F-2 (K y) x = K (K y)
Fiszero F0 = F0 False I S K = False S K = K = True
Fiszero F(n+1) False I S K = S Fn False I S K = Fn I I S K = I S K = S K = False
pair = λx.λy. λp. p x y
F2C = λn.(λp. n p(p p) False) (pair (λf.λy.λx. pair f (Csucc y)) C0)
S (S (K (S S (K (K (S K))))) (S S (S K))) (K (S (S (S K K) (K (S (K (S (K (S (K (S (K (S (K (S (K (S S (K (S (K (S (K (S (K K))) S)) (S (K (S (K S) K))))))) K)) S)) K)) S)) (S (S K K)))) K))) (S K)))
(pair f Cm) (pair f Cn) = (pair f Cn) f Cm = f f Cn Cm

--

--

Dutch computer scientist, game player, puzzle lover, and recumbent biker.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
John Tromp

Dutch computer scientist, game player, puzzle lover, and recumbent biker.