Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems

Emma Ahrens; Jan-Christoph Kassing; Joost-Pieter Katoen; J\"urgen Giesl

REVIEW 2 major objections 3 minor 29 references

Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems

T0 review · 2 major / 3 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2505.08496 v1 pith:4BER5F6V submitted 2025-05-13 cs.LO

Emma Ahrens , Jan-Christoph Kassing , Jürgen Giesl , Joost-Pieter Katoen This is my paper · ORCID

classification cs.LO MSC 68Q4216Y60

keywords RewritingSemiringsSemanticsTerminationVerificationAbstractreductionsystemsProvenanceanalysisComplexity

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

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.

What carries the argument

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$.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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$.

Reading between the lines

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

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.

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.

Desk Editor's Note

read the 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.

What 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.

Real 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.

This 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.

Referee Report

2 major / 3 minor

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.

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 (2)

[Section 5.1, Theorem 25] 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 5.1, Theorem 25 (statement formatting)] 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.

minor comments (3)

[Appendix B, proof of Theorem 32] 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.
[Appendix A.1, Definition 45 discussion] 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.
[Appendix B, Lemma 46] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the derivation is self-contained; the only flagged issue is a correctness gap in Theorem 25, not a circular reduction.

full rationale

Every load-bearing theorem is proved from the definitions rather than assumed. Definition 14 defines JaK as a supremum over finite-depth reduction trees; Theorem 32's soundness is an induction using monotonicity of aggregators, and its completeness chooses e(a)=JaK and uses continuity, so the embedding conditions are not a restatement of boundedness. The expressivity examples in Sects. 4.1-4.5 are explicit encodings with specified fNF and Aggr functions, not fitted parameters, and the comparison to the authors' weighted-programming work [6] in Appendix A is illustrative only and does not support any central theorem. The one notable defect is Theorem 25 in Sect. 5.1, whose first clause states an 'iff' but is proved in Appendix B only in the 'if' direction and via a separate sufficient condition; that is a correctness error, not a circular reduction, so it leaves the circularity score at zero.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper introduces new formal objects, namely sequence ARSs, weighted ARSs, aggregators, and reduction trees, but these are explicitly defined constructions inside standard mathematics and not postulated entities with independent empirical consequences. There are no fitted free parameters; all parameters in examples are chosen inputs, not fitted values, and the central theorems are parameter-free.

assumptions (4)

domain assumption The semiring is naturally ordered and a complete lattice (Definition 7).
Used in Corollary 15 to guarantee that the supremum defining JaK exists; this restricts the framework to semirings such as extended naturals, extended reals, arctic and tropical semirings, and product semirings, while excluding ordinary (N,+,*).
domain assumption For the completeness direction of Theorem 32, addition and multiplication are continuous in the strong sense of Definition 30, preserving arbitrary suprema.
Explicitly stated before Theorem 32; this property is not needed for soundness, only for the 'only if' direction, and it is not satisfied by all complete lattice semirings such as confidence semiring multiplication.
domain assumption Theorem 29 assumes the sARS is terminating, finitely non-deterministic, and finitely branching, and the semiring has the extremal property.
These are sufficient conditions for boundedness; the proof relies on König's lemma to bound the number of finite reduction trees rooted at an object.
standard math Standard set-theoretic background: objects form a set, reduction relations are arbitrary, and König's lemma applies to finitely branching trees.
Used in the proof of Theorem 29 and in Lemma 47 to construct uncountably many reduction trees.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems." pith.science (2026). https://pith.science/paper/4BER5F6V

@misc{pith2026250508496,
  author       = {Pith},
  title        = {Pith review of: Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4BER5F6V}},
  note         = {Machine review of arXiv:2505.08496}
}

read the original abstract

We present novel semiring semantics for abstract reduction systems (ARSs). More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a semiring. Inspired by provenance analysis in database theory and logic, we obtain a formalism that can be used for provenance analysis of arbitrary ARSs. Our semantics handle (possibly unbounded) non-determinism and possibly infinite reductions. Moreover, we develop several techniques to prove upper and lower bounds on the weights resulting from our semantics, and show that in this way one obtains a uniform approach to analyze several different properties like termination, derivational complexity, space complexity, safety, as well as combinations of these properties.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 8 canonical work pages

