## Abstract

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.
## Keywords

Polytypic programming,
PolyP,
Haskell,
Term rewriting.
## BIBTeX reference:

@InProceedings{janssonjeuringWGP00:rewriting,
author = {Jansson, Patrik and Jeuring, Johan},
title = {A Framework for Polytypic Programming on Terms, with
an Application to Rewriting},
booktitle = WGP,
publisher = "Utrecht University",
note = "UU-CS-2000-19",
year = 2000
}

by
Patrik Jansson /
NOpatrikjSP@AMchalmers.se