The Jekejeke Minlog extension is further based on a forward chaining rule language and on a forward chaining engine. Forward chaining rules allow the declarative definition of the addition and removal of clause objects. Ordinary Prolog rules can be viewed as Horn clauses in the simple case. These rules are usually executed in a backward chaining manner. Backward chaining is based on the notion of solving a sub-goal. To solve a sub-goal zero, one or many new sub-goals need to be solved. The inference step for backward chaining can be schematized as follows:
Horn clause: A :- B1, .., Bn
Sub-goal: B1, .., Bn
Our forward chaining rule language doesn’t demand a considerable different rule format. It is just that that Horn clauses are executed in a different manner. This execution is not anymore based on the notion of solving a sub-goal. Instead the notion of a solved fact is used. From zero, one or many solved facts new solved facts can emerge. The inference step for forward chaining can be schematized as follows:
Fact: B1, .., Bn
Horn clause: A :- B1, .., Bn
In the current Jekejeke Minlog realization Prolog rules that should be executed in a forward chaining manner do use the operator (&:-)/2 instead of the operator (:-)/2. Upon seeing such a rule, the Jekejeke Minlog realization will perform a special compilation. This compilation will produce ordinary Prolog rules that can do a delta computation. The delta computation can compute new facts upon arrival of a single fact. The delta computation is executed in a greedy and exhaustive fashion.
The basic idea to use forward chaining for constraint solving is to store constraints in the for-ward store. When implementing a constraint solver via forward chaining there will be no sep-arate constraint store. All the advantages of clause indexing of facts, which make up the for-ward store, will be available for the constraint solver. Similarly the trailing of facts will carry over to constraints, so that modifications of constraints will be automatically undone during backtracking.
The forward chaining rule language and the forward chaining engine have been enhanced so that they can be used to implement constraint solvers. During constraint solving constraints often need to be replaced by other constraints or constraints have to be eliminated right away. To allow Horn clauses to define such a behaviour we have introduced a new operator (&-)/1 which can be used to mark goals. Facts stemming from such goals will be removed during forward chaining.
The use of the delete mechanism in our forward rule language to define constraint solver has been exemplified in the tutorial example “Little Solver” from the Jekejeke Minlog language manual. In this tutorial a constraint solver for domain intersection is realized. The constraint solver is very primitive and the main rule is the following transformation of two constraints into one constraint. The delete mechanism helps deleting the two old constraints by looking up the corresponding facts and removing them:
x ∈ S, x ∈ T --> x ∈ S ∩ T
The insert of the new constraint is done by the arrival of a new fact in a forward chaining manner. But this is not enough to implement the “Little Solver”. A further not yet mentioned features help implementing it. The forward chaining language allows two mix forward chaining and backward chaining rules. The set intersection of the new fact x ∈ S ∩ T is computed by invoking backward chaining predicate from within one of the forward chaining rules.
The more interesting feature is the way the forward chaining engine can be influenced in its execution. Jekejeke Minlog provides two constructs. The first construct is the asymmetric conjunction (&&)/2. It is already needed in the “Little Solver” example. Without asymmetric conjunction the above replacement rule would fire twice. If a set constraint arrives it would match with the first pattern x ∈ S and fire the rule once, and then it would match with the se-cond pattern x ∈ T again and fire the rule one more time.
The second construct is the cut !/0 inside forward chaining rules. When combined with the asymmetric conjunction (&&)/2 it allows a very fine control of when the firing of forward chaining should stop or not for a fact that has just been arrived. This is used in implementing more complex constraint solvers where a layering of the transformation rules is needed. In the appendix two example extensions of the “Little Solver” are found. There are recommendations when to use the cut !/0 and when not to use the cut !/0.
The first example extension introduces a new constraint that allows the aliasing of variables. The main rule is the following transformation of one constraint into another:
x = y, x ∈ S --> y ∈ SThe aliasing is implemented by a kind of union find algorithm. If aliasing applies the newly arrived fact is transformed according to the above rule and then checked again, and so on. The result is a new version of the “Little Solver” where rules concerning variable aliasing are inserted before the other rules. The rules form a new layer in front of the old transformation rules of the simple “Little Solver”. Here the cut !/0 is needed to stop further firing as soon as an aliasing is detected.
The second example extension introduces a new constraint that allows relating three variables via addition. The main rule is basically suspension until the variables become instantiated:
x = c, x + d = y --> c + d = y
The suspension is implemented by a couple of sub constraints that
model the successive instantiation of the original add constraint.
Since the instantiation happens after the aliasing, again a
modular organization of the forward chaining rules of the extended
“Little Solver” is possible. All the add constraint rules can be
placed after the aliasing rules. But since a single instantiation
can affect multiple add constraints, one must see that the
instantiation reaches all the relevant constraints. Here the cut
!/0 is disallowed, since it would stop further firing as soon as
an instantiation is detected.
Cuts that are used to organize forward chaining rules into layers
behave as red cuts. If they are omitted where they should have
been placed and vice versa, the forward chaining rules will not
produce the right results or throw an error since an incoming fact
is deleted twice. There are also situations where cuts in forward
chaining rules can be used like green cuts. If the logic among
subsequent forward chaining rules is exclusive, placing a cut
might improve their performance.
The CLP(FD) implementation that is bundled with Jekejeke Minlog gives proof of concept that our forward chaining rule language can be used to implement complex constraint solvers. Unfortunately the forward chaining rule language hasn’t evolved yet. We have already introduced a (;)/2 in the body of a forward chaining rule. But we do not yet find the full equivalent of a (->)/2 in the body of a forward chaining rule since we haven’t yet found a way to compile it. The (->)/2 control construct would allow a more performing grouping of recurrent computations among forward chaining rules.
Evolving the forward chaining rule language further poses some interesting conceptual challenges that are non-trivial. The introduction of a (->)/2 control construct would not yet deliver enough expressiveness. It would not allow grouping recurrent computations among forward chaining rules with different rule heads. What we would need would be a control construct that switches between different rule heads. Interestingly the implication (:-)/2 in the rule head could logically allow such a reading. But again we have not yet found an appropriate compilation technique for this construct.