[1]

Gabbay, and Tom S

Samson Abramsky, Dov M. Gabbay, and Tom S. E. Maibaum. Handbook of Logic in Computer Science. Volume 3. Semantic Structures . Clarendon Press, 1994. URL: https://global.oup.com/academic/product/handbook-of-logic-in-computer-science-9780198537625

work page 1994
[2]

On probabilistic term rewriting

Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Sci.\ Comput.\ Program. , 185, 2020. https://doi.org/10.1016/j.scico.2019.102338 doi:10.1016/j.scico.2019.102338

arXiv 2020
[3]

A modular cost analysis for probabilistic programs

Martin Avanzini, Georg Moser, and Michael Schaper. A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. , 4, 2020. https://doi.org/10.1145/3428240 doi:10.1145/3428240

doi:10.1145/3428240 2020
[4]

Term Rewriting and All That

Franz Baader and Tobias Nipkow. Term Rewriting and All That . Cambridge University Press, 1998. https://doi.org/10.1017/CBO9781139172752 doi:10.1017/CBO9781139172752

doi:10.1017/cbo9781139172752 1998
[5]

Principles of Model Checking

Christel Baier and Joost-Pieter Katoen. Principles of Model Checking . MIT Press, 2008

2008
[6]

Weighted programming: a programming paradigm for specifying mathematical models

Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost - Pieter Katoen, and Tobias Winkler. Weighted programming: a programming paradigm for specifying mathematical models. Proc. ACM Program. Lang. , 6( OOPSLA1 ):1--30, 2022. https://doi.org/10.1145/3527310 doi:10.1145/3527310

doi:10.1145/3527310 2022
[7]

Semiring programming: A semantic framework for generalized sum product problems

Vaishak Belle and Luc De Raedt . Semiring programming: A semantic framework for generalized sum product problems. International Journal of Approximate Reasoning , 126:181--201, 2020. https://doi.org/10.1016/j.ijar.2020.08.001 doi:10.1016/j.ijar.2020.08.001

work page doi:10.1016/j.ijar.2020.08.001 2020
[8]

Algorithms with polynomial interpretation termination proof

Guillaume Bonfante, Adam Cichon, Jean - Yves Marion, and H \' e l \` e ne Touzet. Algorithms with polynomial interpretation termination proof. J. Funct. Program. , 11(1):33--53, 2001. https://doi.org/10.1017/S0956796800003877 doi:10.1017/S0956796800003877

doi:10.1017/s0956796800003877 2001

Show all 29 references

[9]

Quasi-interpretations a way to control resources

Guillaume Bonfante, Jean - Yves Marion, and Jean - Yves Moyen. Quasi-interpretations a way to control resources. heor. Comput. Sci. , 412(25):2776--2796, 2011. https://doi.org/10.1016/j.tcs.2011.02.007 doi:10.1016/j.tcs.2011.02.007

2011 doi
[10]

Probabilistic rewrite strategies

Olivier Bournez and Claude Kirchner. Probabilistic rewrite strategies. Applications to ELAN . In Proc.\ RTA '02 , LNCS 2378, pages 252--266, 2002. https://doi.org/10.1007/3-540-45610-4_18 doi:10.1007/3-540-45610-4_18

2002 doi
[11]

Proving positive almost-sure termination

Olivier Bournez 1 and Florent Garnier. Proving positive almost-sure termination. In Proc.\ RTA '05 , LNCS 3467, pages 323--337, 2005. https://doi.org/10.1007/978-3-540-32033-3_24 doi:10.1007/978-3-540-32033-3_24

2005 doi
[12]

Semiring provenance in the infinite

Sophie Brinke, Erich Grädel, Lovro Mrkonjić, and Matthias Naaf. Semiring provenance in the infinite. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen , OASIcs 119, pages 3:1--3:26, 2024. https://doi.org/10.4230/OASIcs.Tannen.3 doi:10.4230/OASIcs.Tannen.3

