{"id":"8af14654-ffd1-49a9-a945-7dca51f21ea6","arxiv_id":"2505.08496","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A single semiring-based semantics for abstract reduction systems unifies termination, complexity, safety, and probabilistic analysis of rewriting.","lead":"The paper introduces weighted abstract reduction systems, where every reduction step carries a semiring weight, and defines the weight of an object as the supremum of weights over all finite reduction trees. This creates one formalism that can express termination, derivational complexity, memory bounds, safety, and probabilistic almost-sure termination as special cases.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 25's claimed 'iff' is false: unboundedness can arise from an increasing loop with no normal form of weight ⊤, refuting a stated main result.","rationale":"The reader's verdict of ACCEPT with no load-bearing error misses a false theorem in the main results. The central framework (Definition 14, Theorem 32) may be salvageable, and the 'if' direction of Theorem 25 and Theorem 29 are sufficient and likely correct, so the paper's core unification claim is not disproven. However, a stated 'iff' characterizing boundedness is refuted by a simple wARS and by the paper's own Example 42. This moves the verdict to CONDITIONAL: the paper should be accepted only after Theorem 25 is corrected (e.g., by replacing the 'iff' with the true implication), and ideally after the authors check whether any downstream claims rely on the false direction. The remaining concerns, such as the nonstandard infinite product in Definition 8 and the need for finite non-determinism when reading boundedness as safety, are secondary and do not change this assessment.","tokens_in":26618,"tokens_out":26690,"duration_ms":287365,"concrete_test":"Instantiate the counterexample: A={a}, a s→[a], S=SN∞, Aggr_{a→[a]}=1+v1, fNF on empty NF→. Compute JaK = sup_{d∈N} d = ∞ = ⊤ via Definition 14; since NF→=∅, the condition 'fNF(a)=⊤ for some a∈NF→' is vacuously false. If this computation yields JaK=⊤, Theorem 25's 'only if' fails. The same check applies to Example 42's runtime wARS, where normal-form weight is 0 but Jidle(ε)K=∞.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Theorem 25 (Section 5.1) states: 'A wARS is not bounded iff fNF(a)=⊤ for some a∈NF→.' The 'only if' direction is false. Consider the wARS with A={a}, the only rule a→[a], S=SN∞, Aggr_{a→[a]}=1⊕v1, and fNF the empty function on NF→=∅. For every finite-depth tree of depth d, the weight is d, so by Definition 14 JaK=⊤, the wARS is not bounded, yet no normal form has weight ⊤. The paper itself contains this situation in Example 42, where the runtime wARS over the OS example has the single normal form run(ε) with fNF(run(ε))=0, but the loop idle(ε)→wait(ε)→idle(P1)→run(P1)→idle(ε) yields Jidle(ε)K=∞. Thus the theorem as stated is internally inconsistent with Theorem 41 and with Example 42. The proof in Appendix B only establishes the 'if' direction and the separate sufficient condition; it never proves the converse. Since boundedness is the central technical notion of the paper and Theorem 25 is listed as a main result, this is a load-bearing correctness error, not a typo. The fix is straightforward: the first clause should be only an implication, deleting the false converse.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper defines weighted abstract reduction systems (wARSs), in which a sequence abstract reduction system is equipped with a complete-lattice semiring, an interpretation of normal forms fNF, and an aggregator function for each reduction step. The weight JaK of an object is the least upper bound of the weights of all finite-depth reduction trees rooted at a. The authors show that this single formalism captures termination, derivational complexity, space consumption, safety, probabilistic almost-sure termination, formal-language semantics, and combinations of these properties via product semirings. The main technical contributions are sufficient conditions for boundedness (Theorems 25 and 29), a sound and, for continuous semirings, complete interpretation method for boundedness (Theorem 32), an approximation result for deterministic systems (Theorem 37), and a loop-based criterion for proving unboundedness (Theorem 41). An appendix gives all proofs and a comparison with weighted imperative programs.","tokens_in":26850,"tokens_out":6385,"duration_ms":72891,"significance":"The framework is clean and genuinely unifying: the definitions are self-contained, the central theorems are proved in Appendix B, and the paper is honest about its limitations, e.g., the impossibility of expressing best-case properties such as starvation freedom with the current supremum-based semantics (Section 4.6). The tuple-semiring examples show that the formalism yields combined safety-and-complexity analyses that are not obtainable by performing the two analyses separately. If the incorrect statement discussed below is corrected, the paper is a solid contribution to rewriting theory and semiring semantics. The soundness of the main framework does not depend on the faulty 'iff'; the affected theorem is a stated main result, however, so the correction must be made before publication.","major_comments":[{"comment":"The first clause of Theorem 25, stated as 'A wARS is not bounded iff fNF(a)=⊤ for some a∈NF→', is false in the 'only if' direction. Consider the wARS with A={a}, the only reduction a→[a], S=SN∞, aggregator Aggr_{a→[a]}=1⊕v1, and no normal forms. For the finite-depth reduction tree of depth d the root weight is d, so by Definition 14 we have JaK=⊤, yet no normal form has weight ⊤. The paper itself contains this situation: in Example 42 the runtime wARS over the operating-system example has the single normal form run(ε) with fNF(run(ε))=0, but the loop idle(ε)→wait(ε)→idle(P1)→run(P1)→idle(ε) yields Jidle(ε)K=∞. The proof in Appendix B proves only the 'if' direction and the separate sufficient condition with universally bounded fNF and selective aggregators; it does not prove the converse. This is a load-bearing correctness error in a listed main result and must be fixed. The first clause should be weakened to the implication: if fNF(a)=⊤ for some a∈NF→, then the wARS is not bounded; the converse does not hold in general.","section":"Section 5.1, Theorem 25"},{"comment":"Apart from the mathematical error, the display of Theorem 25 conflates two different statements: an 'iff' claim and a separate sufficient condition. The two clauses should be presented as distinct items so that it is clear the second is not the converse of the first. This is a presentation issue, but it likely contributed to the incorrect formulation of the first clause.","section":"Section 5.1, Theorem 25 (statement formatting)"}],"minor_comments":[{"comment":"In the proof of the 'only if' direction, the set in the equation for a∈NF→ is written as '{T | T∈ e(a)}'; this should be '{T | T∈ Φ(a)}'. The later use of 'Φ(a)⊆Φ(a)' for the set of trees whose first reduction is a→B is also confusing; introduce a separate name such as Φ_B(a) for this restricted set.","section":"Appendix B, proof of Theorem 32"},{"comment":"In the final paragraph of A.1 the text says 'Jδ0K = wp JSkiAlgK (1)(δ0) = n0⊕y = max{n0,y}'. Since the tropical semiring Strop has addition min, the last expression should be min{n0,y}, matching the earlier sentence in the same section. The current text is internally inconsistent.","section":"Appendix A.1, Definition 45 discussion"},{"comment":"The definitions of lb(T) and ub(T) both use 't≤t' with the same letter t for the quantified lower or upper bound. Use a distinct letter, e.g., 'l≤t for all t∈T' and 't≤u for all t∈T', to make the proof readable.","section":"Appendix B, Lemma 46"}],"recommendation":"major_revision","confidential_remarks":"The false 'iff' in Theorem 25 is the only substantive correctness problem I found. It is confined to the statement of that theorem and its proof does not support the converse; the other central theorems and the framework itself appear sound. Since the authors already prove the needed sufficient direction, the repair is local and should not require any change to the main semantic construction. I recommend major revision rather than rejection, provided the authors correct the theorem statement and adjust any downstream wording that refers to it as an equivalence."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"One thing to know up front: the stress-test note is a false alarm. It reads Theorem 25 as an iff and then refutes the converse. Theorem 25 is titled \"Sufficient Condition for Boundedness (1)\" and the proof proves exactly the two sufficient conditions listed. The text's \"iffNF(a)=...\" is a typesetting artifact for \"if fNF(a)=...\". The unbounded-loop example (Example 42) is consistent with the theorem as stated; it just shows the sufficient condition isn't necessary.\n\nWhat the paper actually does: it introduces weighted ARSs—sARS with aggregator functions over a complete-lattice semiring—and defines the weight of an object as a supremum over all finite-depth reduction trees. The semantics handle infinite reductions and unbounded nondeterminism because the semiring is complete. That's a clean and genuinely unifying framework: termination, derivational complexity, memory bounds, safety, formal-language semantics, and probabilistic almost-sure termination all become special cases. The interpretation method (Theorem 32) is the technical core; it gives sound boundedness, and completeness when the semiring operations are continuous. The loop-based unboundedness criterion (Theorem 41) is a genuine lower-bound tool. I went through the appendix proofs for the main theorems; they are honest and check out. The product-semiring examples (e.g., complexity + safety) show the framework does something you can't get by just running separate analyses. Citations are appropriate, including the self-citation to the weighted programming work; the appendix comparison is legitimate.\n\nReal soft spots, in proportion: the framework requires a naturally ordered semiring that is a complete lattice, so plain N with + and × needs a top element added. The authors say this up front, so it's not hidden. Example 19 uses a weight for an infinite tree that isn't formally defined by Definition 14 (which only handles finite depth); the authors should either extend the definition or mark that as informal. Minor typos exist. None of this touches the main theorems.\n\nThis is a theory paper, no tool support or machine-checked proofs, but the definitions are sharp and the examples illustrate the range well. The paper deserves a serious referee: I'd send it out, and I'd probably accept after minor revision. It's a useful reference for anyone working on rewriting semantics or unified verification.","headline":"A solid unifying framework for semiring semantics of rewriting; the supposedly false Theorem 25 is a misreading, and the paper's main results hold up.","tokens_in":27403,"tokens_out":4397,"would_cite":true,"duration_ms":39738,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q42","16Y60"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proposes one semiring semantics under which termination, derivational complexity, space bounds, safety, and their combinations are all instances of a single boundedness question.","keywords":["Rewriting","Semirings","Semantics","Termination","Verification","Abstract reduction systems","Provenance analysis","Complexity analysis"],"falsifier":"To test Theorem 32, one could search for a bounded wARS over a continuous complete lattice semiring that admits no embedding $e:A\\to S\\setminus\\{\\top\\}$ satisfying the two dominance inequalities; the theorem says none exists, so any such example would refute its claimed completeness.","tokens_in":26405,"feed_emoji":"🔁","tokens_out":11733,"duration_ms":107378,"temperature":0.7,"pith_summary":"This paper proposes one semantic framework, the weighted abstract reduction system (wARS), in which each reduction step of an abstract rewrite system carries a value from a complete lattice semiring. The weight of an object is the least upper bound, over all finite-depth reduction trees starting from it, of the aggregated weights of its possible reductions; the least upper bound makes the worst-case, demonic resolution of non-determinism explicit. The paper argues that termination, derivational complexity, space consumption, safety, expected runtime of probabilistic rewrite systems, formal-language behavior, and any Cartesian-product combination of these are all instances of one question: is the weight of every object below the semiring's top element? On that reading, the classical interpretation method for termination becomes a general boundedness technique, sound in all complete lattice semirings and complete when addition and multiplication are continuous. The payoff, if the unification holds, is that proof technology developed for one analysis transfers automatically to all the others.","feed_headline":"A single weight function unifies termination, complexity, and safety","feed_subtitle":"Give each step a semiring value: termination, runtime, memory, and safety become one boundedness question.","key_machinery":"The machinery is the weighted abstract reduction system (wARS): a sequence abstract reduction system (sARS), where a step sends one object to an ordered sequence of successors, paired with a complete lattice semiring $S$, an interpretation $f_{\\mathrm{NF}}$ of normal forms, and an aggregator $\\mathrm{Aggr}_{a\\to B}$ for each reduction rule. Aggregators are terms built from semiring constants, variables, $\\oplus$, and $\\odot$, so they compose child weights into a parent weight. Weight is then defined demonically as $\\llbracket a \\rrbracket = \\bigsqcup\\{\\llbracket T \\rrbracket \\mid T\\in\\Phi(a)\\}$, the least upper bound over all finite-depth reduction trees rooted at $a$; the completeness of the lattice is what makes this supremum well defined even for unbounded non-determinism and infinite reductions. On top of this definition, Theorem 32 supplies the main proof technique: an embedding $e$ that dominates the normal-form interpretation and every aggregator instance is a global upper bound on $\\llbracket a \\rrbracket$.","core_discovery":"The paper's central claim is that the weight $\\llbracket a \\rrbracket$ of an object, defined as $\\bigsqcup\\{\\llbracket T \\rrbracket \\mid T\\in\\Phi(a)\\}$, is the right generalization of both termination and complexity measures: depending on the semiring, the interpretation of normal forms, and the aggregators, boundedness of $\\llbracket a \\rrbracket$ means termination, a derivational complexity bound, a space bound, safety along every run, or a combination of these. Its main theorem is the embedding characterization: if there is an embedding $e:A\\to S\\setminus\\{\\top\\}$ with $e(a)\\succeq f_{\\mathrm{NF}}(a)$ for normal forms and $e(a)\\succeq \\mathrm{Aggr}_{a\\to B}[e(b)\\mid b\\in B]$ for every reduction, then $e(a)\\succeq \\llbracket a \\rrbracket$ for all $a$; conversely, when the semiring operations are continuous, any bounded wARS admits such an embedding. This turns the interpretation method for termination into a sound, and under continuity complete, method for proving boundedness in any semiring instance. The paper also establishes sufficient conditions for boundedness from local properties, a monotone depth-truncation approximation for deterministic systems, and an increasing-loop criterion that certifies unboundedness.","pith_inferences":["Because the semantics is worst-case, a companion best-case or angelic semantics would be required for liveness properties such as starvation freedom; the paper explicitly identifies this as future work.","The completeness of the embedding criterion is tied to continuity of $\\oplus$ and $\\odot$; if non-continuous complete lattice semirings matter in applications, boundedness may hold there without a local certificate, so automation would need different witnesses.","One can read $\\llbracket a \\rrbracket$ as a provenance value: it records, in semiring-weighted form, why and how an object reduces, so provenance-style explanation questions from databases may transfer to rewrite systems.","Existing termination proof search strategies, such as those based on well-founded orders and path orderings, might be re-targeted to search for embeddings $e$ in arbitrary semirings; the paper sketches SMT-based automation but does not develop it."],"forward_implications":["Termination of a finitely non-deterministic ARS is equivalent to $\\llbracket a \\rrbracket < \\infty$ in the counting semiring $\\mathbb{N}_\\infty$, so termination proofs become boundedness proofs in a single framework.","The interpretation method transfers across properties: one embedding certificate can prove a derivational complexity bound, a memory bound, or a safety property, depending on the semiring in use.","Product semirings let a single proof establish combined properties, such as 'every run either terminates or stays safe', which separate analyses cannot prove because they enforce the quantifiers independently.","For probabilistic rewrite systems, boundedness in $\\mathbb{R}_\\infty$ with the right aggregators witnesses positive and strong almost-sure termination, as well as finite expected derivational complexity.","Unboundedness can be certified uniformly by increasing loops: a loop whose induced weight polynomial grows by a fixed $t$ with $\\bigoplus_{i=1}^\\infty t = \\top$ forces $\\llbracket a \\rrbracket = \\top$."],"supporting_citations":[{"why":"Supplies the semiring-provenance paradigm that the paper lifts from database provenance to abstract reduction systems.","marker":"[19]"},{"why":"Provides the interpretation method for proving termination that Theorem 32 generalizes to boundedness in arbitrary semirings.","marker":"[26]"},{"why":"Provides the probabilistic abstract reduction systems and expected-complexity concepts behind the PAST and SAST examples.","marker":"[2]"},{"why":"Gives the weighted imperative programming semantics whose weakest preweightings the paper shows are expressible as a wARS instance.","marker":"[6]"},{"why":"Justifies the infinite sums and products over complete lattice semirings used in aggregators and in the increasing-loop theorem.","marker":"[12]"},{"why":"Supplies the standard definitions of abstract reduction systems, rewrite rules, and termination used throughout the paper.","marker":"[4]"},{"why":"Provides the term rewriting background and standard interpretation-based termination techniques that the paper extends.","marker":"[29]"}],"fun_headline_variants":["Semiring weights unify termination, complexity, and safety","One weight function for termination, runtime, memory, and safety","Weighted rewriting: a single semiring measures all reduction properties","Semiring semantics turn boundedness into termination, complexity, and safety"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the semiring's natural order is a complete lattice, so the supremum in the definition of $\\llbracket a \\rrbracket$ exists for every set of finite reduction trees; without such arbitrary suprema, the weight of an object is not defined for ordinary semirings like the natural numbers.","fun_headline_variants_meta":{"raw":{"variants":["Semiring weights unify termination, complexity, and safety","One weight function for termination, runtime, memory, and safety","Weighted rewriting: a single semiring measures all reduction properties","Semiring semantics turn boundedness into termination, complexity, and safety"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000536,"raw_usage":{"total_tokens":2572,"prompt_tokens":942,"completion_tokens":1630,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":558,"completion_tokens_details":{"reasoning_tokens":1559}},"tokens_in":558,"tokens_out":1630,"duration_ms":12075,"temperature":1.0,"reasoning_tokens":1559,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T21:54:41.855125+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"To test Theorem 32, one could search for a bounded wARS over a continuous complete lattice semiring that admits no embedding $e:A\\to S\\setminus\\{\\top\\}$ satisfying the two dominance inequalities; the theorem says none exists, so any such example would refute its claimed completeness.","supporting_citations":[{"cited_title":"Lankford","cited_arxiv_id":null,"evidence_quote":"Provides the interpretation method for proving termination that Theorem 32 generalizes to boundedness in arbitrary semirings."},{"cited_title":"Semiring provenance in the infinite","cited_arxiv_id":null,"evidence_quote":"Justifies the infinite sums and products over complete lattice semirings used in aggregators and in the increasing-loop theorem."},{"cited_title":"Term Rewriting Systems , volume 55 of Cambridge Tracts in Theoretical Computer Science","cited_arxiv_id":null,"evidence_quote":"Provides the term rewriting background and standard interpretation-based termination techniques that the paper extends."}],"review_version":1}