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