ACD Term Rewriting

arXiv:cs/0608016v1 [] 3 Aug 2006

Gregory J. Duck, Peter J. Stuckey, and Sebastian Brand
NICTA Victoria Laboratory
Department of Computer Science & Software Engineering,
University of Melbourne, Australia

Abstract. In this paper we introduce Associative Commutative Distributive Term Rewriting (ACDTR), a rewriting language for rewriting
logical formulae. ACDTR extends AC term rewriting by adding distribution of conjunction over other operators. Conjunction is vital for expressive term rewriting systems since it allows us to require that multiple
conditions hold for a term rewriting rule to be used. ACDTR uses the
notion of a “conjunctive context”, which is the conjunction of constraints
that must hold in the context of a term, to enable the programmer to
write very expressive and targeted rewriting rules. ACDTR can be seen
as a general logic programming language that extends Constraint Handling Rules and AC term rewriting. In this paper we define the semantics
of ACDTR and describe our prototype implementation.

1

Introduction

Term rewriting is a powerful instrument to specify computational processes. It is
the basis of functional languages; it is used to define the semantics of languages
and it is applied in automated theorem proving, to name only a few application
areas.
One difficulty faced by users of term rewriting systems is that term rewrite
rules are local, that is, the term to be rewritten occurs in a single place. This
means in order to write precise rewrite rules we need to gather all relevant
information in a single place.
Example 1. Imagine we wish to “program” an overloaded ordering relation for
integers variables, real variables and pair variables. In order to write this the
“type” of the variable must be encoded in the term1 as in:
int(x) ≤ int(y) → intleq(int(x), int(y))
real(x) ≤ real(y) → realleq(real(x), real(y))
pair(x1 , x2 ) ≤ pair(y1 , y2 ) → x1 ≤ y1 ∨ x1 = y1 ∧ x2 ≤ y2
In a more standard language, the type information for variables (and other
information) would be kept separate and “looked up” when required.
⊓
⊔
1

Operator precedences used throughout this paper are: ∧ binds tighter than ∨, and
all other operators, e.g. ¬, =, bind tighter than ∧.

Term rewriting systems such as constraint handling rules (CHRs) [5] and
associative commutative (AC) term rewriting [3] allow “look up” to be managed
straightforwardly for a single conjunction.
Example 2. In AC term rewriting the above example could be expressed as:
int (x) ∧ int (y) ∧ x ≤ y → int(x) ∧ int(y) ∧ intleq(x, y)
real (x) ∧ real (y) ∧ x ≤ y → real (x) ∧ real (y) ∧ realleq (x, y)
pair (x, x1 , x2 ) ∧ pair (y, y1 , y2 ) ∧ x ≤ y → pair (x, x1 , x2 ) ∧ pair (y, y1 , y2 )∧
(x1 ≤ y1 ∨ x1 = y1 ∧ x2 ≤ y2 )
where each rule replaces the x ≤ y by an appropriate specialised version, in the
conjunction of constraints. The associativity and commutativity of ∧ is used to
easily collect the required type information from a conjunction.
⊓
⊔
One difficulty remains with both AC term rewriting and CHRs. The “look
up” is restricted to be over a single large conjunction.
Example 3. Given the term int(x1 ) ∧ int(y1 ) ∧ pair (x, x1 , x2 ) ∧ pair (y, y1 , y2 ) ∧
x ≤ y. Then after rewriting x ≤ y to (x1 ≤ y1 ∨ x1 = y1 ∧ x2 ≤ y2 ) we could not
rewrite x1 ≤ y1 since the types for x1 , y1 appear in a different level.
In order to push the type information inside the disjunction we need to
distribute conjunction over disjunction.
⊓
⊔
Simply adding distribution rules like
A ∧ (B ∨ C) → A ∧ B ∨ A ∧ C
A ∧ B ∨ A ∧ C → A ∧ (B ∨ C)

(1)
(2)

does not solve the problem. Rule (1) creates two copies of term A, which increases
the size of the term being rewritten. Adding Rule (2) to counter this effect results
in a non-terminating rewriting system.
1.1

Conjunctive context

We address the non-termination vs. size explosion problem due to distributivity
rewrite rules in a similar way to how commutativity is dealt with: by handling
distributivity on the language level. We restrict ourselves to dealing with expanding distributivity of conjunction ∧ over any other operator, and we account
for idempotence of conjunction.2 Thus we are concerned with distribution rules
of the form
P ∧ f (Q1 , . . . , Qn ) → P ∧ f (P ∧ Q1 , . . . , P ∧ Qn ).
2

(3)

This means that conjunction is distributive over any function f in presence of a
redundant copy of P , i.e. P ∧ (P ∧ f (Q1 , . . . , Qn )) → P ∧ f (P ∧ Q1 , . . . , P ∧ Qn ).
We use idempotence to simplify the RHS and derive (3).

2

Let us introduce the conjunctive context of a term and its use in rewrite
rules, informally for now. Consider a term T and the conjunction C ∧ T modulo
idempotence of ∧ that would result from exhaustive application of rule (3) to
the superterm of T . By the conjunctive context of T we mean the conjunction C.
Example 4. The conjunctive context of the boxed occurrence of x in the term
(x = 3) ∧ (x2 > y ∨ ( x = 4) ∧ U ∨ V ) ∧ W,
is (x = 3) ∧ U ∧ W .

⊓
⊔

We allow a rewrite rule P → T to refer to the conjunctive context C of the rule
head P . We use the following notation:
C \ P ⇐⇒ T.
This facility provides ∧-distributivity without the undesirable effects of rule (3)
on the term size.
Example 5. We can express that an equality can be used anywhere “in its scope”
by viewing the equality as a conjunctive context:
x = a \ x ⇐⇒ a.
Using this rule on the term of Example 4 results in
(x = 3) ∧ (32 > y ∨ (3 = 4) ∧ U ∨ V ) ∧ W
⊓
⊔

without dissolving the disjunction.
1.2

Motivation and Applications

Constraint Model Simplification. Our concrete motivation behind associative commutative distributive term rewriting (ACDTR) is constraint model
mapping as part of the G12 project [7]. A key aim of G12 is the mapping of solver
independent models to efficient solver dependent models. We see ACDTR as
the basis for writing these mappings. Since models are not flat conjunctions of
constraints we need to go beyond AC term rewriting or CHRs.
Example 6. Consider the following simple constraint model inspired by the Social Golfers problem. For two groups g1 and g2 playing in the same week there
can be no overlap in players: maxOverlap(g1 , g2 , 0) The aim is to maximise the
number of times the overlap between two groups is less than 2; in other words
minimise the number of times two players play together in a group.
^
constraint
maxOverlap(g1 , g2 , 0)
∀w∈Weeks
∀g1 ,g2 ∈weeks[w]
g1 <g2

