{"id":"8176c8a3-39dc-4651-815d-08162ae197b6","arxiv_id":"1908.11769","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Synchronous composition of egalitarian rewrite systems, with synchronization by equality of partial properties on states and transitions, is formalized and shown coherent with the split translation back to standard rewriting logic.","lead":"This paper defines synchronous composition for rewriting logic: independent component specifications are composed by requiring user-defined properties on states and transitions to agree at every step. It matters because it gives a structured path to component-based design and verification for Maude-style formal modeling tools.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1 is false as stated: §3.2.3's rule generation never produces a one-component move when the other component is in a state with no outgoing rules, while the §3.1.3 product semantics explicitly allows idling; a two-state counterexample refutes Proposition 5 and Theorem 1.","rationale":"The reader's concern is a scope limitation: the paper gives no general decomposition of non-topmost systems into topmost components, so the practical coverage of the theorem may be narrower than claimed. The counterexample above is stronger and more load-bearing: it violates Theorem 1 even inside the stated hypotheses (topmost components, totally defined properties, empty synchronization). The paper's central promise—that composition plus split lets a specifier use ordinary Maude-style engines on the result—depends directly on Theorem 1. Without it, sem(split(R)) and split(sem(R)) can disagree even in the simplest deadlock case. A repair is conceivable (for example, generate explicit idling rules for every state of every component, or alter the product semantics to disallow idling at deadlocked states), but as written the definitions in §3.1.3 and §3.2.3 are inconsistent. This is an internal correctness failure, not merely an unproved generalization, so the appropriate verdict is stronger than conditional acceptance.","tokens_in":41713,"tokens_out":18733,"duration_ms":176560,"concrete_test":"Encode the counterexample in the paper's own definitions (or in Maude with the proposed extension): R1 = (a, t, a′, rule a -[t]-> a′), R2 = (b, no rules), Y=∅. Compute the two sides of Theorem 1: verify that sem(split(R)) has no transition out of ⟨a,b⟩ because no pair of rules can generate a left-only rule, whereas split(sem(R)) contains the path ⟨a,b⟩→⟨t,b⟩→⟨a′,b⟩ by the idling clause. If both checks succeed, the theorem is falsified; if an implementation hides idling rules, print the generated rule set for R2 with no rules to expose the discrepancy.","verdict_should_be":"REJECT","load_bearing_attack":"Proposition 5 and Theorem 1 are false as stated. In the definition of composition for plain rewrite systems (§3.2.3), the rule set is generated \"for each pair of rules\" q1→q1′ from R1 and q2→q2′ from R2; the left-only rule ⟨q1,q2⟩→⟨q1′,q2⟩ is thereby produced only for those q2 that are the left side of some rule of R2. The plain-transition-structure product in §3.1.3, however, allows ⟨q1,q2⟩→⟨q1′,q2⟩ whenever q1→q1′ and q2=q2′, with no requirement that q2 has an outgoing transition. So if one component reaches a terminal state, the intended product can still progress by idling the dead component, but the generated rewrite system has no rule at all from the pair. Concretely, take R1 with rule a -[t]-> a′ and R2 with a single state b and no rules, with Y=∅; all properties are vacuously total and both components are topmost. Then sem(split(R)) has no rewrites from ⟨a,b⟩, while split(sem(R)) has ⟨a,b⟩→⟨t,b⟩→⟨a′,b⟩. Thus the \"easy application of definitions\" in Proposition 5 and the induction step of Theorem 1 are unsound.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":42020,"tokens_out":7261,"duration_ms":72308,"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":[{"comment":"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.","section":"Section 3.2.3"},{"comment":"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.","section":"Section 2.8"},{"comment":"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.","section":"Section 3.2.4"}],"minor_comments":[{"comment":"In the proof of Proposition 1, 'atomic(T1) = atomic(T1)' should presumably read 'atomic(T1) = atomic(T2)'.","section":"Section 3.1.4"},{"comment":"Similarly, the proof of Proposition 4 contains 'atomic(R1) = atomic(R1)', which should be 'atomic(R1) = atomic(R2)'.","section":"Section 3.2.4"},{"comment":"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.","section":"Section 4"},{"comment":"In Definition 8, the second bullet says 'for all p1∈Σi|State'; this should be 'p1∈Σ1|State'.","section":"Definition 8"},{"comment":"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.","section":"Section 3.2.1"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nThe paper's central theorem doesn't hold as stated. The stress-test note is right: in §3.2.3, the composition of plain rewrite systems only generates rules for each pair of rules from the two components. If one component is in a state with no outgoing rules, there is no pair, so no idling move is generated, even though the product transition structure of §3.1.3 allows a component to stay still while the other moves. The concrete counterexample—R1 with a→a', R2 a single state and no rules, Y=∅—breaks Proposition 5 and Theorem 1. This is a load-bearing flaw, not a cosmetic gap.\n\nThat's a pity, because the paper has real merits. The idea of egalitarian rewrite systems, with transition terms as first-class citizens and synchronisation by equality of partially defined properties, is thoughtfully developed. The split operation is a sensible bridge back to standard rewriting logic. The examples (mutex, computer architecture, controlled trains) are instructive and well explained. The authors are also candid that much of this adapts existing ideas, which is honest.\n\nThe other weaknesses the reader flagged are real but secondary: proofs of Proposition 3 and Theorem 1 are sketched rather than detailed, the implementation is future work, and the decomposition into topmost components (Section 2.8) is described informally without a general correctness proof. But the terminal-state idling bug is more serious, and it wasn't caught in the review. It may be fixable—for instance, by generating idling rules even when the partner has no rule, or by changing the product semantics to match the generated rules. But as written, the central coherence theorem is false.\n\nThis paper deserves a serious referee, but it shouldn't be accepted as is. I'd send it back with a request to fix the composition definition and resubmit. For my own work, I wouldn't cite it in its current form. But it's worth a reading group discussion, if only to untangle the counterexample and think about whether the fix is natural.","headline":"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.","tokens_in":42540,"tokens_out":3595,"would_cite":false,"duration_ms":31221,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q42","68Q60","68Q85"],"pacs":[],"model":"deepseek-v4-flash","headline":"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…","keywords":["compositional specification","rewriting logic","synchronous composition","egalitarian transition systems","transition terms","Maude","modularity","split operation"],"falsifier":"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.","tokens_in":41492,"feed_emoji":"🧩","tokens_out":9024,"duration_ms":83202,"temperature":0.7,"pith_summary":"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.","feed_headline":"Sync by property equality makes rewrite systems compositional","feed_subtitle":"A semantics-preserving 'split' maps synchronized egalitarian systems to plain ones, so existing Maude engines still run.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Lays out rewriting logic, proof terms, and the concurrent rewriting model that the egalitarian systems adapt.","marker":"(Meseguer 1992)"},{"why":"Documents the Maude language, Full Maude, and model checker that motivate the split and remain the target for execution.","marker":"(Clavel et al. 2007)"},{"why":"Presents the earlier synchronous product of rewrite systems by rule-label coincidence that this paper generalizes to property-based synchronization.","marker":"(Martín et al. 2016b)"},{"why":"Introduces TLR* and the egalitarian state/transition perspective that motivates first-class transition terms and computability conditions.","marker":"(Meseguer 2008)"},{"why":"Supplies the topmostness notion and rule-completion results that justify the topmost requirement on plain composition.","marker":"(Meseguer and Thati 2007)"},{"why":"Provides the large alternating-bit-protocol example and parameterized-programming encapsulation that the present framework is designed to support.","marker":"(Martín et al. 2018)"}],"fun_headline_variants":["Composition and interpretation commute in rewriting","Sync then split: rewriting logic goes compositional","Split bridges compositional specs to plain rewrite systems","Egalitarian rewrite systems made compositional","Compositional rewriting: split then compose, same result"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Composition and interpretation commute in rewriting","Sync then split: rewriting logic goes compositional","Split bridges compositional specs to plain rewrite systems","Egalitarian rewrite systems made compositional","Compositional rewriting: split then compose, same result"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000733,"raw_usage":{"total_tokens":3226,"prompt_tokens":839,"completion_tokens":2387,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":455,"completion_tokens_details":{"reasoning_tokens":2320}},"tokens_in":455,"tokens_out":2387,"duration_ms":17019,"temperature":1.0,"reasoning_tokens":2320,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T10:07:40.942823+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}