Rewriting Logic

Origin. Meseguer introduced rewriting logic (1992). Unifies many computational paradigms. States as algebraic terms, transitions as rewrite rules. Foundation for Maude language. Reflects concurrent systems, OO programming, real-time systems.

Models. Computation as rewriting. State: term in equational theory. Transition: rewrite rule l → r (labeled). Concurrency: independent rewrites in parallel. Reflection: rewriting logic can represent itself. Unifies logic and computation.

Formalism.

Rewrite theory: R = (Σ, E, L, R) where:

Σ: signature (sorts, operations)
E: equations (structural equivalence)
L: labels for rules
R: labeled rewrite rules [l]: t → t'

Rewrite rule: [l]: t(x₁,...,xₙ) → t'(x₁,...,xₙ) if C

Applies modulo equations E.

Sequent: [α]: t →* t' (labeled derivation from t to t')

Inference rules:

Reflexivity: [id]: t → t
Congruence: if [α]: t → t', then [f(α)]: f(t) → f(t')
Transitivity: if [α]: t₁ → t₂ and [β]: t₂ → t₃, then [α;β]: t₁ → t₃
Replacement (E): if t =_E t' and [α]: t → t'', then [α]: t' → t''

Concurrent rewriting: Independent subterms rewrite in parallel. Natural model of concurrency.

Reflection: Rewriting logic can represent rewriting logic. Meta-level reasoning.

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Rewrites	Single step
→*	—	Rewrites many	Transitive closure
=_E	—	Equivalent	Modulo equations
[l]	—	Label	Rule identifier
Σ	U+03A3	Signature	Sorts, ops
E	—	Equations	Structural
R	—	Rules	Transitions

Metatheory. Meseguer (1992) supplied a model theory as well as a proof theory. The models of a rewrite theory are categories: objects are E-equivalence classes of terms, morphisms are equivalence classes of proof terms, and the operations of Σ act functorially. The four inference rules are sound and complete for this class of models, and the initial model is the term model, so a rewrite is a concurrent computation and its proof term is the record of which rules fired where. The division between E and R is what yields true concurrency: equations are structural and unobservable, rules are state change, and rewriting takes place on E-classes rather than terms. Clavel and Meseguer proved reflection: a finitely presented universal rewrite theory faithfully represents every finitely presented theory together with its terms, so meta-level manipulation of theories happens inside the logic. Derivability t →* t' is recursively enumerable but not decidable.

Applies to. Maude language. Formal methods. Protocol specification. Real-time systems. Biological modeling. Theorem proving. Language semantics.

Limitations. Reachability is only semi-decidable, so Maude's search and its LTL model checker are decision procedures exactly when the state space reachable from the initial term is finite, which excludes unbounded and parametric systems. Executability imposes conditions the logic cannot discharge: E must be Church–Rosser and terminating modulo the structural axioms and R must be coherent with E, all three undecidable, and the Church-Rosser and coherence checkers establish sufficient conditions rather than deciding. Matching modulo associativity and commutativity is NP-complete and one term can have exponentially many matches, so a rewrite step is not unit cost. The rules say what may happen and never what must: fairness, priority and scheduling lie outside the logic, which is why a separate strategy language is needed. Time and probability require the distinct semantics of Real-Time Maude and PMaude.