Pith. sign in

REVIEW 3 major objections 5 minor 20 references

Compositional specification in rewriting logic

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper claims that a synchronous-composition operation based on equality of user-defined properties makes rewriting-logic specifications compositional, and that a semantics-preserving split translation lets the resulting systems run…

desk verdict Theorem 1 and Proposition 5 are false as stated because the composed rewrite system omits idling moves when a component is terminal; the paper's central claim needs repair, but the framework is worth engaging. read the letter →

arxiv 1908.11769 v3 pith:2AMK3J5F submitted 2019-08-30 cs.LO

Óscar Martín , Alberto Verdejo , Narciso Martí-Oliet This is my paper · ORCID
classification cs.LO MSC 68Q4268Q6068Q85
keywords compositionalspecificationrewritinglogicsynchronouscompositionegalitariantransitionsystemstermsMaudemodularitysplitoperation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Rewriting logic is naturally concurrent because subterms of the state term rewrite simultaneously, but the global state term makes it hard to specify systems as independent components. The paper proposes synchronous composition: each component is an egalitarian rewrite system in which states and transitions are both first-class terms, and components interact only by requiring chosen properties of their current stages to be equal. This is formalized both at the level of rewrite systems and at the level of the transition structures that give them semantics. The central result is that a split operation translates any composed egalitarian system in the stated class into an ordinary rewrite system with equivalent semantics, so the compositional style can use the existing execution and verification machinery for rewriting logic.

What carries the argument

The machinery is the egalitarian rewrite rule $t \xrightarrow{[\ell]} t'$ in which the rule label is itself a term $\ell$ of sort Trans, together with partial property functions $p : \mathrm{Stage} \to [s]$ and synchronization criteria $Y$ consisting of equalities $p_1(g_1) = p_2(g_2)$ at simultaneously visited stages. A rule instance is executed as two half-rewrites, $t \to \ell$ and $\ell \to t'$, so a transition forgets its origin state and carries only the parameters the specifier put into its term. The split operation maps each such rule to the two plain rules $t \to \ell$ and $\ell \to t'$, making every stage a state of a standard rewrite system. Theorem 1, the commutativity of $\mathrm{sem}$ and $\mathrm{split}$, is what guarantees this translation preserves the behaviour of the composed specification.

What would settle it

Take a plain rewrite system with a rule that rewrites a proper subterm, such as $a \to a'$ inside a context $f(a,b)$, while another rule independently rewrites $b$; decompose it into topmost components with added synchronization criteria as Section 2.8 suggests, and compare the reachable rewrite sequences of the original system with those of $\mathrm{split}$ of the decomposed composition. Any mismatch between the two reachability behaviours would show that the class covered by the semantics-preservation theorem is narrower than the paper's compositional method claims.

Watch

Extended reading notes

Core claim

At the center of the paper is Theorem 1: for every egalitarian rewrite system $R$ with totally defined properties and topmost atomic components, $\mathrm{sem}(\mathrm{split}(R)) \equiv \mathrm{split}(\mathrm{sem}(R))$, where $\mathrm{sem}$ maps rewrite systems to transition structures and $\mathrm{split}$ turns egalitarian systems into plain ones. The paper's reading of this identity is that composition and interpretation commute: describing a system as a set of independently specified components and composing them synchronously, then splitting the result, yields the same transition structure as splitting each component first and then composing the ordinary systems. Consequently the split is a sound bridge from the compositional specification style back to standard rewrite systems, and standard engines can be run on the assembled specification. The framework also makes states and transitions interchangeable, so a composed system may have one component in a state while another is between states, and this is handled without leaving rewriting logic.

Load-bearing premise

The load-bearing premise is that every component of a composed system can be assumed topmost, meaning its rules act on the whole component state, and that every property used for synchronization is totally defined, with the paper offering a decomposition method but no general proof that an arbitrary non-topmost rewrite system can be faithfully decomposed that way.

Editorial extensions

