A Framework for Polytypic Programming on Terms, with an Application to Rewriting

Rewriting is a typical example of a polytypic function. Given any value of a datatype (an algebra of terms), and rules to rewrite values of that datatype, we want a function that rewrites the value to normal form if the value is normalizable. This paper develops a polytypic rewriting function that uses the parallel innermost rewriting strategy. It improves upon our earlier work on polytypic rewriting in two fundamental ways. Firstly, the rewriting function uses a term interface that hides the polytypic part from the rest of the program. The term interface is a framework for polytypic programming on terms. This implies that the rewriting function is independent of the particular implementation of polytypism. We give several functions and laws on terms, which simplify calculating with programs. Secondly, the rewriting function is developed together with a correctness proof. We just present the result of the correctness proof, the proof itself is published elsewhere