2010 | OriginalPaper | Chapter
Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
Authors : Camilo Rocha, José Meseguer
Published in: Logic for Programming, Artificial Intelligence, and Reasoning
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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
$\mathcal{R} = (\Sigma,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.,
$\mathcal{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
$\rightarrow_\mathcal{R}$
associated to a rewrite theory
$\mathcal{R}$
(and also about the joinability relation
$\downarrow_\mathcal{R}$
) is both characterized and illustrated with an example.