On the Expressive Power of Rewriting

In this paper we address the open problem of classifying the expressive power of classes of rewriting systems. We introduce a framework to reason about the relative expressive power between classes of rewrite system, with respect to every property of interest P. In particular, we investigate four main classes of rewriting systems: left-linear Term Rewriting Systems, Term Rewriting Systems, Normal Conditional Term Rewriting Systems and Join Conditional Term Rewriting Systems. It is proved that, for all the main properties of interest of rewriting systems (completeness, termination, confluence, normalization etc.) these four classes form a hierarchy of increasing expressive power, with two total gaps, between left-linear TRSs and TRSs, and between TRSs and normal CTRSs, and with no gaps between normal CTRSs and join CTRSs. Therefore, these results formally prove the strict increase of expressive power between left-linear and non left-linear term rewriting, and between unconditional and conditional term rewriting, and clarify in what sense normal CTRSs can be seen as equivalent in power to join CTRSs.