maximise

X

holds(maxOverlap(g1 , g2 , 1))

∀w1 ,w2 ∈Weeks
∀g1 ∈weeks[w1 ]
∀g2 ∈weeks[w2 ]
g1 <g2

3

Consider the following ACDTR program for optimising this constraint model.
maxOverlap(a, b, c1 ) \ maxOverlap(a, b, c2 ) ⇐⇒ c2 ≥ c1 | true
holds(true) ⇐⇒ 1
holds (false) ⇐⇒ 0
The first rule removes redundant maxOverlap constraints. The next two rules
implement partial evaluation of the holds auxiliary function which coerces a
Boolean to an integer.
By representing the constraint model as a giant term, we can optimise the
model by applying the ACDTR program. For example, consider the trivial case
with one week and two groups G1 and G2 . The model becomes
maxOverlap(G1 , G2 , 0) ∧ maximise(holds (maxOverlap(G1 , G2 , 1))).
The subterm holds(maxOverlap(G1 , G2 , 1)) simplifies to 1 using the conjunctive
context maxOverlap(G1 , G2 , 0).
⊓
⊔
It is clear that pure CHRs are insufficient for constraint model mapping for
at least two reasons, namely
– a constraint model, e.g. Example 6, is typically not a flattened conjunction;
– some rules rewrite functions, e.g. rules (2) and (3) rewriting function holds,
which is outside the scope of CHRs (which rewrite constraints only).

Global Definitions. As we have seen conjunctive context matching provides
a natural mechanism for making global information available. In a constraint
model, structured data and constraint definitions are typically global, i.e. on the
top level, while access to the data and the use of a defined constraint is local, e.g.
the type information from Example 1. Another example is partial evaluation.
Example 7. The solver independent modelling language has support for arrays.
Take a model having an array a of given values. It could be represented as the
top-level term array (a, [3, 1, 4, 1, 5, 9, 2, 7]). Deeper inside the model, accesses to
the array a occur, such as in the constraint x > y + lookup(a, 3). The following
rules expand such an array lookup:
array(A, Array) \ lookup(A, Index ) ⇐⇒ list element(Array, Index )
list element([X|Xs], 0) ⇐⇒ X
list element ([X|Xs], N ) ⇐⇒ N > 0 | list element (Xs, N − 1)
Referring to the respective array of the lookup expression via its conjunctive
context allows us to ignore the direct context of the lookup, i.e. the concrete
constraint or expression in which it occurs.
⊓
⊔
4

Propagation rules. When processing a logical formula, it is often useful to be
able to specify that a new formula Q can be derived from an existing formula
P without consuming P . In basic term rewriting, the obvious rule P ⇐⇒ P ∧ Q
causes trivial non-termination. This issue is recognised in CHRs, which provide
support for inference or propagation rules. We account for this fact and use rules
of the form P =⇒ Q to express such circumstances.
Example 8. The following is the classic CHR leq program reimplemented for
ACD term rewriting (we omit the basic rules for logical connectives):
leq(X, X) ⇐⇒ true
leq(X, Y ) \ leq(Y, X) ⇐⇒ X = Y
leq(X, Y ) \ leq(X, Y ) ⇐⇒ true
leq(X, Y ) ∧ leq(Y, Z) =⇒ leq(X, Z)

(reflexivity)
(antisymmetry)
(idempotence)
(transitivity)

These rules are almost the same as the CHR version, with the exception of
the second and third rule (antisymmetry and idempotence) which generalise its
original by using conjunctive context matching.
⊓
⊔
Propagation rules are also used for adding redundant information during model
mapping.
The rest of the paper is organised as follows. Section 2 covers the standard
syntax and notation of term rewriting. Section 3 defines the declarative and operational semantics of ACDTR. Section 4 describes a prototype implementation
of ACDTR as part of the G12 project. Section 5 compares ACDTR with related
languages. Finally, in Section 6 we conclude.

2

Preliminaries

In this section we briefly introduce the notation and terminology used in this
paper. Much of this is borrowed from term rewriting [3].
We use T (Σ, X) to represent the set of all terms constructed from a set of
function symbols Σ and set of variables X (assumed to be countably infinite).
We use Σ (n) ⊆ Σ to represent the set of function symbols of arity n.
A position is a string (sequence) of integers that uniquely determines a subterm of a term T , where ǫ represents the empty string. We define function T |p ,
which returns the subterm of T at position p as
T |ǫ = T
f (T1 , . . . , Ti , . . . , Tn )|ip = Ti |p
We similarly define a function T [S]p which replaces the subterm of T at position
p with term S. We define the set Pos(T ) to represent the set of all positions of
subterms in T .
An identity is a pair (s, t) ∈ T (Σ, X) × T (Σ, X), which is usually written as
s ≈ t. Given a set of identities E, we define ≈E to be the set of identities closed
under the axioms of equational logic [3], i.e. symmetry, transitivity, etc.
5

We define the congruence class [T ]≈E = {S ∈ T (Σ, X)|S ≈E T } as the set
of terms equal to T with respect to E.
Finally, we define function vars(T ) to return the set of variables in T .

3

Syntax and Semantics

The syntax of ACDTR closely resembles that of CHRs. There are three types of
rules of the following form:
(simplification)
(propagation)
(simpagation)

r @ H ⇐⇒ g | B
r @ H =⇒ g | B
r @ C \ H ⇐⇒ g | B

where r is a rule identifier, and head H, conjunctive context C, guard g and body
B are arbitrary terms. The rule identifier is assumed to uniquely determine the
rule. A program P is a set of rules.
We assume that vars(g) ⊆ vars(H) or vars(g) ⊆ vars(H) ∪ vars(C) (for
simpagation rules). The rule identifier can be omitted. If g = true then the guard
can be omitted.
We present the declarative semantics of ACDTR based on equational logic.
First we define the set of operators that ACDTR treats specially.
Definition 1 (Operators). We define the set of associate commutative operators as AC. The set AC must satisfy AC ⊆ Σ (2) and (∧) ∈ AC.
For our examples we assume that AC = {∧, ∨, +, ×}. We also treat the operator
∧ as distributive as explained below.
ACDTR supports a simple form of guards.
Definition 2 (Guards). A guard is a term. We denote the set of all “true”
guards as G, i.e. a guard g is said to hold iff g ∈ G. We assume that true ∈ G
and false 6∈ G.
We can now define the declarative semantics for ACDTR. In order to do so
we employ a special binary operator where to explicitly attach a conjunctive
context to a term. Intuitively, the meaning of T where C is equivalent to that of
T provided C is true, otherwise the meaning of T where C is unconstrained. For
Boolean expressions, it is useful to interpret where as conjunction ∧, therefore
where-distribution, i.e. identity (6) below, becomes equivalent to ∧-distribution
(3). The advantage of distinguishing where and ∧ is that we are not forced to
extend the definition of ∧ to arbitrary (non-Boolean) functions.
We denote by B the following set of built-in identities:
A◦B ≈B ◦A
(A ◦ B) ◦ C ≈ A ◦ (B ◦ C)
T ≈ (T where true)
A ∧ B ≈ (A where B) ∧ B
T where (W1 ∧ W2 ) ≈ (T where W1 ) where W2
f (A1 , ..., Ai , ..., An ) where W ≈ f (A1 , ..., Ai where W, ..., An ) where W
6

