Under consideration for publication in Theory and Practice of Logic Programming

1

Logical Algorithms meets CHR

arXiv:0901.1230v1 [cs.PL] 9 Jan 2009

A Meta-Complexity Result for Constraint Handling Rules with Rule Priorities
Leslie De Koninck
Department of Computer Science, K.U.Leuven, Belgium
(e-mail: FirstName.LastName @cs.kuleuven.be)
submitted 20 December 2007; revised 20 December 2008; accepted 9 January 2009

Abstract
This paper investigates the relationship between the Logical Algorithms language (LA) of
Ganzinger and McAllester and Constraint Handling Rules (CHR). We present a translation
schema from LA to CHRrp : CHR with rule priorities, and show that the meta-complexity
theorem for LA can be applied to a subset of CHRrp via inverse translation. Inspired by the
high-level implementation proposal for Logical Algorithm by Ganzinger and McAllester
and based on a new scheduling algorithm, we propose an alternative implementation for
CHRrp that gives strong complexity guarantees and results in a new and accurate metacomplexity theorem for CHRrp . It is furthermore shown that the translation from Logical
Algorithms to CHRrp combined with the new CHRrp implementation, satisfies the required
complexity for the Logical Algorithms meta-complexity result to hold.
KEYWORDS: Constraint Handling Rules, Logical Algorithms, complexity analysis.

1 Introduction
Constraint Handling Rules (CHR) (Frühwirth 1998) is a high-level rule based language, originally designed for the implementation of constraint solvers, but also
increasingly used as a general purpose programming language. Recently, it was
shown that all algorithms can be implemented in CHR while preserving both time
and space complexity (Sneyers et al. 2005). We assume some familiarity with CHR
and refer to (Frühwirth 1998) for more details.
In “Logical Algorithms” (LA) (Ganzinger and McAllester 2002) (and based on
previous work in (Ganzinger and McAllester 2001; McAllester 1999)), Ganzinger
and McAllester present a bottom-up logic programming language for the purpose of facilitating the derivation of complexity results of algorithms described
by logical inference rules. This problem is far from trivial because the runtime
is not necessarily proportional to the derivation length (i.e., the number of rule
applications), but also includes the cost of pattern matching for multi-headed
rules, as well as the costs related to high-level execution control which is specified using rule priorities in the Logical Algorithms language. The language of
Ganzinger and McAllester resembles CHR in many ways and has often been referred
to in the discussion of complexity results of CHR programs (Christiansen 2005;

2

Leslie De Koninck

Frühwirth 2002b; Schrijvers and Frühwirth 2006; Sneyers et al. 2006a). In particular, in (Christiansen 2005), Christiansen uses the meta-complexity theorem that
accompanies the Logical Algorithms language, and notes that the CHR system used
(SICStus CHR by Holzbaur et al. (Holzbaur and Frühwirth 1998)) does not always
exhibit the right complexity because previously computed partial rule matches are
not stored.
The aim of this paper is to investigate the relationship between both languages.
More precisely, we look at how the meta-complexity theorem for Logical Algorithms can be applied to (a subset of) CHR, and how CHR can be used to implement Logical Algorithms with the correct complexity. First, we present a translation schema from Logical Algorithms to CHRrp : CHR extended with rule priorities
(De Koninck et al. 2007b). Logical Algorithms derivations of the original program
correspond to CHRrp derivations in the translation and vice versa. We also show
how to translate a subclass of CHRrp programs into Logical Algorithms. This allows us to apply the meta-complexity theorem for Logical Algorithms to these
CHRrp programs as well. Because the Logical Algorithms meta-complexity theorem is based on an optimized implementation, it gives more accurate results than
the implementation independent meta-complexity theorem of (Frühwirth 2002a;
Frühwirth 2002b) while being more general than the ad-hoc complexity derivations
in (Schrijvers and Frühwirth 2006; Sneyers et al. 2006a).
Our current implementation of CHRrp as presented in (De Koninck et al. 2008)
does not guarantee the complexity required for the meta-complexity theorem for
Logical Algorithms to hold via translation to CHRrp . Another issue is that the
translation from CHRrp to Logical Algorithms is restricted to a subset of CHRrp .
Therefore, we propose a new implementation of CHRrp , designed such that it supports a new meta-complexity theorem for the complete CHRrp language, while also
ensuring that Logical Algorithms programs translated into CHRrp are executed
with the correct complexity.
The implementation is based on the high-level implementation proposal for Logical Algorithms as given in (Ganzinger and McAllester 2002), and on a new scheduling data structure proposed in (De Koninck 2007). By using a CHR system with advanced indexing support, such as the K.U.Leuven CHR system (Schrijvers and Demoen 2004),
our implementation achieves the complexity required to enable a new and accurate
meta-complexity result for the whole CHRrp language.

Overview The rest of this paper is organized as follows. In Section 2, the syntax
and semantics of the Logical Algorithms language and CHRrp are reviewed and the
known meta-complexity theorems for both languages are presented. In Section 3 a
translation of LA programs to CHRrp programs is presented and in Section 4, the
opposite is done for a subset of CHRrp . Section 5 proposes an alternative implementation for CHRrp which enables a new meta-complexity theorem for this language,
given in Section 6. Some concluding remarks are given in Section 7.

Logical Algorithms meets Constraint Handling Rules

3

2 Logical Algorithms and CHRrp
In this section, we give an overview of the syntax and semantics of Logical Algorithms (Section 2.1) and CHRrp (Section 2.2). In Section 2.3, we review the
meta-complexity results that are known for both languages.

2.1 Logical Algorithms
This subsection gives an overview of the syntax and semantics of the Logical Algorithms language.

2.1.1 Syntax
A Logical Algorithms program P = {r1 , . . . , rn } is a set of rules. In (Ganzinger and McAllester 2002),
a graphical notation is used to represent rules. We use a new textual representation
that is closer to the syntax of CHR. A Logical Algorithms rule is an expression
r @ p : A1 , . . . , An ⇒ C
where r is the rule name, the atoms Ai (for 1 ≤ i ≤ n) are the antecedents and
C is the conclusion, which is a conjunction of atoms whose variables appear in
the antecedents. Rule r has priority p where p is an arithmetic expression whose
variables (if any) occur in the first antecedent A1 . If p contains variables, then
r is called a dynamic priority rule. Otherwise, it is called a static priority rule.
In the graphical notation of (Ganzinger and McAllester 2002), the above rule is
represented as shown below.
A1
..
.
An
(r,p)
C
The arguments of an atom are either Herbrand terms or (integer) arithmetic expressions. There are two types of atoms: comparisons and user-defined atoms. A
comparison has the form x < y, x ≤ y, x = y or x 6= y with x and y arithmetic
expressions or, in case of (=)/2 and (6=)/2, Herbrand terms. Comparisons are only
allowed in the antecedents of a rule and all variables in a comparison must appear
in earlier antecedents. A user-defined atom can be positive or negative. A negative
user-defined atom has the form del(A) where A is a positive user-defined atom. A
ground user-defined atom is called an assertion.
Example 1
An example rule (from Dijkstra’s shortest path algorithm as presented in (Ganzinger and McAllester 2002))
with name d2 and priority 1 is
d2 @ 1 : dist(V,D1 ), dist(V,D2 ), D2 < D1 => del(dist(V,D1 )).

4

Leslie De Koninck

The antecedent D2 < D1 is a comparison, the atoms dist(V,D1) and dist(V,D2)
are positive user-defined antecedents. The negative ground atom del(dist(a,5))
is an example of a negative assertion.

2.1.2 Operational Semantics
A Logical Algorithms state σ consists of a set of (positive and negative) assertions. A
state can simultaneously contain the positive assertion A and the negative assertion
del(A). In the rest of this paper, we sometimes use the word database as a synonym
for a LA execution state. Let D be the usual interpretation for the comparisons.
Given a program P , the following transition converts one state into the next:
LA

1. Apply σ ֌P σ ∪ θ(C) if there exists a (renamed apart) rule r in P of
priority p of the form
r @ p : A1 , . . . , An ⇒ C
and a ground substitution θ such that for every antecedent Ai ,
• D |= θ(Ai ) if Ai is a comparison
• θ(Ai ) ∈ σ and del(θ(Ai )) ∈
/ σ if Ai is a positive user-defined atom
• θ(Ai ) ∈ σ if Ai is a negative user-defined atom
Furthermore, θ(C) * σ and no rule of priority p′ and substitution θ′ exists
with θ′ (p′ ) < θ(p) for which the above conditions hold.
A state is called final if no more transitions apply to it. A non-final state has priority
p if the next firing rule instance has priority p. The condition θ(C) * σ ensures
that no rule instance fires more than once and prevents trivial non-termination. This
condition, combined with the fact that each transition only creates new assertions,
causes the consecutive states in a derivation to be monotone increasing. Although
the priorities restrict the possible derivations, the choice of which rule instance to
fire from those with equal priority is non-deterministic.

2.2 CHRrp : CHR with Rule Priorities
CHRrp is CHR extended with user-definable rule priorities. It is introduced in
(De Koninck et al. 2007b) as a solution to the lack of high-level execution control
in CHR. In this section, we review the syntax and semantics of CHRrp .

2.2.1 Syntax
A constraint c(t1 , . . . , tn ) is an atom of predicate c/n with ti a host language value
(e.g., a Herbrand term in Prolog) for 1 ≤ i ≤ n. There are two types of constraints:
built-in constraints and CHR constraints (also called user-defined constraints). The
CHR constraints are solved by the CHR program whereas the built-in constraints
are solved by an underlying constraint solver (e.g., the Prolog unification algorithm).

Logical Algorithms meets Constraint Handling Rules

5

