SK numerals

Church Numerals

Church numerals are the standard way of representing natural numbers in the lambda calculus. Cn, the Church numeral for n, iterates a given function n times on a given argument. So we have

C0 f x = f⁰ x = x
C1 f x = f¹ x = f x
C2 f x = f² x = f (f x)

etcetera. We can define a successor function “Csucc” which iterates a given function one more time than a given numeral does:

Csucc = λn.λf.λx. f (n f x)

(λn.λf.λx. n f (f x) works equally well). Each Church numeral Cn is thus itself the n’th iterate of Csucc on C0:

Cn = Cn Csucc C0

The best thing about Church numerals is the ease of defining arithmetic operators. It is straightforward to verify that

add = λm.λn.λf.λx. m f (n f x)
mul = λm.λn.λf. m (n f)
pow = λm.λn. n m

work as advertised.

E.g. pow C2 C3 = C3 C2 = λf. C2 (C2 (C2 f)) = λf.((f²)²)² = λf.f⁸ = C8

Much less straightforward is the predecessor operator, that takes C(n+1) to Cn and leaves C0 unchanged:

Cpred = λn.λf.λx. n(λg.λh. h(g f))(λu. x)(λu. u)

Wikipedia tries to explain its operation in detail.

Even less straightforward is the following division operator that springs from the creative mind of Bertram Felgenhauer:

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)

whose operation is illustrated in this Algorithmic Information Theory github repository.

SK Combinatory Logic

Combinatory Logic is concerned with terms consisting of the 2 basic combinators

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

combined through application. It turns out that any closed lambda term is equivalent to a combinator. For example, the identity combinator can be obtained as

I = S K K

since I x = S K K x = K x (K x) = x.

While reading Stephen Wolfram’s latest book, I came across an interesting alternative to Church numerals for Combinatory Logic:

F0 = K
F1 = S K
F2 = S (S K)
F3 = S ( S (S K)))

etcetera, so S iterated n times on K, or Fn = Cn S K.

This takes economy to an extreme, by using the 2 primitive combinators S and K as the very building blocks of numbers:

F0 = K
Fsucc = S

We have

F0 x y = x
F(n+1) x y = S Fn x y = Fn y (x y)

so that

F1 x y = y
F2 x y = x y
F3 x y = y (x y)
F4 x y = x y (y (x y))

etcetera, which can be shown by induction so satisfy the Fibonacci recurrence

F(n+2) x y = (Fn x y) (F(n+1) x y)

with sum replaced by application! Consequently, there are exactly fib(n) occurrences of variable y in Fn x y.

In honor of this close connection we denote these SK numerals with the letter F . Curiously, F0 and F1 coincide with the standard representations of booleans

True = K
False = S K

The big question, though, is whether they work as numerals. The ultimate test of that is the ability to convert them back into Church numerals. Wolfram’s book suggests a way to do that by applying an SK numeral to x and y that are both Church numerals, perhaps C3 and C2, which leads to all applications working as powers. For example, F3 C3 C2 = C2 (C3 C2) = C2 C8 = C256. And from that we could work our way back to the 3, resulting in a size 181 conversion combinator.

A more elegant conversion can be obtained by defining predecessor and iszero operators, and using these to count down to zero

Fpred = λn.λx.λy. n (K y) x
Fiszero = λn. n False I S K
F2C = λn. Fiszero n C0 (Csucc (F2C (pred n)))

We may check that

Fpred F1 x y = F1 (K y) x = x
Fpred F2 x y = F2 (K y) x = K y x = y

and by induction, Fpred F(n+1) = Fn holds for all n. In fact, it works so well, it lets us venture into the negative numbers:

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)

etcetera. And Fsucc works on these negative numerals too.

Fiszero however works on non-negative numerals only, as follows:

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

Using the optimal Y combinator S S K (S (K (S S (S (S S K)))) K), F2C is combinator of size 69, a huge improvement.

But it turns out we can do better still, courtesy of good old Bertram:

pair = λx.λy. λp. p x y
F2C = λn.(λp. n p(p p) False) (pair (λf.λy.λx. pair f (Csucc y)) C0)

This size 60 combinator

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

applies the SK numeral to x and y that are both pairs of some function and a church numeral. Applying one such pair to another results in the function applied to itself and the two numerals:

(pair f Cm) (pair f Cn) = (pair f Cn) f Cm = f f Cn Cm

so all function f has to do is take the successor of the right Church numeral and wrap it back up into a pair. In the F2C definition above, p is a wrapped C0 and (p p) becomes a wrapped C1.

And that wraps us our brief exploration of SK numerals.

--

--

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

John Tromp

19 Followers

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