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