Constructor equivalent term rewriting systems (Q689634)

We restrict ourselves to the class of orthogonal term rewriting systems (formerly called regular systems). The class of strongly sequential term rewriting systems (SS) was defined by \textit{Huet} and \textit{Lévy}. Strongly sequential systems admit an efficient one-step reduction strategy; strong sequentiality is decidable but is conjectured to be NP- complete. The class of forward-branchingsystems (FB) is a subclass of \(SS\); forward-branching systems admit an efficient strategy for seuqences of reductions; the forward-branching property can be decided in polynomial time. \textit{Thatte} demonstrated the possibility of simulating an orthogonal \(TRS\) with a left-linear constructor system obtained from the original system via a simple transformation. With examples, we point out that Thatte's transformation does not always preserve orthogonality and that if it does, it does not always preserve strong sequentiality. This leads us to define a new subclass of \(SS\): the class of constructor equivalent systems (\(CE\)) for which Thatte's transformation preserves strong sequentiality. We give a simple characterization of \(CE\) and show that it is a subclass of \(FB\). This work motivates our choice of studying nonconstructor systems linke \(FB\).