Initiality + Nondeterminism => Junk

Keywords: algebraic specification, initial semantics, nondeterminism, underspecification

Abstract: is well known that the presence of disjunction in a specification precludes the existence of initial models. However, one might consider underspecification as a special version of nondeterminism, and consequently hope that initial models for nondeterministic specifications might alleviate this problem. We review three kinds of initial models for Horn specifications of nondeterminism. In each we find elements which are not intended by the specifier - *intuitive junk*. We point out that nondeterminism subsumes underspecification as a special case, and that it is the latter which is responsible for the *junk* in the models. We suggest that disjunction in the specifications of nondeterminism is the apropriate mechanism for capturing underspecification, and show how this is reflected in the concept of quasi-initiality of model classes. Keywords: