@article{wgjsc,
year={1994},
author={Claus-Peter Wirth\protect\index{Wirth, Claus-Peter}
and Bernhard Gramlich\protect\index{Gramlich, Bernhard}},
title={A Constructor-Based Approach for Positive/Negative-Conditional Equational Specifications},
journal={\jscname},
volume={17},
pages={51--90},
publisher={\academicpress},
note={\url{http://www.ags.uni-sb.de/~cp/p/jsc94}},
abstract={We study
algebraic
specifications given by finite sets R
of positive/negative-conditional equations
(i.e.\
universally quantified first-order
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
constructor-based
approach
for assigning appropriate semantics
to such specifications.
We
introduce two
syntactic
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 sub-universe which contains the
set of evaluation
values of all constructor
ground terms;
secondly,
we restrict
the constructor equations
to have ``Horn''-form
and to be ``constructor-preserving''.
A
reduction relation
for R
is defined,
which
allows to
generalize
the
fundamental
results for positive-conditional
rewrite systems,
which does not need to be noetherian
or restricted to ground terms,
and which is monotonic w. r. t.
consistent extension of the specification.
Under the assumption of confluence,
the factor algebra of the
ground 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
constructor ground terms than necessary.
To achieve decidability of reducibility
we define several kinds of compatibility
of R with a reduction ordering
and
present a complete critical-pair
test a la Knuth-Bendix
for the
confluence of the reduction relation.},
}