Optimizing Tree Rewriting

 

An experimental rewriting optimizer based on partial evaluation techniques has been implemented in release 2.3.4 of Prop. The optimizer can be enabled with the option -Orewriting .

Informally speaking, the rewriting optimizer will try to locate ``longer'' reduction sequence and add these to your rewriting rules. The result is that during execution these bigger reduction steps are taken whenever possible.

For example, consider the Wff datatype defined in section 6.4.1. Suppose we have the following two rewriting rules in our rule set:

   Not(Not X): X
|  FORALL(X,A,P): Not(EXISTS(X,A,Not(P)))

Given an input term of the form FORALL(X,A,Not(P)), the term will first be reduced to Not(EXISTS(X,A,Not(Not(P)))) via the second rule, then to Not(EXISTS(X,A,P)) via the first rule. The optimizer can discover that this two step reduction can be compressed into one step if the rewriting system is augmented with the following rule:

   FORALL(X,A,Not P): Not(EXISTS(X,A,P))

Note that this augmented rule is a specialization of the two rules given by the user. In general, the rewriting optimizer will repeatedly look for useful specializations and add them to the user rule set ¹¹. These specialized rules will perform multiple reductions in one single step.

To make use of the optimizer, the rewriting system must have the following properties:

1. It must be strongly normalizing, i.e. it will terminate under all inputs.
2. It must be confluent, or else confluence is not necessary. Notice that the optimizer can and will alternate the reduction order of a rule set. Thus if a rewriting system is non-confluent, an optimized rewriting system may give a different result.

In addition, the following things should hold to maximize the effectiveness of the optimizer.

1. Indices (i.e. state caching) should be enabled. Otherwise the optimizer will not be able to optimize a rule.
2. Specializable rules must be simple, i.e. the right hand side must be written as an expression consist of only Prop datatypes. If the right hand side is a complex statement or if it involves external function calls, the optimizer will fail to analyze it properly.
3. Only bottom-up rules may be present.
4. Avoid conditional rules whenever possible.

Finally, it should be warned that an optimized rewriting system may generate a lot more code than the un-optimized one. The user should view the generated report and check that excessive specializations have not been performed.