A Rewrite Stack Machine for ROC!

\ROC is a deterministic rewrite strategy language which includes the rewrite rules as basic operators, and the deterministic choice and the repetition as high-level strategy operators. In this paper we present a method which, for a given term rewriting system (TRS) \mathbf{R}$, constructs a new TRS $\overline{\mathbf{R}}$ such that $\overline{\mathbf{R}}$-rewriting is equivalent (sound and complete) with $\mathbf{R}$-rewriting constrained by \ROC. Since $\overline{\mathbf{R}}$ uses a stack, it is called a \emph{rewrite stack machine}.