Ke Li. # Approximate and optimal strategies for non-ambiguous and left linear term rewriting systems online

. **(page 1 of 2)**

Online Library → Ke Li → Approximate and optimal strategies for non-ambiguous and left linear term rewriting systems → online text (page 1 of 2)

Font size

mr^Pl^^^'

Computer Science Department

TECHNICAL REPORT

Approximate and Optimal Strategies

for Non-ambiguous and Left Linear

Term Rewriting Systems

Ke Li

Technical Report 475

November 1989

NEW YORK UNIVERSITY

in

I

O 5 where t and 5 are terins. As a convention,

if a \'ariable occurs at the right side of a rule, it must be occur at the left side of

the rule. Generally, a term rewriting system is denoted by R and is abbreviated by

TRS.

A â– position within a term is a sequence of positive integers, describing the path

from the root function symbol to the head of the subterm at that position. For

example, 2.2 is the position of y in term g{a, f(x,y), z). By i/p, we denote the

subterm of t at position p. If the subterm t/j) of term t is replaced by term s, we

denote the new term by t[s]p. A substitution is a mapping from variables to terms.

If cr is a substitution, a can be extended to a function from terms to terms in such

a way that f(ti, ...,tâ€ž)a = f{i\a, ...,tâ€ža). Term t matching with term 5 means there

is a substitution a such that ta = s. t unifi.able with .^ means there is a substitution

a such that to â€” so. Term i rewTites to term 5, denoted by < â€” > 5, if there are

position p in r being applied to t matches with t itself other than

a proper subterm of t. Given a TRS R, if term t â€”* t and t cannot be rewritten

further by rules in R, we say t is irreducible and i is a normal form of t.

A TRS is terminating if for any term t there is no infinite chain t â€”^ ti â€”* t2 â€”^ â– â– â– â€¢

A TRS is confluent, if we have t â€”^ S\ and ^ -^ ^2, then there exists a term u such

that s\ -^ u and S2 â€”* u. It is easy to show that for any terminating and confluent

TRS, a term has a unique normal form. Any TRS to be discussed is assumed

terminating.

Given a term rewriting system, any term which is matched by a left side of a

rule is called a redex (of the rule). If a redex is not a proper subterm of any redex,

it is called an outermost redex. Let i be a term and s a proper subterm of t. The

path from the root of t to the root of s (excluding the root of 5) is called the root

path of s in t. Let i be a term, 5 a proper subterm of i, and s a redex. If the root

path of a variable at the left side of a rule r matches a substring of the root path

of 5 in i, 5 is called a variable redex (of r) in t.

Subclasses of TRS

â€¢ Non-ambiguous TRS: Thei'e are no pair of left sides t and 5 of the rules such that

a non- variable subterm of t is unifiable with ^. If the left side of rule 7- is unified

with a non-variable subterm of the left side of rule r', we say r superposes r'.

â€¢ Left-linear TRS: Any variable occurs at left side of any rule at most once.

â€¢ Right-linear TRS: Any variable occurs at right side of any rule at most once.

â€¢ Linear TRS: Both left linear and right linear.

â€¢ Variable less TRS: For each rule, if variable x occurs at both left side and right

side, the number of occurrences at right side is not greater than that at left side.

â€¢ Variable more TRS: For each rule, if variable x occurs at both left side and right

side, the number of occurrences at left side is not greater than that at right side.

â€¢ Varaible equal TRS: For each rule, if variable x occurs at both left side and right

side, the numbers of occurrences at both sides are equal.

It is interesting to know Dauchet's result [DauS9] that any Turing machine can

be simulated by only one rule which is non-ambiguous, left-linear and \'ariable more.

In his paper, variable more is said variable preserving.

A non-ambiguous TRS is a confluent TRS [HuetS0][KB70]. In the following, we

only consider non-ambiguous and left linear TRSs, so any TRS to be addressed is

assumed both terminating and confluent.

Rewriting strategies

â€¢ Outermost strategy. To rewrite a term, choose an outermost redex.

