Ke Li.

Dag representation and optimization of rewriting online

. (page 1 of 2)
Online LibraryKe LiDag representation and optimization of rewriting → online text (page 1 of 2)
Font size
QR-code for this ebook

', i •■.•!••/!■. ■l.WJilV.'TSliT .-•Wi T.;iV

Computer Science Department


Dag Representation and
Optimization of Rewriting

Ke Li

Technical Report 518

September 1990


(0 ?
loo C ^

4J O

Pi «5

4J C

M r, |1 jD^a^l. □

Termination and Confluence

We say a TRS R is terminating if for any term /. there is no infinite rewriting chain
using R for t.

Proposition A If R i» terminating, then Rdag z-'* terminating.

Proof: If there is an infinite sequence of rewritings using Rjag- hy proposition 3. we
can construct an infinite secjuence of rewritings using R. contrary to tlie conchtion
that 7? is terminating. Therefore. R^ag is terminating. D

A TRS R is said confl.uent if for any t. two rewriting clcri\"ations / — « .sj and / — >_.

imply that there exists a term t' such that there are two rewriting derivations .Si -^ t'

and $2 — ♦ ^'•

Unfortunately, the condition that 7? is confluent does not guarantee that R.^.^g
is confluent. One of courter-examples is given by [HPSSb]: R — {/(.r) — > g(.r..r).
f(a) — > .V. g(a.a') — > A', a — > a', a' — » a]. R is confluent for tree representation. For
dag representation, term f(a) can be rewritten to A' and g(a.a). but the latter can
only be rewritten to g(a'.a'). that means g(a.a) cannot be rewritten to .V liy rule
gia.a') -^ X.

In this paper, our major concern is that given a terminating and confluent TRS.
how to compute normal forms for terms fast. Fortunately, if 7? is hofli terminating
and confluent, we can guarantee that Rdag is terminating and confluent. To j^rove
this, we need the proposition below:

Proposition 5 t is reducible using R if and only iftjag ^-^ reducible u.^ing Rd^g-

Proof: First, because matching (special case of uniflcation) between dags ol:)tains
the same substitution for variables as matching between the corresponding trees (see
[PW7S]), we have the claim that t can be matched by .s if and only if tjag can be
matched by s^ag-

Therefore, t can be rewritten by a rule r from 7? if and only if /j,,., can be rewritten
by the corresponding rule of r from Rdag- n

Proposition G If R !.>•• terminating and confluent, then Rdag z-' trrminafinq and con-

Proof: Termination of Rdag is proved above. \\'e prove confluence of Rdag '^^ follows.
Given any term tjag- suppose there are two rewriting derivations tdag — * ^dag f '"2 in R
such that a non-variable subterm of /j can be unified with I2. excei)t that /j -+ 7-1 and
/o -^ '"2 are the same rule and the non-variable subterm is /i itsrlf.

Because unification between dags obtains the same suljstitution for variables as
unification between corresponding trees (see [PW7S]). for R and corresponding Rdag-
if there are two rules Idag -^ rdag in Rdag and /^^^ -► r^^^ such that a non-variable
subterm of Idag can be unified with I'^^^. then we have two rules in / ^ r and /' -^ r'
in R such that a non-variable subterm of / can be imified with /'. Therefore, we have
Proposition 7 If R la non- ambiguous, then Rdag is non-ambiguous.

Normal Form Computation

We are concerned about how to eflRciently compute normal forms for terms gi\-en
terminating and confluent TRSs. For a terminating and confluent TRS. any term
has a unique normal form. We have already shown that if R is terminating and
confluent, then Rdag is terminating and confluent. Naturally, we would ask if any f
has the same normal form using R as tdag has using Rdag-

Proposition 8 If R is te.rm,ina.ting and confluent, the normal form of any term f
using R is the tree representation of the normal form, of tdag using Rdag-

Proof: By proposition 6. Rdag is terminating and confluent, tdag has a unique normal
form t'^^g. that means, there is a dag rewriting derivation Ddag using Rdag that rewrites
idag to t'^^g. By proposition 3. there is a tree rewriting derivation D using R that
rewrites t to /'. By proposition 5. /' is irreducible. Since / has only one normal form.
t' is the unique normal form of /. n

Intuitively, for a terminating and confluent TRS. we can use the corresponding dag
TRS to compute the unique normal form for any term more efficiently, since several
rewriting steps in tree rewriting are replaced by one dag rewriting step. Stai)le"s
speed-up theorem in [StaSOb] implies the following proposition:

Proposition 9 Let R be a and non -ambiguous TRS. i be a.ny term. \f\
the length of the shortest derivation to compute t 's normal form, and \tdag\ ibe length
of the shortest derivation to compute tdag'^" normal form. Then. \tdag\ < |'|-


The '"graph rewriting" [BEG87] and "jungle evaluation'" [HPSSa] have some trouble
when they are used for non-lcft-linear rewriting systems. Our systems can be eas-
ily used for non-lcft-linear systems. The matching algorithm has no problem when
dealing with non-linear terms represented by dags [PW7S]. In dag representation,
the same variables share the same node. Therefore, the dag rewriting for a non-lcft-
linecir rule is no different from the dag rewriting for a left-linear. To make clear, we
give an example for a non-left-linear system. Meanwhile, to show how dag rewriting
saves rewriting steps, we draw out for tree rewriting and dag rewriting all jiossiljle
derivations that rewrite a given term to its normal form. See figure 4. Wc simply see
that by dag rewriting, we ha\'e not only shorter derivations but also a much smaller
term space (that are all terms in all derivations). This becomes important when we
design strategies for optimization of rewriting. In the following section, we will give
several efficient strategies.

Example. System={/(x, x) —^ g{h{x). x). g{x. y) — > A'(x. y).a — > c. h — + d] and term



f(c,a) g(h(a).a) f(c.c7g(h(^c),a) gXhla).c)^ X(h(<

g(li(c^) N{h(a).a)

dag rewriting

Figure 4

4 Optimization of Dag Rewriting

Dag representation of rewriting systems can speed up the rewriting process, as de-
scribed in the previous sections. In this section, we will consider how to speed up
dag rewriting and propose several strategies for this purpose.

Optimization of rewriting has been discussed on tree representation [HL79]. Sonu-
researches [BL79][PMT74] have been done for dag rewriting, but they addressed only
recursive programs, other than term rewriting systems that are our target.

Let f be a term and x a variable. N urn\'ar(x J) denotes the number of occur-
rences of J mi. We define:


Variable -fewer TRS: For any variable x and any rule / — > r. .\ inv^'ari.r. I) >


Online LibraryKe LiDag representation and optimization of rewriting → online text (page 1 of 2)