Rewrite Definitions

Functional languages are a convenient formalism for expressing functions over trees. Another convenient formalism is formed by rewrite rules[EM85]. For instance, if we have a certain equivalence over terms, then rewrite rules expressing this equivalence might define a procedure for computing a normal form of a term. Another use for term rewriting is as an alternative way of defining functions. For example to implement the function `plus' on natural numbers one can define `plus' as an operator and specify the rewrite rules such that the normal form does not contain a plus. The result of normalising (term rewriting) then is that the function is `evaluated'. (This is all abstract data type theory.) The notation for term rewrite rules is very simple. For example:  

Neg(x) -> <:  Minus(Zero(), x)  >;

In this example x is a variable, used in the term in the right-hand side. The meaning of this example is that every occurrence of the operator Neg is replaced by an equivalent construct.

In general both sides are terms with variables, where all variables of the right-hand side also appear on the left-hand side. Actually, the left-hand side can be the same kind of pattern that is allowed in function definitions. To allow `greater control' (a euphemism for hacking...) we allow arbitrary C functions and string- and int-denotations in the right-hand side (see below). For the collection of rewrite rules, the system generates a function rewrite_phylum for each phylum, which has the normalised form as its result. This function can be called in the same way as any other function.

The rewrite functions have an additional argument of type rview. Rewrite views can be used to group rewrite rules in separate rewrite systems. Rewrite rules can be made specific for a set of rewrite views   (or, added to one or more rewrite systems) by naming these views between the angle open bracket and the colon of a rewrite rule. For example:

Neg(x) -> < view1 view2:  Minus(Zero(), x)  >;

An omitted view list defaults to all rewrite views. If no views are specified, the angle brackets and colon may be omitted (as we usually do), as we show below for the rewrite rule for Neg(x) that we gave above.  

Neg(x) -> Minus(Zero(), x);

This is equivalent to a view list that only contains the view name base_rview. The type rview is an enumeration type of all view names occurring in the rewrite rules. It always contains the view name base_rview.

Rewrite views can be declared as in the following example:  

%rview view1 view2; /* the `%' is part of the keyword */

Rewrite views should be declared. If the termprocessor input contains one or more rewrite view declarations it will report errors for all rewrite views that are used and not declared. The use of view declarations may help to find typing errors in view names - in term processor input that does not contain view declarations, the misspelling of a view name may just introduce a new view (with the misspelled name).

If several rewrite rules share the same left-hand side, they may be combined by grouping the right-hand sides (with seperating commas), provided that all the angle brackets haven't been omitted from the right-hand sides. If several rewrite rules share the same right-hand side, they may be combined by grouping the left-hand sides (with seperating commas). The general form of a rewrite rule is shown below:

pattern1, pattern2, ... -> < v1 v2 ... : ... >, ..., < vn ... : ... > ;

How we can prove that a rewrite system always yields a normal form is beyond the scope of this manual, but informally stated, each rule should bring the term `closer' to its normal form, and the order in which the rules are applied (the rewrite strategy)  should not matter. Two simple warnings: never ever use a rule in which the right-hand side is equal to the left-hand side, or a rule that directly expresses a commutative property.

The default rewrite strategy is leftmost innermost. In the case of overlapping patterns , where more than one left-hand side matches, the most specific match is taken.

Rewrite rules with functional right-hand sides are a bit harder to prove correct. The first requirement of course is that the arguments and the results of those functions should have the correct types, which lint can check. The second requirement is that the rule is meaningful, but that is hard to check automatically. The writer of such rules should convince herself of the correctness of the rewrite rules. Here we give some considerations that can be used in doing so. The `purpose' of a rewrite system is to convert a term to its normal form. Now let us look closer at a rule with a function in it:

Operator(x) -> Function(x);

The rewrite system uses this rule when it has a subterm that matches the left-hand side, and `assumes' that substituting it by the right-hand side brings it closer to the normal form. It then continues applying rules on the new term. The function Function should therefore bring the expression closer to the normal form. Now what about the argument x of Function? It is not known whether or not it is in normal form already (although the default strategy, which is leftmost innermost, does guarantee this). Therefore, Function cannot assume that its argument is in normal form. This is not usually a problem, but if it is, the function rewrite_phylum can be used in the function definition to guarantee this. The other side of the picture is that the result of Function does not have to be in normal form, which is convenient for the writer of Function.