â€¢ Variable-delay strategy. To rewrite a term, if there are non-variable-redexes,

choose a non-variable-redex to rewrite; otherwise, arbitrarily choose a variable-

redex to rewrite.

â€¢ Innermost strategy. To rewrite a term, choose an innermost redex.

A rule applied "to", "on", "inside", "above" a term: Let rule r rewrite term t.

If r root-writes t, we call r is applied on t or the rewriting of r occurs on t; if r

root-writes a proper subterm of i, we call t is applied inside t or the rewriting of r

occurs inside i; if we don't care whether this rewriting occurs on or inside t, we say

r is applied to t or the rewriting of r occurs to t. Let 6 be a proper subterm of t. If

r root-writes a subterm of t which is a proper superterm of s, we say the rewriting

occurs above s in t.

A sequence of rewritings which reduce a term to its normal form is called a

derivation (for that term). We may talk about a deriv'ation without mentioning a

term the derivation is applied to. In this case we keep in mind that the derivation

is applied to some term. Let D he a derivation for a term. The ith rewriting in

D is called the ith derivation step and denoted by D\i]. D[i,j]{i < j) denotes all

rewritings from D[i] through D[j]. \D\ is the' length of D that is the number of

rewritings in D. If two derivations reduce the same term to its normal form (the

normal form is unique because of confluent property), they are called equivalent

derivations. Given a TRS and a term, a deri\^tion with the shortest length among

all the equivalent derivations for that term is called an optimal derivation (for that

term). We call a derivation an outermost derivation if in each derivation step,

use outermost strategy. We call a derivation a variable- delay derivation if in each

derivation step, use variable-delay strategy. We call a derivation an innermost

derivation if in each derivation step, use innermost strategy.

Let s be a proper subterm of term t. Any proper subterm of t whose root is not

on the root path of 5 in ^ is called a general sibling.

3 Non-ambiguous, Left linear and Variable Less

TRSs

Combining conditions left linear and ^-ariable less together is condition linear. In

this part, we discuss approximate strategies for non-ambiguous and linear TRSs. '

Proposition 1. For a non-ambiguous TRS, if t is a redex of rule r : s â€”* s' and

a proper subterm t' of t is a redex, t' must be a variable redex of r in t.

Proof. If t' is not a variable redex of r in i, by the condition that t is a redex of r, t'

is matched by a non-\-ariable subterm of s. Suppose rule r' root-rewrites t'. Then

r' superposes r, contrary to the non-ambiguity condition. â–¡

Proposition 2. For a non-ambiguous TRS, only one rule can root-rewrite a term.

Proof. If two rules can root-rewrite a term, then the left sides of the rules will be

able to unify with each other, contrary to the non-ambiguity condition. â–¡

Theorem 1. For a non-ambiguous and linear TRS, each non-outermost derivation

D has an equivalent outermost derivation D' which has no more derivation steps

than D.

Proof. Let R he a. non-ambiguous and linear TRS, D a derivation, and tail-

length(D) the length of the subderivation in D from the first non-outermost rewrit-

ing through the end.

We use induction on tail-lengthfD) to prove:

Claim: D is equi\'alent to an outermost derivation D' such that tail-length(r)')=0

and \D'\ < \D\.

Basis. tail-length(D)â€” 0. Trivial.

Induction. Suppose the claim holds for the derivation with less tail-length function

value than D. Suppose the first non-outermost rewriting occurs on the redex s.

There must be an outermost redex Sout containing s properly. Since R is non-

ambiguous, 5 must be a variable redex in Sout- Suppose the rule appliable on Sout

is r which has variables xi,...,Xk at the left side and the subterms matched with

xi,...,Xk are Si,...,^^. 5 is a subterm of one of {si, ...,5^). Suppose Dta,i is the

subderivation of D from the rewriting of s through the end. We discuss in cases

what rewriting will happen to Sont or above Sout in Dtaii- Let Dkead denote the

remaining subderivation in D except Dtaii-

