| An SOS Message: Conservative Extension in Higher-Order Positive/Negative Conditional Term Rewriting (1998) | |||||||||||||||||
Abstract | |||||||||||||||||
| . General theorems in structured operational semantics can be transformed into related results in conditional term rewriting. We apply this approach to obtain a conservative extension theorem for higher-order conditional term rewriting systems with negative conditions. This result is useful, for instance, in modular specification of abstract data types, and in software renovation factories. 1 Introduction There is a strong link between the worlds of conditional term rewriting [23, 7] and of structured operational semantics (SOS) [29]. In fact, from a conceptual level they can be seen as identical. In both fields, terms are built from a set of function symbols. The binary relations on terms, rewrite steps and transitions, both are defined inductively by means of proof rules, called conditional rewrite rules or transition rules, respectively. Those rules, together with the validity, or non-validity, of a number of relations between terms, may imply the validity of another relation... | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||