Online Library → Ke Li → Dag representation and optimization of rewriting → online text (page 1 of 2)

Font size

', i â€¢â– .â€¢!â€¢â€¢/!â– . â– l.WJilV.'TSliT .-â€¢Wi T.;iV

Computer Science Department

TECHNICAL REPORT

Dag Representation and

Optimization of Rewriting

Ke Li

Technical Report 518

September 1990

NEW YORK UNIVERSITY

(0 ?

loo C ^

4J O

Pi Â«5

4J C

C O

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-

fluent.

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 term.inat.ing 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\ < |'|-

Non-left-linear

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

fia.a).

f(a.a

f(a,a;

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

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

X(h(c).c)

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:

10

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

Computer Science Department

TECHNICAL REPORT

Dag Representation and

Optimization of Rewriting

Ke Li

Technical Report 518

September 1990

NEW YORK UNIVERSITY

(0 ?

loo C ^

4J O

Pi Â«5

4J C

C O

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-

fluent.

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 term.inat.ing 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\ < |'|-

Non-left-linear

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

fia.a).

f(a.a

f(a,a;

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

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

X(h(c).c)

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:

10

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

1 2

Online Library → Ke Li → Dag representation and optimization of rewriting → online text (page 1 of 2)