There are three types of Constraint Handling Rules: simplification rules, propagation rules and simpagation rules. They have the following form:
Simplification p :: r @
H r ⇐⇒ g | B
Propagation
p :: r @ H k
=⇒ g | B
Simpagation
p :: r @ H k \ H r ⇐⇒ g | B
where p is the rule priority, r is the rule name, H k and H r are non-empty sequences
of CHR constraints and are called the heads of the rule. The rule guard g is a
sequence of built-in constraints and the rule body B is a sequence of both CHR and
built-in constraints. The rule priority is either a number in which case the rule is
called a static priority rule, or an arithmetic expression whose variables appear in
the heads H k and/or H r in which case the rule is called a dynamic priority rule. We
say that priority p is higher than priority p′ if p < p′ . For simplicity, we sometimes
assume priorities are integers and the highest priority is 1. Finally, a program P is
a set of CHR rules. Apart from the rule priorities, CHRrp is identical to CHR.
2.2.2 Operational Semantics
Operationally, CHR constraints have a multi-set semantics. To distinguish between
different occurrences of syntactically equal constraints, CHR constraints are extended with a unique identifier. An identified CHR constraint is denoted by c#i
with c a CHR constraint and i the identifier. We write chr(c#i) = c and id(c#i) = i
and pointwise extend these functions to sets and sequences of constraints.
The operational semantics of CHRrp , called the priority semantics and denoted
by ωp , is given in (De Koninck et al. 2007b) as a state transition system, similar
to the approach of (Duck et al. 2004) for the theoretical and refined operational
semantics of CHR. A CHR execution state σ is represented as a tuple hG, S, B, T in
where G is the goal, a multi-set of constraints to be solved; S is the CHR constraint
store, a set of identified CHR constraints; B is the built-in store, a conjunction of
built-in constraints; T is the propagation history, a set of tuples denoting the rule
instances that have already fired; and n is the next free identifier, used to identify
new CHR constraints. The transitions of ωp are shown in Table 1 where D denotes
¯X Y denotes the existential closure of Y apart
the built-in constraint theory and ∃
from the variables in X. The transitions are exhaustively applied starting from the
state hG, ∅, true, ∅i1 with G the initial goal. We have used the simpagation rule
form to denote any type of rule in the Apply transition. For simplification rules,
H1 and H1′ are empty, and for propagation rules, H2 and H2′ are empty.
The following theorem on the correspondence between the ωp semantics of CHRrp
and the theoretical operational semantics ωt of CHR (see e.g. (Duck et al. 2004)),
is proven in (De Koninck et al. 2007b).
Theorem 1
Every derivation D under ωp is also a derivation under ωt . If a state σ is a final
state under ωp , then it is also a final state under ωt .
In the refined operational semantics of CHR (Duck et al. 2004), the textual order

6

Leslie De Koninck
ωp

1. Solve h{c} ⊎ G, S, B, T in ֌ P hG, S, c ∧ B, T in where c is a built-in constraint.
ωp

2. Introduce h{c} ⊎ G, S, B, T in ֌P hG, {c#n} ∪ S, B, T in+1 where c is a CHR
constraint.
ωp
3. Apply h∅, H1 ∪ H2 ∪ S, B, T in ֌P hθ(C), H1 ∪ S, B, T ∪ {t}in where P contains
a rule of priority p of the form
p :: r @ H1′ \H2′ ⇐⇒ g | C
and a matching substitution θ such that chr(H1 ) = θ(H1′ ), chr(H2 ) = θ(H2′ ), D |=
¯ B θ(g); θ(p) is a ground arithmetic expression and t = hr, id(H1 ) ++ id(H2 )i ∈
B→∃
/
T . Furthermore, no rule of priority p′ and substitution θ′ exists with θ′ (p′ ) < θ(p)
for which the above conditions hold.

Table 1. Transitions of ωp

of the program rules determines which
constraint. However, only rule instances
are considered, and so a higher priority
constraint does not participate, will not
support dynamic rule priorities.

rule is tried next for the current active
in which the active constraint takes part
fireable rule instance in which the active
fire. The textual rule order also does not

2.2.3 Differences compared to Logical Algorithms
CHRrp differs from Logical Algorithms in the following ways:
• A Logical Algorithms state is a set of ground assertions, while the CHR
constraint store is a multi-set and may also contain non-ground constraints.
• In Logical Algorithms, built-in constraints are restricted to ask constraints
and only include comparisons; CHRrp supports any kind of built-in constraints.
• A removed CHR constraint may be reasserted and can then participate again
in rule firings whereas a removed LA assertion cannot be asserted again.
• A Logical Algorithms rule may contain negated heads. In contrast, CHRrp
requires all heads to be positive.1
• In the Logical Algorithms language, the priority of a dynamic priority rule is
determined by the variables in the left-most head, whereas in CHRrp it may
depend on multiple heads.
We note that rules for which the priority depends on more than one head, can easily
be transformed into the correct form as follows. Given a Logical Algorithms rule of
the form
r @ p : A1 , . . . , Am , Am+1 , . . . , An ⇒ C

1

See (Van Weert et al. 2006) for an extension of CHR with negation as absence. However, the
semantics of that form of negation is different from the one in Logical Algorithms.

Logical Algorithms meets Constraint Handling Rules

7

where the priority expression p is fully determined by the variables from the antecedents A1 , . . . , Am . This rule can be transformed into the equivalent rules
r1 @ 1 : A1 , . . . , Am ⇒ priorityr (p)
r2 @ p : priorityr (p), A1 , . . . , Am , Am+1 , . . . , An ⇒ C
where priorityr /1 is a new user-defined predicate. Now the first head of the dynamic
priority rule determines the rule priority. The above transformation causes the
creation of priorityr /1 assertions. We have that every execution state of the transformed program can be mapped on a corresponding execution state of the original
program (assuming rule priorities are allowed to depend on multiple heads) by
removing these priorityr /1 assertions.
2.3 Meta-Complexity Results
The Logical Algorithms language was designed with a meta-complexity result in
mind. Such a result has also been formulated for CHR. In this subsection, we review
both results and give a first intuition on how they relate to each other.
2.3.1 The Logical Algorithms Meta-Complexity Result
A prefix instance of a Logical Algorithms rule r @ p : A1 , . . . , An ⇒ C is a tuple
hr, i, θi with θ a ground substitution defined on the variables occuring in A1 , . . . , Ai
and 1 ≤ i ≤ n. Its antecedents are θ(A1 ), . . . , θ(Ai ). A strong prefix firing is a prefix
instance whose antecedents hold in a state with priority lower or equal to the prefix’
rule priority. In (Ganzinger and McAllester 2002), also the concept of a weak prefix
firing is defined, but it is of no importance for our purposes. The time complexity for
running Logical Algorithms programs is given in (Ganzinger and McAllester 2002)
as O(|σ0 | + Ps + (Pd + Ad ) · log N ) where σ0 is the initial state and |σ0 | is its size. Ps
is the number of strong prefix firings of static priority rules and Pd is the number of
strong prefix firings of dynamic priority rules; Ad is the number of assertions that
may participate in a dynamic priority rule instance; and N is the number of distinct
priorities. The following example is adapted from (Ganzinger and McAllester 2002).
Example 2 (Dijkstra’s Shortest Path)
The rules below implement Dijkstra’s single source shortest path algorithm.
d1 @ 1
: source(V) => dist(V,0).
d2 @ 1
: dist(V,D1 ), dist(V,D2 ), D2 < D1 => del(dist(V,D1 )).
d3 @ D+2 : dist(V,D), e(V,C,U) => dist(U,D+C).

A source(V ) assertion means that V is the (unique) source node for the algorithm.
A dist(V ,D) assertion means that the shortest path distance from the source node
to node V does not exceed D. Finally, an e(V ,C,U ) assertion means that there
is an edge from node V to node U with cost (weight) C. Given an initial state
consisting of one source/1 assertion and e e/3 assertions, we can derive that the

8

Leslie De Koninck

number of strong prefix firings is O(1) for rule d1, and O(e) for both rules d2 and
d3, and so both Ps and Pd are O(e). This result is based on the fact that at priority
2 and lower (numerically larger), there is at most one (positive) dist/2 assertion
for each node, and each of these assertions represent the shortest path distance
from the source node to this node. This means that at most e dist/2 assertions are
ever created, and Ad = O(e). Finally, the number of distinct priorities is bounded
by the number of dist/2 assertions, i.e., N = O(e). Using the meta-complexity
theorem, we find that the total complexity is O(e + e + (e + e) · log e) = O(e log e).
2.3.2 The “As Time Goes By” Approach
In (Frühwirth 2002a; Frühwirth 2002b), an upper bound on the worst case time
complexity of a CHR program P is given as
!
X
nr
O D
(1)
(cmax (OHr + OGr ) + (OCr + OBr ))
r∈P

where D is the maximal derivation length (i.e., the maximal number of rule firings),
cmax is the maximal number of CHR constraints in the store, and for each rule
r ∈ P:
• nr is the number of heads in r
• OHr is the cost of head matching, i.e. checking that a given sequence of nr
constraints match with the nr heads of rule r
• OGr is the cost of checking the guard
• OCr is the cost of adding built-in constraints after firing
• OBr is the cost of adding and removing CHR constraints after firing
For programs with simplification and simpagation rules only, the maximal derivation length can be derived using an appropriate ranking on constraints that decreases after each rule firing (Frühwirth 2000a). We note that finding such a ranking
is not trivial. The meta-complexity result is based on a naive CHR implementation, and therefore on the one hand gives an upper bound on the time complexity
for any reasonable implementation of CHR, but on the other hand often largely
overestimates the worst case time complexity on optimized implementations.2 The
following example is adapted from (Frühwirth 2002a).
Example 3 (Boolean)
The rules below implement the boolean and(X, Y, X ∧ Y ) constraint given that 1
represents true and 0 represents false.
and(0,Y,Z) <=> Z = 0.
and(X,1,Z) <=> X = Z.
and(X,X,Z) <=> X = Z.

2

and(X,0,Z) <=> Z = 0.
and(1,Y,Z) <=> Y = Z.
and(X,Y,1) <=> X = 1, Y = 1.

Built-in constraints may lead to a worse complexity in practical optimized implementations if
many constraints are repeatedly reactivated without this resulting in new rule firings. We return
to this issue in Section 6.3.

Logical Algorithms meets Constraint Handling Rules

9

Let the rank of an and/3 constraint be one, then the rank of the head of each rule
equals one, and the rank of the body equals zero because by definition, all built-in
constraints have a rank of zero. For a goal consisting of n and/3 constraints, the
derivation length is n, which is also the maximal number of CHR constraints in
the store. The cost of head matching, (implicit) guard checking, removing CHR
constraints and asserting built-in constraints can all be considered constant. Then
using (1), we derive that the total runtime complexity is O(n2 ).
2.3.3 A First Comparison
Although at this point we do not intend to make a complete comparison between
both results, we can already show that the Logical Algorithms result in a sense is at
least as accurate as Frühwirth’s approach, at least as far as programs without builtin tell constraints are concerned. The reasoning is as follows. In each derivation step,
a constant number of atoms (constraints) are asserted. Let cmax be the maximal
number of (strictly) positive assertions in any given state. Furthermore assume rules
have positive heads
 only, then each of the asserted atoms can participate in at most
P
nr −1
strong prefix firings. Because only O(c + D) constraints are ever
n
·
c
r
max
r∈P
asserted where c is the number of CHR constraints in the initial goal and D is the
derivation length, the total number of strong prefix firings Ps + Pd is
!
X
nr −1
O (c + D) ·
cmax
r∈P

and because c = O(cmax ) we also have the following bound
!
X
nr
O D·
cmax

(2)

r∈P

In absence of (dynamic) priorities, the total runtime complexity according to the
Logical Algorithms meta-complexity result is bounded by the same formula (2) and
hence is at least as accurate as the result of (Frühwirth 2002b) given that the cost
of both head matching (OHr ) and adding and removing CHR constraints (OBr ) is
constant for each rule r.
3 Translating Logical Algorithms into CHRrp
In this section, we show how Logical Algorithms programs can be translated into
CHRrp programs. CHR states of the translated program can be mapped onto LA
states of the original. With respect to this mapping, both programs have the same
derivations.
3.1 The Translation Schema
The translation of a LA program P is denoted by T (P ) = TS/D (P ) ∪ TR (P ). The
definitions of TS/D (P ) and TR (P ) are given below.

10

Leslie De Koninck
3.1.1 Set and Deletion Semantics

We represent Logical Algorithms assertions as CHR constraints consisting of the
assertion itself and an extra argument, called the mode indicator, denoting whether
it is positively asserted (“p”), negatively asserted (“n”) or both (“b”). For every
user-defined predicate a/n occurring in P , TS/D (P ) contains the following rules to
deal with a new positive or negative assertion:
1 :: ar (X̄, M ) \ a(X̄) ⇐⇒ M 6= n | true
1 :: ar (X̄, n), a(X̄) ⇐⇒ ar (X̄, b)
2 :: a(X̄) ⇐⇒ ar (X̄, p)
1 :: ar (X̄, M ) \ del(a(X̄)) ⇐⇒ M 6= p | true
1 :: ar (X̄, p), del(a(X̄)) ⇐⇒ ar (X̄, b)
2 :: del(a(X̄)) ⇐⇒ ar (X̄, n)
If a representation already exists, one of the priority 1 rules updates this representation. Otherwise, one of the priority 2 rules generates a new representation. At
lower (numerically larger) priorities, it is guaranteed that every assertion, whether
asserted positively, negatively or both, is represented by exactly one constraint in
the store.
3.1.2 Rules
Given a LA rule r ∈ P of the form
r @ p : A1 , . . . , An ⇒ C
We first split up the antecedents into user-defined antecedents and comparison
antecedents by using the split function defined below.
(
h[A|Au ], Ac i if A is a user-defined atom
split([A|T ]) =
hAu , [A|Ac ]i if A is a comparison
where split(T ) = hAu , Ac i
split([]) =h[], []i
In the Logical Algorithms language, a given assertion may participate multiple
times in the same rule instance, whereas in CHR all constraints in a single rule
instance must be different. To overcome this semantic difference, a single LA rule
is translated as a set of CHR rules such that every CHR rule covers a case of
syntactically equal head constraints. Let hAu , Ac i = split([A1 , . . . , An ]) with Au =
[Au1 , . . . , Aum ] and Ac = [Ac1 , . . . , Acl ]. Let P be the set of all partitions of {1, . . . , m}.
For a given partition ρ ∈ P, the following function returns the most general unifier
that unifies all antecedents {Ai | i ∈ S} for every S ∈ ρ where mgu(S) is the most
general unifier of all elements in S.
partition to mgu(ρ, [Au1 , . . . , Aum ]) = ◦ mgu({Aui | i ∈ S})
S∈ρ

Logical Algorithms meets Constraint Handling Rules

11

¯∅ θ(Ac )}. PU contains
Let PU = {hρ, θi | ρ ∈ P ∧θ = partition to mgu(ρ, Au )∧D |= ∃
all partitions for which partition to mgu is defined and for which the comparison
antecedents Ac are still satisfiable after applying the unifier. The next step is to
filter out antecedents so that every set in the partition has only one representative.
This is done by computing filter(θ(Au ), ρ) for each hρ, θi ∈ PU where the filter
function is as follows:
(
[θ(Aui )|filter(T, ρ)] if ∃S ∈ ρ : i = min(S)
u
filter([θ(Ai )|T ], ρ) =
filter(T, ρ)
otherwise
f ilter([], ) =[]
Finally, we add mode indicators to all remaining user-defined antecedents:
(
′
h[ar (X̄, p)|Am ], N i
if Au = a(X̄)
u′
modes([A |T ]) =
′
h[ar (X̄, N ′ )|Am ], [N ′ 6= p|N ]i if Au = del(a(X̄))
where hAm , N i = modes(T )
modes([]) =h[], []i
The modes function returns both the resulting antecedents and the necessary conditions on the mode indicators of these antecedents. For every hρ, θi ∈ PU, the
CHR translation TR (P ) contains a rule
p + 2 :: rρ @ H =⇒ g1 , g2 | C ′
where hH, g1 i = modes(filter(θ(Au ), ρ)), g2 = θ(Ac ) and C ′ = θ(C).
3.1.3 Examples
We illustrate the translation schema on some examples.
Example 4
A LA implementation of Dijkstra’s shortest path algorithm is
d1 @ 1
: source(V) => dist(V,0).
d2 @ 1
: dist(V,D1 ), dist(V,D2 ), D2 < D1 => del(dist(V,D1 )).
d3 @ D+2 : dist(V,D), e(V,C,U) => dist(U,D+C).

Its translation is
1 :: er (V,C,U,M) \ e(V,C,U) <=> M \= n | true.
1 :: er (V,C,U,n) , e(V,C,U) <=> er (V,C,U,b).
2 ::
e(V,C,U) <=> er (V,C,U,p).
1 :: er (V,C,U,M) \ del(e(V,C,U)) <=> M \= p | true.
1 :: er (V,C,U,p) , del(e(V,C,U)) <=> er (V,C,U,b).
2 ::
del(e(V,C,U)) <=> er (V,C,U,n).
... % (similar rules f or source/1 and dist/2)
3 :: d11

@ sourcer (V,p) ==> dist(V,0).

12

Leslie De Koninck

3 :: d21/2 @ distr (V,D1 ,p), distr (V,D2 ,p) ==> D2 < D1 | del(dist(V,D1 )).
D+4 :: d31/2 @ distr (V,D,p), er (V,C,U,p) ==> dist(U,D+C).

Example 5
A rule from the union-find implementation of (Ganzinger and McAllester 2002) is
the following:
uf4 @ 1 : union(X,Y), find(X,Z), find(Y,Z) => del(union(X,Y)).

Because antecedents find(X,Z) and find(Y,Z) are unifiable, this leads to the
following two CHR rules:
3 :: uf41/2/3 @ unionr (X,Y,p), findr (X,Z,p), findr (Y,Z,p) ==> del(union(X,Y)).
3 :: uf41/23 @ unionr (X,X,p), findr (X,Z,p) ==> del(union(X,X)).

3.2 The Correspondence between LA and CHRrp Derivations
In this subsection, we show that every derivation of the original program under
the Logical Algorithms semantics, corresponds to a derivation of the translation
under the ωp semantics of CHRrp . In order to do so, we introduce a mapping
function chr to la between reachable CHR execution states and Logical Algorithms
states; see (Duck et al. 2007) for a formal definition of reachability. Reachability is
considered with respect to initial states of the form hG, ∅, true, ∅in where the userdefined constraints in G are of the form a(X̄) and del(a(X̄)) and do not include
constraints of the form ar (X̄, M ).
chr to la(σ) = {a(X̄) | a(X̄) ∈ A ∨ (ar (X̄, M ) ∈ A ∧ M 6= n)}
∪ {del(a(X̄)) | del(a(X̄)) ∈ A ∨ (ar (X̄, M ) ∈ A ∧ M 6= p)}
where σ = hG, S, B, T in and A = G ∪ chr(S). The mapping function also takes
into account the constraints that are still in the goal and those for which the
set and deletion semantics rules have not yet fired. In the rest of this section,
we first show how CHR execution states are normalized and then show that in a
Logical Algorithms state and its corresponding normalized CHR execution state,
corresponding rule instances can fire. We start by defining a pre-normal form.
Definition 1 (Pre-normal Form)
A (reachable) state σ is in pre-normal form if and only if σ = h∅, S, true, T in ,
all constraints in S are of the form ar (X̄, M )#i, and if ar (X̄, M1 )#i1 ∈ S and
ar (X̄, M2 )#i2 ∈ S then i1 = i2 (and consequently M1 = M2 ).
The following lemma shows that every reachable state is pre-normalized before rules
are tried with priority > 2.
Lemma 1 (Pre-normalization)
ωp
For every reachable state σ, there exists a finite derivation D = σ ֌∗T (P ) σ ∗ such
that σ ∗ is in pre-normal form, chr to la(σ) = chr to la(σ ∗ ), and all rules fired in D
have priority 1 or 2. Every state has a unique pre-normal form with respect to the
chr to la mapping function.

Logical Algorithms meets Constraint Handling Rules

13

Proof
We introduce the following ranking function on CHR states:
kσk = 2 · {a(X̄) | a(X̄) ∈ A} ⊎ {del(a(X̄)) | del(a(X̄)) ∈ A} + |G|
where σ = hG, S, true, T in , A = G ⊎ chr(S) and if X is a (multi-)set, |X| is its
cardinality. Clearly, the rank of any state is positive, and if kσk = 0, state σ is in prenormal form. If σ is not in pre-normal form, then there exists at least one transition
ωp

σ ֌T (P ) σ ′ . We show that for all such transitions chr to la(σ) = chr to la(σ ′ ) and
kσ ′ k < kσk, which ensures termination.
If the goal G is not empty, then only the Introduce transition is applicable.
Every application of this transition moves a CHR constraint from the goal to the
CHR constraint store, so kσ ′ k = kσk − 1. By definition, chr to la(σ ′ ) = chr to la(σ)
(because the chr to la function does not distinguish between the goal and the CHR
constraint store).
If the goal G is empty then given that σ is not in pre-normal form, chr(S) contains
a constraint of the form a(X̄) or del(a(X̄)). We look into detail to the case of
a(X̄) ∈ chr(S); the case of del(a(X̄)) ∈ chr(S) is similar. We start by showing
that at least one rule of priority 1 or 2 is applicable. Next, we show that each rule
application decreases the norm and maintains the invariance with respect to the
chr to la function.
Assume a(X̄) ∈ chr(S). If ar (X̄, p) ∈ chr(S) or ar (X̄, b) ∈ chr(S) then the
following rule of T (P ) is applicable:
1 :: ar (X̄, M ) \ a(X̄) ⇐⇒ M 6= n | true
If ar (X̄, n) ∈ chr(S) then the rule below applies:
1 :: ar (X̄, n), a(X̄) ⇐⇒ ar (X̄, b)
Finally, if no rule of priority 1 can be applied, which implies that no constraint of
the form ar (X̄, M ) ∈ chr(S), then the following T (P ) rule can fire:
2 :: a(X̄) ⇐⇒ ar (X̄, p)
This covers all possibilities. Now we look at what happens after firing one of the
priority 1 or 2 rules. The rule
1 :: ar (X̄, M ) \ a(X̄) ⇐⇒ M 6= n | true
removes a constraint a(X̄)#i from S and has an empty body, so kσ ′ k = kσk − 2.
Since M 6= n the removed constraint was already represented by the ar (X̄, M )
constraint and so chr to la(σ ′ ) = chr to la(σ). Firing
1 :: ar (X̄, n), a(X̄) ⇐⇒ ar (X̄, b)
causes the removal of two constraints from S, namely ar (X̄, n)#i and a(X̄)#j.
Furthermore, it adds a new constraint ar (X̄, b) to G. This results in kσ ′ k = kσk − 1.
The new constraint represents the combined mode of both removed constraints and
hence chr to la(σ ′ ) = chr to la(σ). Finally, the rule
2 :: a(X̄) ⇐⇒ ar (X̄, p)

14

Leslie De Koninck

is only applicable if chr(S) does not contain a constraint of the form ar (X̄, M ).
It removes a constraint a(X̄)#i from S and adds a new constraint ar (X̄, p) to G,
resulting in kσ ′ k = kσk − 1. The new representation covers the positive assertion
and so chr to la(σ ′ ) = chr to la(σ).
In summary, if the goal is empty and σ is not in pre-normal form, a rule of
priority 1 or 2 can fire and so no rule with lower priority is applicable. All applicable transitions strictly decrease the value of the ranking function and so the
pre-normalization terminates. Finally, none of the possible transitions changes the
value of chr to la.
The state σ ∗ is called a pre-normalization of σ.
Definition 2 (Implied Rule Instance)
A rule instance θ(r) is implied in a state σ if θ(C) ⊆ chr to la(σ) with θ(σ) the
conclusion of θ(r).
Lemma 2 (Normalization)
Let there be given a pre-normalized state σ = h∅, S, true, T in . If there exists
ωp

a transition σ ֌T (P ) σ ′ in which an implied rule instance fires, then the prenormalization of σ ′ has the form h∅, S, true, T ′ in′ with T ′ ) T . In other words
chr to la(σ) = chr to la(σ ′ ) and the CHR constraint store after pre-normalization is
unchanged from the one before the implied rule instance fired while the propagation
history is increased.
Proof
Let θ(r) be the implied rule instance with conclusion θ(C). Since θ(C) ⊆ chr to la(σ)
with σ = h∅, S, true, T in , we have σ ′ = hθ(C), S, true, T ∪ {t}in and chr to la(σ) =
chr to la(σ ′ ) with t the propagation history tuple corresponding to θ(r). The goal
G of σ ′ equals θ(C) and so it holds that if a(X̄) ∈ G then a(X̄, p) ∈ chr(S) or
a(X̄, b) ∈ chr(S) and if del(a(X̄)) ∈ G then a(X̄, n) ∈ chr(S) or a(X̄, b) ∈ chr(S).
Now all constraints in the goal are first introduced in the CHR constraint store.
Next, the newly introduced CHR constraints are removed one by one using one of
the following rules:
1 :: ar (X̄, M ) \ a(X̄) ⇐⇒ M 6= n | true
1 :: ar (X̄, M ) \ del(a(X̄)) ⇐⇒ M 6= p | true
These rules remove all the constraints that were introduced from the goal and do
not change the rest of the CHR constraint store, hence after pre-normalization, the
CHR constraint store equals that of state σ again.
Because the CHR constraint store remains unchanged after firing an implied rule
instance and pre-normalizing the resulting state, only finitely many such rule instances can fire before either reaching a final execution state, or a state in which a
non-implied rule instance can fire. We call such a state normalized.

Logical Algorithms meets Constraint Handling Rules

15

Definition 3 (Normal Form)
A pre-normalized CHR execution state σ is in normal form if it is a final state
ωp

ωp

(σ 6֌T (P ) ) or there exists a transition σ ֌T (P ) σ ′ such that chr to la(σ ′ ) +
chr to la(σ), i.e., in which a non-implied rule instance is fired.
Lemma 3
For every Logical Algorithms state σLA and every normalized CHR execution state
LA

σ = h∅, S, true, T in such that σLA = chr to la(σ), there exists a transition σLA ֌P
ωp

′
σLA
if and only if there exists a transition σ ֌T (P ) σ ′ firing a non-implied rule
′
instance such that σLA
= chr to la(σ ′ ).

Proof
′
A transition of σLA to σLA
implies there exists a fireable rule instance θ(r) of a
rule r in P with priority p of the form
r @ p : A1 , . . . , An ⇒ C
Let hAu , Ac i = h[Au1 , . . . , Aum ], [Ac1 , . . . , Acl ]i = split([A1 , . . . , An ]) where we use the
split function defined in Section 3.1. The user-defined antecedents can be partitioned
into sets of syntactically equal antecedents with respect to the matching substitution
θ. The following function returns this partition:
substitution to partition(θ, [Au1 , . . . , Aum ]) = {S1 , . . . , Sm }
where Si = {j | θ(Aui ) = θ(Auj )}. Let ρ = substitution to partition(θ, Au ). From the
partition, we find the most general unifier θ′ that unifies all antecedents {Aui | i ∈ S}
for every S ∈ ρ: θ′ = partition to mgu(ρ, Au ) with partition to mgu as defined in
Section 3.1. Clearly, θ′ exists and is more general than θ. The applicability of the
Apply transition means that for all comparison antecedents Aci with 1 ≤ i ≤ l,
¯∅ θ′ (Ac ∧ . . . ∧ Ac ) and consequently a rule rρ
D |= θ(Aci ) and so it holds that D |= ∃
1
l
exists. This rule looks as follows:
p + 2 :: rρ @ H1 , . . . , Hk =⇒ g1 , g2 | C ′
with h[H1 , . . . , Hk ], g1 i = modes(Af ), Af = [Af1 , . . . , Afk ] = filter(θ′ (Au ), ρ), g2 =
θ′ (Ac ) and C ′ = θ′ (C). The modes and filter functions are as defined in Section 3.1.
Let θ′′ be a ground matching substitution such that θ = θ′′ |vars(θ) ◦ θ′ where
θ′′ |vars(θ) is the projection of θ′′ on the variables in θ. Since θ′ is more general
than θ, θ′′ exists. For all i ∈ {1, . . . , k}, if Afi = a(X̄) then Hi = ar (X̄, p). Because of the applicability of Logical Algorithms rule r in state σLA , θ′′ (a(X̄)) ∈
σLA and θ′′ (del(a(X̄))) ∈
/ σLA , so Hi′ = θ′′ (ar (X̄, p))#idi ∈ S and θ′′ (Hi ) =
f
′
chr(Hi ). Similarly, if Ai = del(a(X̄)) then Hi = ar (X̄, N ) and g1 contains N 6= p;
θ′′ (del(a(X̄))) ∈ σLA and as a result Hi′ = θ′′ (ar (X̄, N ′ ))#idi ∈ S with N ′ = n or
N ′ = b. Since N only appears in Hi and the guard N 6= p, we can further impose
that θ′′ (N ) = N ′ and then θ′′ (Hi ) = chr(Hi′ ).
All θ′′ (Afi ) are different for 1 ≤ i ≤ k, and therefore, all idi must be different.
¯∅ θ(Ac ) for 1 ≤ i ≤ l and because θ′′ (g1 ) = [N1 6= p, . . . , No 6= p] with
From D |= ∃
i

16

Leslie De Koninck

¯∅ θ′′ (g1 ∧ g2 ). We conclude that θ′′
Nj = n or Nj = b for 1 ≤ j ≤ o, D |= true → ∃
is a ground matching substitution that matches the head with constraints from S
and for which the guard is entailed.
It is not possible that hrρ , id(H)i ∈ T because chr to la grows monotonically,
which implies that θ(C) = θ′′ (C ′ ) ∈ chr to la(σ) = σLA which contradicts with the
applicability of θ(r) in σLA .
If we ignore rule priorities, all conditions are satisfied so that rule instance θ(rρ )
can fire. The resulting state σ ′ has the form hθ(C), S, true, T ∪ {hrρ , id(H)i}in .
′
′
= σLA ∪ θ(C) then σLA
=
Clearly, if σLA = chr to la(h∅, S, true, T in ) and σLA
′
chr to la(σ ). We now prove that every CHR transition firing a non-implied rule
instance corresponds to a Logical Algorithms transition, also ignoring rule priorities.
Both results combined give us that the priority of the highest priority rule instance
is equal in both σ and σLA .
A transition of σ = h∅, S, true, T in to σ ′ implies that T (P ) contains a rule
p + 2 :: rρ @ H =⇒ g1 , g2 | C ′
and so the Logical Algorithms program P contains a rule
r @ p : A1 , . . . , An ⇒ C
Let hAu , Ac i = split([A1 , . . . , An ]) and θ = partition to mgu(ρ, Au ). If Ai = a(X̄) ∈
Au then θ(ar (X̄, p)) ∈ H. If Ai = del(a(X̄)) ∈ Au then θ(ar (X̄, N )) ∈ H and
(N 6= p) ∈ g1 . Finally, if Ai ∈ Ac then θ(Ai ) ∈ g2 . There exists a (ground)
¯∅ θ′ (g1 ∧ g2 ).
matching substitution θ′ such that θ′ (H) ∈ chr(S) and D |= ∃
′′
′
′
Let θ = θ ◦ θ and let σLA = chr to la(σ). Because θ is a ground substitution,
¯∅ θ′ (g1 ∧ g2 ) implies that for all Ai ∈ Ac , D |= θ′′ (Ai ). For all positive userD |= ∃
defined antecedents Ai = a(X̄) ∈ Au , we have that θ′′ (a(X̄, p)) ∈ chr(S) and so
θ′′ (Ai ) ∈ σLA and del(θ′′ (Ai )) ∈
/ σLA . For all negative user-defined antecedents
Ai = del(a(X̄)) ∈ Au , we have that θ′′ (ar (X̄, N )) ∈ chr(S) with N = b or N = n
and so θ′′ (Ai ) ∈ σLA . We have assumed that θ′ (rρ ) is not an implied rule instance
and so θ′ (C ′ ) = θ′′ (C) * σLA .
If we again ignore rule priorities, all conditions are satisfied so that rule instance
′
θ′′ (r) can fire in state σLA and it holds that σLA
= σLA ∪ θ′′ (C) = chr to la(σ ′ )
′
′
′
since σ = hθ (C ), S, true, T ∪ {hrρ , id(H)i}in . Now we have that both the original
program P and its translation T (P ) can fire corresponding rule instances if we
ignore priorities, and so their highest priority rule instances also correspond.
Theorem 2
ωp
For every reachable CHRrp state σ, if σ ֌T (P ) σ ′ then either chr to la(σ) =
LA

chr to la(σ ′ ) or chr to la(σ) ֌P chr to la(σ ′ ).
Proof
Implied by Lemmas 1, 2 and 3.

Logical Algorithms meets Constraint Handling Rules

17

Theorem 3
For every Logical Algorithms state σi and reachable CHRrp state σi′ such that
ωp

chr to la(σi′ ) = σi , there exists a finite CHRrp derivation σi′ ֌∗T (P ) σi′∗ for which
ωp

LA

holds that chr to la(σi′∗ ) = σi such that if σi ֌P σj then σi′∗ ֌T (P ) σj′ with
chr to la(σj′ ) = σj and if σi is a final state then σi′∗ is also a final state.
Proof
Implied by Lemmas 1, 2 and 3.
Given a Logical Algorithms state σ, we can use hσ, ∅, true, ∅i1 as initial state for
the CHRrp derivation. Theorem 3 is illustrated by the figure below.
LA

σi

ωp

σi ֌P σj

ωp

hσi , ∅, true, ∅i1 ֌∗T (P ) σi′ ֌∗T (P ) σi′∗

ωp

σi′∗ ֌T (P ) σj′

LA

σi 6֌P

ωp

σi′∗ 6֌T (P )

3.3 Weak Bisimulation
To capture the meaning of the above correspondence results, we relate them to the
notion of (weak) bisimulation. A bisimulation is a relation between the states of a
labeled transition system (LTS). A relation R ⊆ S1 × S2 between the states in S1
α
α
and those in S2 is a bisimulation if p R q and p → p′ implies that q → q ′ with
α
α
p′ R q ′ , and similarly, p R q and q → q ′ implies that p → p′ with p′ R q ′ . Here, α is
α
the label of the transition p → p′ from state p to state p′ . If a transition from p to
τ
′
p has no observable effect, it is called a silent transition and denoted by p → p′ .
α
A relation R ⊆ S1 × S2 is a weak bisimulation if p R q and p → p′ implies that
τ ∗
α
τ ∗
q → q∗ → q∗′ → q ′ with p′ R q ′ , and vice versa with the roles of p and q swapped.
∗
τ
Here p → p′ means p and p′ are linked by zero or more silent transitions.
Let S1 be the set of valid Logical Algorithms states for program P and let S2 =
ωp

{chr to la(σ) | hG, ∅, true, ∅i1 ֌∗T (P ) σ ∧ G ∈ S1 }, i.e., S2 is found by applying
the chr to la mapping function all reachable CHRrp states for program T (P ). We
transform the state transition systems for Logical Algorithms and CHRrp to labeled
LA

transition systems as follows: a Logical Algorithms transition σ ֌P σ ′ corresponds
α
to an LTS transition σ → σ ′ with α = σ ′ \ σ, i.e., α represents the state change
ωp

from σ to σ ′ . A CHRrp transition σ ֌T (P ) σ ′ corresponds to an LTS transition
α
chr to la(σ) → chr to la(σ ′ ) with α = chr to la(σ ′ ) \ chr to la(σ) if this set is not
empty and α = τ otherwise.
Corollary 1
The equality relation between the states of S1 and S2 is a weak bisimulation.

18

Leslie De Koninck
4 Translating a subset of CHRrp into Logical Algorithms

In the previous section, we have shown that Logical Algorithms programs can be
translated into equivalent CHRrp programs. In this section, we show how to do
the opposite, i.e., how CHRrp programs can be translated into equivalent Logical
Algorithms programs. This allows us to apply the meta-complexity theorem for
Logical Algorithms to the translation of these CHRrp programs.
We impose some restrictions on the CHRrp programs that can be translated.
These restrictions result from the fact that the Logical Algorithms language does
not have the concept of an underlying constraint solver that offers both ask and tell
built-in constraints. In principle, the complete CHRrp language could be translated
into LA, as the subset of CHRrp for which we propose a translation is already
Turing complete (Sneyers 2008, Chapter 10), and therefore so is the LA language.
However, in general, this requires a LA implementation of the built-in constraint
solver used by the CHRrp program. Since this built-in solver is not part of the
CHRrp program, we restrict our translation schema to programs that do not make
use of such a solver. In particular, we only support the translation of the positive
range-restricted ground segment of CHRrp (Betz 2007):
1. In all reachable states σ = hG, S, B, T in : vars(S) = ∅. In words, all (stored)
CHR constraints are ground.
2. All built-in constraints are comparisons; there are no built-in tell constraints.
The first property holds if the initial goal is ground and all rules are variable restricted, which means that all variables in the body of a rule, also appear in one
of the rule heads. The second property implies that all reachable states are of the
form hG, S, true, T in , i.e., the built-in constraint store always equals true.
To simplify the presentation, we also assume that the priority of dynamic priority
rules is determined by the arguments of its left-most head. In general, we can use the
transformation schema given in Section 2.2.3 to ensure that the resulting Logical
Algorithms rules have the correct syntactical form.
4.1 The Translation Schema
We now show how the rules of a CHRrp program P are transformed into Logical
Algorithms rules that form a program T (P ). To increase readability, we distinguish
between simplification and simpagation rules on the one hand, and propagation
rules on the other. A simpagation rule of the form
p :: r @ H1 , . . . , Hl−1 \Hl , . . . , Hm ⇐⇒ g | B1 , . . . , Bo
is transformed into
id
r′ @ p : H1id , . . . , Hm
, Alldiff, g, next id(Idnext ) ⇒
id
del(Hlid ), . . . , del(Hm
), del(next id(Idnext )),

B1id , . . . , Boid , next id(Idnext + o)
where Hiid = c(X̄,Idi ) if Hi = c(X̄), Biid = c(X̄,Idnext + i − 1) if Bi = c(X̄)
¯∅ Hi = Hj ∧ g}. The disequalities in Alldiff are
and Alldiff = {(Idi 6= Idj ) | D |= ∃

Logical Algorithms meets Constraint Handling Rules

19

between those heads that are unifiable and for which the guard is still satisfiable
after this unification. The next_id/1 antecedent is used to retrieve the next free
identifier to be used to identify constraints in the body, cf. the ωp operational
semantics of CHRrp . The case of a simplification rule is similar. A propagation rule
of the form
p :: r @ H1 , . . . , Hm =⇒ g | B1 , . . . , Bo
is transformed into the following two rules
id
r1′ @ p : H1id , . . . , Hm
, Alldiff, g ⇒ token(r, [Id1 , . . . , Idm ])
id
, Alldiff, g, token(r, [Id1 , . . . , Idm ]), next id(Idnext ) ⇒
r2′ @ p : H1id , . . . , Hm

del(token(r, [Id1 , . . . , Idm ])), del(next id(Idnext )),
B1id , . . . , Boid , next id(Idnext + o)
where Hiid , Biid and Alldiff are as before. The first of these rules generates a token.
This token is removed by the second rule. The tokens are needed to prevent a
given rule instance from firing more than once.3 Note that the transformation into
two rules and the use of tokens does not increase the complexity compared to the
original rule, as there is only one token for each combination of rule and constraint
identifiers (as well as only one positive next_id/1 assertion in any state).
The initial database consists of the goal (where each constraint is extended with
a unique identifier) and a next_id(Idnext) assertion (with Idnext the next free
identifier).
Example 6 (Merge Sort )
The following CHRrp program implements a merge sort algorithm. Its input consists
of a series of n (a power of 2) number/1 constraints. Its output is a sorted list of
the numbers in the input, represented as arrow/2 constraints, where arrow(X,Y )
indicates that X is right before Y .
1 :: ms1 @ arrow(X,A) \ arrow(X,B) <=> A < B | arrow(A,B).
2 :: ms2 @ merge(N,A), merge(N,B) <=> A < B | merge(2*N+1,A), arrow(A,B).
3 :: ms3 @ number(X) <=> merge(0,X).

Its Logical Algorithms translation is
ms1′ @ 1 : arrow(X,A,Id1 ), arrow(X,B,Id2 ), A < B, next_id(NId) =>
del(arrow(X,B,Id2 )), del(next_id(NId)),
arrow(A,B,NId), next_id(NId+1).
ms2′ @ 2 : merge(N,A,Id1 ), merge(N,B,Id2 ), A < B, next_id(NId) =>
del(merge(N,A,Id1 )), del(merge(N,B,Id2 )), del(next_id(NId)),
merge(2*N+1,A,NId), arrow(A,B,NId+1), next_id(NId+2).
ms3′ @ 3 : number(X,Id), next_id(NId) => del(number(X,Id)),
del(next_id(NId)), merge(0,X,NId), next_id(NId+1).

3

In (De Koninck et al. 2007a), an erroneous translation was presented which did not use tokens,
and in which a propagation rule could fire infinitely many times because the constraints in the
body are assigned new identifiers each time the rule is fired.

20

Leslie De Koninck

Note that in rules ms1 and ms2, the guard prevents the constraints matching the
heads from being equal, and so there are no disequality constraints between the
CHR constraint identifiers. In (De Koninck et al. 2007a) it is derived that the total
runtime of this Logical Algorithms program is O(n log n). We defer the complexity
analysis of the merge sort algorithm to Section 6.1 where we analyse the CHRrp
implementation directly using a new meta-complexity theorem for CHRrp .
Example 7 (Less-or-Equal )
To illustrate how propagation rules are dealt with, we show the translation of a
rule of the leq program which is given further on in Example 9. The rule
3 :: transitivity @ leq(X,Y), leq(Y,Z) ==> leq(X,Z).

is translated into
transitivity′1 @ 3 : leq(X,Y,Id1 ), leq(Y,Z,Id2 ), Id1
token(transitivity,[Id1 ,Id2 ]).
transitivity′2 @ 3 : leq(X,Y,Id1 ), leq(Y,Z,Id2 ), Id1
token(transitivity,[Id1 ,Id2 ]), next_id(NId)
del(token(transitivity,[Id1 ,Id2 ])),
leq(X,Z,NId), next_id(NId+1).

\= Id2 =>
\= Id2 ,
=>
del(next_id(NId)),

Note that since in the original rule, the two heads leq(X,Y) and leq(Y,Z) are
unifiable (and there is furthermore no guard to prevent this from happening), we
have to add an explicit disequality between the constraint identifiers for these heads:
Id1 \= Id2 .
4.2 Correspondence
In this subsection, we prove that a CHRrp program and its translation to Logical
Algorithms are operationally equivalent. Again we introduce a mapping function:
la to chr(σ) = h∅, S, true, T in
where the CHR constraint store S = {c(X̄)#Id | c(X̄, Id) ∈ σ ∧ del(c(X̄, Id)) ∈
/ σ},
the propagation history T = {hR, Idsi | del(token(R, Ids)) ∈ σ}, and the next free
identifier n is such that next id(n) ∈ σ and del(next id(n)) ∈
/ σ. In the following, we
consider a Logical Algorithms state σ reachable with respect to program T (P ) if it
can be derived from an initial state consisting of CHR constraints extended with
unique identifiers, and a single next_id/1 assertion with as argument the next free
identifier. In this case, reachability amongst others implies that there can be only
one (strictly) positive next_id/1 assertion in any state, and no two CHR constraint
representations share their identifier.
First, we define the priority-ignoring operational semantics LA′ of Logical Algorithms, as being the same as its regular operational semantics except that priorities
are ignored, i.e., the next applicable rule instance in any state is independent of
the priorities. Next, we state two lemmas that relate a CHRrp program P and
its translation T (P ) under respectively the theoretical operational semantics ωt of

Logical Algorithms meets Constraint Handling Rules

21

CHR and this priority-ignoring operational semantics LA′ of Logical Algorithms.
Note that the ωt semantics of CHR also ignores rule priorities.
Lemma 4
LA′

For every reachable Logical Algorithms state σi it holds that if σi ֌ T (P ) σj , then
either it holds that la to chr(σi ) = la to chr(σj ) or there exists a finite CHR derivaωt

ωt

tion la to chr(σi ) = h∅, S, true, T in ֌P hC, S ′ , true, T ′ in ֌∗P h∅, S ′′ , true, T ′ in′ =
la to chr(σj ) consisting of an Apply transition, followed by zero or more Introduce
transitions.
Proof
LA′

Consider a transition σi ֌ T (P ) σj . The only type of transition in Logical Algorithms is the Apply transition which fires a rule. If la to chr(σi ) = la to chr(σj ),
then this rule must be of the form
id
r1′ @ p : H1id , . . . , Hm
, Alldiff, g ⇒ token(r, [Id1 , . . . , Idm ])

because all other types of rules either delete the representation of a CHR constraint
which changes the CHR constraint store, or remove a token which results in an
extended propagation history. We call the fired rule a token generation rule.
If la to chr(σi ) 6= la to chr(σj ) and the rule fired is of the form
id
r′ @ p : H1id , . . . , Hm
, Alldiff, g, next id(Idnext ) ⇒
id
del(Hlid ), . . . , del(Hm
), del(next id(Idnext )),

B1id , . . . , Boid , next id(Idnext + o)
which corresponds to a simplification (l = 1) or simpagation (l > 1) rule. We further
assume the case of a simpagation rule; the case of a simplification rule is similar. If
r′ ∈ T (P ) (with l > 1), then P contains a rule
p :: r @ H1 , . . . , Hl−1 \Hl , . . . , Hm ⇐⇒ g | B1 , . . . , Bo
Since the conditions for the Logical Algorithms Apply transition are satisfied,
there exists a ground matching substitution θ such that for each antecedent Hiid =
c(X̄, Idi ) (1 ≤ i ≤ m) it holds that θ(Hiid ) ∈ σ and del(θ(Hiid )) ∈
/ σ and so by
definition of the la to chr function, θ(Hi #Idi ) ∈ S where la to chr(σi ) = σi′ =
h∅, S, true, T in . For each comparison gi ∈ g, it holds that D |= θ(gi ) and so D |=
¯∅ θ(g). Since r is a simpagation rule, the propagation history T does not
true → ∃
contain any element of the form hr, i. In summary, all conditions are satisfied such
that the rule instance θ(r) can fire in state σi′ under operational semantics ωt .
After firing θ(r) in state σi′ , the resulting state equals hθ(B1 ∧. . .∧Bo ), S ′ , true, T in
where S ′ = S \ {θ(Hl #Idl ), . . . , θ(Hm #Idm )}. In this state, we can apply the Introduce o times before reaching a state with an empty goal. There are o! possible orders in which the introductions can be applied; the one we need is the
order in which the Bi constraints appear in the rule body. Following this order,
the state resulting from the introductions equals σj′ = h∅, S ′′ , true, T i(n+o) where
S ′′ = S ′ ∪ {θ(B1 )#n, . . . , θ(Bo )#(n + o − 1)}. It is easy to see that this state σj′

22

Leslie De Koninck

equals la to chr(σj ), the state resulting from firing Logical Algorithms rule instance
θ(r′ ) in state σi .
If la to chr(σi ) 6= la to chr(σj ) and the rule fired is not of the form shown above,
then it must have the following form
id
r2′ @ p : H1id , . . . , Hm
, Alldiff, g, token(r, [Id1 , . . . , Idm ]), next id(Idnext ) ⇒

del(token(r, [Id1 , . . . , Idm ])), del(next id(Idnext )),
B1id , . . . , Boid , next id(Idnext + o)
the corresponding CHRrp rule in P looks like
p :: r @ H1 , . . . , Hm =⇒ g | B1 , . . . , Bo
Again, since the conditions for the Logical Algorithms Apply transition are satisfied, there exists a ground matching substitution θ such that for each antecedent
Hiid = c(X̄, Idi ) (1 ≤ i ≤ m) in rule r2′ it holds that θ(Hiid ) ∈ σ and del(θ(Hiid )) ∈
/σ
and so by definition of the la to chr function, θ(Hi #Idi ) ∈ S where la to chr(σi ) =
σi′ = h∅, S, true, T in . For each comparison gi ∈ g, it holds that D |= θ(gi ) and so
¯∅ θ(g). The propagation history T cannot contain hr, θ([Id1 , . . . , Idm ])i
D |= true → ∃
because by definition of the la to chr function this would imply that the atom
token(r, θ([Id1 , . . . , Idm )) was deleted in some earlier state, which contradicts with
the applicability of the Apply transition on rule instance θ(r2′ ). Again, all conditions are satisfied such that θ(r) can fire in state σi′ .
After firing θ(r) in state σi′ , the resulting state equals hθ(B1 ∧. . .∧Bo ), S, true, T ′ in
where T ′ = T ∪ {hr, [Id1 , . . . , Idm ]i}. In this state, we can apply the Introduce
transition o times before reaching a state with an empty goal. Given again that
these introductions are applied in the order in which the Bi constraints appear
in the rule body, then the resulting state equals σj′ = h∅, S ′ , true, T ′ i(n+o) where
S ′ = S ∪ {θ(B1 )#n, . . . , θ(Bo )#(n + o − 1)}. It is again easy to see that this state σj′
equals la to chr(σj ), the state resulting from firing Logical Algorithms rule instance
θ(r2′ ) in state σi .
Lemma 5
For every reachable CHRrp state σi and reachable Logical Algorithms state σi′ with
LA′

la to chr(σi′ ) = σi , there exists a finite Logical Algorithms derivation σi′ ֌ ∗T (P ) σi′∗
ωt

ωt

with la to chr(σi′∗ ) = σi such that if σi = h∅, S, true, T in ֌P hC, S ′ , true, T ′ in ֌∗P
h∅, S ′′ , true, T ′ in′ = σj where the derivation consists of a single Apply transiLA′

tion, followed by zero or more Introduce transitions, then σi′∗ ֌ T (P ) σj′ with
la to chr(σj′ ) = σj and if σi is a final state then σi′∗ is also a final state.
Proof
Let there be given a reachable Logical Algorithms state σi′ with la to chr(σi′ ) = σi .
Because of Lemma 4, state σi is also reachable in CHRrp with respect to program
ωt
ωt
P . Assume σi = h∅, S, true, T in ֌P hC, S ′ , true, T ′ in ֌∗P h∅, S ′′ , true, T ′ in′ = σj
where the derivation consists of a single Apply transition, followed by zero or more

Logical Algorithms meets Constraint Handling Rules

23

Introduce transitions, and let θ(r) be the CHRrp rule instance that fired in state
σi . If r is simplification (l = 1) or simpagation (l > 1) rule
p :: r @ H1 , . . . , Hl−1 \Hl , . . . , Hm ⇐⇒ g | B1 , . . . , Bo
¯∅ θ(g).
then θ(Hi )#idi ∈ S for 1 ≤ i ≤ m with idi 6= idj if i 6= j, and D |= ∃
Furthermore, T (P ) contains a rule
id
r′ @ p : H1id , . . . , Hm
, Alldiff, g, next id(Idnext ) ⇒
id
del(Hlid ), . . . , del(Hm
), del(next id(Idnext )),

B1id , . . . , Boid , next id(Idnext + o)
′
Now let θ′ be a ground matching substitution such that θ′ |vars(θ) = θ where θvars(θ)
′
′
is the projection of θ on the variables in θ, and such that both θ (Idi ) = idi
for 1 ≤ i ≤ m and θ′ (Idnext ) = n. Since for 1 ≤ i ≤ m, Hiid = c(X̄, Id i ) if
¯∅ θ(g)
Hi = c(X̄), it holds that θ′ (Hiid ) ∈ σi′ and del(θ′ (Hiid )) ∈
/ σi′ . Also, D |= ∃
implies D |= θ(gi ) for each comparison gi ∈ g. Note that because θ(g) is ground,
there is no existential quantification. The Alldiff conditions hold because θ′ (Id i ) =
θ′ (Id j ) implies that i = j. Finally, because of the reachability of state σi′ , there is
exactly one strictly positive next_id/1 assertion in σi′ whose argument equals n.
Finally, the rule conclusion cannot be already included in the state σi′ because it
includes amongst others the deletion of at least one of the antecedents. Therefore,
all conditions are satisfied such that rule instance θ′ (r′ ) can fire in state σi′ , resulting
in a state σj′ = la to chr(σj ).
Now assume that in the CHRrp state σi , a rule instance θ(r) fires where r is a
propagation rule:

p :: r @ H1 , . . . , Hm =⇒ g | B1 , . . . , Bo
In this case the Logical Algorithms translation T (P ) contains the following rules:
r1′ @ p : H1id , . . . , Hnid , Alldiff, g ⇒ token(r, [Id1 , . . . , Idn ])
r2′ @ p : H1id , . . . , Hnid , Alldiff, g, token(r, [Id1 , . . . , Idn ]), next id(Idnext ) ⇒
del(token(r, [Id1 , . . . , Idn ])), del(next id(Idnext )),
B1id , . . . , Blid , next id(Idnext + l)
A similar analysis as above shows that there exists a matching substitution θ′ with
θ′ |vars(θ) = θ and both θ′ (Idi ) = idi for 1 ≤ i ≤ m and θ′ (Idnext ) = n, such that rule
instance θ′ (r1′ ) can fire (ignoring priorities) if token(r, [id 1 , . . . , id n ]) ∈
/ σi′ and θ′ (r2′ )
′ ′
′
′
otherwise. If θ (r1 ) fires then the resulting state σi∗ = σi ∪ {token(r, [id 1 , . . . , id n ])}
and clearly la to chr(σi′∗ ) = la to chr(σi′ ). Moreover, in state σi′∗ , rule instance θ′ (r2′ )
can fire and for the resulting state σj′ it holds that la to chr(σj′ ) = σj . If already
token(r, [id 1 , . . . , id n ]) ∈ σi′ then the same reasoning holds with σi′ = σi′∗ .
Finally, assume that CHRrp state σi is a final state. If σi′ is not a final Logical
Algorithms state, then because of Lemma 4, the only applicable rules are those
that do not change the result of the la to chr function. Only the token generation
rules satisfy this property. Since they only generate tokens and these tokens do not

24

Leslie De Koninck

appear in their antecedents, these rules can fire only finitely many times before a
final Logical Algorithms state σi∗ is reached.
Finally, we state two theorems that essentially are the same as the lemmas above,
except that they do take into account rule priorities.
Theorem 4
LA

For every reachable Logical Algorithms state σi it holds that if σi ֌T (P ) σj , then
either it holds that la to chr(σi ) = la to chr(σj ) or there exists a finite CHR derivaωp

ωp

tion la to chr(σi ) = h∅, S, true, T in ֌P hC, S ′ , true, T ′ in ֌∗P h∅, S ′′ , true, T ′ in′ =
la to chr(σj ) consisting of an Apply transition, followed by zero or more Introduce
transitions.
Theorem 5
For every reachable CHRrp state σi and reachable Logical Algorithms state σi′ with
LA

la to chr(σi′ ) = σi , there exists a finite Logical Algorithms derivation σi′ ֌∗T (P ) σi′∗
ωp

ωp

with la to chr(σi′∗ ) = σi such that if σi = h∅, S, true, T in ֌P hC, S ′ , true, T ′ in ֌∗P
h∅, S ′′ , true, T ′ in′ = σj where the derivation consists of a single Apply transiLA

tion, followed by zero or more Introduce transitions, then σi′∗ ֌T (P ) σj′ with
la to chr(σj′ ) = σj and if σi is a final state then σi′∗ is also a final state.
Proof
Both theorems are implied by Lemmas 4 and 5, combined with the fact that in
corresponding states, corresponding rules can fire which have the same priority.
Therefore, the highest priority applicable rule instances are also equal in corresponding states.
5 Implementing CHRrp , the Logical Algorithms way
This section presents a new implementation for CHRrp , based on the implementation proposal for Logical Algorithms presented in (Ganzinger and McAllester 2002),
as well as on the scheduling algorithm presented in (De Koninck 2007). The purpose
of this implementation is not to replace our existing CHRrp implementation as presented in (De Koninck et al. 2008), but to support a new meta-complexity theorem
for CHRrp , based on the result for Logical Algorithms, and extended towards the
full CHRrp language. This includes in particular support for non-ground constraints
and a built-in constraint theory. We note that a better worst case complexity for
certain operations is not always worthwhile in practice due to larger constant factors
in the average case. Also, the proposed implementation may not always achieve a
better complexity than the existing implementation. The main purpose remains to
have a relatively straightforward way to derive for a given CHRrp program, a bound
that is guaranteed to be an upper bound for at least the implementation proposed.
Since the meta-complexity result is insensitive to constant factors, we can present
the new implementation as a source-to-source transformation to regular CHR.
The proposed implementation consists of the compilation of the CHRrp rules

Logical Algorithms meets Constraint Handling Rules

25

of the input program into regular CHR rules in which matching is made explicit,
combined with a scheduler module that is responsible for the execution control.
The implementation is correct if it is executed according to the refined operational semantics of CHR (Duck et al. 2004), which describes the execution strategy followed by most current CHR implementations. We have based our implementation on the high-level implementation proposal for Logical Algorithm of
(Ganzinger and McAllester 2002), extended where necessary to support general
built-in constraints. By using a CHR implementation with advanced indexing support, like for example the K.U.Leuven CHR system (Schrijvers and Demoen 2004),
our implementation also offers strong complexity guarantees that facilitate a new
meta-complexity theorem for CHRrp , similar to the one for Logical Algorithms (see
Section 6). In the following, we make use of Prolog as CHR’s host language, but
the implementation can easily be adapted to work with a different host language.

5.1 Overview
The implementation is based on a form of lazy (on-demand) matching with retainment of previously computed partial matches. It combines the concept of alpha
and beta memories from the RETE algorithm (Forgy 1982), with lazy matching
as for example implemented by the LEAPS algorithm (Miranker et al. 1990).4 The
basic idea is as follows. A new constraint can function both as a single headed
partial or full match, and as an extension of an existing partial match into either a
new (larger) partial match or a full match. In order to extend partial matches, all
previously computed matches are stored. A scheduler decides which partial match
is extended with which constraint, or which full match has its corresponding rule
instance fired. More details on the scheduler are given in Section 5.3.
First, to simplify the presentation, we propose an alternative syntax for CHRrp
rules. An intermediate form CHRrp rule looks as follows:
p :: r @ s1 A1 , . . . , sn An ⇐⇒ B
where si ∈ {+, −, ?} and Ai is an atom for 1 ≤ i ≤ n. If si = + or si = − then
Ai must be a CHR constraint and if si =? then Ai must be a built-in constraint.
An intermediate form CHRrp rule corresponds to a regular CHRrp rule as follows:
a term +A corresponds to a kept head A, a term −A corresponds to a removed
head A, and a term ?A corresponds to a conjunct of the rule guard. The main
advantage of the intermediate form is that it supports specifying a join order for
the heads, as well as an evaluation order for the guards. In particular it supports
specifying the evaluation of part of the guard after having computed only a partial
rule match. The intermediate form gives us the same syntactical flexibility as exists
in the Logical Algorithms language where comparisons are interleaved with the
(kept and removed) user-defined antecedents.

4

Most current CHR systems, including the K.U.Leuven CHR system and the CHRrp system of
(De Koninck et al. 2008), use a variant of the LEAPS algorithm for rule matching.

26

Leslie De Koninck

Consider, in general, a simpagation rule of the form
p :: r @ H1 , . . . , Hi \Hi+1 , . . . , Hn ⇐⇒ g | B
where the guard g is a conjunction of atomic guards g1 , . . . , gm . We can rewrite this
rule in intermediate form syntax (amongst others) as follows:
p :: r @ + H1 , . . . , +Hi , −Hi+1 , . . . , −Hn , ?g1 , . . . , ?gm ⇐⇒ B
In the following, we assume that all rules have the following form
p :: r @ ± H1 , ?g1 , ±H2 , ?g2 , . . . , ±Hn , ?gn ⇐⇒ B
where ± means + or −. Each gi (1 ≤ i ≤ n) can be a conjunction of primitive
built-in constraints, and can in particular also be equal to true. The transformation
from regular CHRrp syntax to intermediate form syntax can be done automatically
using the above transformation schema, or by hand.
Using terminology similar to that of (Ganzinger and McAllester 2002), we refer
to a partial match, matching the heads H1 , . . . , Hi and satisfying the partial guard
g1 ∧ . . . ∧ gi−1 , as a suspended strong prefix firing. If also the partial guard gi is
satisfied, we speak of a regular (or non-suspended ) strong prefix firing. A constraint
matching the next head Hi+1 is called a prefix extension of such a (regular) strong
prefix firing. A prefix firing that consists of all heads is (also) called a (suspended
or regular) rule firing. Here, a rule firing actually means a rule instance that is
fireable. To avoid confusion, we refer to the actual firing of such a rule firing as
firing a rule instance. Every prefix firing contains the left-most head and hence
determines the rule priority. In our implementation, we assume that all guards
are monotone, i.e., once they are entailed by the built-in constraint store, they
remain entailed in any later state. This is in fact required by the CHR operational
(and declarative) semantics, although most current CHR systems also support nonmonotone (impure) guards like for example var/1 in CHR on top of Prolog.
5.2 Program-Dependent Part
The program-dependent part of our implementation (i.e., the part that depends on
the actual program to be implemented) consists of rules for
• generating a representation for CHR constraint occurrences and deleting them
when the represented constraint is removed;
• generating and scheduling constraints representing prefix firings, prefix extensions and rule firings and deleting them when a constituent constraint is
removed;
• matching prefix firings with prefix extensions, firing rule instances, and managing suspended prefix and rule firings.
The different types of rules of the program-dependent part are illustrated by using
a running example program, namely Dijkstra’s shortest path algorithm, already
given in the Logical Algorithms language in Example 2 and given here in CHRrp
intermediate form syntax. To illustrate non-trivial head matching, we have added
a rule d1 that removes simple loops from the input graph.

Logical Algorithms meets Constraint Handling Rules

1
1
1
D + 2

::
::
::
::

d1
d2
d3
d4

@
@
@
@

-e(V,_,V),
+source(V),
-dist(V,D1 ),
+dist(V,D),

?true
?true
?true, +dist(V,D2 ), ?(D2 < D1 )
?true, +e(V,C,U), ?true

<=>
<=>
<=>
<=>

27

true.
dist(V,0).
true.
dist(U,D+C).

5.2.1 Constraint Occurrence Representation
rp

Although CHR constraints and CHR constraints obviously have the same syntax
and semantics (i.e., multi-set semantics with non-monotone deletion), we introduce
a new representation for them to allow unambiguous reference, reduce work in
case of constraint reactivation, and support the efficient deletion of those prefix
firings, prefix extensions, and rule firings in which they participate (see further).
For each CHRrp constraint of predicate c/n, we create a set of unique occurrence
representations c_occ_i/(n + 1), one for each occurrence of the predicate in a rule
head. The arguments of a c_occ_i/(n+1) constraint consist of the arguments of the
original c/n constraint, together with a unique constraint identifier that is shared by
all occurrence representations. This identifier is an uninstantiated variable as long
as the constraint is in the store and is instantiated the moment that the constraint
is to be deleted. For each user-defined constraint predicate c/n with m occurrences,
the occurrence representations are generated using rules of the following form.
c(X1 ,...,Xn ) <=> c_occ_1(X1 ,...,Xn ,Id), ..., c_occ_m(X1 ,...,Xn ,Id).

For the example program, these rules look as follows.
source(V) <=> source_occ_1(V,Id).
dist(V,D) <=> dist_occ_1(V,D,Id), dist_occ_2(V,D,Id), dist_occ_3(V,D,Id).
e(V,C,U) <=> e_occ_1(V,C,U,Id), e_occ_2(V,C,U,Id).

5.2.2 RETE Memory Constraints
Regular and suspended prefix firings as well as prefix extensions are represented as
CHR constraints. We call them RETE memory constraints because they coincide
with the alpha and beta memories of the RETE algorithm. The RETE memory
constraints contain all arguments of their constituent CHR constraints, as well
as their identifiers. Each RETE memory constraint moreover has its own unique
identifier. We use the following functors for RETE memory constraints:
• r_pf_i for a regular (non-suspended) prefix firing of rule r, consisting of i
heads, and r_pf_i_suspended for its suspended version
• r_pe_i for a prefix extension, consisting of the i + 1th head of rule r
• r_rf for a (regular) rule firing of rule r and r_rf_suspended for its suspended
version.
If in a rule r, the partial guard after the ith head equals true, then there is no
suspended version of the i-headed prefix firings of r, or of its rule firings if r is an
i-headed rule. In the example program, the following prefix firings, prefix extensions
and rule firings are defined:

28

Leslie De Koninck
•
•
•
•

d1_rf/4
d2_rf/3
d3_pf_1/4, d3_pe_1/3, d3_rf/6 and d3_rf_suspended/6
d4_pf_1/4, d4_pe_1/4 and d4_rf/7
5.2.3 Suspended Prefix and Rule Firings

Suspended prefix and rule firings are converted into regular prefix and rule firings
as soon as the relevant part of the guard is entailed. If on the other hand this partial
guard is disentailed, the suspended prefix or rule firing is removed. Given a rule in
intermediate form syntax
p :: r @ ± H1 , ?g1 , ±H2 , ?g2 , . . . , ±Hn , ?gn ⇐⇒ B
we generate the following rules:
• For each i-headed suspended prefix firing:
r_pf_i_suspended(X1 ,...,Xm ,Id1 ,...,Idi ,SId) <=>
gi | r_pf_i(X1 ,...,Xm ,Id1 ,...,Idi ,SId),
schedule_pf(r_i(Y1 ,...,Yl ),p,SId).
r_pf_i_suspended(X1 ,...,Xm ,Id1 ,...,Idi ,SId) <=> \+ gi | true.

where Y1 , . . . ,Yl are those variables in X1 , . . . ,Xm that also appear in Hi+1
• For each rule firing:
r_rf_suspended(X1 ,...,Xm ,Id1 ,...,Idn ,SId) <=> gn |
r_rf(X1 ,...,Xm ,Id1 ,...,Idn ,SId), schedule_rf(p,SId).
r_rf_suspended(X1 ,...,Xm ,Id1 ,...,Idn ,SId) <=> \+ gn | true.

Note that if gi or gn equals true, then we can apply unfolding to replace occurrences
of respectively r_pf_i_suspended/(m + i + 1) and r_rf_suspended/(m + n + 1) by
the bodies of the corresponding rules above (see (Tacchella et al. 2007)). After this
unfolding step, some of the above rules may be removed. In the example program,
only a rule firing of rule d3 can be suspended. The code below is generated for such
a rule firing.
d3_rf_suspended(V,D1 ,D2 ,Id1 ,Id2 ,SId) <=>
D2 < D1 | d3_rf(V,D1 ,D2 ,Id1 ,Id2 ,SId), schedule_rf(1,SId).
d3_rf_suspended(V,D1 ,D2 ,Id1 ,Id2 ,SId) <=> \+ (D2 < D1 ) | true.

In the second rule above, \+ (C) is a safe approximation of the negation of constraint C, i.e., it is only entailed if constraint C cannot possibly hold. In the Prolog
context, the built-in negation as failure can be used.
Suspended constraints are attached to all guarded variables so that they are
reactivated whenever one of these variables is affected by a built-in constraint. We
assume that both attaching and detaching can be done in constant time, although
certain current CHR implementations like the K.U.Leuven CHR system do not
support detaching in constant time.

Logical Algorithms meets Constraint Handling Rules

29

5.2.4 Scheduling
Each constraint occurrence corresponds to a (potentially suspended) rule firing if
it is the only head of a single headed rule, a (potentially suspended) prefix firing if
it is the first head of a multi-headed rule, and a prefix extension in all other cases.
A conversion between constraint occurrence and rule firing, prefix firing or prefix
extension is made as soon as the constraint in question matches with the head. If
such a match is shown to be impossible, the constraint occurrence is discarded. Let
there be given a head constraint c(X1 , . . . , Xn ). The following function is used to
construct a head match.
(
h[X|Ȳ ], gi
if X is a variable and X ∈
/ vars(X̄)
head match([X|X̄]) =
h[Y |Ȳ ], (Y = X) ∧ gi otherwise
where hȲ , gi = head match(X̄)
head match([]) =h[], truei
Now, for each rule in intermediate form syntax
p :: r @ ± H1 , ?g1 , ±H2 , ?g2 , . . . , ±Hn , ?gn ⇐⇒ B
and for 1 ≤ i ≤ n we generate the rules below where Hi = c(X1′ , . . . , Xn′ ) is
the j th occurrence of the user-defined constraint predicate c/n, h[X1 , . . . ,Xn ], gi =
head match([X1′ , . . . , Xn′ ]), and {Y1 , . . . ,Ym } = vars(Hi ) \ vars({H1 , . . . , Hi−1 }).
• If i = n = 1:
c_occ_j(X1 ,...,Xn ,Id) <=> g | r_rf_suspended(Y1 ,...,Ym ,Id,SId).
c_occ_j(X1 ,...,Xn ,Id) <=> \+ g | true.

• If i = 1 and n > 1:
c_occ_j(X1 ,...,Xn ,Id) <=> g | r_pf_1_suspended(Y1 ,...,Ym ,Id,SId).
c_occ_j(X1 ,...,Xn ,Id) <=> \+ g | true.

• Otherwise, if i > 1:
c_occ_j(X1 ,...,Xn ,Id) <=> g |
r_pe_i − 1(Y1 ,...,Ym ,Id,SId), schedule_pe(r_i − 1(Z1 ,...,Zl ),SId).
c_occ_j(X1 ,...,Xn ,Id) <=> \+ g | true.

where {Z1 , . . . ,Zl } = vars(Hi ) ∩ vars({H1 , . . . , Hi−1 }).
In the above, if g = true then the second rule of each pair of rules can be discarded.
The suspended prefix and rule firings can sometimes be replaced by regular prefix
and rule firings by unfolding (see Section 5.2.3).
In the example program, only the first occurrence of the e/3 constraint has a
non-trivial head match (the first and last argument must be the same). All prefix
and rule firings are followed by the trivial guard true and so we only generate
regular prefix and rule firings. They are scheduled using the schedule_pf/3 and
schedule_rf/2 predicates.
source_occ_1(V,Id) <=> d2_rf(V,Id,SId), schedule_rf(1,SId).

30

Leslie De Koninck

dist_occ_1(V,D,Id) <=> d3_pf_1(V,D,Id,SId), schedule_pf(d3_1(V),1,SId).
dist_occ_2(V,D,Id) <=> d3_pe_1(D,Id,SId), schedule_pe(d3_1(V),SId).
dist_occ_3(V,D,Id) <=> d4_pf_1(V,D,Id,SId), schedule_pf(d4_1(V),D+2,SId).
e_occ_1(V,C,U,Id) <=> V = U | d1_rf(V,C,Id,SId), schedule_rf(1,SId).
e_occ_1(V,C,U,Id) <=> \+ (V = U) | true.
e_occ_2(V,C,U,Id) <=> d4_pe_1(C,U,Id,SId), schedule_pe(d3_1(V),SId).

Prefix firings and extensions are scheduled using a key containing their shared
variables. For example for the prefix firings consisting of the first head of rule d3
and the corresponding prefix extensions consisting of the second head of the same
rule, the key equals d3_1(V).
Similar to the suspended prefix and rule firings, the constraint occurrences are attached to all guarded variables. We again assume that both attaching and detaching
can be done in constant time.
5.2.5 Matching and Firing
The scheduler initiates the firing of a rule instance by asserting a fire/1 constraint,
and the matching of a prefix firing with a prefix extension by asserting a match/2
constraint. These constraints have as arguments the identifiers of the corresponding
RETE memory constraints. After matching a prefix firing with a prefix extension,
a new suspended prefix or rule firing is generated. For a given n-headed rule r with
n > 1 and for 1 ≤ i ≤ n − 2, we generate the following rule
r_pf_i(X1 ,...,Xm ,Id1 ,...,Idi ,SId1 ), r_pe_i(Xm+1 ,...,Xl ,Idi+1 ,SId2 ) \
match(SId1 ,SId2 ) <=> Idi+1 \== Id1 , ..., Idi+1 \== Idi |
r_pf_i + 1_suspended(X1 ,...,Xl ,Id1 ,...,Idi+1 ).

and similarly for i = n − 1:
r_pf_n − 1(X1 ,...,Xm ,Id1 ,...,Idn−1 ,SId1 ), r_pe_n − 1 (Xm+1 ,...,Xl ,Idn ,SId2 ) \
match(SId1 ,SId2 ) <=> Idn \== Id1 , ..., Idn \== Idn−1 |
r_rf_suspended(X1 ,...,Xl ,Id1 ,...,Idn ).

A rule firing of an n-headed rule r with body B is fired as follows:
r_rf_i(X1 ,...,Xm ,Id1 ,...,Idn ,SId), fire(SId) <=>
Idr(1) = dead, ..., Idr(l) = dead, B.

where r(1), . . . , r(l) are the indices of the removed heads of the rule (if any). We
furthermore add the following rules at the end of the code, to make sure the CHR
compiler detects that the match/2 and fire/1 constraints are never to be stored.
match(_,_) <=> true.
fire(_) <=> true.
For the example program, the generated code is as follows:
d1_rf(V,C,Id,SId), fire(SId) <=> Id = dead.
d2_rf(V,Id,SId), fire(SId) <=> dist(V,0).
d3_pf_1(V,D1 ,Id1 ,SId1 ), d3_pe_1(D2 ,Id2 ,SId2 ) \ match(SId1 ,SId2 ) <=>

Logical Algorithms meets Constraint Handling Rules

31

Id2 \== Id1 | d3_rf_suspended(V,D1 ,D2 ,Id1 ,Id2 ,SId).
d3_rf(V,D1 ,D2 ,Id1 ,Id2 ,SId), fire(SId) <=> Id1 = dead.
d4_pf_1(V,D,Id1 ,SId1 ), d4_pe_1(C,U,Id2 ,SId2 ) \ match(SId1 ,SId2 ) <=>
Id2 \== Id1 | d4_pf(V,D,C,U,Id1 ,Id2 ,SId), schedule_rf(D+2,SId).
d4_rf(V,D,C,U,Id1 ,Id2 ,SId), fire(SId) <=> dist(U,D+C).
match(_,_) <=> true.
fire(_) <=> true.

5.2.6 Clean-up
Whenever a constraint’s identifier variable is instantiated, its occurrence representations, as well as those RETE memory constraints in which it participates, are
removed. The rules look as follows.
• For the ith occurrence representation for constraint predicate c/n:
c_occ_i(X1 ,...,Xn ,Id) <=> nonvar(Id) | true.

• For an i-headed suspended prefix firing of rule r:
r_pf_i_suspended(X1 ,...,Xm ,Id1 ,...,Idi ,SId) <=> nonvar(Id1 ) | true.
...
r_pf_i_suspended(X1 ,...,Xm ,Id1 ,...,Idi ,SId) <=> nonvar(Idi ) | true.

• For an i-headed regular prefix firing of rule r:
r_pf_i(X1 ,...,Xm ,Id1 ,...,Idi ,SId) <=> nonvar(Id1 ) | remove_pf(SId).
...
r_pf_i(X1 ,...,Xm ,Id1 ,...,Idi ,SId) <=> nonvar(Idi ) | remove_pf(SId).

• For a prefix extension of an i-headed prefix firing of rule r:
r_pe_i(X1 ,...,Xm ,Id,SId) <=> nonvar(Id) | remove_pe(SId).

• For a suspended rule firing of an n-headed rule r:
r_rf_suspended(X1 ,...,Xm ,Id1 ,...,Idn ,SId) <=> nonvar(Id1 ) | true.
...
r_rf_suspended(X1 ,...,Xm ,Id1 ,...,Idn ,SId) <=> nonvar(Idn ) | true.

• For a regular rule firing of an n-headed rule r:
r_rf(X1 ,...,Xm ,Id1 ,...,Idn ,SId) <=> nonvar(Id1 ) | remove_rf(SId).
...
r_rf(X1 ,...,Xm ,Id1 ,...,Idn ,SId) <=> nonvar(Idn ) | remove_rf(SId).

The predicates remove_pf/1, remove_pe/1 and remove_rf/1 remove respectively
a prefix firing, prefix extension and rule firing from the schedule. The following
clean-up rules are generated for the example program.
source_occ_1(V,Id)
dist_occ_1(V,D,Id)
dist_occ_2(V,D,Id)
dist_occ_3(V,D,Id)

<=>
<=>
<=>
<=>

nonvar(Id)
nonvar(Id)
nonvar(Id)
nonvar(Id)

|
|
|
|

true.
true.
true.
true.

32

Leslie De Koninck

e_occ_1(V,C,U,Id)
e_occ_2(V,C,U,Id)

<=> nonvar(Id) | true.
<=> nonvar(Id) | true.

d1_rf(V,C,Id,SId)
d2_rf(V,Id,SId)
d3_pf_1(V,D1 ,Id1 ,SId)
d3_pe_1(D2 ,Id2 ,SId)
d3_rf(V,D1 ,D2 ,Id1 ,Id2 ,SId)
d3_rf(V,D1 ,D2 ,Id1 ,Id2 ,SId)
d4_pf_1(V,D,Id1 ,SId)
d4_pe_1(C,U,Id2 ,SId)
d4_rf(V,D,C,U,Id1 ,Id2 ,SId)
d4_rf(V,D,C,U,Id1 ,Id2 ,SId)

<=>
<=>
<=>
<=>
<=>
<=>
<=>
<=>
<=>
<=>

nonvar(Id)
nonvar(Id)
nonvar(Id1 )
nonvar(Id2 )
nonvar(Id1 )
nonvar(Id2 )
nonvar(Id1 )
nonvar(Id2 )
nonvar(Id1 )
nonvar(Id2 )

|
|
|
|
|
|
|
|
|
|

remove_rf(SId).
remove_rf(SId).
remove_pf(SId).
remove_pe(SId).
remove_rf(SId).
remove_rf(SId).
remove_pf(SId).
remove_pe(SId).
remove_rf(SId).
remove_rf(SId).

d3_rf_suspended(V,D1 ,D2 ,Id1 ,Id2 ,SId) <=> nonvar(Id1 ) | true.
d3_rf_suspended(V,D1 ,D2 ,Id1 ,Id2 ,SId) <=> nonvar(Id2 ) | true.

5.3 Program-Independent Part: the Scheduler
The scheduler implements the schedule_rf/2, remove_rf/1, schedule_pf/3,
remove_pf/1, schedule_pe/2 and remove_pe/1 predicates. It furthermore implements the execute/0 predicate which retrieves and executes the highest priority
scheduled task. This task either is the firing of a rule instance by asserting a fire/1
constraint, or the matching of a prefix firing with a prefix extension by asserting a
match/2 constraint. The execute/0 predicate recursively calls itself until no more
tasks are scheduled. It is first called after processing the initial goal.
For the implementation of the scheduler, we use a variant of the scheduling algorithm presented in (De Koninck 2007). This algorithm can be used to maintain
which prefix firings are still to match with which prefix extensions. It is roughly
based on the W(r, t) data structures used in (Ganzinger and McAllester 2002). Such
a data structure consists of a series (implemented as a linear linked list) of prefix
blocks, which are sets of prefix firings and (apart from the last one) are associated
with a prefix extension.
The semantics of the W(r, t) data structure is that the prefix firings of a given
prefix block are still to match with the prefix extension associated to it, as well
as with all prefix extensions associated to subsequent prefix blocks. The last prefix
block has no associated prefix extension, and represents those prefix firings that have
been matched with all prefix extensions and hence are passive (or completed using
the terminology of (Ganzinger and McAllester 2002)). Whenever a prefix extension
is deleted, its prefix block is merged with the next prefix block.
There is one W(r, t) data structure for each prefix length of each rule and for
each combination of arguments shared between a prefix firing and prefix extension.
Each prefix block is represented as a (local) priority queue whose items are the
block’s prefix firing. The highest priority item of each prefix block, together with
its associated prefix extension, is also represented in a global priority queue. This
prefix block representative is updated whenever the highest priority prefix firing
of the prefix block is removed, a new prefix firing has the highest priority, or the

Logical Algorithms meets Constraint Handling Rules

33

associated prefix extension is removed. The global priority queue furthermore contains a representative for each rule firing. The reason for using two layers of priority
queues is to reduce the amount of work needed when the prefix firings of a prefix
block all become passive due to a prefix extension removal. It is the global priority
queue that determines the next task to perform, i.e., matching a prefix firing with
a prefix extension, or firing a rule instance.
In the context of CHRrp , built-in constraint (in particular equality constraints) on
the arguments shared between a prefix firing and extension, may require merging of
W(r, t) data structures. The data structure of (De Koninck 2007) supports schedule merges in quasi constant time. The most notable difference with the W(r, t)
data structure of (Ganzinger and McAllester 2002) is that the prefix blocks form a
circular linked list. Using this representation, merging schedules consists of crosslinking the circular lists and reactivating the prefix firings that were passive before
the merge. Special care is taken to prevent both that a prefix firing is being matched
with the same prefix extension more than once, and that a prefix firing ‘misses’ a
prefix extension.
One consequence of using a circular linked list instead of a linear one to represent
the prefix blocks, is that it is unclear (or more precisely, too expensive to decide)
which prefix firings become passive whenever a prefix extension is deleted. Therefore, this decision is postponed until the scheduler tries to match the prefix firing
with the next prefix extension in line. For complexity reasons, it is important that all
prefix firings that have simultaneously been reactivated, and have not been matched
with a prefix extension since this reactivation, are simultaneously made passive in
time independent of the number of prefix firings affected. In (De Koninck 2007),
a so-called element schedule based on a stack is proposed to supports this. In our
context, we need an element schedule that is based on priority queues. It works as
follows.
We use three types of priority queues. The first one is a single global priority
queue which contains an item for each rule firing, for each active prefix firings that
either has not been passive before or has been matched with at least one prefix
extension since its last activation, and finally, for each set of prefix firings that have
been simultaneously activated and have not been matches with a prefix extension
since. A second type of priority queues is called a local queue and represents the
above mentioned sets of prefix firings. Finally, the third type of queues is the passive
queue which contains an item for each passive (completed) prefix firing. There is
one passive queue for each schedule. Essentially, we again use two layers of priority
queues. Whenever a set of previously passive prefix firings, represented as a passive
priority queue, is reactivated because of a new prefix extension or because of a
schedule merge, this passive priority queue becomes a local priority queue and has
a representative inserted into the global priority queue. If such a representative
is the highest priority item in the global priority queue, and an execute/0 call
is made, then the highest priority prefix firing of the represented local priority is
removed and dealt with as an ordinary prefix firing. The representatives of local
priority queues are updated (and potentially removed) similarly to how this is done
in the W(r, t) data structure of (Ganzinger and McAllester 2002).

34

Leslie De Koninck

global queue
prefix block
{PF1 ,PF2 ,PF3 }
PF1
PE1
RF1
rule firing
LQ1
{PF4 ,PF5 }
PE2
PF4
local queue
passive queue
PF8
PF5
PF6
PF2
RF2
PF7
PF3

Figure 1. Example schedule with global, local and passive priority queues
Example 8
Figure 1 illustrates the prefix blocks, the different types of priority queues, and their
contents. The global queue, which is shared by all schedules, contains the rule firings
RF 1 and RF 2 , the prefix firings PF 1 , PF 4 , PF 5 and PF 8 (the last of which belongs
to another schedule), and the local queue representative LQ 1 . The represented local
queue contains the prefix firings PF 2 and PF 3 which are by definition also in the
same prefix block. The schedule’s passive queue contains the prefix firings PF 6 and
PF 7 . The schedule has two prefix blocks, which are associated with respectively
the prefix extensions PE 1 and PE 2 .
Using our approach, the cost of deleting items from the global priority queue can
be amortized to one of the following events: a new rule firing, a new prefix firing, a
new prefix extension (for each representative of a local priority queue), or a match
between a prefix firing and a prefix extension (which corresponds to either a new
larger prefix firing, or a rule firing).
In (Ganzinger and McAllester 2002), retrieving the schedule for a given prefix
firing or prefix extension is done by hashing. In our approach, we use a variant
of hashing, which we call non-ground hashing and which consists of first replacing
all variables by a unique identifier, and then using the resulting (ground) term for
hashing. Unifications may require rehashing the affected keys and potentially also
the merging of schedules.
5.4 Priority Queues
A priority queue or heap is a data structure that contains a set of prioritized items
and supports the following operations: inserting and removing an item, finding a
highest priority item and merging with another queue. The implementation proposal
in (Ganzinger and McAllester 2002) suggests the use of two types of priority queues,
one for the fixed priorities, where each of the supported operations takes constant
time, and Fibonacci heaps for the dynamic priorities.
Fibonacci heaps (Fredman and Tarjan 1987) are a type of priority queue that of-

Logical Algorithms meets Constraint Handling Rules

35

fer O(1) amortized time insertion, heap merging and finding a highest priority item,
and O(log n) amortized time item removal with n the number of items in the queue.
It is suggested in (Ganzinger and McAllester 2002) that by using only one node per
priority, using linked lists to represent the items that share this priority, the item
removal cost can be reduced to O(log N ) with N the number of distinct priorities.
However, this increases the cost of heap merging from O(1) for a single merge operation to a total cost of O(n log N ) for merging heaps when there are n items in total
and N distinct priorities (as is shown in an Appendix of (De Koninck et al. 2007a)).
A CHR implementation of Fibonacci heaps is described in (Sneyers et al. 2006a).
It can easily be extended to support multiple heaps that can be merged and to use
only one node for each distinct priority per heap.

6 A New Meta-Complexity Result for CHRrp
In this section, we give a new meta-complexity result for CHRrp . It extends the
result via translation to Logical Algorithms, by also supporting built-in constraints
and non-ground CHR constraints. We make the following assumptions:
• Hash tables support O(1) insertion, removal, and retrieval of all elements that
match a given (ground) key.
• The inverse of the Ackermann function (α(n)) is a constant.
The first assumption is also made in (Ganzinger and McAllester 2002) and holds
on average as long as the hash function is good enough. The second assumption is
needed for our scheduling data structure (De Koninck 2007) which internally makes
use of the union-find algorithm. The inverse of the Ackermann function is positive
and less than 5 for all practical purposes.
We start by looking at the complexity of the different operations supported by
our scheduler.
Lemma 6 (Scheduler Costs)
Let N be the number of distinct priorities, and assume that a priority queue merge
takes some abstract time T , then the schedule operations have the following amortized cost:
• O(1) and O(log N ) for each schedule_pf/3, remove_pf/1, remove_pe/1,
remove_rf/1 and execute/0 operation involving respectively a static and
dynamic priority rule
• O(T + 1) and O(T + log N ) for each schedule_pe/2 operation involving
respectively a static and dynamic priority rule
• O(1) for each schedule merge and schedule_rf/2 operation
Proof
We only consider the costs related to the priority queue operations. The other costs
are shown to be (quasi) constant in (De Koninck 2007). We now look at the different
operations in detail:

36

Leslie De Koninck

• A schedule_pf/3 call consists of inserting the new prefix firing into the global
priority queue. We also account to this event, the cost of making the new prefix
instance passive the first time. That operation consists of a removal from the global
priority queue and an insertion into the schedule’s passive queue. The total cost is
O(1) if the element has a static priority, and O(log N ) if it has a dynamic priority.
• A schedule_pe/2 call requires the insertion of a new representative for the local
priority queue of reactivated prefix firings, into the global priority queue. We also
take into account here, the cost of making all the reactivated prefix firings passive
that have not been matched with a prefix extension since the reactivation. That
operation consists of removing the representative and merging the local priority
queue with the schedule’s passive queue. The cost is O(T + 1) for a static priority
rule and O(T + log N ) time for a dynamic priority one.
• A schedule_rf/2 call requires an insertion into the global priority queue which
takes O(1) time.
• A remove_pf/1 call consists of deleting the prefix firing from the global priority
queue, from a local priority queue or from a passive queue. A deletion from a local
queue may moreover require an update of the global queue (removal and insertion).
In total, this takes O(1) time for a static priority rule and O(log N ) time for a
dynamic priority rule.
• A remove_pe/1 call does not require any priority queue operations, and so the cost
is O(1).
• A remove_rf/1 call requires a removal from the global priority queue which takes
O(1) time if it involves a static priority rule and O(log N ) time if it involves a
dynamic priority rule.
• An execute/0 call requires retrieval and potential removal (if the retrieved item
corresponds to a rule firing, or to a prefix firing that becomes passive) of the highest
priority item in the global priority queue. If the retrieved item represents a prefix
firing or set of prefix firings that need to be made passive, the cost of this operation
is already accounted for by a previous schedule_pf/3 or schedule_pe/2 operation.
In such case, we call the execute/0 call unsuccessful. An unsuccessful execute/0
call is followed by another execute/0 call until either such a call is successful, or
the global priority queue is empty and thus a final state is reached. The cost of
all unsuccessful execute/0 calls can be amortized to previous events. If in case
of a successful execute/0 call, the item retrieved from the global priority queue
corresponds to the representative of a local priority queue, the operation requires a
removal of the highest priority item (prefix firing) from this local queue, an insertion
of the prefix firing into the global priority queue, and potentially the insertion of a
new representative for the local queue into the global queue. The cost of a successful
execute/0 call therefore equals O(1) if it involves a static priority rule and O(log N )
otherwise.
• A schedule merge requires the reactivation of the passive prefix firings of the merged
schedules. The cost analysis is similar to that of a schedule_pe/2 call. Moreover,
each schedule merge can be accounted for by at least one schedule_pe/2 call as
the resulting schedule contains at least one prefix extension more than each of the
original schedules, and so the number of schedule merges is bounded by the number

Logical Algorithms meets Constraint Handling Rules

37

of prefix extensions. Therefore, the cost of a single schedule merge can be considered
constant.

In the above lemma, we have made abstraction of the cost of priority queue merge
operations. Such merges take place when the prefix firings in a local priority queue
all become passive. In such an event, the local priority queue is merged with the
schedule’s passive queue. It is easy to see that the cost of merging priority queues
for static priorities takes constant time per merge operation. In Section 5.4 a bound
is given on the total cost of merging Fibonacci heaps with one node per distinct
priority, given the number of items ever inserted into the heaps. The following
lemma makes use of this result.
Lemma 7 (Fibonacci Heap Merging Cost )
The total cost of Fibonacci heap merges is O((Pd + Ad ) · log N ) where Pd is the
number of strong prefix firings of dynamic priority rules, Ad is the number of
constraints that may participate in a dynamic priority rule instance, and N is the
number of distinct rule priorities.
Proof
We count the number of items ever inserted into the local and passive Fibonacci
heaps, and then apply the result of Section 5.4. A local priority queue basically is the
same as a passive priority queue in which items are no longer inserted. Therefore,
a merge between a local queue and a passive queue can be seen as a special case of
a merge between two passive queues and so we only need to consider these passive
priority queues. Each item inserted in such a queue is either a prefix firing that has
never been passive before, or a prefix firing that has been matched with a prefix
extension at least once since its last activation. The total number of these items is
O(Pd +Ad ) because each prefix firing that has been matched with a prefix extension
is by definition a strong prefix firing, and each new prefix firing either results from
matching a (smaller) strong prefix firing and extension and hence corresponds to
a (potentially suspended) strong prefix firing, or consists of a single head in which
case it corresponds to a constraint assertion. Now given the number of items ever
inserted into the passive priority queues, the total cost of merging Fibonacci heaps
hence is O((Pd + Ad ) · log N )).
We are now ready to formulate the new meta-complexity theorem.
Theorem 6
Let As and Ad be the number of assertions of constraints with an occurrence in
respectively a static and dynamic priority rule. Let Ps and Pd be the number of
strong prefix firings of respectively static and dynamic priority rules. The time
complexity of a CHRrp program executed using our implementation is
ask
tell
ask
O((1 + CB
) · (As + Ps + (Ad + Pd ) · log N ) + B · CB
· (K + CB
· S))
ask
where N is the number of distinct priorities, CB
is the cost of evaluating a builttell
in ask constraint, CB is the cost of solving a built-in tell constraint, and B is

38

Leslie De Koninck

the number of built-in tell constraints asserted in rule bodies; K is the maximum
number of distinct combinations (keys) of arguments shared between prefix firings
and extensions in which any given variable occurs, and S is the maximum number of
suspended strong prefix firings (i.e., those that are followed by a non-trivial guard)
and suspended instances of constraint occurrences (i.e., whose arguments are not
mutually distinct variables) in which any given variable occurs.
Proof
Each new CHR constraint causes the creation of constraint occurrences which are
converted into RETE memory constraints as soon as the implicit guard on the
constraint arguments is entailed (i.e., the constraint matches the head in question). These RETE memory constraints are scheduled using schedule_pf/3 for
the single-headed prefix firings, schedule_rf/2 for the single-headed rule firings,
and schedule_pe/2 for the prefix extensions. The total cost of these operations,
including the cost of priority queue merges (for the schedule_pe/2 calls), equals
O((1 + Cbask ) · (As + (Ad + Pd ) log N )). Each constraint deletion causes the deletion
of those RETE memory constraints in which the deleted constraint participated.
The total cost related to deletion therefore is O(As + Ps + (Ad + Pd ) log N ). Each
prefix firing is inserted into its schedule at most once and hence it can also be
removed from this schedule only once (when one of its constituent constraints is
removed). Those prefix firings that consist of at least two heads, correspond to a
strong prefix firing as they are generated at a priority higher or equal to that of the
highest priority rule firing. Thus, using Lemma 6 and including the cost of checking
the relevant parts of the guard, the cost for inserting (and deleting) these prefix
firings is O((1 + Cbask ) · (Ps + Pd log N )).
A built-in tell constraint is processed as follows. The keys used to identify the
schedules and that are affected by the built-in constraint, are rehashed. If the builtin constraint causes two or more schedules to have the same key, these schedules are
merged. The cost of rehashing is proportional to the number of affected keys and the
cost of a schedule merge is constant by Lemma 6. A built-in constraint moreover
requires the reactivation of the suspended prefix firings and rule firings, as well
as those constraint occurrences for which it is not decided whether they match
with the corresponding head or not. The reactivated prefix and rule firings have
their guard checked and are potentially scheduled as regular (non-suspended) prefix
and rule firings. The reactivated constraint occurrences also have their (implicit)
guard checked, and are potentially scheduled as single-headed prefix firings, singleheaded rule firings, or prefix extensions. The cost of the scheduling operations was
already taken into account above. The remaining cost per built-in tell constraint is
O(Cbtell · (K + Cbask · S)).
The values of S and K might be difficult to determine in practice, but we can
use an upper bound of O(As + Ad + Ps + Pd ) for both parameters. The reasoning
for S is that the number of suspended prefix firings is smaller than the number of
prefix firings and the number of suspended constraint occurrences is smaller than
the number of assertions times the number of rule heads in the program. For K,

Logical Algorithms meets Constraint Handling Rules

39

we have that the number of keys shared between prefix firings and extensions is
limited by the total number of prefix firings and extensions. We have used the cost
of solving a built-in tell constraint as an upper bound on the number of variables
that are affected.
The meta-complexity theorem also applies to (regular) CHR programs, which
can be seen as a special case of CHRrp programs in which all rules have the same
(static) priority; see Theorem 3 of (De Koninck et al. 2007b) for more details.
6.1 Examples
We illustrate the meta-complexity theorem on some examples, and compare with
the results obtained by using the approach of (Frühwirth 2002b).
Example 9 (Less-or-Equal )
The less-or-equal (leq) program is classic CHR example. It implements a lessthan-or-equal-to constraint by eventually translating it into equality constraints. A
CHRrp implementation of the program consists of the following rules.
1
2
2
3

::
::
::
::

idempotence
reflexivity
antisymmetry
transitivity

@
@
@
@

leq(X,Y) \ leq(X,Y) <=> true.
leq(X,X) <=> true.
leq(X,Y), leq(Y,X) <=> X = Y.
leq(X,Y), leq(Y,Z) ==> leq(X,Z).

Given an initial goal consisting of n leq/2 constraints where the arguments are
taken from a set of n distinct variables, we derive the following values for the
parameters:
• Ps : the number of strong prefix firings is O(n2 ) for the idempotence rule, O(n)
for the reflexivity rule, O(n2 ) for the antisymmetry rule, and O(n3 ) for
the transitivity rule. These numbers are found by looking at the degrees of
freedom for each constraint occurrence, based on the domain of the arguments,
and given those arguments that are already fixed by the left-most heads. For
example for the transitivity rule, we know that there are O(n2 ) constraints
matching the first head, and O(n) constraints matching the second head,
given the first. Our reasoning is based on the fact that at priority 2 and lower
(numerically larger), all leq/2 constraints have set semantics because of the
idempotence rule.
• As : the number of leq/2 constraints asserted is O(n3 ) (by the transitivity
rule).
• B: the number of built-in constraints is bounded by the number of rule firings
of the antisymmetry rule, and hence is O(n2 ).
• K: the schedule keys are the combination of X and Y in both the antisymmetry
rule and the idempotence rule, and Y in the transitivity rule. There are
at most O(n) different keys in which any given variable occurs.
• S: for any variable, and in a state in which a built-in constraint can be asserted, there are up to O(n) suspended instances of the leq/2 occurrence in
the reflexivity rule. There can be no suspended prefix or rule firings.

40

Leslie De Koninck
• Cbask and Cbtell : the cost of evaluating a built-in ask constraint and the cost
of solving a built-in tell constraint is constant (at least for the given query
pattern).

Filling in these parameters in the formula given by Theorem 6 gives us a worst case
time complexity of
O((1 + 1) · (n3 + n3 + (0 + 0) · log 3) + n2 · 1 · (n + 1 · n)) = O(n3 )
This corresponds to the actual worst-case complexity for an initial goal of the form
{leq(X1,X2 ), . . . , leq(Xn−1,Xn ), leq(Xn,X1 )}
The approach of (Frühwirth 2002b) does not apply since the transitivity rule is
a propagation rule and hence no suitable ranking function can be found.
Example 10 (Merge Sort )
Consider the CHRrp implementation of the merge sort algorithm, first given in
Example 6 (Section 4) and repeated here for easy reference.
1 :: ms1 @ arrow(X,A) \ arrow(X,B) <=> A < B | arrow(A,B).
2 :: ms2 @ merge(N,A), merge(N,B) <=> A < B | merge(2*N+1,A), arrow(A,B).
3 :: ms3 @ number(X) <=> merge(0,X).

We show that the total runtime of the algorithm is O(n log n) given an initial goal
consisting of n number/1 constraints.
No new number/1 constraints are ever asserted. Rule ms3 converts one number/1
constraint into one merge/2 constraint each time it fires. The number of (strong)
prefix firings for rule ms3 hence is O(n). Rule ms2 decreases the number of merge/2
constraints by one and so it can fire n − 1 times. In any state, there are at most
two merge/2 constraints with the same first argument. This invariant holds in the
initial state because there are no merge/2 constraints in the initial goal and rule
ms2 can fire after each new merge/2 constraint assertion, enforcing the invariant.
Because of the invariant, the number of prefix firings for rule ms2 is limited to O(n).
Using similar reasoning it holds that in any state, there are at most two arrow/2
constraints in the store with the same first argument. Now we define that in a
given state, two numbers X1 and Xm are connected by a chain of length m − 1
if the following constraints are in the store: arrow(X1,X2 ), arrow(X2,X3 ), . . . ,
arrow(Xm−1,Xm ). At priority 2 it holds that for each merge(N ,X) constraint
in the store, the maximal length of a chain starting in X is N . Indeed, this holds
for the initial merge(0, ) constraints and if it holds for merge(N , ) constraints,
it also holds for merge(2 · N + 1, ) constraints, because when such a constraint
is asserted, two chains of length N are linked with an extra arrow/2 constraint
and merged by up to 2 · N firings of rule ms1. Two merge(N , ) constraints are
combined into a merge(2 · N + 1, ) constraint, so the n merge(0, ) constraints
asserted by rule ms3 are replaced by n/2 merge(1, ) constraints, which in turn are
combined into n/4 merge(3, ) constraints and so on until finally 1 merge(n−1, )
constraint remains. The sum of all N in these merge(N , ) constraints is O(n log n).

Logical Algorithms meets Constraint Handling Rules

41

Rule ms1 fires O(N ) times after every new merge(N , ) constraint assertion and
because there are at most two arrow/3 constraints with the same first argument,
there are O(n log n) strong prefix firings of rule ms1.
In conclusion, for an initial goal consisting of n number/1 constraints, there are
O(n log n) strong prefix firings for rule ms1, O(n) for rule ms2 and O(n) for rule ms3.
Using the meta-complexity theorem, which simplifies to the one for Logical Algorithms because there are no built-in tell constraints, the total runtime is O(n log n),
which is also a tight complexity bound. We now compare this result with the result
found by using the meta-complexity theorem of (Frühwirth 2002b).
Using a similar analysis as above, we can derive that D = O(n log n) and cmax =
O(n) where n is the number of number/1 constraints in the query. Note that in
Theorem 4.2 of (Frühwirth 2002b), a worst case upper bound of cmax = O(c + D)
is used, with c the number of constraints in the query, which becomes cmax =
O(n log n) in this example. The bound we use is tight, i.e., cmax = Θ(n). The cost
of head matching (OHr ), guard checking (OGr ), adding built-in constraints (OCr ),
and adding and removing CHR constraints (OBr ), can all be assumed constant.
The number of heads nr of a rule r ∈ P is at most 2. Filling in these numbers, we
derive a total worst case complexity of O(n3 log n), which is clearly suboptimal.
Example 11 (Dijkstra’s Shortest Path)
A Logical Algorithms implementation of Dijkstra’s shortest path algorithm is given
in (Ganzinger and McAllester 2002) and in Example 2. A very similar implementation in CHRrp is given in (De Koninck et al. 2007b) and shown below.
1 :: d1 @ source(V) ==> dist(V,0).
1 :: d2 @ dist(V,D1 ) \ dist(V,D2 ) <=> D1 < D2 | true.
D + 2 :: d3 @ dist(V,D), e(V,C,U) ==> dist(U,D+C).

Given a goal consisting of one source/1 constraint and e e/3 constraints, the
runtime complexity of this implementation is O(e log e). The analysis is essentially the same as the one for the Logical Algorithms implementation as given
in (Ganzinger and McAllester 2002); see also Example 2.
6.2 Comparison with the Logical Algorithms meta-complexity result
In (De Koninck et al. 2007a), we have presented a direct implementation of the
Logical Algorithms language into CHR that satisfies the complexity requirements
needed for the Logical Algorithms meta-complexity result to hold. In this subsection, we show that this implementation has become somewhat obsolete because we
can achieve the same result by combining the translation from Logical Algorithms
to CHRrp of Section 3, with the CHRrp implementation presented in Section 5. We
assume here that the comparison antecedents in Logical Algorithms programs are
scheduled after the corresponding user-defined antecedents in the translation, and
that the guards on the mode indicators (these have the form N 6= p) are scheduled
right after the head to which they apply.

42

Leslie De Koninck

Theorem 7
The time complexity of Logical Algorithms programs executed by first translating
them into CHRrp programs using the translation schema of Section 3, and then
executing the resulting CHRrp program using the implementation of Section 5, is
O(|σ0 |+Ps +(Pd +Ad )·log N ) with S0 , Ps , Pd , Ad and N as defined in Section 2.3.1.
Proof
The translation of a Logical Algorithms program P consists of two parts as defined
in Section 3. The first part, denoted by TS/D (P ), contains for each user-defined
predicate a/n the following rules:
1 :: ar (X̄, M ) \ a(X̄) ⇐⇒ M 6= n | true
1 :: ar (X̄, n), a(X̄) ⇐⇒ ar (X̄, b)
2 :: a(X̄) ⇐⇒ ar (X̄, p)
1 :: ar (X̄, M ) \ del(a(X̄)) ⇐⇒ M 6= p | true
1 :: ar (X̄, p), del(a(X̄)) ⇐⇒ ar (X̄, b)
2 :: del(a(X̄)) ⇐⇒ ar (X̄, n)
It is easy to see that for an initial goal containing no constraints of the form
ar (X̄, M ) and since these are the only rules that assert such a constraint, in any
state it holds that if ar (X̄, M1 )#i1 and ar (X̄, M2 )#i2 are in the CHR constraint
store, then i1 = i2 and M1 = M2 . This implies that the number of strong prefix
firings for these rules is bounded by the number of assertions of a(X̄) or del(a(X̄)).
The second part of the translation, denoted by TR (P ), contains for each Logical
Algorithms rule
r @ p : A1 , . . . , An ⇒ C
a set of rules
p + 2 :: rρ @ H =⇒ g1 , g2 | C ′
as shown in the translation schema of Section 3.1.2. Amongst these rules is one,
say rρ′ , with a maximal number of heads, namely as many as there are user-defined
antecedents in A1 , . . . , An . Because the (implicit and explicit) guards on the mode
indicators of the head constraints are scheduled as soon as they are decidable, and
because the comparisons are scheduled at corresponding places, it is easy to see
that the number of strong prefix firings of rule rρ′ is the same as the number of
strong prefix firings of Logical Algorithms rule r. The other rρ rules are restricted
versions of rρ′ and therefore have at most as many strong prefix firings as rρ′ .
The assertions with occurrences in dynamic priority rules are of the form ar (X̄, ).
The set and deletion semantics rules ensure that the number of these assertions is
the same in the original program and in its translation. Finally, we note that the
number of assertions with occurrences in a static priority rule, As , is bounded by the
number of assertions in the initial goal |σ0 | plus the number of rule firings times the
maximal number of body literals in any rule. Therefore, As = O(|σ0 |+Ps +Pd ). Now
using our new meta-complexity result for CHRrp (Theorem 6), we derive that the

Logical Algorithms meets Constraint Handling Rules

43

total runtime complexity of the translated program is O(|σ0 |+Ps +(Pd +Ad )·log N ).

6.3 Comparison with the “As Time Goes By” approach
In Section 2.3.3 we already briefly compared the Logical Algorithms meta-complexity
theorem with the theorem given by Frühwirth in (Frühwirth 2002b). In this subsection, we make the comparison complete by also considering built-in constraints,
using the new meta-complexity theorem presented in Section 6.
Let there be given a CHRrp program P in which each rule has the same (static)
priority. Theorem 3 in (De Koninck et al. 2007b) states that such a CHRrp program and its corresponding CHR program (which is found by removing the rule
priorities) have the same derivations. Therefore, such programs are suitable for comparing the result of (Frühwirth 2002b) with the result of Theorem 6 in Section 6.
In Section 2.3.3 we have already shown that the number of strong prefix firings is
P
r
where D is the derivation length (i.e., the number of rule firO D · r∈P cnmax
ings), and cmax is the maximal number of CHR constraints in the store in any state.
The number of constraint assertions is O(cmax + D). If we assume that the initial
goal does not contain any built-in constraints (as is done in (Frühwirth 2002b)),
then the number of built-in constraints
is O(D). The number of suspended prefix

P
nr
firings is bounded by O
r∈P cmax in any state and the number of suspended assertions by O(cmax ). Now, filling in these parameters in the CHRrp meta-complexity
result gives us that the total runtime complexity is
!
X
nr
O (1 + OC ) · D
(3)
(cmax · OGr )
r∈P

P

where OC = r∈P (OCr ). This formula strongly resembles the result of (Frühwirth 2002b)
which, assuming the cost of head matching OHr and adding and removing CHR
constraints OBr is constant, equals
!
X
nr
O D
(4)
(cmax · OGr + OCr )
r∈P

The difference lies in how built-in tell constraints are dealt with. In our CHRrp
implementation, as well as in any CHR implementation based on the refined operational semantics of CHR, a built-in tell constraint causes the constraints or matches
whose variables are affected, to be reconsidered.5 Because each individual (atomic)
built-in constraint is dealt with separately, this may cost more in total than the
naive approach taken in (Frühwirth 2002b) in which after each rule firing, all constraints or matches are reconsidered once. So, while in certain rather exceptional
cases, a naive approach to dealing with built-in tell constraints might in fact be better than the usual approach of selective reactivation (as can be seen by comparing
5

Which constraints are reactivated depends on the wake-up policy used for the Solve transition,
see also (Schrijvers 2005, Section 5.4.2).

44

Leslie De Koninck

Formulas (3) and (4)), in general we expect the latter approach to be an improvement over the naive one. Moreover, in these exceptional cases, the meta-complexity
theorem of (Frühwirth 2002b) does not apply to optimized CHR implementations
like the K.U.Leuven CHR system, i.e., in these cases it does not overestimate the
actual worst case time complexity.
Noteworthy is that the approach of (Frühwirth 2002b) only considers simplification (and implicitly also simpagation) rules. This restriction is related to the
termination analysis which is used to find an upper bound on the number of rule
applications. However, if we can find such an upper bound by other means, also
propagation rules can be supported. For instance, the termination analysis presented in (Pilozzi and De Schreye 2008) can be used for this purpose.

7 Conclusions
In this paper, we have investigated the relationship between the Logical Algorithms
language and Constraint Handling Rules. We have presented an elegant translation
schema from Logical Algorithms to CHRrp : CHR extended with user-definable rule
priorities. The original program and its translation are shown to be essentially
weakly bisimilar. However, our current CHRrp system (De Koninck et al. 2008)
does not give the complexity guarantees needed for the Logical Algorithms metacomplexity theorem to hold via this translation.
As a first step towards applying the Logical Algorithms meta-complexity result
to CHRrp programs, we have shown how a subclass of CHRrp can be translated
into Logical Algorithms. By using this translation, we can directly apply the metacomplexity theorem for Logical Algorithms to the translated CHRrp programs. A
drawback is that the CHRrp programs that can be translated this way, are restricted
to those that do not make use of an underlying constraint solver.
In order to remedy both the limitation that the translation from Logical Algorithms to CHRrp does not exhibit the required complexity when executing translated Logical Algorithms programs using our CHRrp system, and the restriction
of those CHRrp programs that can be translated to Logical Algorithms and hence
to which the Logical Algorithms meta-complexity result can be applied, we have
proposed a new implementation for the complete CHRrp language that gives strong
complexity guarantees. The implementation is based on the high-level implementation proposal of (Ganzinger and McAllester 2002) as well as on the scheduling data
structure of (De Koninck 2007), and consists of the compilation of CHRrp rules into
(regular) CHR rules, combined with a scheduler that controls the execution. The
implementation supports a new and accurate meta-complexity theorem for CHRrp .
When combining the translation from Logical Algorithms to CHRrp with the new
implementation, the new meta-complexity theorem implies the Logical Algorithms
meta-complexity result. Moreover, it is shown that in general – apart from some
rather exceptional cases, see Section 6.3 – the new theorem is at least as accurate
as the meta-complexity result for CHR given by Frühwirth in (Frühwirth 2002b).
This is illustrated on two non-trivial examples, one of which contains both built-

Logical Algorithms meets Constraint Handling Rules

45

in constraints and propagation rules and therefore cannot be analyzed using the
Logical Algorithms approach or Frühwirth’s result.
7.1 Related Work
The time complexity of programs is in general expressed in terms of the number of
elementary operations, e.g., the number of logical inferences in Prolog, function applications in a functional programming language, or rule applications in a language
such as CHR. However, while in most languages, these elementary operations all
take constant time, this is not the case in a language like CHR where each rule
application results from a complex matching phase.
In this work, we have made a mapping from the number of elementary operations (like prefix and rule firings or constraint assertions) to time complexity.
To the best of our knowledge, and apart from the results in (McAllester 1999;
Ganzinger and McAllester 2001; Ganzinger and McAllester 2002) and (Frühwirth 2002a;
Frühwirth 2002b), there is no other work with a similar goal. There are many
other formalisms though in which elementary operations take more than constant
time. One such formalism is term rewriting, as implemented by the Maude system
(Clavel et al. 1999) or the ACD term rewriting language (Duck et al. 2006). It is
known that AC matching, which is used by most of these languages, is NP-complete.
Another formalism is that of production rule systems like Drools (Proctor et al. 2007)
or Jess (Friedman-Hill 2007). Production rules are in many ways similar to Constraint Handling Rules. However unlike CHR, these systems are not often used as
general purpose programming language, and therefore, algorithmic complexity has
never been much of a concern. More work exists on the derivation of the number of
elementary operations. In the context of CHR, this mostly concerns the number of
rule firings, which is often derived as part of termination analysis (Frühwirth 2000b;
Pilozzi et al. 2007; Voets et al. 2007).
Another related topic is that of space complexity, an issue that is not dealt with
in this paper. In the context of CHR, the memory reuse techniques developed in
(Sneyers et al. 2006b) are crucial to achieve optimal space complexity as is shown in
(Sneyers et al. 2008). The latter also introduces a space complexity meta-theorem
for CHR, stating that the space complexity is O(D + p) where D is the derivation
length and p is the number of propagation rule firings (which takes into account
the size of the propagation history).
7.2 Future Work
For a previous version of this paper (De Koninck et al. 2007a), we have made an
actual implementation for the Logical Algorithms language in CHR. This implementation satisfies the complexity requirements needed for the Logical Algorithms
meta-complexity theorem to hold, when executed using the K.U.Leuven CHR system on top of SWI-Prolog. However, the very large constant factors and the high
memory consumption makes that the system is not very useful in practice. Currently, we have no running version of the alternative implementation for CHRrp

46

Leslie De Koninck

presented in Section 5. The reason is that this implementation proposal is based
on a similar approach as the Logical Algorithms one, and in particular the more
complicated scheduler is expected to be slow in practice. However, we do intend
to investigate the advantages and disadvantages of a lazy RETE based matching
algorithm for CHR(rp ) compared to the LEAPS style matching that is currently
used by almost all systems. A simplified version of the scheduling data structure
of (De Koninck 2007) which would offer less complexity guarantees, but might be
faster in the average case, could be used for this purpose.
We have already mentioned in the related work discussion that a space complexity result for our alternative implementation is currently lacking. The RETE style
matching we used is in general far from optimal as far as memory usage is concerned, in particular compared to LEAPS style matching as is used by most CHR
systems. However, in the CHR context, built-in constraints may require maintaining a propagation history which in the worst case requires as much memory as the
alpha and beta memories in RETE matching. Therefore, it would be interesting to
more formally compare both styles of matching in terms of memory consumption
in the context of CHR.
Acknowledgements
The author would like to thank Tom Schrijvers, Bart Demoen and the anonymous
reviewers for their helpful and insightful comments. This research is funded by a
Ph.D. grant of the Institute for the Promotion of Innovation through Science and
Technology in Flanders (IWT-Vlaanderen).
References
Betz, H. 2007. Relating coloured Petri nets to Constraint Handling Rules. In 4th Workshop on Constraint Handling Rules, K. Djelloul, G. J. Duck, and M. Sulzmann, Eds.
U.Porto, 33–47.
Christiansen, H. 2005. CHR grammars. Theory and Practice of Logic Programming 5, 45, 467–501.
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martı́-Oliet, N., Meseguer, J.,
and Quesada, J. F. 1999. The Maude system. In 10th International Conference on
Rewriting Techniques and Applications, P. Narendran and M. Rusinowitch, Eds. Lecture
Notes in Computer Science, vol. 1631. Springer, 240–243.
De Koninck, L. 2007. Mergeable schedules for lazy matching. Tech. Rep. CW 505,
Department of Computer Science, K.U.Leuven.
De Koninck, L., Schrijvers, T., and Demoen, B. 2007a. The correspondence between
the Logical Algorithms language and CHR. In 23rd International Conference on Logic
Programming, V. Dahl and I. Niemelä, Eds. Lecture Notes in Computer Science, vol.
4670. Springer, 209–223.
De Koninck, L., Schrijvers, T., and Demoen, B. 2007b. User-definable rule priorities
for CHR. In 9th International ACM SIGPLAN Conference on Principles and Practice
of Declarative Programming, M. Leuschel and A. Podelski, Eds. ACM Press, 25–36.
De Koninck, L., Stuckey, P. J., and Duck, G. J. 2008. Optimizing compilation of
CHR with rule priorities. In 9th International Symposium on Functional and Logic
Programming.

Logical Algorithms meets Constraint Handling Rules

47

Duck, G. J., Stuckey, P. J., and Brand, S. 2006. ACD term rewriting. In 22nd
International Conference on Logic Programming, S. Etalle and M. Truszczynski, Eds.
Lecture Notes in Computer Science, vol. 4079. Springer, 117–131.
Duck, G. J., Stuckey, P. J., Garcı́a de la Banda, M., and Holzbaur, C. 2004.
The refined operational semantics of Constraint Handling Rules. In 20th International
Conference on Logic Programming, B. Demoen and V. Lifschitz, Eds. Lecture Notes in
Computer Science, vol. 3132. Springer, 90–104.
Duck, G. J., Stuckey, P. J., and Sulzmann, M. 2007. Observable confluence for
Constraint Handling Rules. In 23rd International Conference on Logic Programming,
V. Dahl and I. Niemelä, Eds. Lecture Notes in Computer Science, vol. 4670. Springer,
224–239.
Forgy, C. L. 1982. Rete: A fast algorithm for the many pattern/many object pattern
match problem. Artificial Intelligence 19, 1, 17–37.
Fredman, M. L. and Tarjan, R. E. 1987. Fibonacci heaps and their uses in improved
network optimization algorithms. Journal of the ACM 34, 3, 596–615.
Friedman-Hill, E. 2007.
JESS 7.0p2: The rule engine for the Java platform.
http://herzberg.ca.sandia.gov/jess.
Frühwirth, T. 1998. Theory and practice of Constraint Handling Rules. Journal of
Logic Programming 37, 1-3, 95–138.
Frühwirth, T. 2000a. Proving termination of constraint solver programs. In New Trends
in Contraints, Joint ERCIM/Compulog Net Workshop, Paphos, Cyprus, October 1999,
Selected papers, K. R. Apt, A. C. Kakas, E. Monfroy, and F. Rossi, Eds. Lecture Notes
in Computer Science, vol. 1865. Springer, 298–317.
Frühwirth, T. 2000b. Proving termination of constraint solver programs. In Joint
ERCIM/Compulog Net Workshop on New Trends in Contraints, K. R. Apt, A. C. Kakas,
E. Monfroy, and F. Rossi, Eds. Lecture Notes in Computer Science, vol. 1865. Springer,
298–317.
Frühwirth, T. 2002a. As time goes by: Automatic complexity analysis of simplification
rules. In 8th International Conference on Principles of Knowledge Representation and
Reasoning, D. Fensel, F. Giunchiglia, D. L. McGuinness, and M.-A. Williams, Eds.
Morgan Kaufmann, 547–557.
Frühwirth, T. 2002b. As time goes by II: More automatic complexity analysis of concurrent rule programs. In Quantitative Aspects of Programming Languages, Selected
Papers. Electronic Notes in Theoretical Computer Science, vol. 59.
Ganzinger, H. and McAllester, D. A. 2001. A new meta-complexity theorem for
bottom-up logic programs. In 1st International Joint Conference on Automated Reasoning, R. Goré, A. Leitsch, and T. Nipkow, Eds. Lecture Notes in Computer Science,
vol. 2083. Springer, 514–528.
Ganzinger, H. and McAllester, D. A. 2002. Logical algorithms. In 18th International
Conference on Logic Programming, P. J. Stuckey, Ed. Lecture Notes in Computer Science, vol. 2401. Springer, 209–223.
Holzbaur, C. and Frühwirth, T. 1998. Constraint Handling Rules reference manual, release 2.2. Tech. Rep. TR-98-01, Österreichisches Forschungsinstitut für Artificial
Intelligence, Wien.
McAllester, D. A. 1999. On the complexity analysis of static analyses. In 6th International Symposium on Static Analysis, A. Cortesi and G. Filé, Eds. Lecture Notes in
Computer Science, vol. 1694. Springer, 312–329.
Miranker, D. P., Brant, D. A., Lofaso, B., and Gadbois, D. 1990. On the performance of lazy matching in production systems. In 8th National Conference on Artificial
Intelligence. AAAI Press / The MIT Press, 685–692.

48

Leslie De Koninck

Pilozzi, P. and De Schreye, D. 2008. Termination analysis of CHR revisited. In 24th
International Conference on Logic Programming, M. Garcı́a de la Banda and E. Pontelli,
Eds. Lecture Notes in Computer Science, vol. 5366. Springer, 501–515.
Pilozzi, P., Schrijvers, T., and De Schreye, D. 2007. Proving termination of CHR in
Prolog: A transformational approach. In 9th International Workshop on Termination,
D. Hofbauer and A. Serebrenik, Eds. 30–33.
Proctor, M., Neale, M., Frandsen, M., Griffith, Jr, S., Tirelli, E.,
Meyer, F., and Verlaenen, K. 2007.
Drools Documentation, Version 4.0.3.
http://www.jboss.com/products/rules.
Schrijvers, T. 2005. Analyses, optimizations and extensions of Constraint Handling
Rules. Ph.D. thesis, K.U.Leuven, Leuven, Belgium.
Schrijvers, T. and Demoen, B. 2004. The K.U.Leuven CHR system: implementation
and application. In First Workshop on Constraint Handling Rules: Selected Contributions, T. Frühwirth and M. Meister, Eds. Ulmer Informatik-Berichte, vol. 2004-01.
Universität Ulm, 1–5.
Schrijvers, T. and Frühwirth, T. 2006. Optimal union-find in Constraint Handling
Rules. Theory and Practice of Logic Programming 6, 1&2.
Sneyers, J. 2008. Optimizing compilation and computational complexity of Constraint
Handling Rules. Ph.D. thesis, K.U.Leuven, Leuven, Belgium.
Sneyers, J., Schrijvers, T., and Demoen, B. 2005. The computational power and
complexity of Constraint Handling Rules. In 2nd Workshop on Constraint Handling
Rules, T. Schrijvers and T. Frühwirth, Eds. Reports CW, vol. 421. Departement of
Computer Science, K.U.Leuven, Belgium, 3–17.
Sneyers, J., Schrijvers, T., and Demoen, B. 2006a. Dijkstra’s algorithm with Fibonacci heaps: An executable description in CHR. In 20th Workshop on Logic Programming, M. Fink, H. Tompits, and S. Woltran, Eds. INFSYS Research Report, vol.
1843-06-02. TU Wien, 182–191.
Sneyers, J., Schrijvers, T., and Demoen, B. 2006b. Memory reuse for CHR. In 22nd
International Conference on Logic Programming, S. Etalle and M. Truszczynski, Eds.
Lecture Notes in Computer Science, vol. 4079. Springer, 72–86.
Sneyers, J., Schrijvers, T., and Demoen, B. 2008. The computational power and complexity of Constraint Handling Rules. http://www.cs.kuleuven.be/∼jon/ – Submitted
to ACM TOPLAS.
Tacchella, P., Meo, M. C., and Gabbrielli, M. 2007. Unfolding in CHR. In 9th
International ACM SIGPLAN Conference on Principles and Practice of Declarative
Programming, M. Leuschel and A. Podelski, Eds. ACM Press, 179–186.
Van Weert, P., Sneyers, J., Schrijvers, T., and Demoen, B. 2006. Extending CHR
with negation as absence. In 3rd Workshop on Constraint Handling Rules, T. Schrijvers and T. Frühwirth, Eds. Reports CW, vol. 452. Department of Computer Science,
K.U.Leuven, Belgium, 125–140.
Voets, D., Pilozzi, P., and De Schreye, D. 2007. A new approach to termination
analysis of Constraint Handling Rules. In 4th Workshop on Constraint Handling Rules,
K. Djelloul, G. J. Duck, and M. Sulzmann, Eds. U.Porto, 77–89.