If this is right

  • A specifier can write a train, a memory, or a mutex controller as an isolated component, attach it to others by synchronization criteria, and then use the split system with ordinary rewriting-based execution and model checking.
  • A non-atomic egalitarian system is computable exactly when its atomic components are computable, so executability requirements do not have to be re-established for whole composed systems.
  • Complex interactions such as summing two properties or synchronizing on a non-equality relation can be encoded by adding a small connector component, because connectors are themselves egalitarian rewrite systems synchronized by equality.
  • Because states and transitions can synchronize with each other, one component can be mid-transition while another is in a state, and the composed system's global state/transition distinction is naturally blurred.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The train/reckoner example reads the synchronization criteria as assume-guarantee contracts; formalizing that reading into a compositional proof rule for temporal formulas over split systems would be a natural test of the framework.
  • The split's rule explosion, already visible in the paper's own train example with 24 combinations, is the main practical obstacle; a lazy or reachability-driven split that generates composed rules only when their membership conditions are satisfiable would likely scale much better than the naive construction.
  • The total-property restriction could be probed empirically: apply the paper's state-duplication totalization to a set of partial-interface specifications and check whether the resulting split systems remain equivalent to the intended behaviour.
  • The same property-as-port pattern should transfer beyond Maude to give other rewriting-based formalisms a compositional layer, since the core definitions do not depend on any particular implementation of rewriting logic.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper develops a framework for compositional specification in rewriting logic. It introduces egalitarian rewrite systems, in which transitions are first-class terms rather than atomic labels, together with a synchronous composition operation based on equality of user-defined state/transition properties. The paper also defines plain rewrite systems and transition structures, a split translation from egalitarian to plain systems, and semantic maps. The central claim is Theorem 1: for egalitarian rewrite systems with topmost components and totally defined properties, the semantic map and the split operation commute, so that composed egalitarian specifications can be translated into standard rewrite systems while preserving semantics. The paper includes motivating examples, a worked train/controller specification, and a discussion of related work.

Significance. The proposal is original and well motivated: treating transitions as terms, synchronising on arbitrary properties, and providing a split translation are genuinely useful ideas for bringing compositionality to rewriting-logic-based tools such as Maude. The definitions are careful and the examples are instructive. However, the main coherence theorem is false as stated, because the composition operation on plain rewrite systems does not match the composition of their transition-structure semantics: idling of a component in a terminal state is allowed by the product semantics but not generated by the rule construction. This is a load-bearing defect, not a presentation issue. If repaired, the framework could provide a practical route from composed egalitarian specifications to standard rewriting engines, but the paper's central correctness claim currently fails.

major comments (3)
  1. [Section 3.2.3] The composition of plain rewrite systems is defined by generating rules 'for each pair of rules' from R1 and R2. Consequently, a left-only move ⟨q1,q2⟩→⟨q1',q2⟩ is generated only when q2 is the left-hand side of some rule of R2. In contrast, the composition of plain transition structures in Section 3.1.3 admits this move whenever q1→q1' and q2=q2', with no requirement that q2 has an outgoing transition. Thus a component in a terminal state cannot idle in a composed rewrite system, although the intended product semantics allows it. Concretely, let R1 be the plain rewrite system with a single rule a→a' and R2 be the system with a single state b and no rules; both are topmost, Y=∅ satisfies the hypotheses vacuously, and all properties are trivially totally defined. Then sem(split(R1||∅R2)) has no transition from ⟨a,b⟩, because the generated rewrite system has no rules at all, whereas split(sem(R1||∅R2)) has the transition ⟨a,b⟩→⟨a',b⟩. Proposition 5 is therefore false, and since the induction step of Theorem 1 invokes Proposition 5, Theorem 1 is false as stated. The fix is to add explicit idling/stuttering rules for every state of each component in the rewrite-system composition, or to otherwise ensure that terminal states can be left unchanged while the other component progresses, and then to re-prove Proposition 5 and Theorem 1.
  2. [Section 2.8] The main theorem is restricted to components that are topmost and to totally defined properties, but the paper's broader methodological claims are not so restricted. Section 2.8 argues that a non-topmost rewrite system can be decomposed into topmost components with additional synchronisation criteria, yet no general construction or correctness proof is given. As a result, the paper does not establish that the compositionality methodology applies to the general class of rewrite systems suggested by the introduction, and the practical scope of Theorem 1 is narrower than the paper's motivating discussion implies. The authors should either provide the missing decomposition construction and prove that it preserves the intended semantics, or explicitly state that the framework is intended only for systems that are already topmost.
  3. [Section 3.2.4] The atomic base case of Theorem 1 is dismissed with 'it is not difficult to see' that both sides reduce to the same plain transition structure. Given the subtlety of the half-rewrite relation and the role of equations and membership conditions, this step deserves a detailed verification. In particular, one must check that the reachable-stage structure induced by the split rewrite rules exactly matches the bipartite adjacency structure of split(sem(R)), including the treatment of terms that belong to both State and Trans sorts, if such overlap is possible in an order-sorted signature.
