Are Rule Engines Turing Complete?
Following on from a blog from Peter Lin "Should a rule engine support FOL", I thought I would blog my own findings in this quagmire. My first order logic (FOL) understanding was and still is basic. Rule Engines support propositional logic, FOL extends propositional logic with universal and existential quantifiers - so I thought that any Rule Engine that provides those two conditional elements ('forall', 'exists') should be capable of expressing any FOL statement. FOL is supposedly able to express any mathematical problem and thus Turing complete (in the lax programming interpretation), following from this logic any Rule Engine that implements universal and existential quantifiers, such as CLIPS, are Turing complete.
As an initial test of this I thought it should be possible to declaratively express cardinality with Clips, this turned out harder than I thought. Firstly it was really hard to find any website that gave any meaningful explanations/help on FOL, beyond the basics - it seems people love just quoting gibberish, see this wikipedia quote on Second Order Logic and cardinality, wikipedia did not mention cardinality and FOL:
"In a second order logic that permits quantifying over functions, it is possible to write formal sentences which mean "the domain is finite" or "the domain is of countable cardinality." To say that the domain is finite, use the sentence which says that every injective function on the domain is surjective. To say that the domain has countable cardinality, use the sentence which says that there is a bijection between every two infinite subsets of the domain. It is not possible to characterize finiteness or countability in first-order logic."
Probably the best site I found that shows more complex English statements and their FOL equivalent is from Peter Suber http://www.earlham.edu/~peters/courses/log/transtip.htm. At least the author clearly demonstrates he knows what he's explaining, which supports the quote in Peter Lin's blog "You don't really understand something until you can explain it to some one else clearly". It was the only place that explained how to do cardinality with FOL. The part that surprised me with cardinality in FOL is that you have to repeat the existential quantifier for each number. In English language terms, taken from Peter Suber's page "at least two things are human" is expressed with "there is a human x, and a human y, and x is not the same thing as y" and "at least three things are human" is expressed with "there is a human x, and a human y, and a human z, and x is not the same as y or z, y is not the same as x or z and z is not the same as x or y", that?s pretty verbose and definitely not efficient from a computational implementation.
What was interesting, and impacted my naive understanding of Turing complete with regards to Rule Engines, is that it turned out that you couldn't express this type of problem using the Clips 'exists' conditional element, that I know of in a declarative form - although I could think of possible ways not using 'exists', but then that means I can't truly express this using FOL. This makes me think that while Rule Engines extend propositional logic with FOL conditional elements their expressiveness, while useful, is more limited than that compared to what?s possible with FOL notation.
If you look at Jess or JRules, and I'm sure other engines, they have extended their language with 'accumulate'/'collect' conditional elements CEs to express cardinality. I have seen papers which takes this approach with FOL, extending the symbol table to be able to more easily express cardinality. I thought the 'accumulate' CEs were just to make cardinality easier, and not to address the limitations to fully express FOL, with this new insight discovered in the above paragraph on 'exists' in Clips I now doubt my correct use of Turing complete to describe any Rule Engine that implements 'not', 'exists', 'forall' and 'accumulate'. By this I mean what other limitations in expressiveness do Rule Engines have, compared to FOL statements? I simply don't have the understanding/knowledge to make this statement and be sure it is true. So either we need to prove this or find alternative ways to classify the declarative expressiveness of Rule Engines.
