=Paper=
{{Paper
|id=Vol-1433/tc_44
|storemode=property
|title=CHR Exhaustive Execution - Revisited
|pdfUrl=https://ceur-ws.org/Vol-1433/tc_44.pdf
|volume=Vol-1433
|dblpUrl=https://dblp.org/rec/conf/iclp/ElsawyZA15
}}
==CHR Exhaustive Execution - Revisited ==
https://ceur-ws.org/Vol-1433/tc_44.pdf
Technical Communications of ICLP 2015. Copyright with the Authors. 1
CHR Exhaustive Execution - Revisited
AHMED ELSAWY1 , AMIRA ZAKI1,2 , SLIM ABDENNADHER1
1 German University in Cairo, Egypt; 2 Ulm University, Germany
(e-mail: {ahmed.el-sawy,amira.zaki,slim.abdennadher}@guc.edu.eg)
submitted 29 April 2015; accepted 5 June 2015
Abstract
Constraint Handling Rules (CHR) apply guarded rules to rewrite constraints in a con-
straint store, until a final 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 finds 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. Fur-
thermore, the approach is generalized for all types of CHR rules.
KEYWORDS: Declarative programming, Constraint Handling Rules, Exhaustive execu-
tion, Source-to-source transformation, Full-search space exploration
1 Introduction
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 (Frühwirth
2009). Rules rewrite a multi-set of constraints until a final state is reached where no
more rules are applicable (Frühwirth et al. 1996). The execution is committed-choice
and fired rules cannot be retracted, thus CHR can not backtrack over alternatives.
The execution of a query by a CHR program is known as a derivation from an
initial state to a final 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 confluent programs, this is not a problem because all derivation paths ulti-
mately lead to the same final state. However non-confluent programs, such as those
used for agent programming, would produce different final states depending on the
chosen derivation path. Due to the committed-choice nature of CHR, it might not
be possible to reach all final 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 (Duck et al. 2007; Lam
and Sulzmann 2006) can be modeled in CHR to describe the behavior of an agent
2 A. Elsawy, A. Zaki and S. Abdennadher
in a world of objects (Elsawy et al. 2014). An agent holding an object X can be
represented by a hold(X) constraint. The agent picks-up an object X in a get(X)
constraint. An agent not holding any objects can be represented by an empty con-
straint, and an object Y that has been put-down can be represented with a clear(Y)
constraint. The first CHR rule below allows an empty-handed agent who should get
an object X to hold it. The second rule allows an agent that is holding an object Y
and wants to get another object X to place down Y as a clear object and then hold
X, the agent has to clear object X, because it can carry at most one object.
Example 1 (Blocks World)
rule-1 @ get(X), empty <=> hold(X).
rule-2 @ get(X), hold(Y) <=> hold(X), clear(Y).
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 first path would have the agent get the box first then the cup, hence
ending up to be holding the cup. This final state would be expressed by ‘hold(cup),
clear(box)’. The other scenario is that the agent gets the cup first, 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 final states. The CHR
implementation of the K.U. Leuven system (Frühwirth and Raiser 2011) entails
that only one final state is reached ‘hold(cup), clear(box)’.
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)
Fig. 1: Derivation tree for Example 1 with query: empty,get(box),get(cup), only the
left final state with a double border is reached using the K.U. Leuven system
CHR runs on top of a host language like Prolog which provides evaluation of built-
in constraints. Constraint Handling Rules with Disjunction (CHR∨ ) is an extension
of CHR (Abdennadher and Schütz 1998) which allows disjunctive bodies and hence
introduces Prolog’s backtracking over alternatives. Application of a transition rule
generates a branching derivation which can be utilized to overcome the committed-
choice execution 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 (Elsawy et al. 2014) as a source-to-source transformation. This involved trans-
forming the CHR program into an extended CHR program featuring exhaustive
completion to fully explore a goal’s search space.
The transformation of (Elsawy et al. 2014) involved changing a derivation into
a search tree with disjunctive branches, such that it can be exhaustively traversed
to reach all leaves. The approach involved annotating rule constraints with their
CHR Exhaustive Execution - Revisited 3
occurrence within the program and the current tree depth while searching. An
initial query was transformed into one that would trigger all different permutations
of the two reference arguments, and hence this would generate a complete tree of
all possible constraint/rule matchings. For the Blocks World example, part of the
transformed derivation tree in shown in Figure 2.
empty, get(box ), get(cup), depth(0)
empty(0, 0), get(box ), empty(1, 0), get(box ),
get(cup), depth(0) get(cup), depth(0)
empty(0, 0), empty(0, 0), empty(0, 0), empty(1, 0), empty(1, 0), empty(1, 0),
get(box , 0, 0), get(box , 1, 0), get(box , 2, 0), get(box , 0, 0), get(box , 1, 0), get(box , 2, 0),
get(cup), get(cup), get(cup), get(cup), get(cup), get(cup),
depth(0) depth(0) depth(0) depth(0) depth(0) depth(0)
... ... ... ... ... ...
Fig. 2: Part of derivation tree of same query but under transformed exhaustive pro-
gram of (Elsawy et al. 2014). Annotations are ignored for equivalence of constraints, i.e.
get(box, , ) is equivalent to get(box), etc.
However, there were two main problems with the transformation. First, the search
tree generated contained several duplicated branches. The tree was complete, how-
ever many redundant matchings were tried, which could be optimized greatly. Sec-
ondly, the approach was presented for only one type of CHR rules known as simpli-
fication 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 (Martinez 2011) is a similar work
aimed to explore all possible execution choices using derivation nets. However, no
implementation nor definition of an operational semantics was provided.
Therefore this work aims to revisit the exhaustive execution problem, by de-
signing a more generic and efficient 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 defining 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 (Elsawy et al. 2014).
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 find all paths from source
to destination in a graph, a simple CHR program can be written to find a single path
from source to destination. Then the exhaustive program would automatically find
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 previ-
ous approach. Section 4 introduces an application for the exhaustive transformation,
then the paper concludes with mention of possible future work in Section 5.
4 A. Elsawy, A. Zaki and S. Abdennadher
2 Constraint Handling Rules, by example
Constraint Handling Rules (CHR) (Frühwirth 2009; Frühwirth and Raiser 2011)
consist of guarded rewrite rules that perform conditional transformation of multi-
sets of constraints, known as the constraint store. The rules used in the Blocks World
example are simplification rules, which replaces the left-hand side constraints with
the right-hand side ones. However, there are two more types of rules, propagation
and simpagation rules. All rules have an optional unique identifier separated from
the rule body by @. For all rules, Hk and/or Hr form the rule head. Hk and Hr
are sequences of user-defined CHR constraints that are kept and removed from
the constraint store respectively. Guard is the rule guard consisting of a sequence
of built-in constraints, and B is the rule body comprising of CHR and built-in
constraints. The generalized rules are of the forms shown below:
simpagation-id @ Hk \ Hr ⇔ Guard | B
simplification-id @ Hr ⇔ Guard | B
propagation-id @ Hk ⇒ Guard | B
An example CHR program with the three types of rules with unique identifiers is
shown below; all the rules have true guard expressions which are thus eliminated.
simplification @ a, b <=> c.
propagation @ a, b ==> c.
simpagation @ a \ b <=> c.
The first simplification 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 \ 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
simplification propagation simpagation
c a, b, c a, c
Fig. 3: Complete derivation tree for query ‘a,b’
(Koninck et al. 2008) depicted a CHR derivation as a tree, consisting of a set of
nodes and directed edges connecting these nodes. The root node corresponds to the
initial state or goal. A leaf node represents a successful or failed final state. Edges
between nodes denote the applied rules. Due to the clarity offered by derivation
trees for such derivations, in this work all examples will be depicted using trees.
3 Source-to-Source Transformation
In this work, a transition is defined as a tuple (ruleid , ID1 , . . . , IDm ), where ruleid
is a rule identifier from the given program, and ID1 to IDm are the identifiers of the
CHR Exhaustive Execution - Revisited 5
constraints in the goal that matched the head constraints of ruleid . The transfor-
mation is based on the fact that CHR exhaustively applies transitions until a final
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 )
G ti
t1 t2 tn ∨
G1 G2 ... Gn Gi , history({}) G, history(H ∪ ti )
Fig. 4: Left - original program derivation tree, Right -transformed program derivation tree
The first derivation applies transition ti on state G leading to state Gi , on the
other hand, the second derivation makes no changes on state G, except that the
transition information is stored in a transition application history. The idea of using
a history or token store was used in (Abdennadher 1997) to avoid non-termination
due to propagated constraints. Similarly, in this work the transition application
history is used to prevent applying the stored transitions a second time before a
different transition is applied. Thus CHR will apply an applicable transition tj on
the derived state, if tj is not in the transition application history. This is shown
by Figure 4, the tree on the left represents the application of transitions t1 , . . . , tn
on state G leading to states G1 , . . . , Gn . The tree on the right shows how the
transformed program applies transition ti and uses disjunction to derive two states
representing Gi and G, where the latter state does not allow the application of
transition ti using the transition application history. This will eventually lead to
the application of all the remaining transitions.
3.1 Transformation
The transformation extends every user defined constraint by a unique identifier, 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 identifier.
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 ) ⇔ c t (X1 , . . . , Xn , V ), id (V + 1)
Moreover, our source-to-source transformation applies a specific transformation for
every rule type simplification, propagation, and simpagation in the source program.
1. Transformation of simplification rules is defined as follows:
Every simplification rule in the source program, defined as (ruleid @ Hr ⇔ Guard
| B ) is transformed to rule :
6 A. Elsawy, A. Zaki and S. Abdennadher
ruleid t @ Hrt , history(L) ⇔ transition ∈
/ L, Guard |
t
B , history({}) ∨ Hr , history(transition ∪ L)
where transition = (ruleid , ID1 , . . . , IDm )
Hr = c1 (X11 , . . . , X1n1 ), . . . , cm (Xm1 , . . . , Xmnm )
Hrt = c1t (X11 , . . . , X1n1 , ID1 ), . . . , cm
t
(Xm1 , . . . , Xmnm , IDm )
Transformed simplification rules extend head constraints with the constraint
identifier 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 identifiers
ID1 , . . . , IDm . Applying the rule entails two derivations, the first 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 infinitely 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 identifiers of the constraints that fired the transformed rule to prevent
these constraints from firing the same rule again. In other words, this propagation
history simulates the propagation history used by CHR. Transformation of
propagation rules is defined by the following rule transformation:
Every propagation rule in the source program, defined as (ruleid @ Hk ⇒ Guard |
B ) is transformed to rule :
ruleid t @ Hkt \ history(L), prop history(P ) ⇔ transition ∈ / L, transition ∈
/ P,
Guard | B , history({}), 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 ), . . . , cm
t
(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
CHR Exhaustive Execution - Revisited 7
once. Applying the transformed rules entails two derivations, the first 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
simplification rules of the form (Hk , Hr ⇔ Guard | B , Hk ), therefore our
proposed transformation transforms simpagation rules from the source programs
to simplification rules, adds the identifiers to the user defined constraints in the
head and the body of the transformed constraints, and applies the simplification
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, defined as (ruleid @ Hk \
Hr ⇔ Guard | B ) is transformed to rule :
ruleid t @ Hkt , Hrt , history(L) ⇔ transition ∈ / L, Guard |
B , Hkt , history({}) ∨ 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 )
t
Hrt = cjt (Xj 1 , . . . , Xj nj , IDj ), . . . , cm (Xm1 , . . . , Xmnm , IDm )
Transformed simpagation rules are applied if the kept and removed head
constraints did not previously fire the rule, and if the Guard holds. Firing the rule
entails two derivations, the first 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.
3.2 Example
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)
8 A. Elsawy, A. Zaki and S. Abdennadher
<=> \+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, empty#1, get(box )#3,
get(box )#3, get(cup)#2,
history([]) history([(rule1, 2, 1)])
rule2 rule1
empty#1, get(box )#3,
hold(box )#5, hold(cup)#4, hold(box )#4,
get(cup)#2,
clear (cup), get(box )#3, get(cup)#2,
history([(rule1, 3, 1),
history([]) history([(rule2, 3, 4)]) history([])
(rule1, 2, 1)])
rule2
hold(cup)#5, hold(box )#4,
clear (box ), get(cup)#2,
history([]) history([(rule2, 2, 4)])
Fig. 5: Derivation tree of Blocks World transformed program. For simplicity a constraint
c(X1 , . . . , Xn , ID) is represented as c(X1 , . . . , Xn )#ID
As shown in the tree, the derived final 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 final states from the deriva-
tion 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 final state.
Depending on the application, deriving all intermediate and final 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 first approach is presented in the previous work pre-
sented in (Elsawy et al. 2014). This approach adds pruning rules to the transformed
program for every CHR rule in the source program. These rules will be applied only
if no other rules are applicable and will prune final states if these states would fire
a CHR rule and the transition application history is not checked. A simpler ap-
proach is to check the transition application history, if a final state is derived by
the transformed program and the transition application history of this state is not
empty, then this state corresponds to an intermediate state, because transitions in
the transition application history are applicable on this state.
CHR Exhaustive Execution - Revisited 9
3.3 Evaluation
Initial Goal Transformation 1 Transformation 2
empty, get(i1), get(i2) 29 5
empty, get(i1), get(i2), get(i3) 157 16
empty, get(i1), get(i2), get(i3), get(i4) 1169 65
empty, get(i1), get(i2), get(i3), get(i4), get(i5) 11557 326
empty, get(i1), get(i2), get(i3), get(i4), get(i5), get(i6) 141809 1957
Table 1: Blocks World Comparison (number of results)
Initial Goal Transformation 1 Transformation 2
empty, get(i1), get(i2) 0 0
empty, get(i1), get(i2), get(i3) 0 0
empty, get(i1), get(i2), get(i3), get(i4) 15 0
empty, get(i1), get(i2), get(i3), get(i4), get(i5) 141 0
empty, get(i1), get(i2), get(i3), get(i4), get(i5), get(i6) 1810 47
Table 2: Blocks World Comparison (runtime in milliseconds)
In this subsection we evaluate the proposed source-to-source transformation and
compare it to the previous source-to-source transformation presented in (Elsawy
et al. 2014) in terms of performance. Two metrics are used to show the difference in
performance between the two approaches. The first metric is the number of results
derived by the transformed programs, while the second metric is the total runtime in
milliseconds of the transformed programs. Transformation 1 represents the proposed
source-to-source transformation in (Elsawy et al. 2014), while Transformation 2 is
the transformation presented in this paper.
Table 1 shows that the proposed source-to-source transformation produces less
number of results compared to the source-to-source transformation proposed in (El-
sawy et al. 2014). Similarly, Table 2 shows a dramatic decrease in the time taken
to fully explore the derivation tree of transformation 1. The used metrics show that
the source-to-source transformation proposed in this paper performs better than
the source-to-source transformation proposed in (Elsawy et al. 2014).
4 Application
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 exe-
cution to solve complex problems by writing simpler code. For example to find all
paths from source to destination in a graph, one could write a CHR program that
finds a single path from source to destination. Then the exhaustive program would
automatically find all paths, by fully exploring all derivations.
For the graph in Figure 6, there are two paths from node b to f. With exhaustive
10 A. Elsawy, A. Zaki and S. Abdennadher
CHR execution, one can write a program that declaratively defines 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 first 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 b c
d e 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 ob-
tained using the transformation presented in this work, however the listing of the
transformed program is omitted due to space limitations.
5 Conclusion
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 execu-
tion strategy. The transformation exhaustively traverses the search space, which is
created without duplicating derivation paths. This transformation is more efficient
than the previous approach of (Elsawy et al. 2014), as was shown in the evaluation.
As future work, we intend to explore different 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-first transformation of (De Koninck et al. 2006). Moreover,
the transformation can be performed for probabilistic CHR rules. The exhaustive
execution will then accumulate probabilities along each traversal path to provide
all final states with all their probabilities of occurrence. This can be useful for
probabilistic agent-oriented programming.
CHR Exhaustive Execution - Revisited 11
Appendix - Soundness and Completeness of the Transformation
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 ∈ / L, t ∈
/ P , Guard |
B , Hk , trans history({}), prop history(P ∪ {t}) ∨
Hk , Hr , trans history(L ∪ {t}), 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
defined above, applying t on state S 0 will derive:
S 0 7→t (St0 ∧ trans history(φ) ∧ prop history(P ∪ {t})) ∨ (S ∧ trans history(T ∪
{t}) ∧ prop history(P )).
where St0 = St if transition t is applied on S ; S 7→t St
Definition 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 defined on S and S 0 , such that E3 (S , S 0 ) holds iff 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 G 0 and G, where G 0 = G ∧trans history(φ)∧prop history(φ),
E3 (G, G 0 ) 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.
0
Induction step. We prove that for any transition t applicable on S 0 , such that S 0 7→t St ,
0
then there exists a state St derived by P , such that E3 (St , St ) 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 corre-
sponding rule in P with rule head H , then if transition t applicable on state S 0 , then t is
applicable on state S .
12 A. Elsawy, A. Zaki and S. Abdennadher
• 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.
Definition 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 defined on S and S 0 , such that E4 (S , S 0 ) holds iff S 0 = (S ∧
trans history(φ) ∧ prop history(HS 0 )) and HS = HS 0 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 G 0 = (G ∧ trans history(φ) ∧ prop history(φ)), where G 0 and G are
the initial goals of programs P T and P respectively. Since HG = φ, then E4 (G, G 0 ) 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(HS 0 )) and HS = HS 0
• 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 =
HS 0 , then t ∈ 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→t 0 (St00 ∧ trans history(φ) ∧ prop history(HS 0 ∪ {t 0 })) ∨ (S ∧ trans history({t 0 }) ∧
prop history(HS 0 ))
— Case t = t 0 : then St00 = St , and since HSt = HS 0 ∪{t 0 } then E4 (St , St00 ∧trans history(φ)∧
prop history(HS 0 ∪ {t 0 })) 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→t 0 (S ∧ trans history({t 0 }) ∧ prop history(HS 0 ))
– since S 0 = (S ∧ trans history(φ) ∧ prop history(HS 0 )), then:
(S ∧trans history(φ)∧prop history(HS 0 )) 7→t 0 (S ∧trans history({t 0 })∧prop history(HS 0 )
– Thus CHR will apply one or more transitions from transitions(S 0 ):
(S ∧trans history(φ)∧prop history(HS 0 )) 7→+ (S ∧trans history(T )∧prop history(HS 0 ))
where T ⊂ transitions(S 0 )
– Eventually CHR will apply transition t, since t ∈ / T : (S ∧ trans history(T ) ∧
prop history(HS 0 )) 7→t St ∧ trans history(φ) ∧ prop history(HS 0 ∪ {t}), then
E4 (St , St ∧ trans history(φ) ∧ prop history(HS 0 ∪ {t})) holds.
CHR Exhaustive Execution - Revisited 13
References
Abdennadher, S. 1997. Operational semantics and confluence of constraint propagation
rules. In Proceedings of the 3rd Intl. Conf. on Principles and Practice of Constraint
Programming. 252–266.
Abdennadher, S. and Schütz, H. 1998. CHR∨ : A flexible query language. In Flexible
Query Answering Systems. Lecture Notes in Computer Science, vol. 1495. Springer-
Verlag, 1–14.
De Koninck, L., Schrijvers, T., and Demoen, B. 2006. Search strategies in
CHR(Prolog). In Proceedings of 3rd Workshop on Constraint Handling Rules.
K.U.Leuven, Technical report CW 452, 109–124.
Duck, G. J., Stuckey, P. J., and Sulzmann, M. 2007. Observable confluence for
constraint handling rules. In Logic Programming. Lecture Notes in Computer Science,
vol. 4670. 224–239.
Elsawy, A., Zaki, A., and Abdennadher, S. 2014. Exhaustive execution of CHR
through source-to-source transformation. In Logic-Based Program Synthesis and Trans-
formation - 24th International Symposium, LOPSTR 2014, Canterbury, UK, September
9-11, 2014. Revised Selected Papers, M. Proietti and H. Seki, Eds. Vol. 8981. Springer,
59–73.
Frühwirth, T. 2009. Constraint Handling Rules. Cambridge University Press.
Frühwirth, T., Brisset, P., and Molwitz, J.-R. 1996. Planning cordless business
communication systems. IEEE Expert: Intelligent Systems and Their Applications,
50–55.
Frühwirth, T. and Raiser, F., Eds. 2011. Constraint Handling Rules: Compilation,
Execution, and Analysis. Books on Demand.
Koninck, L. D., Schrijvers, T., and Demoen, B. 2008. A flexible search framework
for CHR. Vol. 5388. Springer, 16–47.
Lam, E. S. and Sulzmann, M. 2006. Towards Agent Programming in CHR. In CHR’06:
Proceedings of 3rd CHR Workshop. 17–31.
Martinez, T. 2011. Angelic CHR. In CHR’11: Proceedings of the 8th Workshop on
Constraint Handling Rules. 19–31.