In the past, Stephen Wolfram has offered prizes for proofs that are in line with his particular way of thinking about the world. Now we have a prize for proving that S is all you need.

Wolfram recently made a personal discovery of combinatory calculus, which is basically another way to write the lambda calculus or any other production system. This sounds complicated, but it isn't. In fact it is easy enough to understand especially if you are a programmer.

What is the combinatory calculus?

It was invented in 1920 and Wolfram claims it is the earliest example of a universal computation, i.e. equivalent to a Turing machine or anything else that has the same power as a Turing machine. It is very easy to understand as long as you think of it as a game with symbols - which is what the lambda calculus and other production rules are.

The combinatory calculus has just two rules or combinators:

K - the manufacturer of constants

(K x) maps any symbol to x i.e.. it is a constant function and

(K x) y =x

S - a general function application:

(S(x,y,z)) = (x z (y z))

which you can think of as x applied to y after applying each to z.

You can gain some idea of how things work by deriving the identity function, i.e. the combinator that when applied to a symbol gives that symbol:

(S K K x) =(K x (K x) = x

and I = S K K

From here you can go on to create symbol sequences that can be regarded as integers and a combinator that "adds one" to each sequence by moving it on to the next in the sequence. This is arithmetic and from here we have the rest of mathematics.

It has been shown that the K and S combinators are universal in the sense that they can be used to implement a Turing machine which in turn can compute anything that is computable. (Actually the proof is a two-step procedure - you can show that any lambda calculus term can be converted into an expression involving K and S and, as lambda calculus is equivalent to a Turing machine so are combinators.)

After looking at some examples, Wolfram has come to the conclusion that it seems likely that S on its own is universal.

This isn't unlikely as there are a number of logical functions, e.g. NAND, that are universal and even single computer instructions, such as the Intel x86 mov instruction, that are universal.

So how do you go about proving that S is universal?

There are some suggestions on Wolfram's blog:

The best case as far as I am concerned is specific Wolfram Language code that implements the solution. If the S combinator is in fact universal, then the code should provide a “compiler” that takes, say, a Turing machine or cellular automaton specification, and generates an S combinator initial condition, together with code for the “detector” and “decoder”. But how will we validate that this code is “correct”?

Personally my preferred attack would be to show that K can be derived from nothing but S. If S is universal this has to be possible. Of course, if S isn't universal we might spend a long time trying to derive K without proving anything.

This is an interesting challenge because it is easy enough to understand and doesn't require deep math to get started. Even so I would recommend reading the rest of the blog and become familiar with the workings of K and S first.

•  Mike James is the author of The Programmer’s Guide To Theory which as its subtitle "Great ideas explained" suggests, sets out to present the fundamental ideas of computer science, such as computability, lambda calculus and Turing Machines, in an informal and yet informative way. 

More Information

1920, 2020 and a $20,000 Prize: Announcing the S Combinator Challenge

Related Articles

A New Kind of Science Is Ten

$30,000 For Rule 30

A Computable Universe - Roger Penrose On Nature As Computation

The Universe as a Computer

To be informed about new articles on I Programmer, sign up for our weekly newsletter, subscribe to the RSS feed and follow us on Twitter, Facebook or Linkedin.

Comments

Make a Comment or View Existing Comments Using Disqus

or email your comment to: comments@i-programmer.info

<ASIN:1871962439>

<ASIN:B081YS81L7>