Constructors, Sufficient Completeness and Deadlock Freedom of Generalized Rewrite Theories

Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into {\em constructors} and {\em defined} symbols. But what should sufficient completeness mean for a rewrite theory $\rcal = (\Sigma,E,R)$ with equations $E$ and non-equational rules $R$ describing concurrent transitions in a system? The present work argues that a rewrite theory naturally has {\em two} notions of constructor: the usual one for its equations $E$, and a more restrictive one for its rules $R$. The intuition is that a function symbol $f$ that is a constructor for the equations $E$ may be a {\em defined symbol} for the rules $R$. All this can be very useful both to check the completeness of specification with non-equational rules, and for inductive reasoning purposes in rewriting logic. This paper studies the relation between these two notions in the more general case when rewrite theories can have (i) a frozenness map restricting rewriting with $R$, and (ii) a context-sensitive map restricting rewriting with the equations $E$, as it is possible for specifications in the Maude language. It also investigates a syntactic characterization for the notion of deadlock states of a rewrite theory, which appears promising for solving some reachability problems. Sufficient conditions allowing the automatic checking of sufficient completeness, and other related properties, by equational tree automata modulo equational axioms such as as associativity, commutativity, and identity are also given. They are used to extend the Maude Sufficient Completeness Checker from the checking of equational theories to that of both equational and rewrite theories. Finally, the usefulness of the proposed notion of constructors in proving inductive theorems about the reachability rewrite relation $\rightarrow_\rcal$ associated to a rewrite theory $\rcal$ (and also about the joinability relation $\downarrow_\rcal$) is both characterized and illustrated with examples.NSF grant CNS 07-16638NSF grant CCF 09-05584unpublishednot peer reviewe