A Constructor-Based Approach to
Positive/Negative-Conditional
Equational Specifications

Claus-Peter Wirth and Bernhard Gramlich
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, W-6750 Kaiserslautern, Germany
E-mail: {wirth, gramlich}@informatik.uni-kl.de

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.

Keywords