Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

Abstract

Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite theory R=(Σ,E,R) with equations E and non-equational rules R describing concurrent transitions in a system? This work argues that a rewrite theory naturally has two notions of constructor: the usual one for its equations E, and a different one for its rules R. The sufficient completeness of constructors for the rules R turns out to be intimately related with deadlock freedom, i.e., R has no deadlocks outside the constructors for R. The relation between these two notions is studied in the setting of unconditional order-sorted rewrite theories. Sufficient conditions are given allowing the automatic checking of sufficient completeness, deadlock freedom, and other related properties, by propositional tree automata modulo equational axioms such as associativity, commutativity, and identity. 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 →R associated to a rewrite theory R (and also about the joinability relation ↓R ) is both characterized and illustrated with an example.

Se ha estudiado a fondo la integridad suficiente para las especificaciones de ecuaciones, donde los símbolos de función se clasifican en constructores y símbolos definidos. Pero, ¿qué debería significar suficiente completitud para reescribir la teoría R=(Σ,E,R) con ecuaciones E y reglas no ecuacionales R que describen transiciones concurrentes en un sistema? Este trabajo argumenta que una teoría de reescritura tiene naturalmente dos nociones de constructor: la habitual para sus ecuaciones E, y otra diferente para sus reglas R. La suficiente completitud de constructores para las reglas R resulta estar íntimamente relacionada con la libertad de interbloqueo, es decir, R no tiene interbloqueos fuera de los constructores de R. La relación entre estas dos nociones se estudia en el marco de las teorías de reescritura ordenadas por orden incondicional. Se dan condiciones suficientes que permiten la comprobación automática de la integridad suficiente, la libertad de interbloqueo y otras propiedades relacionadas, mediante axiomas ecuacionales de módulos de autómatas proposicionales como la asociatividad, la conmutatividad y la identidad. Se utilizan para extender el verificador de integridad suficiente de Maude desde la verificación de teorías ecuacionales hasta la de teorías ecuacionales y de reescritura. Finalmente, se caracteriza e ilustra con un ejemplo la utilidad de la noción de constructores propuesta para probar teoremas inductivos sobre la relación de reescritura de alcanzabilidad →R asociada a una teoría de reescritura R (y también sobre la relación de capacidad de unión ↓R).