Copyright
Ke Li.

Approximate and optimal strategies for non-ambiguous and left linear term rewriting systems online

. (page 1 of 2)
Online LibraryKe LiApproximate and optimal strategies for non-ambiguous and left linear term rewriting systems → online text (page 1 of 2)
Font size
QR-code for this ebook


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


1

Online LibraryKe LiApproximate and optimal strategies for non-ambiguous and left linear term rewriting systems → online text (page 1 of 2)