Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.13201

Compact Quantitative Equational Theories as Monad Restrictions

Matteo Mio·Colin Riba
View original source ↗Read source document ↗Export metadata ↓

Abstract

Proofs in quantitative algebra are, generally, infinite objects due to the presence of infinitary rules in the deductive apparatus. A quantitative equational theory is called compact if all its consequences are derivable by means of finite proofs, that is, proofs not using any instances of the infinitary rules. This definition is purely logical. In this work we give an equivalent, but categorical, characterisation based on the notion of monad restriction.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Matteo Mio, Colin Riba. 2026-10-09. Compact Quantitative Equational Theories as Monad Restrictions. https://arxiv.org/abs/2610.13201

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Reasoning about Quality in Hyperproperties

Hyperproperties allow one to specify properties of systems that inherently involve not single executions of the system, but several of them at once: observational determinism and non-inference are two examples of such properties used to study the security of systems. Logics like HyperLTL have been studied in the past to model check hyperproperties of systems. However, most of the time, requiring strict security properties is actually ineffective as systems do not meet such requirements. To overcome this issue, we introduce qualitative reasoning in HyperLTL, inspired by a similar work on LTL by Almagor, Boker and Kupferman where a formula has a value in the interval [0, 1], obtained by considering either a propositional quality (how much the specification is satisfied), or a temporal quality (when the specification is satisfied). We show decidability of the approximated model checking problem, as well as the model checking of large fragments.

cs.LO↗
arXiv2026

Just Previsions

Previsions are positively homogeneous functionals, and are generalized forms of integration functionals. We investigate previsions -- just previsions, not sublinear or superlinear previsions as in previous work. We show that every prevision can be expressed as an infimum of sublinear previsions, and as a supremum of superlinear previsions under mild conditions. This extends to homeomorphisms between spaces of previsions and certain hyperspaces over spaces of sublinear or superlinear previsions, which can also be characterized in terms of orthogonality relations, making the construction a variant of a double powerspace construction.

cs.LO↗
arXiv2026

Solving VeriContest with a Lean-Backed Rust Verifier

VeriContest is a benchmark of 1007 competitive-programming problems in Rust, each with a Verus specification, a judge-accepted solution, and a Verus proof. Its authors report that proof generation is the bottleneck for frontier models: given the specification and the code, the best model produces an accepted Verus proof for 13.95% of the problems on the first attempt. We report on solving the same proof-generation task with Rust-Prover, a verifier for Rust backed by Lean 4. The Verus specification and the Rust code are restated and translated into Lean, each specification becomes a theorem, and agents prove the theorems with Lean's kernel as the final check. All 1325 theorems of all 1007 problems were proved. 1259 of them were proved in one run of under 32 hours on Claude Opus 5.5, at a median of 3.2 minutes and $1.17 per proof, and 70% of them on the first iteration. The restated specifications were checked against the benchmark's test suites, and reviewed where no suite applies. None was wrong or weakened. The translated Lean programs were run on 21,413 of the benchmark's test cases and produced the same output as the Rust programs on every one. Across four Claude and four GPT models at five reasoning-effort settings, every current frontier model proves nearly all of a ten-theorem sample at every setting, and more effort raises the cost without raising the number of proofs. The cheapest Claude setting, Sonnet 5.5 at low effort, proves all of the 50 hardest theorems. We also rerun the benchmark's own Verus protocol with Claude Opus 5.5 on the 50 problems with the longest reference proofs. Opus 5.5 alone fails to prove one of them.

cs.LO↗