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. Rewriting logic is reflective. Sound and complete for intended semantics. True concurrency model. Church-Rosser (with conditions). Termination: undecidable in general. Decidable fragments extensively studied.

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

Limitations. Termination not guaranteed. Efficiency depends on strategy. Learning curve for reflection. Tool ecosystem specific. Concurrent semantics complex. Strategy language needed.