minor comments (5)
  1. [Section 3.1.4] In the proof of Proposition 1, 'atomic(T1) = atomic(T1)' should presumably read 'atomic(T1) = atomic(T2)'.
  2. [Section 3.2.4] Similarly, the proof of Proposition 4 contains 'atomic(R1) = atomic(R1)', which should be 'atomic(R1) = atomic(R2)'.
  3. [Section 4] In the displayed composed rule for the reckoner example, the condition contains '... : State /\ /\ < moving, moving, lmoving | D > : State', with a duplicated '/\'. This appears to be a typographical error.
  4. [Definition 8] In Definition 8, the second bullet says 'for all p1∈Σi|State'; this should be 'p1∈Σ1|State'.
  5. [Section 3.2.1] The proof of Proposition 3 is only a sketch: the semantic equivalence of the transformed rule is argued informally, and the final claim that the resulting rule is readable is asserted without a full case analysis. This proposition is not used in the main theorem, but it should still be proved carefully if it is to be stated as a proposition.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: Theorem 1 is derived from definitions and structural induction; self-citations are motivational, not load-bearing.

full rationale

The paper's central result, Theorem 1, is not equivalent to its inputs by construction. The proof is a structural induction on egalitarian rewrite systems. In the atomic case, the equality sem(split(R)) = split(sem(R)) is checked directly from the definitions of split and of the half-rewrite semantics. In the composed case, the proof uses the defining equations split(R1 ||_Y R2) = split(R1) ||_Y split(R2) and sem(R1 ||_Y R2) = sem(R1) ||_Y sem(R2), and then invokes Proposition 5, which states that for plain rewrite systems the semantics of the syntactic composition is equivalent to the composition of the semantics. That proposition is a genuine semantic preservation claim proved from the rule-generation and product-transition definitions; it is not an assumed instance of the theorem. No parameter is fitted and no quantity is renamed as a prediction. The self-citations (Martín et al. 2016a,b, 2018) are used for motivation, examples, and parameterized-programming tooling, but they are not premises of the commutativity result; no load-bearing uniqueness theorem is imported from the authors' earlier work. The skeptical counterexample about terminal components concerns the correctness or scope of Proposition 5 and Theorem 1 as stated; a false theorem can still be non-circular, and the mismatch between rule generation and the product transition relation is a soundness issue rather than a circularity issue. Accordingly, no circular step is identified.

Assumptions & free parameters 0 free parameters · 5 assumptions · 3 invented entities

No numerical free parameters are fitted; the framework's inputs are the specifier's choice of properties, transition-term variable scope, and synchronization criteria, which are part of the specification method rather than fitted constants. The load-bearing assumptions are the topmostness restriction, the existence of common equational theories for property values, and the expressiveness limit of membership equational logic for partial properties. The invented entities are formal constructs defined in the paper, not empirical postulates.

assumptions (5)
  • standard math Order-sorted membership equational logic as the base logic (Meseguer 1992).
    The whole framework builds on membership equational logic, its equations, membership axioms, kind completion, and normal forms; cited as standard from the rewriting logic literature.
  • domain assumption Atomic components are topmost, and composition of plain rewrite systems requires topmost operands.
    Section 3.2.1 requires State and Trans sorts with no Stage subterm, and Section 3.2.3 restricts plain composition to topmost systems. The paper suggests decomposing non-topmost systems into topmost ones (Section 2.8) without giving a general correctness proof.
  • domain assumption A common equational theory with protected inclusion exists for comparing property values across components.
    Section 3.2.2 requires that for each criterion (p1,p2), the codomain sorts have a common equational subtheory with equal ground terms, so that equality can be checked. This restricts what components can be synchronized.
  • domain assumption Membership equational logic cannot express negative sort assertions, forcing total properties in the plain composition.
    Section 3.2.3 explains that undefined properties cannot be checked with positive membership conditions, so the plain-system composition requires totally defined properties. The paper discusses state replication as a workaround.
  • ad hoc to paper Every atomic egalitarian rewrite system can be transformed into a readable one (Proposition 3).
    Readability is a property invented for this paper to avoid counterintuitive semantics of rules like x-[a]->x. The proof of the transformation is sketched with variable renaming and condition duplication, not machine-checked.
