Information Technology Reference
In-Depth Information
Transformed graphs need not be acyclic, but will conform to full structure shar-
ing in that different vertices represent different terms (or equivalence classes).
The transformation rules crucially depend on an ordering
1
.
on
K
3.1
Initial Graphs
We consider directed graphs where each vertex
v
is labeled by (i) a function
symbol of
, denoted by
Constant
(
v
). In addition, edges are classified as
equality
,
rewrite
,or
subterm
edges. We write
u −
E
v
and
u →
R
v
to denote equality and rewrite edges (be-
tween vertices
u
and
v
), respectively. Subterm edges are also labeled by an index,
and we write
u →
i
S
v
. Informally, this subterm edge indicates that
v
represents
the
i
-th subterm of the term represented by
u
.
An
initial
graph
DAG
(
E
) represents a set of equalities
E
as well as the
subterm structure of terms in
E
. It is characterized by the following conditions:
(i) If
Symbol
(
v
) is a constant, then
v
has no outgoing subterm edges; and (ii)
if
Symbol
(
v
) is a function symbol of arity
n
, then there is exactly one edge of
the form
v →
i
S
v
i
,foreach
i
with 1
Σ
, denoted by
Symbol
(
v
), and (ii) a constant of
K
≤ i ≤ n
. (That is, the number of outgoing
vertices from
v
reflects the arity of
Symbol
(
v
).)
The term
Term
(
v
)
represented
by a vertex
v
is recursively defined as follows:
If
Symbol
(
v
) is a constant, then
Term
(
v
)=
Symbol
(
v
); if
Symbol
(
v
) is a func-
tion symbol of arity
n
,then
Term
(
v
)=
Symbol
(
v
)(
Term
(
v
1
)
,...,Term
(
v
n
)),
where
v →
i
S
v
i
,for1
≤ i ≤ n
.Evidently,
Term
(
v
) is a term over signature
Σ
.
We require that distinct vertices of
DAG
(
E
) represent different terms. More-
over, we insist that
DAG
(
E
) contain no rewrite edges and that each equality
edge
u −
E
v
correspond to an equality
s ≈ t
of
E
(with
u
and
v
representing
s
and
t
, respectively), and vice versa.
The vertices of the graph
DAG
(
E
) also represent flat terms over the ex-
tended signature
. More specifically, if
Symbol
(
v
) is a constant, then
ExtTerm
(
v
)=
Constant
(
v
), and if
Symbol
(
v
) is a function symbol of ar-
ity
n
,then
ExtTerm
(
v
)=
Symbol
(
v
)(
Constant
(
v
1
)
,...,Constant
(
v
n
))
,
where
v →
i
S
v
i
,for1
Σ ∪K
≤ i ≤ n
.
We should point out that the labels
Constant
(
v
) allow us to dispense with the
extension rule of abstract congruence closure [2, 3]. The initial graph
DAG
(
E
)
contains only subterm and equality edges. Rewrite edges are introduced during
graph transformations. The term representation schema for transformed graphs
is also more complex, see Section 4.
3.2
Graph Transformation
We define the graph transformations by rules. The first rule,
Orient
,canbe
used to replace an equality edge,
v −
E
w
,byarewriteedge,
v →
R
w
,provided
Constant
(
v
)
Constant
(
w
). If the ordering
is total, then every equality edge
1
An ordering is an irreflexive and transitive relation on terms. An ordering
is total,
if for any two distinct terms
s
and
t
,
s t
or
t s
.
Search WWH ::
Custom Search