Constraint Handling Rules (CHR) apply guarded rules to rewrite constraints in a constraint store, until a nal state is reached in which no more rules are applicable. The rules cannot be retracted, therefore CHR does not backtrack over alternatives. In this paper, a novel source-to-source transformation is proposed, which transforms any given CHR program to one that backtracks over all possible alternatives. Accordingly, execution of the transformed program nds all possible results that are entailed from the complete search tree of the source program. Compared to a previous approach presented, the newly introduced transformation generates a search tree without redundant computations. Furthermore, the approach is generalized for all types of CHR rules.
Constraint Handling Rules (CHR) is a rule-based programming language, which was
initially designed for implementing constraint solvers but has proven to become an
elegant general-purpose language with a large spectrum of applications
The execution of a query by a CHR program is known as a derivation from an initial state to a nal one. The derivation path depends on the implementation of the CHR system, which invokes a deterministic handling for various factors. These include the order of constraints within the query, the order of rules within the program and the order of constraints within the rules.
For con uent programs, this is not a problem because all derivation paths ultimately lead to the same nal state. However non-con uent programs, such as those used for agent programming, would produce di erent nal states depending on the chosen derivation path. Due to the committed-choice nature of CHR, it might not be possible to reach all nal states for these programs. Hence the need arises to implement a mechanism to enforce search space exploration of a CHR derivation.
The rule-based agent planning Blocks World example
An empty-handed agent who should pick-up a box and a cup is expressed with an
initial query `empty, get(box), get(cup)'. There are two possible scenarios from
this state; the rst path would have the agent get the box rst then the cup, hence
ending up to be holding the cup. This nal state would be expressed by `hold(cup),
clear(box)'. The other scenario is that the agent gets the cup rst, then clears it
and ends up holding the box; which is expressed as `hold(box), clear(cup)'. These
two scenarios can be depicted in Figure 1 as two disjoint nal states. The CHR
implementation of the K.U. Leuven system
empty; get(box ); get(cup) rule-1 rule-1 hold(box ); get(cup) hold(cup); get(box )
rule-2 rule-2 hold(cup); clear(box ) hold(box ); clear(cup)
CHR runs on top of a host language like Prolog which provides evaluation of
builtin constraints. Constraint Handling Rules with Disjunction (CHR_) is an extension
of CHR
Source-to-source transformations can be used to transform CHR programs into
extended ones with additional machinery. This work aims to transform a CHR
committed-choice derivation to a traversable search-tree; the idea was introduced
in
The transformation of
empty; get(box ); get(cup); depth(0) empty(0; 0); get(box ; 0; 0); get(cup); depth(0) : : : empty(0; 0); get(box ); get(cup); depth(0) empty(0; 0); get(box ; 1; 0); get(cup); depth(0) : : : empty(0; 0); get(box ; 2; 0); get(cup); depth(0) : : : empty(1; 0); get(box ; 0; 0); get(cup); depth(0) : : : empty(1; 0); get(box ); get(cup); depth(0) empty(1; 0); get(box ; 1; 0); get(cup); depth(0) : : : empty(1; 0); get(box ; 2; 0); get(cup); depth(0) : : :
However, there were two main problems with the transformation. First, the search tree generated contained several duplicated branches. The tree was complete, however many redundant matchings were tried, which could be optimized greatly. Secondly, the approach was presented for only one type of CHR rules known as simplication rules. The transformation requires an additional handling for a propagation history to handle other CHR rule types (known as propagation and simpagation rules), yet the details of this was not formally investigated.
Alternatively, the angelic semantics of CHR
Therefore this work aims to revisit the exhaustive execution problem, by
designing a more generic and e cient source-to-source transformation that enforces a
full-space exploration of a CHR derivation tree. The new exhaustive transformation
will be formalized in this work by de ning how it handles all types of CHR rules.
An evaluation showing the gained search-space improvement will be also shown in
comparison to previous work
This work also proposes interesting applications for exhaustive CHR, bringing it closer to its declarative form. Exhaustive CHR execution can be utilized to solve complex problems by writing simpler code. For example to nd all paths from source to destination in a graph, a simple CHR program can be written to nd a single path from source to destination. Then the exhaustive program would automatically nd all paths by fully exploring all derivations, without having to write a new program that explicitly explores all paths.
The paper proceeds by introducing Constraint Handling Rules in Section 2. The transformation is presented in Section 3, with evaluation in comparison to the previous approach. Section 4 introduces an application for the exhaustive transformation, then the paper concludes with mention of possible future work in Section 5.
Constraint Handling Rules (CHR)
An example CHR program with the three types of rules with unique identi ers is shown below; all the rules have true guard expressions which are thus eliminated.
The rst simpli cation rule checks if constraints a and b are in the store, it then removes them and adds constraint c. The second propagation rule adds constraint c to the store if constraints a and b are in the store. The third simpagation rule combines the functionality of the previous two rules. If constraints a and b are in the store, then the constraints after n are removed while keeping the ones before it. Here this means removing constraint b, keeping constraint a and adding constraint c. A query `a,b' can have multiple derivation paths, depending on which rule is chosen. All possible derivations are shown in Figure 3.
a; b
c
simpli cation
propagation
a; b; c
simpagation
a; c
In this work, a transition is de ned as a tuple (ruleid ; ID1; : : : ; IDm ), where ruleid is a rule identi er from the given program, and ID1 to IDm are the identi ers of the constraints in the goal that matched the head constraints of ruleid . The transformation is based on the fact that CHR exhaustively applies transitions until a nal state is reached where no more transitions are applicable. If transitions t1; : : : ; tn are applicable on CHR state G , then CHR will deterministically apply only one of these transitions without retracting. The transformation ensures completeness by deriving two CHR states from state G using disjunction and backtracking of Prolog, when transition ti for 1 i n is applied on G .
G; history(H ) G1 t1 G2 t2
G : : : tn ti
_ Gn
The transformation extends every user de ned constraint by a unique identi er, to be used by the transition application history. Constraint id =1 is added to the initial query, initially with the value one. This constraint stores the next unique identi er. For every head constraint c=n that appears in the source program, the following rule is added to the transformed program:
extend c @ c(X1; : : : ; Xn ); id (V ) , ct (X1; : : : ; Xn ; V ); id (V + 1) Moreover, our source-to-source transformation applies a speci c transformation for every rule type simpli cation, propagation, and simpagation in the source program. 1. Transformation of simpli cation rules is de ned as follows:
Every simpli cation rule in the source program, de ned as (ruleid @ Hr , Guard | B ) is transformed to rule : ruleid t @ Hrt ; history (L) , transition 2= L; Guard |
B ; history (fg) _ Hrt ; history (transition [ L) where transition = (ruleid ; ID1; : : : ; IDm ) Hr = c1(X11; : : : ; X1n1 ); : : : ; cm (Xm1; : : : ; Xmnm ) Hrt = c1t(X11; : : : ; X1n1 ; ID1); : : : ; cmt (Xm1; : : : ; Xmnm ; IDm ) Transformed simpli cation rules extend head constraints with the constraint identi er and add the transition application history constraint history =1 to the rules' head. These rules are applied if the Guard holds and the transition application history does not have a record of applying the rule with the identi ers ID1; : : : ; IDm . Applying the rule entails two derivations, the rst derivation applies the corresponding rule from the source program, it adds the body B of the original rule to the goal, moreover it empties the transition application history. The second derivation adds the removed head constraints Hrt to the goal and it adds the transition information to the transition application history. 2. A propagation rule with rule head Hk would be transformed to a simpagation rule with rule head Hk \ history (L), since Hk should be kept in the goal and the transition application history should be updated after the rule is applied. However, this approach might lead to a trivial non-termination because the rule could be applied on the same constraints in nitely many times. Moreover, it is inconsistent with the semantics of CHR because a CHR propagation rule should not be applied with the same constraints more than once. Thus, for propagation rules in the source program, our transformation uses a propagation history prop history =1 besides the transition application history. The propagation history stores the identi ers of the constraints that red the transformed rule to prevent these constraints from ring the same rule again. In other words, this propagation history simulates the propagation history used by CHR. Transformation of propagation rules is de ned by the following rule transformation: ruleid t @ Hkt \ history (L); prop history (P ) , transition 2= L; transition 2= P ; Guard | B ; history (fg); prop history (transition [ P ) _
history (transition [ L); prop history (P ) where transition = (ruleid ; ID1; : : : ; IDm ) Hk = c1(X11; : : : ; X1n1 ); : : : ; cm (Xm1; : : : ; Xmnm ) Hkt = c1t(X11; : : : ; X1n1 ; ID1); : : : ; cmt (Xm1; : : : ; Xmnm ; IDm ) The proposed transformation transforms propagation rules to simpagation rules in which the kept head of the simpagation rule is the head of the propagation rule and the removed head of the simpagation rule is the transition application history and the propagation history. The transformed rule uses the propagation history to guarantee that the kept head constraints do not apply the same rule more than once. Applying the transformed rules entails two derivations, the rst derivation adds the body B of the original rule to the goal, empties the transition application history, and stores the transition information to the propagation history. The second derivation does not apply the original rule's body, thus the propagation history remains unchanged and the transition information is added to the transition application history. 3. Simpagation rules of the form (Hk \ Hr , Guard | B ) are equivalent to simpli cation rules of the form (Hk ; Hr , Guard | B ; Hk ), therefore our proposed transformation transforms simpagation rules from the source programs to simpli cation rules, adds the identi ers to the user de ned constraints in the head and the body of the transformed constraints, and applies the simpli cation rules transformation. Thus simpagation rules from the source program will be transformed according to the following rule transformation : Every simpagation rule in the source program, de ned as (ruleid @ Hk \ Hr , Guard | B ) is transformed to rule : ruleid t @ Hkt ; Hrt ; history(L) , transition 2= L; Guard |
B ; Hkt ; history(fg) _ Hkt ; Hrt ; history(transition [ L) where transition = (ruleid ; ID1; : : : ; IDi ; IDj ; : : : ; IDm ) Hk = c1(X11; : : : ; X1n1 ); : : : ; ci (Xi1; : : : ; Xini ) Hr = cj (Xj 1; : : : ; Xj nj ); : : : ; cm (Xm1; : : : ; Xmnm ) Hkt = c1t(X11; : : : ; X1n1 ; ID1); : : : ; cit (Xi1; : : : ; Xini ; IDi ) Hrt = cjt (Xj 1; : : : ; Xj nj ; IDj ); : : : ; cmt (Xm1; : : : ; Xmnm ; IDm ) Transformed simpagation rules are applied if the kept and removed head constraints did not previously re the rule, and if the Guard holds. Firing the rule entails two derivations, the rst derivation applies the original rule's body, adds the kept head constraints to the goal, and empties the transition application history, while the second derivation adds the kept head and removed head constraints to the goal since the original rule from the source program will not be applied and it adds the transition information to the transition application history.
In the following example we apply the transformation on the CHR program of Example 1. We show the transformed program, in addition to the full search tree generated by it.
Example 2 (Blocks World Revisited) %%%%%%%%%%%%%%%%%%%% Extend Constraints %%%%%%%%%%%%%%%%%%%% extend_empty @ empty, id(I) <=> empty_t(I), I1 is I + 1, id(I1). extend_get @ get(X), id(I) <=> get_t(X,I), I1 is I + 1, id(I1). extend_hold @ hold(X), id(I) <=> hold_t(X,I), I1 is I + 1, id(I1). %%%%%%%%%%%%%%%%%%%% Transformed Rules %%%%%%%%%%%%%%%%%%%% rule1_t @ get_t(X,ID1), empty_t(ID2), history(L) <=> \+member((rule1,ID1,ID2),L) | hold(X),history([]) ; get_t(X,ID1), empty_t(ID2),history([(rule1,ID1,ID2)|L]). rule2_t @ get_t(X,ID1), hold_t(Y,ID2), history(L) <=> \+member((rule2,ID1,ID2),L) | hold(X), clear(Y), history([]) ; get_t(X,ID1), hold_t(Y,ID2), history([(rule2,ID1,ID2)|L]).
Executing the program with the query `empty, get(box), get(cup), history([]), id(1)' produces the tree depicted in Figure 5.
empty; get(box ); get(cup); history([])
rule1 hold(cup)#4; get(box )#3; history([]) rule2 hold(box )#5; clear(cup); history([]) hold(cup)#4; get(box )#3; history([(rule2; 3; 4)]) empty#1; get(box )#3; get(cup)#2; history([(rule1; 2; 1)])
rule1 hold(box )#4; get(cup)#2; history([]) rule2 empty#1; get(box )#3; get(cup)#2; history([(rule1; 3; 1); (rule1; 2; 1)]) hold(cup)#5; clear(box ); history([]) hold(box )#4; get(cup)#2; history([(rule2; 2; 4)])
As shown in the tree, the derived nal states are `hold(box),clear(cup)',`hold(cup), get(box)',`hold(cup),clear(box)', `hold(box),get(cup)', and `empty, get(box), get(cup)'. These results represent all intermediate and nal states from the derivation tree of the Blocks World program. Our proposed transformation derives all states in the derivation tree of any given program because for any CHR state, if a transition is applicable, our program will store the transition information in the transition application history and will make a derivation in which the transition cannot be applied, thus eventually this CHR state will be a nal state.
Depending on the application, deriving all intermediate and nal states might be
unwanted, therefore we present two methods to prune the derived results by the
transformed program that correspond to intermediate results in the derivation tree
of the original program. The rst approach is presented in the previous work
presented in
Initial Goal Transformation 1
Transformation 2 empty, get(i1), get(i2) empty, get(i1), get(i2), get(i3) empty, get(i1), get(i2), get(i3), get(i4) empty, get(i1), get(i2), get(i3), get(i4), get(i5) empty, get(i1), get(i2), get(i3), get(i4), get(i5), get(i6) 29 157 1169 11557 141809 3.3 Evaluation 5 16 65 326 1957 empty, get(i1), get(i2) empty, get(i1), get(i2), get(i3) empty, get(i1), get(i2), get(i3), get(i4) empty, get(i1), get(i2), get(i3), get(i4), get(i5) empty, get(i1), get(i2), get(i3), get(i4), get(i5), get(i6)
In this subsection we evaluate the proposed source-to-source transformation and
compare it to the previous source-to-source transformation presented in
Table 1 shows that the proposed source-to-source transformation produces less
number of results compared to the source-to-source transformation proposed in
One interesting application for the exhaustive execution of CHR, is that in a sense it brings CHR closer to its declarative form. One can utilize the exhaustive execution to solve complex problems by writing simpler code. For example to nd all paths from source to destination in a graph, one could write a CHR program that nds a single path from source to destination. Then the exhaustive program would automatically nd all paths, by fully exploring all derivations.
For the graph in Figure 6, there are two paths from node b to f. With exhaustive CHR execution, one can write a program that declaratively de nes a single path from source to destination, then the exhaustive transformation yields all paths.
A graph can be denoted using edge/2 constraints representing directed edges from the rst argument to the second. Furthermore, nodes containing no outgoing edges are indicated by final/1 constraints. The simple CHR program that searches for a path from X to Y through a search/2 constraint, would produce path/2 constraints for the traversed path and then a found/0 constraint is added to indicate the success of the path.
Example 3 (All Paths) found @ search(X,Y), edge(X,Y) <=> path(X,Y), found. traverse @ search(X,Y), edge(X,Z) <=> path(X,Z), search(Z,Y). notfound @ search(X,_), final(X) <=> fail.
a d b e c f Fig. 6: Graph represented by the constraints `edge(b,a), edge(b,c), edge(b,e), edge(a,d), edge(e,d), edge(c,f), edge(e,f), final(d), final(f)'.
Searching for a path from b to f can be achieved through: `search(b,f),edge(b,a), edge(b,c),edge(b,e),edge(a,d),edge(e,d),edge(c,f),edge(e,f),final(d),final(f)'. By executing the program presented above, we will derive the path `path(b,c), path(c,f),found' only. Applying the source-to-source transformation presented in this work, and executing the transformed program would yield all paths; i.e. `path(b,e), path(e,f),found' and `path(b,c),path(c,f),found'. The exhaustive program is obtained using the transformation presented in this work, however the listing of the transformed program is omitted due to space limitations.
The paper presented a new approach for the exhaustive execution of CHR programs.
The approach involves a source-to-source transformation which expresses any CHR
program as one utilizing disjunction, hence forcing an exhaustive explorative
execution strategy. The transformation exhaustively traverses the search space, which is
created without duplicating derivation paths. This transformation is more e cient
than the previous approach of
As future work, we intend to explore di erent search strategies for the derivation
tree which could lead to implementing intelligent search strategies for any CHR
program. Due to the disjunctive rule bodies, the transformation can also be easily
extended to breadth- rst transformation of
For simplicity of the proof, we generalize the transformation of any rule (ruleid @ Hk \ Hr , Guard | B ) to the following: ruleid @ Hk ; Hr ; trans history (L); prop history (P ) , t 2= L; t 2= P ; Guard | B ; Hk ; trans history (fg); prop history (P [ ft g) _
Hk ; Hr ; trans history (L [ ft g); prop history (P ) where t is the applied transition.
Lemma 1 Let S be a state derived by the source program P and S 0 be a CHR state derived by the transformed program P T such that S 0 = S ^trans history (T )^prop history (P ), let t be some transition applicable on state S 0, according to the transformation rule de ned above, applying t on state S 0 will derive:
S 0 7!t (St0 ^ trans history ( ) ^ prop history (P [ ft g)) _ (S ^ trans history (T [ ft g) ^ prop history (P )). where St0 = St if transition t is applied on S ; S 7!t St De nition 1 Let P be a CHR program and P T be the transformed program of P , let S be a CHR state derived by program P from the initial goal G and S 0 be a CHR state derived by program P T from the initial goal (G ^ trans history ( ) ^ prop history ( )). Let E3 be the property de ned on S and S 0, such that E3(S ; S 0) holds i S 0 = (S ^ trans history ( ) ^ prop history ( ) Theorem 1 (Soundness ) Given a CHR program P, its corresponding transformed program P T , and an initial query G . P T is sound with respect to P if and only if for every CHR state S 0 derived from the initial goal (G ^ trans history ( ) ^ prop history ( )) 7! S 0 by program P T , there exists a CHR state S derived by program P such that (G 7! S ) and E3(S ; S 0) holds.
Proof Base Case. For initial goals G0 and G, where G0 = G ^trans history( )^prop history( ), E3(G; G0) holds.
Hypothesis. Assume that S 0 and S are two CHR states derived by programs P T and P respectively and E3(S ; S 0) holds.
Induction step. We prove that for any transition t applicable on S 0, such that S 0 7!t St0 , then there exists a state St derived by P , such that E3(St ; St0 ) holds.
From the hypothesis: S 0 = (S ^ trans history( ) ^ prop history( )) Since every rule in P T with rule head H ; trans history=1; prop history=1 has a corresponding rule in P with rule head H , then if transition t applicable on state S 0, then t is applicable on state S . Applying t on state S , yields S 7!t St Applying t on state S 0, yields S 0 7!t (St ^ trans history( ) ^ prop history( )) _ (S ^ trans history( ) ^ prop history( )).
E3(St ; St ^trans history( )^prop history( )) holds and E3(S ; S ^trans history( )^prop history( )) holds.
De nition 2 Let P be a CHR program and P T be the transformed program of P , let S be a CHR state derived by program P from the initial goal G and S 0 be a CHR state derived by program P T from the initial goal (G ^ trans history ( ) ^ prop history ( )). Let E4 be the property de ned on S and S 0, such that E4(S ; S 0) holds i S 0 = (S ^ trans history ( ) ^ prop history (HS0 )) and HS = HS0 where HS is the propagation history store of S .
Theorem 2 (Completeness ) Given a CHR program P, its corresponding transformed program P T , and an initial query G . P T is complete if and only if for every CHR state S derived from the initial goal G 7! S by program P , there exists a CHR state S 0 derived by program P T such that (G ^ trans history ( ) ^ prop history ( )) 7! S 0 and E4(S ; S 0) holds. Proof Base case. Initially G0 = (G ^ trans history( ) ^ prop history( )), where G0 and G are the initial goals of programs P T and P respectively. Since HG = , then E4(G; G0) holds. Hypothesis. Assume that S 0 and S are two CHR states derived by programs P T and P respectively and E4(S ; S 0) holds.
Induction Step. We prove that for any transition t applicable on S , such that S 7!t St , then there exists a derivation from S 0 such that S 0 7! St0 and E4(S 0; St0).
From hypothesis: S 0 = (S ^ trans history( ) ^ prop history(HS0 )) and HS = HS0 Since every rule in P with rule head H has a corresponding rule in P T with rule head H ; trans history=1; prop history=1, since the transition history of S 0 is empty, and HS = HS0 , then t 2 transitions(S 0), where transitions(S 0) is the set that contains all applicable transitions on state S 0.
The transformed program will apply transition t 0 from transitions(S 0) : S 0 7!t0 (St00 ^ trans history( ) ^ prop history(HS0 [ ft 0g)) _ (S ^ trans history(ft 0g) ^ prop history(HS0 )) | Case t = t 0 : then St00 = St , and since HSt = HS0 [ft 0g then E4(St ; St00 ^trans history( )^ prop history(HS0 [ ft0g)) holds. | Case t 6= t 0 : For this case we will check the second disjunct from applying transition t 0 on S 0: S 0 7!t0 (S ^ trans history(ft 0g) ^ prop history(HS0 )) { since S 0 = (S ^ trans history( ) ^ prop history(HS0 )), then:
(S ^trans history( )^prop history(HS0 )) 7!t0 (S ^trans history(ft 0g)^prop history(HS0 ) { Thus CHR will apply one or more transitions from transitions(S 0): (S ^trans history( )^prop history(HS0 )) 7!+ (S ^trans history(T )^prop history(HS0 )) where T transitions(S 0) { Eventually CHR will apply transition t, since t 2= T : (S ^ trans history(T ) ^ prop history(HS0 )) 7!t St ^ trans history( ) ^ prop history(HS0 [ ftg), then E4(St ; St ^ trans history( ) ^ prop history(HS0 [ ftg)) holds.