 Authors
 ClausPeter Wirth,
Bernhard Gramlich
 Title
 A ConstructorBased Approach for Positive/NegativeConditional Equational Specifications
 In
 J. Symbolic Computation (1994) 17, pp. 5190, Academic Press
Bib Entry
 Abstract
 We study algebraic specifications given by finite sets R of positive/negativeconditional
equations (i.e. universally quantified firstorder implications with a single equation in the succedent
and a conjunction of positive and negative (i.e. negated) equations in the antecedent). The class of
models of such a specification R does not contain in general a minimum model in the sense that it
can be mapped to any other model by some homomorphism. We present a constructorbased
approach for assigning appropriate semantics to such specifications. We introduce two restrictions:
firstly, for a condition to be fulfilled we require the evaluation values of the terms of the negative
equations to be in the constructor subuniverse which contains the evaluation values of all
constructor ground terms; secondly, we restrict the constructor equations to have ``Horn''form and
to be ``constructorpreserving''. A reduction relation for R is defined, which allows to generalize
the fundamental results for positiveconditional rewrite systems. This reduction relation is
monotonic w.r.t. consistent extension of the specification, which is of practical importance as it
allows for an incremental construction process of complex specifications without destroying
reduction steps which were possible before. Under the assumption of confluence, the factor algebra
of the term algebra modulo the congruence of the reduction relation is a minimal model which is
(beyond that) the minimum of all models that do not identify more objects of the constructor
subuniverse than necessary. We define several kinds of compatibility of R with a reduction
ordering for achieving decidability of reducibility, and present several criteria for the confluence of
our reduction relation.
 Full paper

 Format
 .ps.gz
 Size
 .16 Mbytes