invented entities (3)
  • Stage (supersort of State and Trans)
    purpose: Allow a composition to align a state in one component with a transition in another, since synchronization can be heterogeneous.
    A formal definition (Section 3.1.1), not an empirical object; no falsifiable prediction, but it is defined precisely and used consistently.
  • Synchronous composition operator ||_Y
    purpose: Compose specifications by requiring equality of property values at synchronized stages.
    A formal operator, motivated by process-algebra composition; its adequacy is argued through examples and the split theorem, not through an external prediction.
  • Egalitarian rewrite system with transition terms
    purpose: Make transitions first-class so properties can be evaluated on them and value-passing synchronization can be expressed.
    A formal framework extension; burden is on soundness, not empirical evidence.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Compositional specification in rewriting logic." pith.science (2026). https://pith.science/paper/2AMK3J5F

@misc{pith2026190811769,
  author       = {Pith},
  title        = {Pith review of: Compositional specification in rewriting logic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2AMK3J5F}},
  note         = {Machine review of arXiv:1908.11769}
}
read the original abstract

Rewriting logic is naturally concurrent: several subterms of the state term can be rewritten simultaneously. But state terms are global, which makes compositionality difficult to achieve. Compositionality here means being able to decompose a complex system into its functional components and code each as an isolated and encapsulated system. Our goal is to help bringing compositionality to system specification in rewriting logic. The base of our proposal is the operation that we call synchronous composition. We discuss the motivations and implications of our proposal, formalize it for rewriting logic and also for transition structures, to be used as semantics, and show the power of our approach with some examples. This paper is under consideration in Theory and Practice of Logic Programming (TPLP).

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

20 extracted references · 20 canonical work pages

  1. [20]

    In Communi- cating Sequential Processes: The First 25 Years, Symposium on the Occasion of 25 Years of CSP, London, UK, July 7-8, 2004, Revised Invited Papers , A

    Communicating mobile processes. In Communi- cating Sequential Processes: The First 25 Years, Symposium on the Occasion of 25 Years of CSP, London, UK, July 7-8, 2004, Revised Invited Papers , A. E. Abdallah, C. B. Jones, and J. W. Sanders, Eds. Lecture Notes in Computer Science, vol

    work page 2004

  2. [204]

    Verdejo, A

    Open Publishing Association, Cali, Colombia, 19–30. Verdejo, A. and Mart´ı-Oliet, N.2012. Basic completion strategies as another application of the Maude strategy language. In Workshop on Reduction Strategies in Rewriting and Programming (WRS2011), S. Escobar, Ed. Electronic Proceedings in Theoretical Computer Science, vol

    work page 2012

  3. [1241]

    Kindler, E

    Springer-Verlag, Jyv¨ askyl¨ a, Finland, 220–242. Kindler, E. and Vesper, T.1998. ESTL: A temporal logic for events and states. InApplication and Theory of Petri Nets 1998: 19th International Conference, ICATPN ’98 , J. Desel and M. Silva, Eds. Lecture Notes in Computer Science, vol

    work page 1998

  4. [1988]

    In Ad- vances in Petri nets: APN 1987 , G

    Compositional semantics of pure place/transition systems. In Ad- vances in Petri nets: APN 1987 , G. Rozenberg, Ed. Lecture Notes in Computer Science, vol

    work page 1987

  5. [1997]

    In Re- cent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Tarquinia, Italy, June 1997, Selected Papers

    Mapping tile logic into rewriting logic. In Re- cent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Tarquinia, Italy, June 1997, Selected Papers . Lecture Notes in Computer Science, vol

    work page 1997

  6. [2000]

    In CONCUR 2000—Concurrency Theory: 11th International Conference , C

    Generalized Model Checking: Reasoning about Par- tial State Spaces. In CONCUR 2000—Concurrency Theory: 11th International Conference , C. Palamidessi, Ed. Lecture Notes in Computer Science, vol

    work page 2000

  7. [2001]

    In Programming Languages and Systems: 10th European Symposium on Programming, ESOP 2001, D

    Modal transition systems: A foundation for three-valued program analysis. In Programming Languages and Systems: 10th European Symposium on Programming, ESOP 2001, D. Sands, Ed. Lecture Notes in Computer Science, vol

    work page 2001

  8. [2004]

    In Proceedings of the Fifth International Workshop on Rewriting Logic and Its Appli- cations (WRLA 2004), N

    Towards a strategy language for Maude. In Proceedings of the Fifth International Workshop on Rewriting Logic and Its Appli- cations (WRLA 2004), N. Mart´ ı-Oliet, Ed. Electronic Notes in Theoretical Computer Science, vol

    work page 2004

