Fixed-point Solutions for Ground Term Rewriting Systems.
Dorel Lucanu · 1994
this paper we consider the general case of arbitrary equations s = t where both s and t are terms constructed over a signature F of basic operators (called also constructors or terminals) and a signature Y of variable symbols (called also defined operators or nonterminals). The operational semantics of such a equation is given by ground rewriting on TF[Y . We sketch a way how the fixed-point technique can be applied for the systems of general equations. For notions of universal algebra we refer the reader to [5] and for notions of rewrite systems we refer [1]. The paper has four sections. In the second section we present the systems of regular equations over many-sorted alphabets. The presentation follows the line from [2]. We moreover consider the case when the computations are made modulo Fixed-point Solutions for Ground Term Rewriting Systems 2 an equational theory. We also prove some technical lemmata which allows us to apply, in the third section, the fixed-point technique for the general systems. The fourth section presents some applications of the theory. 2 Systems of regular equations on many-sorted alphabets