2024 doi
[13]

Provenance in databases: Why, how, and where

James Cheney, Laura Chiticariu, and Wang Chiew Tan. Provenance in databases: Why, how, and where. Found. Trends Databases , 1(4):379--474, 2009. https://doi.org/10.1561/1900000006 doi:10.1561/1900000006

2009 doi
[14]

Dannert and Erich Grädel

Katrin M. Dannert and Erich Grädel. Provenance analysis: A perspective for description logics? In Description Logic , Theory Combination , and All That : Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday , LNCS 11560, pages 266--285, 2019. https://doi.org/1...

2019 doi
[15]

Handbook of Weighted Automata

Manfred Droste, Werner Kuich, and Heiko Vogler, editors. Handbook of Weighted Automata . Springer, 2009. https://doi.org/10.1007/978-3-642-01492-5 doi:10.1007/978-3-642-01492-5

2009 doi
[16]

Mechanizing and improving dependency pairs

Jürgen Giesl, Ren\' e Thiemann, Peter Schneider-Kamp, and Stephan Falke. Mechanizing and improving dependency pairs. Journal of Automated Reasoning , 37(3):155--203, 2006. https://doi.org/10.1007/s10817-006-9057-7 doi:10.1007/s10817-006-9057-7

2006 doi
[17]

The termination and complexity competition

J \" u rgen Giesl 4 , Albert Rubio, Christian Sternagel, Johannes Waldmann, and Akihisa Yamada. The termination and complexity competition. In Proc.\ TACAS '19 , LNCS 11429, pages 156--166, 2019. Website of TermComp: https://termination-portal.org/wiki/Termination_Competition....

2019 doi
[18]

Data provenance

Boris Glavic. Data provenance. Found. Trends Databases , 9(3-4):209--441, 2021. https://doi.org/10.1561/1900000068 doi:10.1561/1900000068

2021 doi
[19]

Green, Grigoris Karvounarakis, and Val Tannen

Todd J. Green, Grigoris Karvounarakis, and Val Tannen. Provenance semirings. In Proc.\ PODS '07 , pages 31--40, 2007. https://doi.org/10.1145/1265530.1265535 doi:10.1145/1265530.1265535

2007
[20]

Green and Val Tannen

Todd J. Green and Val Tannen. The semiring framework for database provenance. In Proc.\ PODS '17 , pages 93--99, 2017. https://doi.org/10.1145/3034786.3056125 doi:10.1145/3034786.3056125

2017
[21]

Termination proofs and the length of derivations

Dieter Hofbauer and Clemens Lautemann. Termination proofs and the length of derivations. In Proc.\ RTA '89 , volume LNCS 355, pages 167--177, 1989. https://doi.org/10.1007/3-540-51081-8_107 doi:10.1007/3-540-51081-8_107

1989 doi
[22]

Ngo, Reinhard Pichler, Dan Suciu, and Yisu Remy Wang

Mahmoud Abo Khamis, Hung Q. Ngo, Reinhard Pichler, Dan Suciu, and Yisu Remy Wang. Convergence of Datalog over (pre-) semirings. J. ACM , 71(2):8:1--8:55, 2024. https://doi.org/10.1145/3643027 doi:10.1145/3643027

2024 doi
[23]

Cost-size semantics for call-by-value higher-order rewriting

Cynthia Kop and Deivid Vale. Cost-size semantics for call-by-value higher-order rewriting. In Proc.\ FSCD '23 , LIPIcs 260, 2023. https://doi.org/10.4230/LIPIcs.FSCD.2023.15 doi:10.4230/LIPIcs.FSCD.2023.15

2023 doi
[24]

Weighted relational models of typed lambda-calculi

Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In Proc.\ LICS '13 , pages 301--310, 2013. https://doi.org/10.1109/LICS.2013.36 doi:10.1109/LICS.2013.36

2013 doi
[25]

Lankford

