A Framework for Operational Equational Specifications with Pre-defined Structures

We 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. Our approach allows one to assign easily semantics to such specifications in a denotational and operational fashion. In order to enable functional-style computations, we introduce a semantically enriched notion of term rewriting. This rewrite relation also allows us to infer the consistency of the specification. For the latter purpose one has to show confluence modulo the given structures. We 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.