Conditional Rewriting modulo a Built-in Algebra

Abstract

We present a method to integrate built-in operations that are described by a given built-in algebra into conditional rewriting. 'First, equational specifications will be assigned a suitable semantics that takes into account the predefined structures. The interpretation of ”semantically and syntactically mixed objects” is based on an appropriate introduction of sort hierarchies that allows to separate semantical and syntactical considerations. As a consequence of this separation a great deal of ”classical rewrite theory” as for instance a critical pair lemma can be generalized to our context. Further we are able to construct appropriate well-founded orderings to guarantee the termination of the rewrite relation that allow to integrate semantical informations from the given built-in algebra. In order to illustrate the ideas several examples concerning built-in arithmetic are presented.