(1)
(2)
(3)
(4)
(5)
(6)

for all ◦ ∈ AC, functions f ∈ Σ (n) , and i ∈ {1, . . . , n}.
Definition 3 (Declarative Semantics for ACDTR). The declarative semantics for an ACDTR program P (represented as a multiset of rules) is given
by the function JK defined as follows:
JP K
= {Jθ(R)K | ∀R, θ . R ∈ P ∧ θ(guard(R)) ∈ G} ∪ B
JH ⇐⇒ g | BK
= ∃vars(B)−vars(H) (H ≈ B)
JC \ H ⇐⇒ g | BK = ∃vars(B)−vars(C,H) (H where C ≈ B where C)
JH =⇒ g | BK
= ∃vars(B)−vars(H) (H ≈ H ∧ B)
where function guard(R) returns the guard of a rule.
The function JK maps ACDTR rules to identities between the head and the
body terms, where body-only variables are existentially quantified.3 Note that
there is a new identity for each possible binding of guard(R) that holds in G.
A propagation rule is equivalent to a simplification rule that (re)introduces the
head H (in conjunction with the body B) in the RHS. This is analogous to
propagation rules under CHRs.
A simpagation rule is equivalent to a simplification rule provided the conjunctive context is satisfied.
The built-in rules B from Definition 3 contain identities for creating/destroying (3) and (4), combining/splitting (5), and distributing downwards/upwards (6) a conjunctive context in terms of the where operator.
The set B also contains identities (1) and (2) for the associative/commutative
properties of the AC operators.
Example 9. Consider the following ACDTR rule and the corresponding identity.
JX = Y \ X ⇐⇒ Y K

=

(Y where X = Y ) ≈ (X where X = Y )

(7)

Under this identity and using the rules in B, we can show that f (A)∧(A = B) ≈
f (B) ∧ (A = B), as follows.
f (A) ∧ (A = B)
≈(4)
(f (A) where (A = B)) ∧ (A = B)
≈(6)
(f (A where (A = B)) where (A = B)) ∧ (A = B) ≈(7)
(f (B where (A = B)) where (A = B)) ∧ (A = B) ≈(6)
(f (B) where (A = B)) ∧ (A = B)
≈(4)
f (B) ∧ (A = B)
⊓
⊔
3.1

Operational Semantics

In this section we describe the operational semantics of ACDTR. It is based
on the theoretical operational semantics of CHRs [1,4]. This includes support
for identifiers and propagation histories, and conjunctive context matching for
simpagation rules.
3

All other variables are implicitly universally quantified, where the universal quantifiers appear outside the existential ones.

7

