A framework for operational equational specifications with pre-defined structures (Q1286447)

The authors present a general framework for studying equational specifications with pre-defined structures. The axioms of the specifications are to define new structures in addition to the given ones. In particular, they may define a new operator only partially over some given domain. The approach allows one to assign easily semantics to such specifications in a denotational and operational fashion. In order to enable functional-style computations, the authors introduce a semantically enriched notion of term rewriting. This rewrite relation also allows the authors to infer the consistency of the specification. For the latter purpose one has to show confluence modulo the given structures. The authors outline how to obtain criteria easily for confluence and termination of the rewrite relation of discourse by generalizing results of the classical syntactic rewrite theory. \(\copyright\) Academic Press.