Show all 20 references
  1. [2005]

    In FM 2005: Formal Methods , J

    Combining CSP and B for specification and property verification. In FM 2005: Formal Methods , J. Fitzgerald, I. J. Hayes, and A. Tarlecki, Eds. Springer Berlin Heidelberg, Berlin, Heidelberg, 221–236. Chaki, S., Clarke, E. M., Ouaknine, J., Sharygina, N., and Sinha, N

    2005

  2. [2007]

    In Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES 2006), M

    Deduction, strategies, and rewriting. In Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES 2006), M. Archer, T. B. de la Tour, and C. Mu˜ noz, Eds. Electronic Notes in Theoretical Computer Science, vol

    2006

  3. [2008]

    In Perspectives Workshop: Model Engineering of Complex Systems (MECS), 10.08

    Modeling heterogeneous real-time components in BIP. In Perspectives Workshop: Model Engineering of Complex Systems (MECS), 10.08. - 13.08.2008 , U. Aßmann, J. B´ ezivin, R. F. Paige, B. Rumpe, and D. C. Schmidt, Eds. Dagstuhl Seminar Proceedings, vol. 08331. Schloss Dagstuhl -...

    2008

  4. [2009]

    In Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications (WRLA 2008), G

    A Rewriting Semantics for Maude Strategies. In Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications (WRLA 2008), G. Rosu, Ed. Electronic Notes in Theoretical Computer Science, vol

    2008

  5. [2010]

    The Linear Temporal Logic of Rewriting Maude Model Checker. In Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Se- lected Papers, P. C. ¨Olveczky, Ed. Lecture Note...

    2010

  6. [2012]

    Proceedings - 2012 19th International Symposium on Temporal Representation and Reasoning, TIME 2012 , 13–20

    Efficient regular linear temporal logic using dualization and stratification. Proceedings - 2012 19th International Symposium on Temporal Representation and Reasoning, TIME 2012 , 13–20. Soboci´nski, P

    2012

  7. [2014]

    In From Programs to Systems

    Assembly theories for communication-safe component systems. In From Programs to Systems. The Systems perspective in Computing - ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6,

    2014

  8. [2016]

    In Developements in Computational Models: DCM 2015 Proc

    Compositional model checking of concurrent systems, with Petri nets. In Developements in Computational Models: DCM 2015 Proc. , C. A. Mu˜ noz and J. A. P´ erez, Eds. Electronics Proceedings in Theoretical Computer Science, vol

    2015

  9. [2017]

    In 7th Conference on Algebra and Coalgebra in Com- puter Science, CALCO 2017, June 12-16, 2017, Ljubljana, Slovenia , F

    Cospan/span(graph): an algebra for open, reconfigurable automata networks. In 7th Conference on Algebra and Coalgebra in Com- puter Science, CALCO 2017, June 12-16, 2017, Ljubljana, Slovenia , F. Bonchi and B. K¨ onig, Eds. LIPIcs, vol

    2017

  10. [8373]

    Mart´ın, ´O., Verdejo, A

    Springer, 129–150. Mart´ın, ´O., Verdejo, A. , and Mart´ı-Oliet, N. 2016a. Egalitarian State-Transition Sys- tems. In Rewriting Logic and Its Applications: WRLA 2016 , D. Lucanu, Ed. Lecture Notes in Computer Science, vol

    2016

  11. [9938]

    Mart´ın,´O., Verdejo, A., and Mart´ı-Oliet, N.2018

    Springer, Cham, 141–156. Mart´ın,´O., Verdejo, A., and Mart´ı-Oliet, N.2018. Parameterized programming for com- positional system specification. In Rewriting Logic and Its Applications: WRLA 2018, V. Rusu, Ed. Lecture Notes in Computer Science, vol. 11152. Springer. Mazurkiewicz, A

    2018

  12. [9942]

    Mart´ın, ´O., Verdejo, A

    Springer, Eindhoven, The Netherlands, 98–117. Mart´ın, ´O., Verdejo, A. , and Mart´ı-Oliet, N. 2016b. Synchronous products of rewrite systems. In Automated Technology for Verification and Analysis: ATVA 2016 , C. Artho, A. Legay, and D. A. Peled, Eds. Lecture Notes in Computer ...

    2016

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.