Propagation history. The CHR concept of a propagation history, which prevents trivial non-termination of propagation rules, needs to be generalised over
arbitrary terms for ACDTR. A propagation history is essentially a record of all
propagation rule applications, which is checked to ensure a propagation rule is
not applied twice to the same (sub)term.
In CHRs, each constraint is associated with a unique identifier. If multiple
copies of the same constraint appear in the CHR store, then each copy is assigned
a different identifier. We extend the notion of identifiers to arbitrary terms.
Definition 4 (Identifiers). An identifier is an integer associated with each
(sub)term. We use the notation T #i to indicate that term T has been associated
with identifier i. A term T is annotated if T and all subterms of T are associated
with an identifier. We also define function ids(T ) to return the set of identifiers
in T , and term(T ) to return the non-annotated version of T .
For example, T = f (a#1, b#2)#3 is an annotated term, where ids(T ) = {1, 2, 3}
and term(T ) = f (a, b).
Identifiers are considered separate from the term. We could be more precise
by separating the two, i.e. explicitly maintain a map between Pos(T ) and the
identifiers for T . We do not use this approach for space reasons. We extend
and overload all of the standard operations over terms (e.g. from Section 2) to
annotated terms in the obvious manner. For example, the subterm relation T |p
over annotated terms returns the annotated term at position p. The exception
are elements of the congruence class [T ]≈AC , formed by the AC relation ≈AC ,
which we assume satisfies the following constraints.
A#i ◦ B#j ≈AC B#j ◦ A#i
A#i ◦ (B#j ◦ C#k) ≈AC (A#i ◦ B#j) ◦ C#k
We have neglected to mention the identifiers over AC operators. These identifiers
will be ignored later, so we leave them unconstrained.
A propagation history is a set of entries defined as follows.
Definition 5 (Entries). A propagation history entry is of the form (r @ E),
where r is a propagation rule identifier, and E is a string of identifiers. We
define function entry(r, T ) to return the propagation history entry of rule r for
annotated term T as follows.
entry(r, T )
= (r @ entry(T ))
entry(T1 ◦ T2 )
= entry(T1 ) entry(T2 )
entry(f (T1 , ..., Tn )#i) = i entry(T1 ) ... entry(Tn )

◦ ∈ AC
otherwise

This definition means that propagation history entries are unaffected by associativity, but are effected by commutativity.
Example 10. Consider the annotated term T = f ((a#1 ∧ b#2)#3)#4. We have
that T ∈ [T ]≈AC and T ′ = f ((b#2 ∧ a#1)#3)#4 ∈ [T ]≈AC . Although T
and T ′ belong to [T ]≈AC they have different propagation history entries, e.g.
entry(r, T ) = (r @ (4 1 2)) while entry(r, T ′ ) = (r @ (4 2 1)).
⊓
⊔
8

When a (sub)term is rewritten into another, the new term is assigned a set
of new unique identifiers. We define the auxiliary function annotate(P, T ) = Ta
to map a set of identifiers P and un-annotated term T to an annotated term Ta
such that ids(Ta ) ∩ P = ∅ and |ids(Ta )| = |Pos(T )|. These conditions ensure that
all identifiers are new and unique.
When a rule is applied the propagation history must be updated accordingly
to reflect which terms are copied from the matching. For example, the rule
f (X) ⇐⇒ g(X, X) essentially clones the term matching X. The identifiers,
however, are not cloned. If a term is cloned, we expect that both copies will
inherit the propagation history of the original. Likewise, terms can be merged,
e.g. g(X, X) ⇐⇒ f (X) merges two instances of the term matching X. In this
case, the propagation histories of the copies are also merged.
To achieve this we duplicate entries in the propagation history for each occurrence of a variable in the body that also appeared in the head.
Definition 6 (Updating History). Define function
update(H, Ha , B, Ba , T0 ) = T1
where H and B are un-annotated terms, Ha and Ba are annotated terms, and T0
and T1 are propagation histories. T1 is a minimal propagation history satisfying
the following conditions:
– T0 ⊆ T1 ;
– ∀p ∈ Pos(H) such that H|p = V ∈ X (where X is the set of variables), and
∃q ∈ Pos(B) such that B|q = V , then define identifier renaming ρ such that
ρ(Ha |p ) and Ba |q are identical annotated terms. Then if E ∈ T0 we have
that ρ(E) ∈ T1 .
Example 11. Consider rewriting the term Ha = f ((a#1 ∧ b#2)#3)#4 with a
propagation history of T0 = {(r @ (1 2))} using the rule f (X) ⇐⇒ g(X, X).
The resulting term is Ba = g((a#5 ∧b#6)#7), (a#8 ∧b#9)#10#11 and the new
propagation history is T1 = {(r @ (1 2)), (r @ (5 6)), (r @ (8 9))}.
⊓
⊔
Conjunctive context. According to the declarative semantics, a term T with
conjunctive context C is represented as (T where C). Operationally, we will
never explicitly build a term containing a where clause. Instead we use the
following function to compute the conjunctive context of a subterm on demand.
Definition 7 (Conjunctive Context). Given an (annotated) term T and a
position p ∈ Pos(T ), we define function cc(T, p) to return the conjunctive context
at position p as follows.
cc(T, ǫ)
= true
cc(A ∧ B, 1p)
= B ∧ cc(A, p)
cc(A ∧ B, 2p)
= A ∧ cc(B, p)
cc(f (T1 , . . . , Ti , . . . , Tn ), ip) = cc(Ti , p)
9

(f 6= ∧)

States and transitions. The operational semantics are defined as a set of
transitions on execution states.
Definition 8 (Execution States). An execution state is a tuple of the form
hG, T, V, Pi, where G is a term (the goal), T is the propagation history, V is
the set of variables appearing in the initial goal and P is a set of identifiers.
We also define initial and final states as follows.
Definition 9 (Initial and Final States). Given an initial goal G for program
P , the initial state of G is
hGa , ∅, vars(G), ids(Ga )i
where Ga = annotate(∅, G). A final state is a state where no more rules are
applicable to the goal G.
We can now define the operational semantics of ACDTR as follows.
Definition 10 (Operational Semantics).
hG0 , T0 , V, P0 i ֌ hG1 , T1 , V, P1 i
1. Simplify: There exists a (renamed) rule from P
H ⇐⇒ g | B
such that there exists a matching substitution θ and a term G′0 such that
–
–
–
–

G0 ≈AC G′0
∃p ∈ Pos(G′0 ) . G′0 |p = θ(H)
θ(g) ∈ G
Ba = annotate(P0 , θ(B))

Then G1 = G′0 [Ba ]p , P1 = P0 ∪ ids(G1 ) and T1 = update(H, G′0 |p , B, Ba , T0 ).
2. Propagate: There exists a (renamed) rule from P
r @ H =⇒ g | B
such that there exists a matching substitution θ and a term G′0 such that
–
–
–
–
–

G0 ≈AC G′0
∃p ∈ Pos(G′0 ) . G′0 |p = θ(H)
θ(g) ∈ G
entry(r, G′0 |p ) 6∈ T0
Ba = annotate(P0 , θ(B))

Then G1 = G′0 [G′0 |p ∧ Ba ]p , T1 = update(H, G′0 |p , B, Ba , T0 ) ∪ {entry(r, G′0 |p )}
and P1 = P0 ∪ ids(G1 ).
3. Simpagate: There exists a (renamed) rule from P
C \ H ⇐⇒ g | B
such that there exists a matching substitution θ and a term G′0 such that
10

h(leq(X1 , Y2 )3 ∧4 leq(Y5 , Z6 )7 ∧8 ¬9 leq(X10 , Z11 )12 ), ∅i ֌trans
h(leq(X1 , Y2 )3 ∧4 leq(Y5 , Z6 )7 ∧13 leq(X15 , Z16 )14 ∧8 ¬9 leq(X10 , Z11 )12 ), T i ֌idemp
h(leq(X1 , Y2 )3 ∧4 leq(Y5 , Z6 )7 ∧13 leq(X15 , Z16 )14 ∧8 ¬9 true17 ), T i ֌simplif y
h(leq(X1 , Y2 )3 ∧4 leq(Y5 , Z6 )7 ∧13 leq(X15 , Z16 )14 ∧8 f alse18 ), T i ֌simplif y
h(leq(X1 , Y2 )3 ∧4 leq(Y5 , Z6 )7 ∧13 f alse19 ), T i ֌simplif y
h(leq(X1 , Y2 )3 ∧4 f alse20 ), T i ֌simplif y
h(f alse21 ), T i

Fig. 1. Example derivation for the leq program.

–
–
–
–
–

G0 ≈AC G′0
∃p ∈ Pos(G′0 ) . G′0 |p = θ(H)
∃D.θ(C) ∧ D ≈AC cc(G′0 , p)
θ(g) ∈ G
Ba = annotate(P0 , θ(B))

Then G1 = G′0 [Ba ]p , T1 = update(H, G′0 |p , B, Ba , T0 ) and P1 = P0 ∪ ids(G1 ).
Example. Consider the leq program from Example 8 with the goal
leq(X, Y ) ∧ leq(Y, Z) ∧ ¬leq(X, Z)
Figure 1 shows one possible derivation of this goal to the final state representing
f alse. For brevity, we omit the V and P fields, and represent identifiers as subscripts, i.e. T #i = Ti . Also we substitute T = {transitivity @ (3 2 1 7 5 6)}.
We can state a soundness result for ACDTR.
Theorem 1 (Soundness). If hG0 , T0 , V, Pi ֌∗ hG′ , T ′ , V, P ′ i with respect to
a program P , then JP K |= ∃vars(G′ )−V G0 ≈ G′
This means that for all algebras A that satisfy JP K, G0 and G′ are equivalent
for some assignment of the fresh variables in G′ .

4

Implementation

We have implemented a prototype version of ACDTR as part of the mapping
language of the G12 project, called Cadmium. In this section we give an overview
of the implementation details. In particular, we will focus on the implementation
of conjunctive context matching, which is the main contribution of this paper.
Cadmium constructs normalised terms from the bottom up. Here, a normalised term is one that cannot be reduced further by an application of a rule.
Given a goal f (t1 , ..., tn ), we first must recursively normalise all of t1 , ..., tn (to
say s1 , ..., sn ), and then attempt to find a rule that can be applied to the top-level
of f (s1 , ..., sn ). This is the standard execution algorithm used by many TRSs
implementations.
11

This approach of normalising terms bottom up is complicated by the consideration of conjunctive context matching. This is because the conjunctive context
of the current term appears “higher up” in the overall goal term. Thus conjunctive context must be passed top down, yet we are normalising bottom up. This
means there is no guarantee that the conjunctive context is normalised.
Example 12. Consider the following ACDTR program that uses conjunctive context matching.
X = V \ X ⇐⇒ var(X) ∧ nonvar(V ) | V.
one(X) ⇐⇒ X = 1.
not one(1) ⇐⇒ f alse.
Consider the goal not one(A)∧one(A), which we expect should be normalised to
f alse. Assume that the sub-term not one(A) is selected for normalisation first.
The conjunctive context for not one(A) (and its subterm A) is one(A). No rule
is applicable, so not one(A) is not reduced.
Next the subterm one(A) is reduced. The second rule will fire resulting in
the new term A = 1. Now the conjunctive context for the first term not one(A)
has changed to A = 1, so we expect that A should be rewritten to the number
⊓
⊔
1. However not one(A) has already being considered for normalisation.
The current Cadmium prototype solves this problem by re-normalising terms
when and if the conjunctive context “changes”. For example, when the conjunctive context one(A) changes to A = 1, the term not one(X) will be renormalised
to not one(1) by the first rule.
The general execution algorithm for Cadmium is shown in Figure 2. Function
normalise takes a term T , a substitution θ, a conjunctive context CC and a
Boolean value Ch which keeps track of when the conjunctive context of the
current subterm has changed. If Ch = true, then we can assume the substitution
θ maps variables to normalised terms. For the initial goal, we assume θ is empty,
otherwise if we are executing a body of a rule, then θ is the matching substitution.
Operationally, normalise splits into three cases depending on what T is. If
T is a variable, and the conjunctive context has changed (i.e. Ch = true),
then θ(T ) is no longer guaranteed to be normalised. In this case we return the
result of renormalising θ(T ) with respect to CC. Otherwise if Ch = f alse, we
simply return θ(T ) which must be already normalised. If T is a conjunction
T1 ∧ T2 , we repeatedly call normalise on each conjunct with the other added
to the conjunctive context. This is repeated until a fixed point (i.e. further
normalisation does not result in either conjunct changing) is reached, and then
return the result of apply rule on the which we will discuss below. This fixed
point calculation accounts for the case where the conjunctive context of a term
changes, as shown in Example 12. Otherwise, if T is any other term of the form
f (T1 , ..., Tn ), construct the new term T ′ by normalising each argument. Finally
we return the result of apply rule applied to T ′ .
The function call apply rule(T ′ ,CC) will attempt to apply a rule to normalised
term T ′ with respect to conjunctive context CC. If a matching rule is found, then
12

normalise(T ,θ,CC,Ch)
if is var(T )
if Ch
return normalise(θ(T ),θ,CC,f alse)
else
return θ(T )
else if T = T1 ∧ T2
do
T1′ := T1
T2′ := T2
T1 := normalise(T1′ ,θ,T2′ ∧ CC,true)
T2 := normalise(T2′ ,θ,T1′ ∧ CC,true)
while T1 6= T1′ ∧ T2 6= T2′
return apply rule(T1′ ∧ T2′ ,CC)
else
T = f (T1 , ..., Tn )
T ′ := f (normalise(T1 ,θ,CC,Ch), ..., normalise(Tn ,θ,CC,Ch))
return apply rule(T ′ ,CC)

Fig. 2. Pseudo code of the Cadmium execution algorithm.

the result of normalise(B,θ,CC,f alse) is returned, where B is the (renamed) rule
body and θ is the matching substitution. Otherwise, T ′ is simply returned.

5

Related Work

ACDTR is closely related to both TRS and CHRs, and in this section we compare
the three languages.
5.1

AC Term Rewriting Systems

The problem of dealing with associative commutative operators in TRS is well
studied. A popular solution is to perform the rewriting modulo some permutation
of the AC operators. Although this complicates the matching algorithm, the
problem of trivial non-termination (e.g. by continually rewriting with respect to
commutativity) is solved.
ACDTR subsumes ACTRS (Associative Commutative TRS) in that we have
introduced distributivity (via simpagation rules), and added some “CHR-style”
concepts such as identifiers and propagation rules.
Given an ACTRS program, we can map it to an equivalent ACDTR program
by interpreting each ACTRS rule H → B as the ACDTR rule H ⇐⇒ B. We
can now state the theorem relating ACTRS and ACDTR.
Theorem 2. Let P be an ACTRS program and T a ground term, then
T →∗ S under P iff hTa , ∅, ∅, ids(Ta )i ֌∗ hSa , ∅, ∅, Pi under α(P ) (where
Ta = annotate(∅, T )) for some P and term(Sa ) = S.
13

5.2

CHRs and CHR∨

ACDTR has been deliberately designed to be an extension of CHRs. Several
CHR concepts, e.g. propagation rules, etc., have been adapted.
There are differences between CHRs and ACDTR. The main difference is
that ACDTR does not have a “built-in” or “underlying” solver, i.e. ACDTR is
not a constraint programming language. However it is possible to encode solvers
directly as rules, e.g. the simple leq solver from Example 8. Another important
difference is that CHRs is based on predicate logic, where there exists a distinction between predicate symbols (i.e. the names of the constraints) and functions
(used to construct terms). ACDTR is based on equational logic between terms,
hence there is no distinction between predicates and functions (a predicate is
just a Boolean function). To overcome this, we assume the existence of a set
Pred, which contains the set of function symbols that are Boolean functions.
We assume that AC ∩ Pred = {∧(2) }.
The mapping between a CHR program and an ACDTR program is simply
α(P ) = P ∪ {X ∧ true ⇐⇒ X}.4 However, we assume program P is restricted
as follows:
– rules have no guards apart from implicit equality guards; and
– the only built-in constraint is true
and the initial goal G is also restricted:
– G must be of the form G0 ∧ ... ∧ Gn for n > 0;
– Each Gi is of the form fi (A0 , ..., Am ) for m ≥ 0 and fi ∈ Pred;
– For all p ∈ Pos(Aj ), 0 ≤ j ≤ m we have that if Aj |p = g(B0 , ..., Bq ) then
g (q) 6∈ AC and g (q) 6∈ Pred.
These conditions disallow predicate symbols from appearing as arguments in
CHR constraints.
Theorem 3. Let P be a CHR program, and G an initial goal both satisfying
V
the above conditions, then hG, ∅, true, ∅iV
1 ֌ h∅, S, true, T ii (for some T , i
and V = vars(G)) under the theoretical operational semantics [4] for CHRs
iff hGa , ∅, V, ids(Ga )i ֌ hSa , T ′ , V, Pi (for some T ′ , P) under ACDTR, where
term(Sa ) = S1 ∧...∧Sn and S = {S1 #i1 , ..., Sn #in } for some identifiers i1 , ..., in .
We believe that Theorem 3 could be extended to include CHR programs that
extend an underlying solver, provided the rules for handling tell constraints are
added to the ACDTR program. For example, we can combine rules for rational
tree unification with the leq program from Example 8 to get a program equivalent
to the traditional leq program under CHRs.
ACDTR generalises CHRs by allowing other operators besides conjunction
inside the head or body of rules. One such extension of CHRs has been studied
before, namely CHR∨ [2] which allows disjunction in the body. Unlike ACDTR,
4

There is one slight difference in syntax: CHRs use ‘,’ to represent conjunction,
whereas ACDTR uses ‘∧’.

14

which manipulates disjunction syntactically, CHR∨ typically finds solutions using
backtracking search.
One notable implementation of CHR∨ is [6], which has an operational semantics described as an and/or (∧/∨) tree rewriting system. A limited form of
conjunctive context matching is used, similar to that used by ACDTR, based
on the knowledge that conjunction ∧ distributes over disjunction ∨. ACDTR
generalises this by distributing over all functions.

6

Future Work and Conclusions

We have presented a powerful new rule-based programming language, ACDTR,
that naturally extends both AC term rewriting and CHRs. The main contribution is the ability to match a rule against the conjunctive context of a (sub)term,
taking advantage of the distributive property of conjunction over all possible
functions. We have shown this is a natural way of expressing some problems,
and by building the distributive property into the matching algorithm, we avoid
non-termination issues that arise from naively implementing distribution (e.g.
as rewrite rules).
We intend that ACDTR will become the theoretical basis for the Cadmium
constraint mapping language as part of the G12 project [7]. Work on ACDTR
and Cadmium is ongoing, and there is a wide scope for future work, such as
confluence, termination and implementation/optimisation issues.

References
1. S. Abdennadher. Operational semantics and confluence of constraint propagation
rules. In Gert Smolka, editor, Proceedings of the Third International Conference
on Principles and Practice of Constraint Programming, LNCS 1330, pages 252–266.
Springer-Verlag, 1997.
2. S. Abdennadher and H. Schütz. CHR∨ : A flexible query language. In International
conference on Flexible Query Answering Systems, number 1495 in LNCS, pages
1–14, Roskilde, Denmark, 1998. Springer-Verlag.
3. F. Baader and T. Nipkow. Term rewriting and all that. Cambridge Univ. Press,
1998.
4. G. Duck, P. Stuckey, M. Garcia de la Banda, and C. Holzbaur. The refined operational semantics of constraint handling rules. In B. Demoen and V. Lifschitz,
editors, Proceedings of the 20th International Conference on Logic Programming,
LNCS 3132, pages 90–104. Springer-Verlag, September 2004.
5. T. Frühwirth. Theory and practice of constraint handling rules. Journal of Logic
Programming, 37:95–138, 1998.
6. L. Menezes, J. Vitorino, and M. Aurelio. A High Performance CHR∨ Execution
Engine. In Second Workshop on Constraint Handling Rules, Sitges, Spain, 2005.
7. P.J. Stuckey, M. Garcia de la Banda, M. Maher, K. Marriott, J. Slaney, Z. Somogyi,
M. Wallace, and T. Walsh. The G12 project: Mapping solver independent models
to efficient solutions. In M. Gabrielli and G. Gupta, editors, Proceedings of the
21st International Conference on Logic Programming, number 3668 in LNCS, pages
9–13. Springer-Verlag, 2005.

15

A

Examples

A.1

Further Motivating Examples

Example 13 (Conjunctive Normal Form). One of the roles of mapping models
is to convert a model written in an expressive language into a restricted language which is easy to solve. Many standard approaches to solving propositional
formulae require that the formulae are in conjunctive normal form (CNF). Disjunction ∨ is distributive over ∧, which can be used to establish CNF in a direct
way, using the oriented rule
P ∨ Q ∧ R → (P ∨ Q) ∧ (P ∨ R).
CNF conversion based on this rule can exponentially increase the size of the formula. This undesirable circumstance means that in practice CNF conversions are
preferred that replace subformulae by new propositional atoms, which increases
the formula size at most linearly.
Let us formulate this approach in rewrite rules. To keep this example simple,
we assume that the non-CNF subformula P ∨ Q ∧ R occurs in a positive context
(for example by a preprocessing into negation normal form). We replace Q ∧ R
by a new atom s defined by the logical implication s ⇒ (Q ∧ R). In rewrite rule
form, we have
P ∨ Q ∧ R → (P ∨ s) ∧ (¬s ∨ Q) ∧ (¬s ∨ R).

(8)

Unit resolution and unit subsumption can be formalised in rewrite rules. Here
are two versions, one using conjunctive context and a regular one:
with conj. context:

regular:

P \ P ⇐⇒ true

P ∧P → P
P ∧ (P ∨ Q) → P
P ∧ ¬P → false

P \ ¬P ⇐⇒ false

P ∧ (¬P ∨ Q) → P ∧ Q
We furthermore assume rules eliminating the logical constants true and false
from conjunctions and disjunctions in the obvious way. Let us contrast the two
rule sets for the formula (a∨b∧(c∨d))∧d. The following is a terminating rewrite
history:
with conj. context:

regular:

(a ∨ b ∧ (c ∨ d)) ∧ d

(a ∨ b ∧ (c ∨ d)) ∧ d

֌ (a ∨ b ∧ (c ∨ true)) ∧ d
֌ (a ∨ b ∧ true) ∧ d

֌
֌

(a ∨ s) ∧ (¬s ∨ b) ∧ (¬s ∨ c ∨ d) ∧ d
(a ∨ s) ∧ (¬s ∨ b) ∧ true ∧ d

֌ (a ∨ b) ∧ d

֌

(a ∨ s) ∧ (¬s ∨ b) ∧ d

16

To obtain the simple conjunct (a ∨ b) using the regular rule format, a rule expressing binary resolution, i.e. from (P ∨ S) ∧ (¬S ∨ Q) follows (P ∨ Q), would be
required. However, such a rule is undesirable as it would create arbitrary binary
resolvents, increasing formula size. Moreover, the superfluous atom s remains in
the formula.
⊓
⊔

Example 14 (Type remapping). One of the main model mappings we are interested in expressing is where the type of a variable is changed from a high level
type easy for modelling to a low level type easy to solve. A prime example of this
is mapping a set variable x ranging over finite subsets of some fixed set s to an array x′ of 0/1 variables indexed by s. So for variable x we have e ∈ x ⇔ x′ [e] = 1.
For this example we use the more concrete modelling syntax: t : x indicates variable x has type t, the types we are interested are l..u an integers in the range l to
u, set of S a set ranging over elements in S, and array[I] of E an array indexed
by set I of elements of type E. We use f orall and sum looping constructs which
iterate over sets. This is expressed in ACDTR as follows.

set of s : x ⇐⇒ array[s] of 0..1 : x′ ∧ map(x, x′ )
map(x, x′ ) \ x ⇐⇒ x′
array[s] of 0..1 : x \ card(x) ⇐⇒ sum(e in s) x[e]
array[s] of 0..1 : x ∧
z :: (array[s] of 0..1 : z ∧
⇐⇒
array[s] of 0..1 : y \ x ∩ y
f orall(e in s) z[e] = x[e] && y[e])
array[s] of 0..1 : x ∧
z :: (array[s] of 0..1 : z ∧
⇐⇒
array[s] of 0..1 : y \ x ∪ y
f orall(e in s) z[e] = x[e] || y[e])
array[s] of 0..1 : x \ x = ∅ ⇐⇒ f orall(e in s) x[e] = 0
card(t :: c) ⇐⇒ card(t) :: c
(t1 :: c) ∪ t2 ⇐⇒ t1 ∪ t2 :: c
t1 ∪ (t2 :: c) ⇐⇒ t1 ∪ t2 :: c
(t1 :: c) ∩ t2 ⇐⇒ t1 ∩ t2 :: c
t1 ∩ (t2 :: c) ⇐⇒ t1 ∩ t2 :: c
(t1 :: c) = t2 ⇐⇒ t1 = t2 ∧ c
t1 = (t2 :: c) ⇐⇒ t1 = t2 ∧ c
(t1 :: c) ≤ t2 ⇐⇒ t1 ≤ t2 ∧ c
t1 ≤ (t2 :: c) ⇐⇒ t1 ≤ t2 ∧ c
(t :: c1 ) :: c2 ⇐⇒ t :: (c1 ∧ c2 )
maxOverlap(x, y, c) ⇐⇒ card(x ∩ y) ≤ c

(typec)
(vsubs)
(card)
(cap)
(cup)
(emptyset)
(↑ card)
(↑ cupl)
(↑ cupr)
(↑ capl)
(↑ capr)
(↑ eql)
(↑ eqr)
(↑ leql)
(↑ leqr)
(↑ cc)
(maxO)

The :: constructor adds some local conjunctive context to an arbitrary term (like
where) and the last 11 rules bar 1 move this context outwards to the nearest
predicate scope. The last rule defines the maxOverlap predicate. They are used
to introduce new variables z and their type and the constraints upon then. As
17

an example, consider the following derivation:

֌maxO
֌typec
֌vsubs
֌typec
֌vsubs
֌cap
֌↑card
֌↑leql

set of 1..n : x ∧ set of 1..n : y ∧ maxOverlap(x, y, 1)
set of 1..n : x ∧ set of 1..n : y ∧ card(x ∩ y) ≤ 1
array[1..n] of 0..1 : x′ ∧ map(x, x′ ) ∧ set of 1..n : y ∧ card(x ∩ y) ≤ 1
array[1..n] of 0..1 : x′ ∧ map(x, x′ ) ∧ set of 1..n : y ∧ card(x′ ∩ y) ≤ 1
array[1..n] of 0..1 : x′ ∧ map(x, x′ ) ∧ array[1..n] of 0..1 : y ′ ∧ map(y, y ′ ) ∧
card(x′ ∩ y) ≤ 1
array[1..n] of 0..1 : x′ ∧ map(x, x′ ) ∧ array[1..n] of 0..1 : y ′ ∧ map(y, y ′ ) ∧
card(x′ ∩ y ′ ) ≤ 1
array[1..n] of 0..1 : x′ ∧ map(x, x′ ) ∧ array[1..n] of 0..1 : y ′ ∧ map(y, y ′ ) ∧
card(z :: (array[1..n] of 0..1 : z ∧ f orall(e in 1..n) z[e] = x′ [e] && y ′ [e]) ≤ 1
array[1..n] of 0..1 : x′ ∧ map(x, x′ ) ∧ array[1..n] of 0..1 : y ′ ∧ map(y, y ′ ) ∧
card(z) :: (array[1..n] of 0..1 : z ∧ f orall(e in 1..n) z[e] = x′ [e] && y ′ [e]) ≤ 1
array[1..n] of 0..1 : x′ ∧ map(x, x′ ) ∧ array[1..n] of 0..1 : y ′ ∧ map(y, y ′ ) ∧
card(z) ≤ 1 ∧ array[1..n] of 0..1 : z ∧ f orall(e in 1..n) z[e] = x′ [e] && y ′ [e]

The final goal is a flat conjunction of constraints and types. It can be similarly
translated into a conjunction of pseudo-Boolean constraints that can be sent to
a finite domain solver, by unrolling f orall and replacing the arrays by sequences
of n variables.
⊓
⊔
Example 15 (Rational Tree Unification). We can directly express the rational
tree unification algorithm of Colmerauer5 as an ACD term rewriting system.
f (s1 , . . . sn ) = f (t1 , . . . , tn ) ⇐⇒ s1 = t1 ∧ · · · sn = tn
f (s1 , . . . sn ) = g(t1 , . . . , tm ) ⇐⇒ f alse

(split)
(f ail)

The (split) rule must be defined for each constructor f /n and the (fail) rule for
each pair of different constructors f /n and g/m. The remaining rules are:
x = x ⇐⇒ var(x) | true
t = x ⇐⇒ var(x) ∧ nonvar(t) | x = t
x = s \ x = t ⇐⇒ var(x) ∧ nonvar(s) ∧ size(s) ≤ size(t) | s = t
x = y \ x ⇐⇒ var(x) ∧ var(y) ∧ x 6≡ y | y

(id)
(f lip)
(tsubs)
(vsubs)

where size(t) is the size of the term t in terms of number of symbols, and ≡ is
syntactic identity. Even though the goals are a single conjunction of constraints,
ACD is used for succinctly expressing the (vsubs) rule which replaces one variable
by another in any other position.
5

A. Colmerauer. Prolog and Infinite Trees. Logic Programming, APIC Studies in Data
Processing (16). Academic Press. 1992

18

The following derivation illustrates the unification process in action. The
underlined part show the matching elements

֌f lip
֌vsubs
֌vsubs
֌tsubs
֌split
֌split
֌tsubs
֌split
֌tsubs
֌split
֌id

x = y ∧ f (f (x)) = x ∧ y = f (f (f (y)))
x = y ∧ x = f (f (x)) ∧ y = f (f (f (y)))
x = y ∧ y = f (f (x)) ∧ y = f (f (f (y)))
x = y ∧ y = f (f (y)) ∧ y = f (f (f (y)))
x = y ∧ y = f (f (y)) ∧ f (f (y)) = f (f (f (y)))
x = y ∧ y = f (f (y)) ∧ f (y) = f (f (y))
x = y ∧ y = f (f (y)) ∧ y = f (y)
x = y ∧ f (y) = f (f (y)) ∧ y = f (y)
x = y ∧ y = f (y) ∧ y = f (y)
x = y ∧ y = f (y) ∧ f (y) = f (y)
x = y ∧ y = f (y) ∧ f (y) = f (y)
x = y ∧ y = f (y) ∧ true
⊓
⊔

A.2

Expanded Examples

The purpose of this section is to show some example derivations under the operational semantics of ACDTR, rather than high-level descriptions. We allow for
some shorthand, namely T #i = Ti .
Identifiers and conjunctive context. In this section we explain parts of the
derivation from Example 15 in more detail. The initial goal is
x = y ∧ f (f (x)) = x ∧ y = f (f (f (y)))
which corresponds to the initial state:
h(((x1 = y2 )3 ∧ (f (f (x4 )5 )6 = x7 )8 )9 ∧ (y10 = f (f (f (y11 )12 )13 )14 )15 )16 , ∅,
{x, y}, {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16}i
The initial state is a quadruple contained an annotated version of the goal, an
empty propagation history, the set of variables in the goal and a set of “used”
identifiers.
The first derivation step is a Simplify transition with the f lip rule:
h(((x1 = y2 )3 ∧ (f (f (x4 )5 )6 = x7 )8 )9 ∧ (y10 = f (f (f (y11 )12 )13 )14 )15 )16 , ∅,
{x, y}, {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16}i
֌
h(((x1 = y2 )3 ∧ (x17 = f (f (x18 )19 )20 )21 )9 ∧ (y10 = f (f (f (y11 )12 )13 )14 )15 )16 , ∅,
{x, y}, {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21}i
We have replaced the annotated subterm (f (f (x4 )5 )6 = x7 )8 with x17 =
f (f (x18 )19 )20 )21 (i.e. flipped the operands to the equality) and reannotated the
19

new term with fresh identifiers. These were also added to the set of used identifiers. Since the propagation history is empty, it remains unchanged.
The next derivation step is a Simpagate transition with the vsubs rule.
h(((x1 = y2 )3 ∧ (x17 = f (f (x18 )19 )20 )21 )9 ∧ (y10 = f (f (f (y11 )12 )13 )14 )15 )16 , ∅,
{x, y}, {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21}i
֌
h(((x1 = y2 )3 ∧ (y21 = f (f (x18 )19 )20 )21 )9 ∧ (y10 = f (f (f (y11 )12 )13 )14 )15 )16 , ∅,
{x, y}, {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22}i
The conjunctive context for subterm x17 is
cc(Ga , p) = (x1 = y2 )3 ∧ (y10 = f (f (f (y11 )12 )13 )14 )15 ∧ true
where Ga is the current goal and p is the position of x17 . The first conjunct
matches the conjunctive context of the vsubs rule, thus subterm x17 is replaced
with y21 . Identifier 21 is added to the list of used identifiers.
Execution proceeds until the final state
h(x = y ∧ y = f (y)) ∧ true, ∅, {x, y}, Pi
is reached, for some annotation of the goal and some set of identifiers P. This is
a final state because no more rules are applicable to it.
AC matching and propagation histories. Consider the propagation rule
from the leq program:
trans @ leq(X, Y ) ∧ leq(Y, Z) =⇒ X 6≡ Y ∧ Y 6≡ Z | leq(X, Z)
and the initial state
hleq(A1 , B2 )3 ∧4 leq(B5 , A6 )7 , ∅, {A, B}, {1, 2, 3, 4, 5, 6, 7}i.
We can apply Propagate directly (i.e. without permuting the conjunction)
to arrive at the state:
h(leq(A1 , B2 )3 ∧4 leq(B5 , A6 )7 ) ∧8 leq(A9 , A10 )11 ,
{trans @ (3 1 2 7 6 5)}, {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11}i.
The propagation history prevents the rule from firing on the same terms
again, however we can permute the terms to find a new matching. Namely, we
can permute the annotated goal (which we call Ga )
(leq(A1 , B2 )3 ∧4 leq(B5 , A6 )7 ) ∧8 leq(A9 , A10 )11
to
(leq(B5 , A6 )7 ∧4 leq(A1 , B2 )3 ) ∧8 leq(A9 , A10 )11 .
20

The latter is an element of [Ga ]AC , and the identifiers have been preserved in the
correct way. The entry trans @ (7 6 5 3 1 2) is not in the propagation history,
so we can apply Propagate again to arrive at:
h((leq(B5 , A6 )7 ∧4 leq(A1 , B2 )3 ) ∧12 leq(B13 , B14 )15 ) ∧8 leq(A9 , A10 )11 ,
{trans @ (3 1 2 7 6 5), trans @ (7 6 5 3 1 2)}, {1...15}i.
Now the propagation history prevents the rule trans being applied to the
first two leq constraints. The guard also prevents the trans rule firing on either
of the two new constraints,6 thus we have reached a final state.
Updating propagation histories. Consider a modified version of the previous
example, now with two rules:
X ∧ X ⇐⇒ X
trans @ leq(X, Y ) ∧ leq(Y, Z) =⇒ leq(X, Z)
The first rule enforces idempotence of conjunction.
Consider the initial state:
hleq(A1 , A2 )3 ∧4 leq(A5 , A6 )7 ∧8 leq(A9 , A10 )11 , ∅, {A}, {1...11}i
We apply the trans rule to the first two copies of the leq constraint (with identifiers 3 and 7).
hleq(A1 , A2 )3 ∧4 leq(A5 , A6 )7 ∧8 leq(A9 , A10 )11 ∧12 leq(A13 , A14 )15 ,
{trans @ (3 1 2 7 5 6)}, {A}, {1...15}i
Next we apply idempotence to leq constraints with identifiers 7 and 11.
hleq(A1 , A2 )3 ∧4 leq(A16 , A17 )18 ∧12 leq(A13 , A14 )15 ,
{trans @ (3 1 2 7 5 6), trans @ (3 1 2 18 16 17)}, {A}, {1...18}i
An extra entry (trans @ (3 1 2 18 16 17)) is added to the propagation history
in order to satisfy the requirements of Definition 6. This is because we have
replaced the annotated constraint leq(A5 , A6 )7 with the newly annotated term
leq(A16 , A17 )18 , which defines an identifier renaming
ρ = {5 7→ 16, 6 7→ 17, 7 7→ 18}.
Since E = (trans @ (3 1 2 7 5 6)) is an element of the propagation history, we
have that ρ(E) = (trans @ (3 1 2 18 16 17)) must also be an element, and hence
the history is expanded.

6

Without the guard both ACDTR and CHRs are not guaranteed to terminate.

21

