Algebraic domain equations for specifications containing inequational axioms

Abstract

Algebraic domain equations (ade’s) provide a means for implicitly or recursively specifying parameterized data types. A unique semantics is available provided the respective ade’s are defined over a category of specifications which are solely based on equational axioms. We extend this approach by showing that there exists an appropriate semantics even if the respective specifications contain as well equational as inequational axioms.