Case 1. All rewritings to Sout or above are applied only on or inside s\, ...,Sk. This

case is impossible since r will be appliable, even in the case that R is non-left-linear.

Because identical terms will be rewritten to a same term by the confluence property.

In the following cases, suppose r' is the first rule applied on a redex that is not a

subterm of any one of 5i, ..., Sk and r' is applied to or above Sout â–

Case 2. r' is applied on a proper subterm of Sout- f' superposes r, contrary to the

condition that R is non-ambiguous, so this case is impossible.

Case 3. r' is applied on Sout- Before r' is applied, all rewritings to Sout must be on

or inside Si,...,Sk by case 2. Suppose s, becomes 5,(1 < i < k) and Sgut becomes

^out i^^* before r' is applied.

Because R is left-linear, obviously Xi matches s'-{l < i < k) and r can be applied

on s'g^f. By proposition 2, r' = r.

We move rewriting by r in front of the rewriting on 5, D becoming D' . We

suppose that in D the rewriting on s is D\i] and the rewriting on Sout is -DfiKi < j).

Suppose Sout is rewritten to s'^^^ by r in D' and 5^â€ž( is rewritten to ^"^^ by r in D.

s^^f and s^^( are the same except the changes to ^i, ...,Sk- Since R is linear, we can

assume the variables at the right side of r are x,j , ..., x,:,(l < ii < ... < ij < k).

In D', all 5,j,...,s,j are rewritten to s\^.,...,s\^ by the same rewritings between D[i]

and D[j] in D. All other rewritings between D[i\ and Z>[j] occur on the general

siblings of Sout and they are not affected by moving of the rewriting on Sout-, so they

can be applied in D' . Hence, D' is equivalent D and \D'\ < \D\. tail-length(D') <

tail-length(D). By induction hypothesis, the claim holds for D'.

Case 4. r' is applied above Sout- By case 2, before r' is applied, all rewriting to

Sout rnust be on or inside 3i,...,5a-. If Sout were not a \'ariable redex of r', r would

superpose r'. Therefore Sout is a variable redex of r'. Suppose the term being

rewritten by r' is t. By proposition 1, all proper subterms in t not corresponding to

variables of r' are normal forms. Suppose deri\^tion D^uh reduces a proper subterm

t' of t to its normal form and one step of Dguh is in Dtaii- Obviously, tail-length(Â£)su6)

< tail-length(D). By induction hypothesis, we can obtain an outermost derivation

Dj^(, equivalent to Dsub and |I?sâ€ž(,| < l-D^ubl- Hence, we can move all steps of D^^f,

in front of the rewriting step of 5, and obtain a deri\^tion equix'alent to D with less

tail-length function value. Using the induction hypothesis again for the modified

D, we can prove the claim holds for D. Therefore we can assume that in D, all

derivation steps used in rewriting all proper subterms in t not corresponding to the

variables in r' are in Dkead- In this case, r' is appliable at the beginning of Dtaii, but

this is contrary to the supposition that r is an outermost redex at the beginning of

Dtail-

We have enumerated all cases. The claim does hold. The theorem immediately

follows the claim. r-j

Corollary 1. For any non- ambiguous and linear system, given any term, there

must be an outermost derivation that is optimal among all the derivations for that

term.

The following examples show the importance of the conditions in theorem 1.

Example 1. (Non-ambiguous)

Ambiguovis system: f{a) â€” > f{g{a)), g{a) -^ b, ,a â€”y b

Outmost derivation: f{a) â€” > f{g{a)) â€”* f{b)

Non-outermost derivation: /(a) â€” > f{b)

Example 2. (Left linear and \-ariable less)

Non-right-less system: f{x) â€”* g{x,x),a â€”y b

Outermost derivation: /(a) â€” > g{a,a) â€” > g{b,a) â€”>â– g{b,b)

Non-outermost deriv'ation: /(a) â€” > f{b) â€” > g{b,b)

Proposition 3. Given any non-ambiguous TRS and any term t, if a subterm s of

t is a non-variable redex in t, it m.ust be an outermost redex in t.

Proof. If .s were not an outermost redex in t, there vi'ould be an outermost redex s'

in t vi'hich contains s. By non-ambiguity property, s must be a variable-redex in s\

which is contrary to the given condition. â–¡

Proposition 4. For any non- ambiguous TRS, a variable- delay derivation is an

outermost derivation.

Proof. Let D he & non-outermost deri\'ation for a term. There must be a derivation

step in D such that a non-outermost redex is rewritten. Suppose the non-outermost

redex is s and the outermost redex containing .s is Sout- By non-ambiguous condition,

s must be a variable redex of Sout- By variable-delay strategy, 5 cannot be chosen.

Therefore D is not a \^nable-delay derivation. q

In the case multiple outermost redexes are available, choosing different outer-

most redex has different effect on the length of deri'vations. Variable-delay strategy

seems better than outermost strategy. See the following example.

Example 3.

System: /(x,6) â€”* N ^a ^> b^c -^ d

Outermost deri\'ation: f{c,a.) â€” > f{d,a) â€” > f(d,b) â€”* N

Variable-delay derivation: f{c,a){c is a variable redex) â€”y f{c,b) â€” > A'^

In the above example with the initial term /(c, a), we have two outermost redexes

c and a. By outermost strategy, we arbitrarily choose c or a. But c is a variable redex

of rule f{x,b) â€” > N. Therefore, b}'^ \^riable-delay strategy only a can be chosen.

The more important is that any rewriting on c is wasteful, since the variable x in

the rule /(x, b) â€” > A'^ can match any term when the rule is applied.

Lemma 1. Let D be an outermost derivation of a non-ambiguous TRS and t a

non-variable outermost redex after some steps of D. In D, t remains a non-variable

outermost redex until it is rewritten.

Proof. Suppose after D[i] in D, t is a non-variable outermost redex. If t is no longer

a non-variable outermost redex after D[?4-l], there are only two possibilities: t itself

is rewritten at step D[i + 1] or a redex t' which is above t is rewritten at step Z)[i + 1].

For the lemma, we only need to discuss the latter case. Because t is a non-variable

redex, t is unifiable with a non-\'ariable subterm of \D'\, \D'\ = n. We will construct a derivation D" such that D" is equi\'alent

to D\ \D"\ = n, and D" - D[l,n].

We can prove existence of D" formally by induction. The technique is similar

to the proofs for theorems 1 and 2. Here we give only the challenging part - at the

induction step.

Suppose D[l, I - 1] = D'[l,i - 1] and D[i] j^ D'[i]. That means, after D[i - 1]( =

D'[i â€” 1]), there are multiple non-\^riable outermost redexes, so that D and D'

choose different ones to rewrite. Suppose D rewrites redex t and D' rewrites redex

t'. By lemma 1, a rewriting on t will occur in D'[j] in D' (?' < j < n). Construct

D": '

D"[l,i] = D[l,t]

D"[i + l,j] = D'[t,j-l]

D"[j + l,n] = D'[j + l,n]

Because t is a non-variable outermost redex, any non-\'ariable outermost redexes

rewritten in D'[i,j â€” 1] cannot be above or inside t, so that the rewriting on t does

not affect rewritings in D'[i,j â€” 1]. Furthermore, rewritings oi D'[\,j] and D"[l,j]

generate the same term, which can be reduced to its normal form by D"[j + l,n].

We have proved D" is equivalent to D'. D" has longer identical prefix with D than

D' . By induction, we eventually obtain a derivation D'" such that D'" is equivalent

to D, \D"'\ < |D|, and D'" is identical to the prefix of D. This is ridiculous because

this means D'" does not reduce to normal form.

We conclude that such D and D' cannot exist. â–¡

Lemma 3. For a non-ambiguous TRS, if for a term there is a variable- delay deriva-

tion without any variable redex rewriting, then any variable- delay derivation for that

term has no rewriting on variable redexes.

Proof. Let D and D' be equivalent \^riable-delay derivations, D has no rewritings

Computer Science Department

TECHNICAL REPORT

Approximate and Optimal Strategies

for Non-ambiguous and Left Linear

Term Rewriting Systems

Ke Li

Technical Report 475

November 1989

NEW YORK UNIVERSITY

in

I

O 5 where t and 5 are terins. As a convention,

if a \'ariable occurs at the right side of a rule, it must be occur at the left side of

the rule. Generally, a term rewriting system is denoted by R and is abbreviated by

TRS.

A â– position within a term is a sequence of positive integers, describing the path

from the root function symbol to the head of the subterm at that position. For

example, 2.2 is the position of y in term g{a, f(x,y), z). By i/p, we denote the

subterm of t at position p. If the subterm t/j) of term t is replaced by term s, we

denote the new term by t[s]p. A substitution is a mapping from variables to terms.

If cr is a substitution, a can be extended to a function from terms to terms in such

a way that f(ti, ...,tâ€ž)a = f{i\a, ...,tâ€ža). Term t matching with term 5 means there

is a substitution a such that ta = s. t unifi.able with .^ means there is a substitution

a such that to â€” so. Term i rewTites to term 5, denoted by < â€” > 5, if there are

position p in r being applied to t matches with t itself other than

a proper subterm of t. Given a TRS R, if term t â€”* t and t cannot be rewritten

further by rules in R, we say t is irreducible and i is a normal form of t.

A TRS is terminating if for any term t there is no infinite chain t â€”^ ti â€”* t2 â€”^ â– â– â– â€¢

A TRS is confluent, if we have t â€”^ S\ and ^ -^ ^2, then there exists a term u such

that s\ -^ u and S2 â€”* u. It is easy to show that for any terminating and confluent

TRS, a term has a unique normal form. Any TRS to be discussed is assumed

terminating.

Given a term rewriting system, any term which is matched by a left side of a

rule is called a redex (of the rule). If a redex is not a proper subterm of any redex,

it is called an outermost redex. Let i be a term and s a proper subterm of t. The

path from the root of t to the root of s (excluding the root of 5) is called the root

path of s in t. Let i be a term, 5 a proper subterm of i, and s a redex. If the root

path of a variable at the left side of a rule r matches a substring of the root path

of 5 in i, 5 is called a variable redex (of r) in t.

Subclasses of TRS

â€¢ Non-ambiguous TRS: Thei'e are no pair of left sides t and 5 of the rules such that

a non- variable subterm of t is unifiable with ^. If the left side of rule 7- is unified

with a non-variable subterm of the left side of rule r', we say r superposes r'.

â€¢ Left-linear TRS: Any variable occurs at left side of any rule at most once.

â€¢ Right-linear TRS: Any variable occurs at right side of any rule at most once.

â€¢ Linear TRS: Both left linear and right linear.

â€¢ Variable less TRS: For each rule, if variable x occurs at both left side and right

side, the number of occurrences at right side is not greater than that at left side.

â€¢ Variable more TRS: For each rule, if variable x occurs at both left side and right

side, the number of occurrences at left side is not greater than that at right side.

â€¢ Varaible equal TRS: For each rule, if variable x occurs at both left side and right

side, the numbers of occurrences at both sides are equal.

It is interesting to know Dauchet's result [DauS9] that any Turing machine can

be simulated by only one rule which is non-ambiguous, left-linear and \'ariable more.

In his paper, variable more is said variable preserving.

A non-ambiguous TRS is a confluent TRS [HuetS0][KB70]. In the following, we

only consider non-ambiguous and left linear TRSs, so any TRS to be addressed is

assumed both terminating and confluent.

Rewriting strategies

â€¢ Outermost strategy. To rewrite a term, choose an outermost redex.

â€¢ Variable-delay strategy. To rewrite a term, if there are non-variable-redexes,

choose a non-variable-redex to rewrite; otherwise, arbitrarily choose a variable-

redex to rewrite.

â€¢ Innermost strategy. To rewrite a term, choose an innermost redex.

A rule applied "to", "on", "inside", "above" a term: Let rule r rewrite term t.

If r root-writes t, we call r is applied on t or the rewriting of r occurs on t; if r

root-writes a proper subterm of i, we call t is applied inside t or the rewriting of r

occurs inside i; if we don't care whether this rewriting occurs on or inside t, we say

r is applied to t or the rewriting of r occurs to t. Let 6 be a proper subterm of t. If

r root-writes a subterm of t which is a proper superterm of s, we say the rewriting

occurs above s in t.

A sequence of rewritings which reduce a term to its normal form is called a

derivation (for that term). We may talk about a deriv'ation without mentioning a

term the derivation is applied to. In this case we keep in mind that the derivation

is applied to some term. Let D he a derivation for a term. The ith rewriting in

D is called the ith derivation step and denoted by D\i]. D[i,j]{i < j) denotes all

rewritings from D[i] through D[j]. \D\ is the' length of D that is the number of

rewritings in D. If two derivations reduce the same term to its normal form (the

normal form is unique because of confluent property), they are called equivalent

derivations. Given a TRS and a term, a deri\^tion with the shortest length among

all the equivalent derivations for that term is called an optimal derivation (for that

term). We call a derivation an outermost derivation if in each derivation step,

use outermost strategy. We call a derivation a variable- delay derivation if in each

derivation step, use variable-delay strategy. We call a derivation an innermost

derivation if in each derivation step, use innermost strategy.

Let s be a proper subterm of term t. Any proper subterm of t whose root is not

on the root path of 5 in ^ is called a general sibling.

3 Non-ambiguous, Left linear and Variable Less

TRSs

Combining conditions left linear and ^-ariable less together is condition linear. In

this part, we discuss approximate strategies for non-ambiguous and linear TRSs. '

Proposition 1. For a non-ambiguous TRS, if t is a redex of rule r : s â€”* s' and

a proper subterm t' of t is a redex, t' must be a variable redex of r in t.

Proof. If t' is not a variable redex of r in i, by the condition that t is a redex of r, t'

is matched by a non-\-ariable subterm of s. Suppose rule r' root-rewrites t'. Then

r' superposes r, contrary to the non-ambiguity condition. â–¡

Proposition 2. For a non-ambiguous TRS, only one rule can root-rewrite a term.

Proof. If two rules can root-rewrite a term, then the left sides of the rules will be

able to unify with each other, contrary to the non-ambiguity condition. â–¡

Theorem 1. For a non-ambiguous and linear TRS, each non-outermost derivation

D has an equivalent outermost derivation D' which has no more derivation steps

than D.

Proof. Let R he a. non-ambiguous and linear TRS, D a derivation, and tail-

length(D) the length of the subderivation in D from the first non-outermost rewrit-

ing through the end.

We use induction on tail-lengthfD) to prove:

Claim: D is equi\'alent to an outermost derivation D' such that tail-length(r)')=0

and \D'\ < \D\.

Basis. tail-length(D)â€” 0. Trivial.

Induction. Suppose the claim holds for the derivation with less tail-length function

value than D. Suppose the first non-outermost rewriting occurs on the redex s.

There must be an outermost redex Sout containing s properly. Since R is non-

ambiguous, 5 must be a variable redex in Sout- Suppose the rule appliable on Sout

is r which has variables xi,...,Xk at the left side and the subterms matched with

xi,...,Xk are Si,...,^^. 5 is a subterm of one of {si, ...,5^). Suppose Dta,i is the

subderivation of D from the rewriting of s through the end. We discuss in cases

what rewriting will happen to Sont or above Sout in Dtaii- Let Dkead denote the

remaining subderivation in D except Dtaii-

Case 1. All rewritings to Sout or above are applied only on or inside s\, ...,Sk. This

case is impossible since r will be appliable, even in the case that R is non-left-linear.

Because identical terms will be rewritten to a same term by the confluence property.

In the following cases, suppose r' is the first rule applied on a redex that is not a

subterm of any one of 5i, ..., Sk and r' is applied to or above Sout â–

Case 2. r' is applied on a proper subterm of Sout- f' superposes r, contrary to the

