Let us see now what happens when we use another strategy for rewriting in the original VENDING-MACHINE module. The frewrite command (abbreviated frew) rewrites a term using a depth-first position-fair strategy that makes it possible for some rules to be applied that could be ``starved'' using the leftmost, outermost rule fair strategy of the rewrite command. The strategies for the rewrite and frewrite commands are described in detail in Section 16.2.
Maude> frew [2] in VENDING-MACHINE : $ $ q q .
frewrite [2] in VENDING-MACHINE : $ $ q q .
rewrites: 2 in 0ms cpu (0ms real) (~ rews/sec)
result (sort not calculated): ($ q) ($ $) q q
Maude> frew [12] $ $ q q .
frewrite [12] in VENDING-MACHINE : $ $ q q .
rewrites: 12 in 0ms cpu (0ms real) (~ rews/sec)
result (sort not calculated):
c (q a) ($ q) ($ $) (q q) ($ q) (q q) q q
With two rewrites, one quarter and one dollar are added. With sufficiently many rewrites (twelve will do), a cake and an apple can be obtained.
In contrast to rewrite, that reduces the whole term using equations after each rule rewrite, frewrite only reduces the subterm rewritten (to preserve positions not yet visited). Thus, when rewriting stops, the term may not be fully reduced and hence Maude will not know the exact least sort of the term yet. This is the reason for the (sort not calculated) comment in place of a sort in the result line. In the case of a term with an associative and commutative top operator, the term may not be in its fully flattened form with canonical order of subterms. This accounts for the parentheses in the result term and the fact that the coins and items are not listed in order as they are in the result of a rewrite.
The top-down rule-fair strategy of the rewrite command can result in nontermination even though there is a terminating sequence of rewrites. As an example consider the following module:
mod BB-TEST is
sort Expression .
ops a b bingo : -> Expression .
op f : Expression Expression -> Expression .
rl a => b .
rl b => a .
rl f(b, b) => bingo .
endm
Giving the rewrite command with input term f(a, a) will result
in the following looping computation:
f(a, a) => f(b, a) => f(a, a) => f(b, a) => f(a, a) => ...
This is because using the top-down rule-fair strategy of the rewrite command, the third rule always fails to match and never gets a chance to be applied. As already mentioned above, the frewrite command uses on the other hand a position-fair bottom-up strategy that makes it possible for other rules to be applied. As a consequence, some rewriting computations that could be nonterminating using the rewrite command become terminating with frewrite. For example, using the frewrite command in place of rewrite in the above example we get
Maude> frew in BB-TEST : f(a, a) . frewrite in BB-TEST : f(a, a) . rewrites: 3 in 0ms cpu (0ms real) (~ rews/sec) result Expression: bingo