Rewriting modifiers

In version 2.3.3 onward, rewrite rules can be modified by the keywords: bottomup:, topdown:, before:, preorder: and postorder:. These modifiers alter the order in which a set of rewriting rules is applied.

These modifiers act like delimiters, similar to the way scoping keywords like public:, protected: and private: are used to delimit declarations in C++. For instance, a set of rules prefixed by the modifier topdown: will utilize the topdown strategy for reduction. If no modifier are specified, then bottom-up will be the default.

Note that all five modes of rules can be used together in a rewriting system under tree rewriting mode (see 6.5.1) and their executions are intermixed together.

The semantics of these modifiers are as follows:

bottomup: 

This specifies the modified rewriting rules should be applied in the default bottom-up mode. In this mode, the innermost/leftmost redex is chosen as the next redex. So reduction occurs in a bottomup manner. This means that if a term t is a redex and if the term t contains a subterm t' which is also a redex, t' will be reduced before t.

topdown: 

This specifies the modified rewriting rules should be applied in a topdown mode. In this mode, the rewriter will first try to locate the outermost/leftmost redex. Reduction will occur in a (mostly) topdown manner.

before: 

This specifies that the modified rewriting rules should be tried before the topdown phase. In addition, unlike topdown mode, if state-caching if used (see 6.5.2), the rules are only tried once. Otherwise, these act just like the preorder modifier, described below.

preorder: 

This specifies that the modified rewriting rules should be tried only at the preorder traversal of a term.

postorder: 

This specifies the rewriting rules should be tried only at the postorder traversal of a term.

 
• Rewriting modifier example