Information Technology Reference
In-Depth Information
the original signature. Section 5 contains examples. In Section 6 we discuss the
influence of the ordering on the eciency of our method and present complexity
results. A full version of this article with proofs and more examples is available
at: http://www.csis.pace.edu/ scharff/CC .
2
Preliminaries
We assume the reader is familiar with standard terminology of equational logic
and rewriting. Key definitions are included below, more details can be found
in [1, 4]. In the following, let Σ
be disjoint sets of function symbols. We
call Σ the (basic) signature ,and Σ ∪K
and
K
the extended signature . The elements of
K
are assumed to be constants, and are denoted by subscripted letters c i ( i ≥
0).
Flat Ground Terms. The height
H
of a term is recursively defined by: if
t
is a variable, then
H ( t ) = 0, otherwise
H ( t )= H ( f ( t 1 ,...,t n )) = 1 +
max{H ( t 1 ) ,...,H ( t n )
. A term is said to be flat if its height is 2 at most.
We will consider flat ground terms, i.e., variable-free terms t with H ( t )
}
2.
D-Rules, C-Rules, C-Equalities. A D -rule on Σ∪K
is a rewrite rule f ( c 1 ,...,
c n )
→ c 0 ,where f ∈ Σ
is a function symbol of arity
n
and
c 0 ,c 1 ,...,c n
are
constants of
(respectively, a C -equality )isarule c 0 → c 1
(respectively, an equality c 0 ≈ c 1 ), where c 0 and c 1 are constants of
K
.A C -rule on Σ ∪K
K
.
The constants in
will essentially serve as names for equivalence classes of
terms. Thus, an equation c i ≈ c j
K
indicates that c i and c j
are two names for the
same equivalence class. A constant c i
is said to represent aterm t ∈T
( Σ ∪K
)
via a rewrite system R ,if t ↔ R c i .
Abstract Congruence Closure: A ground rewrite system R = D ∪ C
of D
and C -rules on Σ∪K
is called an abstract congruence closure if: (i) each constant
c 0 ∈K
represents some term t ∈T
( Σ )via R and (ii) R is convergent. If E
is
a set of ground equalities over
T
( Σ ∪K
)and R an abstract congruence closure
( Σ ), s ↔ E t if, and only if, there exists a term
u with s → R u ← R t ,then R is called an abstract congruence closure of E .That
is, the word problem for an equational theory E can be decided by rewriting to
normal form using the rules of an abstract congruence closure R of E .
such that for all terms s and t in
T
3
Graph-Based Congruence Closure
We describe a graph-based method for computing an abstract congruence clo-
sure of a given set of ground equalities E over a signature Σ . First a directed
acyclic graph (DAG) is constructed that represents the set E ,aswellasterms
occurring in E . In addition, each vertex of this initial graph is labeled by a
distinct constant c i
. Next various graph transformation rules are applied
that represent equational inferences with the given equalities. Specifically, there
are four mandatory rules ( Orient , SR , RRout ,and Merge ) and one optional
rule ( RRin ). Exhaustive application of these rules, or saturation , will under cer-
tain reasonable assumptions yield an abstract congruence closure. The vertices
of each (initial and transformed) graph represent equivalence classes of terms.
of
K
Search WWH ::




Custom Search