Take the 2-minute tour ×

I spent a week or two programming a simple logic solver. Having built it, I found myself wondering whether the language it solves is Turing-complete or not. So I coded up a small set of equations which accept any valid expression in the SKI combinator calculus, and produce a result set which contains the normal form of that expression. Since SKI is Turing-complete, proving that my language can execute SKI would demonstrate its Turing-completeness.

There is a glitch, however. The solver does not reduce the expression in normal order. Actually what it does is to try every possible reduction order. Which means that the solution set is typically huge. If a normal form exists, it will be in there somewhere, but it's difficult to tell where.

This brings me to two questions:

  • Is my language Turing-complete? Or do I need to find a better proof?

  • Is the number of solutions a computable function of the input?

(At first I assumed that the size of the solution set was exponential or factorial in the input size. But on closer inspection, this is not true. You can write huge expressions which are already in normal form, and tiny expressions which do not terminate. I have a feeling that determining the size of the solution set might be equivilent to solving the Halting Problem, but I'm not completely sure...)

share|improve this question
What happens if one reduction order does not terminate while another one does? Do you get the terminating one? –  augustss Jun 4 '12 at 9:41
Oh, and your SKI implementation is all the proof I need that it's Turing complete. –  augustss Jun 4 '12 at 9:42
@augustss I have carefully arranged that the code tries normal order reduction first. So if a normal form exists, it will be at a finite position in the solution set. However, if a non-terminating reduction order exists, the soler is guaranteed to find it, and produce an infinite solution set. Is producing an infinite set which contains the right answer somewhere sufficient for Turing-completeness? I mean, simply enumerating all possible SKI expressions would do that... –  MathematicalOrchid Jun 4 '12 at 9:47
First, I assume your solution set is ordered in some fashion when it's presented. (Otherwise you'd not see anything interesting.) If so, why isn't the normal order reduction the first one to appear? –  augustss Jun 4 '12 at 9:53
Solutions are numbered in the order that the solver discovers them. The entire reduction sequence appears, not just the end result. Without knowing how long the reduction sequence is, it's not possible to tell where the irreducible result will appear. –  MathematicalOrchid Jun 4 '12 at 9:59

2 Answers 2

up vote 5 down vote accepted

A) As augustss says, your system is clearly turing complete.

B) You're right that determining solution size is the same as the halting problem. If a sequence doesn't terminate, then you get an infinite solution set. So to determine if the set is infinite, you need to determine if a reduction sequence terminates. But that's precisely the halting problem!

C) As I recall, a system that, given a set of instructions to a turing machine, merely says how many steps they take to terminate (which is, I suppose, the cardinality of your solution set) or fails to terminate if the instructions themselves fail to terminate is in itself turing complete. So that should help with the intuition here.

share|improve this answer
Nice answer, but one thing still worries me: It is possible for an expression to possess a normal form, and yet a reduction order still exists which does not terminate. In this case, the solution set is still infinite, even though the normal order reduction does terminate. So the cardinality of the solution set is not precisely the same as whether the reduction terminates or not... I'm not sure whether or not this invalidates your argument. –  MathematicalOrchid Jun 4 '12 at 19:05

In answer to my own question... I found that by tweaking the source code, I can make it so that if the input SKI expression has a normal form, that normal form will always be solution #1. So if you just ignore any further solutions, the program reduces any SKI expression to normal form.

I believe this constitutes a "better proof". ;-)

share|improve this answer

Your Answer