condition that R is non-ambiguous, so this case is impossible.

Case 3. r' is applied on Sout- Before r' is applied, all rewritings to Sout must be on

or inside Si,...,Sk by case 2. Suppose s, becomes 5,(1 < i < k) and Sgut becomes

^out i^^* before r' is applied.

Because R is left-linear, obviously Xi matches s'-{l < i < k) and r can be applied

on s'g^f. By proposition 2, r' = r.

We move rewriting by r in front of the rewriting on 5, D becoming D' . We

suppose that in D the rewriting on s is D\i] and the rewriting on Sout is -DfiKi < j).

Suppose Sout is rewritten to s'^^^ by r in D' and 5^â€ž( is rewritten to ^"^^ by r in D.

s^^f and s^^( are the same except the changes to ^i, ...,Sk- Since R is linear, we can

assume the variables at the right side of r are x,j , ..., x,:,(l < ii < ... < ij < k).

In D', all 5,j,...,s,j are rewritten to s\^.,...,s\^ by the same rewritings between D[i]

and D[j] in D. All other rewritings between D[i\ and Z>[j] occur on the general

siblings of Sout and they are not affected by moving of the rewriting on Sout-, so they

can be applied in D' . Hence, D' is equivalent D and \D'\ < \D\. tail-length(D') <

tail-length(D). By induction hypothesis, the claim holds for D'.

Case 4. r' is applied above Sout- By case 2, before r' is applied, all rewriting to

Sout rnust be on or inside 3i,...,5a-. If Sout were not a \'ariable redex of r', r would

superpose r'. Therefore Sout is a variable redex of r'. Suppose the term being

rewritten by r' is t. By proposition 1, all proper subterms in t not corresponding to

variables of r' are normal forms. Suppose deri\^tion D^uh reduces a proper subterm

t' of t to its normal form and one step of Dguh is in Dtaii- Obviously, tail-length(Â£)su6)

< tail-length(D). By induction hypothesis, we can obtain an outermost derivation

Dj^(, equivalent to Dsub and |I?sâ€ž(,| < l-D^ubl- Hence, we can move all steps of D^^f,

in front of the rewriting step of 5, and obtain a deri\^tion equix'alent to D with less

tail-length function value. Using the induction hypothesis again for the modified

D, we can prove the claim holds for D. Therefore we can assume that in D, all

derivation steps used in rewriting all proper subterms in t not corresponding to the

variables in r' are in Dkead- In this case, r' is appliable at the beginning of Dtaii, but

this is contrary to the supposition that r is an outermost redex at the beginning of

Dtail-

We have enumerated all cases. The claim does hold. The theorem immediately

follows the claim. r-j

Corollary 1. For any non- ambiguous and linear system, given any term, there

must be an outermost derivation that is optimal among all the derivations for that

term.

The following examples show the importance of the conditions in theorem 1.

Example 1. (Non-ambiguous)

Ambiguovis system: f{a) â€” > f{g{a)), g{a) -^ b, ,a â€”y b

Outmost derivation: f{a) â€” > f{g{a)) â€”* f{b)

Non-outermost derivation: /(a) â€” > f{b)

Example 2. (Left linear and \-ariable less)

Non-right-less system: f{x) â€”* g{x,x),a â€”y b

Outermost derivation: /(a) â€” > g{a,a) â€” > g{b,a) â€”>â– g{b,b)

Non-outermost deriv'ation: /(a) â€” > f{b) â€” > g{b,b)

Proposition 3. Given any non-ambiguous TRS and any term t, if a subterm s of

t is a non-variable redex in t, it m.ust be an outermost redex in t.

Proof. If .s were not an outermost redex in t, there vi'ould be an outermost redex s'

in t vi'hich contains s. By non-ambiguity property, s must be a variable-redex in s\

which is contrary to the given condition. â–¡

Proposition 4. For any non- ambiguous TRS, a variable- delay derivation is an

outermost derivation.

Proof. Let D he & non-outermost deri\'ation for a term. There must be a derivation

step in D such that a non-outermost redex is rewritten. Suppose the non-outermost

redex is s and the outermost redex containing .s is Sout- By non-ambiguous condition,

s must be a variable redex of Sout- By variable-delay strategy, 5 cannot be chosen.

Therefore D is not a \^nable-delay derivation. q

In the case multiple outermost redexes are available, choosing different outer-

most redex has different effect on the length of deri'vations. Variable-delay strategy

seems better than outermost strategy. See the following example.

Example 3.

System: /(x,6) â€”* N ^a ^> b^c -^ d

Outermost deri\'ation: f{c,a.) â€” > f{d,a) â€” > f(d,b) â€”* N

Variable-delay derivation: f{c,a){c is a variable redex) â€”y f{c,b) â€” > A'^

In the above example with the initial term /(c, a), we have two outermost redexes

c and a. By outermost strategy, we arbitrarily choose c or a. But c is a variable redex

of rule f{x,b) â€” > N. Therefore, b}'^ \^riable-delay strategy only a can be chosen.

The more important is that any rewriting on c is wasteful, since the variable x in

the rule /(x, b) â€” > A'^ can match any term when the rule is applied.

Lemma 1. Let D be an outermost derivation of a non-ambiguous TRS and t a

non-variable outermost redex after some steps of D. In D, t remains a non-variable

outermost redex until it is rewritten.

Proof. Suppose after D[i] in D, t is a non-variable outermost redex. If t is no longer

a non-variable outermost redex after D[?4-l], there are only two possibilities: t itself

is rewritten at step D[i + 1] or a redex t' which is above t is rewritten at step Z)[i + 1].

For the lemma, we only need to discuss the latter case. Because t is a non-variable

redex, t is unifiable with a non-\'ariable subterm of \D'\, \D'\ = n. We will construct a derivation D" such that D" is equi\'alent

to D\ \D"\ = n, and D" - D[l,n].

We can prove existence of D" formally by induction. The technique is similar

to the proofs for theorems 1 and 2. Here we give only the challenging part - at the

induction step.

Suppose D[l, I - 1] = D'[l,i - 1] and D[i] j^ D'[i]. That means, after D[i - 1]( =

D'[i â€” 1]), there are multiple non-\^riable outermost redexes, so that D and D'

choose different ones to rewrite. Suppose D rewrites redex t and D' rewrites redex

t'. By lemma 1, a rewriting on t will occur in D'[j] in D' (?' < j < n). Construct

D": '

D"[l,i] = D[l,t]

D"[i + l,j] = D'[t,j-l]

D"[j + l,n] = D'[j + l,n]

Because t is a non-variable outermost redex, any non-\'ariable outermost redexes

rewritten in D'[i,j â€” 1] cannot be above or inside t, so that the rewriting on t does

not affect rewritings in D'[i,j â€” 1]. Furthermore, rewritings oi D'[\,j] and D"[l,j]

generate the same term, which can be reduced to its normal form by D"[j + l,n].

We have proved D" is equivalent to D'. D" has longer identical prefix with D than

D' . By induction, we eventually obtain a derivation D'" such that D'" is equivalent

to D, \D"'\ < |D|, and D'" is identical to the prefix of D. This is ridiculous because

this means D'" does not reduce to normal form.

We conclude that such D and D' cannot exist. â–¡

Lemma 3. For a non-ambiguous TRS, if for a term there is a variable- delay deriva-

tion without any variable redex rewriting, then any variable- delay derivation for that

term has no rewriting on variable redexes.

Proof. Let D and D' be equivalent \^riable-delay derivations, D has no rewritings

1 2

Online Library → Ke Li → Approximate and optimal strategies for non-ambiguous and left linear term rewriting systems → online text (page 1 of 2)