Optimizing Maude Programs via Program Specialization

We develop an automated specialization framework for rewrite theories that model concurrent systems. A rewrite theory R= (Σ, E⊎ B, R) consists of two main components: an order-sorted equational theory E= (Σ, E⊎ B) that defines the system states as terms of an algebraic data type and a term rewriting system R that models the concurrent evolution of the system as state transitions. Our main idea is to partially evaluate the underlying equational theory E to the specific calls required by the rewrite rules of R in order to make the system computations more efficient. The specialization transformation relies on folding variant narrowing, which is the symbolic operational engine of Maude’s equational theories. We provide three instances of our specialization scheme that support distinct classes of theories that are relevant for many applications. The effectiveness of our method is finally demonstrated in some specialization examples.