Term rewriting with traversal functions

Term rewriting is an appealing technique for performing program analysis and program transformation. Tree (term) traversal is frequently used but is not supported by standard term rewriting. We extend many-sorted, first-order term rewriting with <em>traversal functions</em> that automate tree traversal in a simple and type safe way. Traversal functions can be bottom-up or top-down traversals. They can be either sort preserving transformations, or mappings to a fixed sort. We give examples and describe the semantics and implementation of traversal functions.