Table of Contents
In Chapter 12 we saw how term
rewriting can be used to implement transformations on programs
represented by means of terms.
Term rewriting involves exhaustively applying rules to subterms
until no more rules apply.
This requires a strategy for selecting the
order in which subterms are rewritten.
The innermost strategy introduced in Chapter 12 applies rules automatically throughout a
term from inner to outer terms, starting with the leaves.
The nice thing about term rewriting is that there is no need to
define traversals over the syntax tree; the rules express basic
transformation steps and the strategy takes care of applying it
everywhere.
However, the complete normalization approach of rewriting turns out
not to be adequate for program transformation, because rewrite
systems for programming languages will often be non-terminating
and/or non-confluent.
In general, it is not desirable to apply all rules at the same time
or to apply all rules under all circumstances.
Consider for example, the following extension of
prop-dnf-rules with distribution rules to achieve
conjunctive normal forms:
module prop-cnf imports prop-dnf-rules rules E : Or(And(x, y), z) -> And(Or(x, z), Or(y, z)) E : Or(z, And(x, y)) -> And(Or(z, x), Or(z, y)) strategies main = io-wrap(cnf) cnf = innermost(E)
This rewrite system is non-terminating because after applying one of the and-over-or distribution rules, the or-over-and distribution rules introduced here can be applied, and vice versa.
And(Or(Atom("p"),Atom("q")), Atom("r"))
->
Or(And(Atom("p"), Atom("r")), And(Atom("q"), Atom("r")))
->
And(Or(Atom("p"), And(Atom("q"), Atom("r"))),
Or(Atom("r"), And(Atom("q"), Atom("r"))))
->
...
There are a number of solutions to this problem. We'll first discuss a couple of solutions within pure rewriting, and then show how programmable rewriting strategies can overcome the problems of these solutions.
The non-termination of prop-cnf is due to the fact that
the and-over-or and or-over-and distribution rules interfere with
each other.
This can be prevented by refactoring the module structure such that
the two sets of rules are not present in the same rewrite system.
For example, we could split module prop-dnf-rules into
prop-simplify and prop-dnf2 as follows:
module prop-simplify imports prop-eval-rules rules E : Impl(x, y) -> Or(Not(x), y) E : Eq(x, y) -> And(Impl(x, y), Impl(y, x)) E : Not(Not(x)) -> x E : Not(And(x, y)) -> Or(Not(x), Not(y)) E : Not(Or(x, y)) -> And(Not(x), Not(y))
module prop-dnf2 imports prop-simplify rules E : And(Or(x, y), z) -> Or(And(x, z), And(y, z)) E : And(z, Or(x, y)) -> Or(And(z, x), And(z, y)) strategies main = io-wrap(dnf) dnf = innermost(E)
Now we can reuse the rules from prop-simplify without
the and-over-or distribution rules to create a
prop-cnf2 for normalizing to conjunctive normal form:
module prop-cnf2 imports prop-simplify rules E : Or(And(x, y), z) -> And(Or(x, z), Or(y, z)) E : Or(z, And(x, y)) -> And(Or(z, x), Or(z, y)) strategies main = io-wrap(cnf) cnf = innermost(E)
Although this solves the non-termination problem, it is not an ideal solution. In the first place it is not possible to apply the two transformations in the same program. In the second place, extrapolating the approach to fine-grained selection of rules might require definition of a single rule per module.
Another common solution to this kind of problem is to introduce
additional constructors that achieve normalization under a
restricted set of rules. That is, the original set of rules p1
-> p2 is transformed into rules of the form f(p_1) ->
p_2', where f is some new constructor symbol and
the right-hand side of the rule also contains such new
constructors. In this style of programming, constructors such as
f are called functions and are
distinghuished from constructors. Normal forms over such rewrite
systems are assumed to be free of these `function' symbols;
otherwise the function would have an incomplete definition.
To illustrate the approach we adapt the DNF rules by introducing the
function symbols Dnf and DnfR. (We ignore
the evaluation rules in this example.)
module prop-dnf3
imports libstrategolib prop
signature
constructors
Dnf : Prop -> Prop
DnfR : Prop -> Prop
rules
E : Dnf(Atom(x)) -> Atom(x)
E : Dnf(Not(x)) -> DnfR(Not(Dnf(x)))
E : Dnf(And(x, y)) -> DnfR(And(Dnf(x), Dnf(y)))
E : Dnf(Or(x, y)) -> Or(Dnf(x), Dnf(y))
E : Dnf(Impl(x, y)) -> Dnf(Or(Not(x), y))
E : Dnf(Eq(x, y)) -> Dnf(And(Impl(x, y), Impl(y, x)))
E : DnfR(Not(Not(x))) -> x
E : DnfR(Not(And(x, y))) -> Or(Dnf(Not(x)), Dnf(Not(y)))
E : DnfR(Not(Or(x, y))) -> Dnf(And(Not(x), Not(y)))
D : DnfR(Not(x)) -> Not(x)
E : DnfR(And(Or(x, y), z)) -> Or(Dnf(And(x, z)), Dnf(And(y, z)))
E : DnfR(And(z, Or(x, y))) -> Or(Dnf(And(z, x)), Dnf(And(z, y)))
D : DnfR(And(x, y)) -> And(x, y)
strategies
main = io-wrap(dnf)
dnf = innermost(E <+ D)
The Dnf function mimics the innermost normalization
strategy by recursively traversing terms.
The auxiliary transformation function DnfR is used to
encode the distribution and negation rules.
The D rules are default rules that
are only applied if none of the E rules apply, as
specified by the strategy expression E <+ D.
In order to compute the disjunctive normal form of a term, we have
to `apply' the Dnf function to it, as illustrated in
the following application of the prop-dnf3 program:
$cat test1.dnf Dnf(And(Impl(Atom("r"),And(Atom("p"),Atom("q"))),ATom("p")))$./prop-dnf3 -i test1.dnf Or(And(Not(Atom("r")),Dnf(Dnf(ATom("p")))), And(And(Atom("p"),Atom("q")),Dnf(Dnf(ATom("p")))))
For conjunctive normal form we can create a similar definition, which can now co-exist with the definition of DNF. Indeed, we could then simultaneously rewrite one subterm to DNF and the other to CNF.
E : DC(x) -> (Dnf(x), Cnf(x))
In the solution above, the original rules have been completely
intertwined with the Dnf transformation.
The rules for negation cannot be reused in the definition of
normalization to conjunctive normal form.
For each new transformation a new traversal function and new
transformation functions have to be defined.
Many additional rules had to be added to traverse the term to find
the places to apply the rules.
In the modular solution we had 5 basic rules and 2 additional rules
for DNF and 2 rules for CNF, 9 in total. In the functionalized
version we needed 13 rules for each
transformation, that is 26 rules in total.
In general, there are two problems with the functional approach to encoding the control over the application of rewrite rules, when comparing it to the original term rewriting approach: traversal overhead and loss of separation of rules and strategies.
In the first place, the functional encoding incurs a large overhead due to the explicit specification of traversal. In pure term rewriting, the strategy takes care of traversing the term in search of subterms to rewrite. In the functional approach traversal is spelled out in the definition of the function, requiring the specification of many additional rules. A traversal rule needs to be defined for each constructor in the signature and for each transformation. The overhead for transformation systems for real languages can be inferred from the number of constructors for some typical languages:
language : constructors Tiger : 65 C : 140 Java : 140 COBOL : 300 - 1200
In the second place, rewrite rules and the strategy that defines their application are completely intertwined. Another advantage of pure term rewriting is the separation of the specification of the rules and the strategy that controls their application. Intertwining these specifications makes it more difficult to understand the specification, since rules cannot be distinghuished from the transformation they are part of. Furthermore, intertwining makes it impossible to reuse the rules in a different transformation.
Stratego introduced the paradigm of programmable rewriting strategies with generic traversals, a unifying solution in which application of rules can be carefully controlled, while incurring minimal traversal overhead and preserving separation of rules and strategies.
The following are the design criteria for strategies in Stratego:
Basic transformation rules can be defined separately from the strategy that applies them, such that they can be understood independently.
A transformation can select the necessary set of rules from a collection (library) of rules.
A transformation can exercise complete control over the application of rules. This control may be fine-grained or course-grained depending on the application.
Transformations can be defined without overhead for the definition of traversals.
Rules can be reused in different transformations.
Traversal schemas can be defined generically and reused in different transformations.
In the next chapters we will examine the language constructs that Stratego provides for programming with strategies, starting with the low-level actions of building and matching terms. To get a feeling for the purpose of these constructs, we first look at a couple of typical idioms of strategic rewriting.
The basic idiom of program transformation achieved with term rewriting is that of cascading transformations. Instead of applying a single complex transformation algorithm to a program, a number of small, independent transformations are applied in combination throughout a program or program unit to achieve the desired effect. Although each individual transformation step achieves little, the cumulative effect can be significant, since each transformation feeds on the results of the ones that came before it.
One common cascading of transformations is accomplished by
exhaustively applying rewrite rules to a subject term. In Stratego
the definition of a cascading normalization strategy with respect to
rules R1, ... ,Rn can be formalized using
the innermost strategy that we saw before:
simplify = innermost(R1 <+ ... <+ Rn)
The argument strategy of innermost is a
selection of rules. By giving
different names to rules, we can control the
selection used in each transformation. There can be multiple
applications of innermost to different sets of rules,
such that different transformations can co-exist in the same module
without interference. Thus, it is now possible to develop a large
library of transformation rules that can be called upon when
necessary, without having to compose a rewrite system by cutting and
pasting.
For example, the following module defines the normalization of
proposition formulae to both disjunctive and to conjunctive normal
form:
module prop-laws imports libstrategolib prop rules DefI : Impl(x, y) -> Or(Not(x), y) DefE : Eq(x, y) -> And(Impl(x, y), Impl(y, x)) DN : Not(Not(x)) -> x DMA : Not(And(x, y)) -> Or(Not(x), Not(y)) DMO : Not(Or(x, y)) -> And(Not(x), Not(y)) DAOL : And(Or(x, y), z) -> Or(And(x, z), And(y, z)) DAOR : And(z, Or(x, y)) -> Or(And(z, x), And(z, y)) DOAL : Or(And(x, y), z) -> And(Or(x, z), Or(y, z)) DOAR : Or(z, And(x, y)) -> And(Or(z, x), Or(z, y)) strategies dnf = innermost(DefI <+ DefE <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO) cnf = innermost(DefI <+ DefE <+ DOAL <+ DOAR <+ DN <+ DMA <+ DMO) main-dnf = io-wrap(dnf) main-cnf = io-wrap(cnf)
The rules are named, and for each strategy different selections from the ruleset are made.
The module even defines two main strategies, which allows us to use
one module for deriving multiple programs. Using the
--main option of strc we declare
which strategy to invoke as main strategy in a particular
program. Using the -o option we can give a different
name to each derived program.
$ strc -i prop-laws.str -la stratego-lib --main main-dnf -o prop-dnf4
Cascading transformations can be defined with other strategies as
well, and these strategies need not be exhaustive, but can be
simpler one-pass traversals.
For example, constant folding of Boolean expressions only requires a
simple one-pass bottom-up traversal. This can be achieved using the
bottomup strategy according the the following scheme:
simplify = bottomup(repeat(R1 <+ ... <+ Rn))
The bottomup strategy applies its argument strategy to
each subterm in a bottom-to-top traversal. The repeat
strategy applies its argument strategy repeatedly to a term.
Module prop-eval2 defines the evaluation rules for
Boolean expressions and a strategy for applying them using this
approach:
module prop-eval2 imports libstrategolib prop rules Eval : Not(True) -> False Eval : Not(False) -> True Eval : And(True, x) -> x Eval : And(x, True) -> x Eval : And(False, x) -> False Eval : And(x, False) -> False Eval : Or(True, x) -> True Eval : Or(x, True) -> True Eval : Or(False, x) -> x Eval : Or(x, False) -> x Eval : Impl(True, x) -> x Eval : Impl(x, True) -> True Eval : Impl(False, x) -> True Eval : Eq(False, x) -> Not(x) Eval : Eq(x, False) -> Not(x) Eval : Eq(True, x) -> x Eval : Eq(x, True) -> x strategies main = io-wrap(eval) eval = bottomup(repeat(Eval))
The strategy eval applies these rules in a bottom-up
traversal over a term, using the bottomup(s)
strategy. At each sub-term, the rules are applied repeatedly until
no more rule applies using the repeat(s) strategy. This
is sufficient for the Eval rules, since the rules never
construct a term with subterms that can be rewritten.
Another typical example of the use of one-pass traversals is desugaring, that is rewriting language constructs to more basic language constructs. Simple desugarings can usually be expressed using a single top-to-bottom traversal according to the scheme
simplify = topdown(try(R1 <+ ... <+ Rn))
The topdown strategy applies its argument strategy to
a term and then traverses the resulting term.
The try strategy tries to apply its argument strategy
once to a term.
Module prop-desugar defines a number of desugaring
rules for Boolean expressions, defining propositional operators in
terms of others. For example, rule DefN defines
Not in terms of Impl, and rule
DefI defines Impl in terms of
Or and Not. So not all rules should be
applied in the same transformation or non-termination would result.
module prop-desugar
imports prop libstrategolib
rules
DefN : Not(x) -> Impl(x, False)
DefI : Impl(x, y) -> Or(Not(x), y)
DefE : Eq(x, y) -> And(Impl(x, y), Impl(y, x))
DefO1 : Or(x, y) -> Impl(Not(x), y)
DefO2 : Or(x, y) -> Not(And(Not(x), Not(y)))
DefA1 : And(x, y) -> Not(Or(Not(x), Not(y)))
DefA2 : And(x, y) -> Not(Impl(x, Not(y)))
IDefI : Or(Not(x), y) -> Impl(x, y)
IDefE : And(Impl(x, y), Impl(y, x)) -> Eq(x, y)
strategies
desugar =
topdown(try(DefI <+ DefE))
impl-nf =
topdown(repeat(DefN <+ DefA2 <+ DefO1 <+ DefE))
main-desugar =
io-wrap(desugar)
main-inf =
io-wrap(impl-nf)
The strategies desugar and impl-nf define
two different desugaring transformation based on these rules.
The desugar strategy gets rid of the implication and
equivalence operators, while the impl-nf strategy
reduces an expression to implicative normal-form, a format in which
only implication (Impl) and
False are used.
A final example of a one-pass traversal is the downup
strategy, which applies its argument transformation during a
traversal on the way down, and again on the way up:
simplify = downup(repeat(R1 <+ ... <+ Rn))
An application of this strategy is a more efficient implementation of constant folding for Boolean expressions:
eval = downup(repeat(Eval))
This strategy reduces terms such as
And(... big expression ..., False)
in one step (to False in this case), while the
bottomup strategy defined above would first evaluate
the big expression.
Cascading transformations apply a number of rules one after another to an entire tree. But in some cases this is not appropriate. For instance, two transformations may be inverses of one another, so that repeatedly applying one and then the other would lead to non-termination. To remedy this difficulty, Stratego supports the idiom of staged transformation.
In staged computation, transformations are not applied to a subject term all at once, but rather in stages. In each stage, only rules from some particular subset of the entire set of available rules are applied. In the TAMPR program transformation system this idiom is called sequence of normal forms, since a program tree is transformed in a sequence of steps, each of which performs a normalization with respect to a specified set of rules. In Stratego this idiom can be expressed directly according to the following scheme:
strategies
simplify =
innermost(A1 <+ ... <+ Ak)
; innermost(B1 <+ ... <+ Bl)
; ...
; innermost(C1 <+ ... <+ Cm)
In conventional program optimization, transformations are applied throughout a program. In optimizing imperative programs, for example, complex transformations are applied to entire programs. In GHC-style compilation-by-transformation, small transformation steps are applied throughout programs. Another style of transformation is a mixture of these ideas. Instead of applying a complex transformation algorithm to a program we use staged, cascading transformations to accumulate small transformation steps for large effect. However, instead of applying transformations throughout the subject program, we often wish to apply them locally, i.e., only to selected parts of the subject program. This allows us to use transformations rules that would not be beneficial if applied everywhere.
One example of a strategy which achieves such a transformation is
strategies
transformation =
alltd(
trigger-transformation
; innermost(A1 <+ ... <+ An)
)
The strategy alltd(s) descends into a term until a
subterm is encountered for which the transformation s
succeeds. In this case the strategy
trigger-transformation recognizes a program fragment
that should be transformed. Thus, cascading transformations are
applied locally to terms for which the transformation is
triggered. Of course more sophisticated strategies can be used for
finding application locations, as well as for applying the rules
locally. Nevertheless, the key observation underlying this idiom
remains: Because the transformations to be applied are local,
special knowledge about the subject program at the point of
application can be used. This allows the application of rules that
would not be otherwise applicable.
While term rewrite rules can express individual transformation steps, the exhaustive applications of all rules to all subterms is not always desirable. The selection of rules to apply through the module system does not allow transformations to co-exist and may require very small-grained modules. The `functionalization' of rewrite rules leads to overhead in the form of traversal definitions and to the loss of separation between rules and strategy. The paradigm of rewriting with programmable strategies allows the separate definition of individual rewrite rules, which can be (re)used in different combinations with a choice of strategies to form a variety of transformations. Idioms such as cascading transformations, one-pass traversals, staged, and local transformations cater for different styles of applying strategies.
Next up: The next chapters give an in depth overview of the constructs for composing strategies.