Theorem: The language implemented by Logic Box is Turing-complete.

Proof: I have written a program in Logic Box which executes any program 
written in the SKI calculus. The SKI calculus is known to be 
Turing-complete.



Actually, things are not quite so simple. But here goes...

First, the SKI calculus consists of abstract variables, and the three 
combinators "S", "K" and "I", which have the following rules:

   Sfgx => (fx)(gx) => fx(gx)
   Kxy  => x
   Ix   => x

It may seem absurd that this trivial system is Turing-complete. But 
there is actually several even /more/ trivial systems which are somehow 
Turing-complete.

So, how do we implement these transformation rules in Logic Box? Well, 
first we need to decide how to store this stuff. I have chosen to use 
S[], K[] and I[] to stand for the three combinators, and used the 
structure at[x, y] to represent a function application. (In other words, 
what is normally written as "xy" becomes "at[x, y]".) This makes things 
very verbose, but it does work.

The actual transformation rules are now simple enough to write:

   Reduce1{in, out}:
     (~x in = at[I[], x] & out = x) |
     (~x y in = at[at[K[], x], y] & out = x) |
     (~f ~g ~x in = at[at[at[S[], f], g], x] & out = at[at[f, x], at[g, x]])

This simple predicate takes an SKI expression as its first argument, and 
arranges for the second argument to be made equal to the result of a 
single reduction.

Actually, to get a "complete" reduction, you need to add a few extra 
rules to recursively reduce sub-expressions, or the thing never makes 
any progress.

This only performs one reduction step. To make it reduce /all/ the 
steps, you can do

   Reduce{in, out}:
     out = in | ~new Reduce1{in, new} & Reduce{new, out}

Unfortunately, because the OR operator tries /all/ possibilities rather 
than just keeping the first successful one, what this does is to produce 
a result set containing all possible reductions, using all possible 
reduction orders.

So in summary, we can say that running the program produces a result set 
which contains the correct answer /somewhere/, plus a whole heap of 
various intermediate results. As best as I can tell, there's no way to 
determine /where/ in the solutions it is. So I'm not completely sure 
this counts as a valid proof.

The complete test code is here:

Reduce1{in, out}:
   (~arg1 at[I[], arg1] = in & out = arg1) |
   (~arg1 ~arg2 at[at[K[], arg1], arg2] = in & out = arg1) |
   (~fn1 ~fn2 ~arg3 at[at[at[S[], fn1], fn2], arg3] = in & out = 
at[at[fn1, arg3], at[fn2, arg3]]) |
   (~left ~right
     at[left, right] = in &
     (
       ( ~left2 Reduce1{ left,  left2} & out = at[left2, right ]) |
       (~right2 Reduce1{right, right2} & out = at[left , right2])
     )
   )
;

Reduce{in, out}:
   in = out | ~new Reduce1{in, new} & Reduce{new, out}
;

Test1{out}:
   ~s s = S[] &
   ~k k = K[] &
   ~i i = I[] &
   out = at[at[at[at[s, at[at[s, at[k, s]], k]], i], f[]], x[]]
;

The final bit generates the expression S(S(KS)K)Ifx - the Church numeral 
2 - as a simple example which you can run.

   Test1{test} & Reduce{test, out}

It takes many, many steps, but it does eventually produce f(fx) as 
result #7. (And several more times after that, as it explores every 
possible reduction sequence. The number of these is presumably 
exponential in the size of the input...)

I would have to add either a NOT predicate, or an exclusive-OR predicate 
to get this to terminate at normal form.

Post a reply to this message