Dallas S. Lankford. On proving term rewriting systems are N oetherian. Memo mtp-3, math.\ dept.,, Louisiana Technical University, Ruston, LA, 1979. URL: http://www.ens-lyon.fr/LIP/REWRITING/TERMINATION/Lankford_Poly_Term.pdf

1979
[26]

Lankford

Dallas S. Lankford. On proving term rewriting systems are Noetherian . Technical Report Memo MTP-3, Department of Mathematics, Louisiana Technical University, 1979. URL: https://www.ens-lyon.fr/LIP/REWRITING/TERMINATION/Lankford_Poly_Term.pdf

1979
[27]

Complexity analysis for term rewriting by integer transition systems

Matthias Naaf, Florian Frohn, Marc Brockschmidt, Carsten Fuhs, and J \"u rgen Giesl. Complexity analysis for term rewriting by integer transition systems. In Proc.\ FroCoS '17 , LNCS 10483, pages 132--150, 2017. https://doi.org/10.1007/978-3-319-66167-4_8 doi:10.1007/978-3-319...

2017 doi
[28]

Kleene algebra with tests for weighted programs

Igor Sedl \' a r. Kleene algebra with tests for weighted programs. In In Proc.\ ISMVL '23 , pages 111--116, 2023. https://doi.org/10.1109/ISMVL57333.2023.00031 doi:10.1109/ISMVL57333.2023.00031

2023
[29]

Term Rewriting Systems , volume 55 of Cambridge Tracts in Theoretical Computer Science

Terese. Term Rewriting Systems , volume 55 of Cambridge Tracts in Theoretical Computer Science . Cambridge University Press, 2003

2003

Pith tools

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

[1] [1]

Gabbay, and Tom S

Samson Abramsky, Dov M. Gabbay, and Tom S. E. Maibaum. Handbook of Logic in Computer Science. Volume 3. Semantic Structures . Clarendon Press, 1994. URL: https://global.oup.com/academic/product/handbook-of-logic-in-computer-science-9780198537625

work page 1994

[2] [2]

On probabilistic term rewriting

Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Sci.\ Comput.\ Program. , 185, 2020. https://doi.org/10.1016/j.scico.2019.102338 doi:10.1016/j.scico.2019.102338

arXiv 2020

[3] [3]

A modular cost analysis for probabilistic programs

Martin Avanzini, Georg Moser, and Michael Schaper. A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. , 4, 2020. https://doi.org/10.1145/3428240 doi:10.1145/3428240

doi:10.1145/3428240 2020

[4] [4]

Term Rewriting and All That

Franz Baader and Tobias Nipkow. Term Rewriting and All That . Cambridge University Press, 1998. https://doi.org/10.1017/CBO9781139172752 doi:10.1017/CBO9781139172752

doi:10.1017/cbo9781139172752 1998

[5] [5]

Principles of Model Checking

Christel Baier and Joost-Pieter Katoen. Principles of Model Checking . MIT Press, 2008

2008

[6] [6]

Weighted programming: a programming paradigm for specifying mathematical models

Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost - Pieter Katoen, and Tobias Winkler. Weighted programming: a programming paradigm for specifying mathematical models. Proc. ACM Program. Lang. , 6( OOPSLA1 ):1--30, 2022. https://doi.org/10.1145/3527310 doi:10.1145/3527310

doi:10.1145/3527310 2022

[7] [7]

Semiring programming: A semantic framework for generalized sum product problems

Vaishak Belle and Luc De Raedt . Semiring programming: A semantic framework for generalized sum product problems. International Journal of Approximate Reasoning , 126:181--201, 2020. https://doi.org/10.1016/j.ijar.2020.08.001 doi:10.1016/j.ijar.2020.08.001

work page doi:10.1016/j.ijar.2020.08.001 2020

[8] [8]

Algorithms with polynomial interpretation termination proof

Guillaume Bonfante, Adam Cichon, Jean - Yves Marion, and H \' e l \` e ne Touzet. Algorithms with polynomial interpretation termination proof. J. Funct. Program. , 11(1):33--53, 2001. https://doi.org/10.1017/S0956796800003877 doi:10.1017/S0956796800003877

doi:10.1017/s0956796800003877 2001