arXiv weekly literature review

Proof Assistants and Automated Reasoning · primary corpus · published 2026-11-02T09:45:31Z
Jiaxin Xie, Guowei Dou, Xiang Ji, Wensheng Yu
arXiv categories: cs.LO, cs.AI

Mathematical formalization plays an important role in establishing rigorous and machine-verifiable foundations for mathematical reasoning. With the development of large language models (LLMs) and interactive theorem provers, intelligent agents offer a promising approach to automating the formalization of mathematical theories. This paper presents the Math Foundation Formalization Agent (MFF-Agent), a general-purpose intelligent agent designed to support formalization tasks across multiple mathematical domains. The agent integrates the reasoning capabilities of large language models with the formal verification capabilities of the Rocq proof assistant. It incorporates task classification, tool-assisted execution, verification feedback, and state-based task management to support the generation, refinement, and verification of formal proofs. Unlike an approach focused on a single mathematical theory, the agent is examined through case studies involving Morse--Kelley axiomatic set theory (MK), real numbers, propositional logic, and equivalences of the axiom of choice. These cases investigate its applicability across mathematical foundations and distinguish source-level completion, interactive verification, and reproducible compilation. The results demonstrate the feasibility of a unified operational framework for heterogeneous foundation-level tasks and clarify the gap between such a framework and a fully integrated mathematical foundation.

arXiv abstract · PDF

Proof Assistants and Automated Reasoning · primary corpus · published 2026-11-02T09:51:18Z
Qian Cheng, Ruize Tang, Saad Mohammad Rafid Pial, Zhizhen Cathy Cai, Yiming Su, Jackson Clark, Munim Thahmid, Mahdiya Rahman Sukanya, Chris Newcombe, Igor Konnov, Stephan Merz, Xudong Sun, Murat Demirbas, Yu Huang, Markus Alexander Kuppe, Tianyin Xu
arXiv categories: cs.AI, cs.DC, cs.LO, cs.SE

TLAPS-Bench is a benchmark and execution harness for constructing machine-checked proofs for real-world system specifications in TLA+ with agentic AI. Proving correctness of complex system specifications requires discovering inductive invariants, reasoning about intricate state transitions, and decomposing proofs into tractable obligations. TLAPS-Bench provides a proof harness that supports iterative proof development atop the TLA+ Proof System (TLAPS), where agents are equipped with proof tools and libraries, with safeguards against reward hacking. Using the harness, we have employed AI agents to prove desired properties for important system specifications that were not proved before, spanning cache coherence, Byzantine consensus, and write-ahead logs. TLAPS-Bench contains 265 proof targets (each encodes a property to prove) from 95 TLA+ specifications of real-world systems. We evaluated frontier AI agents, represented by Codex with GPT models, on a subset of 70 proof targets across 12 specifications. The highest-scoring model, GPT-6.1 Sol (max), proved 31 (44.3%) proof targets. The results show challenges and opportunities in end-to-end proof development.

arXiv abstract · PDF

Proof Assistants and Automated Reasoning · primary corpus · published 2026-11-03T07:25:42Z
Mostafa 'Neo' Mohsenvand
arXiv categories: cs.LG, cs.CL, cs.LO

Language models are accurate on most long-arithmetic problems, but their accuracy is estimated on samples and carries no guarantee for an unseen input; tool use is exact but moves the computation outside the network. We show that exactness at all input lengths becomes a finite, checkable property of a network when each of its steps reads only a bounded view of an external working memory. In Sketchpad, Qwen3.5-0.8B with a low-rank adapter executes arithmetic procedures on a rendered sheet. Each forward pass reads a three-cell view and emits one step: a digit, a carry or borrow, and the next operation. A fixed runtime moves the view and writes no digit of a result. We prove in Lean that the model is then exact on all inputs of any length if and only if it is exact on the finite set of views the runtime presents, that no finite test suffices when steps also read earlier steps, and that the guarantee tolerates bounded numerical perturbation and extends to compositions of procedures. All 2,446 views pass on the deployment device, a laptop GPU running the model in a web browser. The certified model performs signed addition and subtraction, long multiplication and division, square roots and greatest common divisors at arbitrary length. It solved 200 of 200 pre-registered problems in the browser, and 220 of 220 sums of up to 1,000 digits and products of up to 20 digits, of which GPT-6.1 Sol, the strongest of ten other models, solved 217. A symbolic runtime built on these procedures solves, expands and factors polynomials with every number computed by the model, and a multiplicative gate on the adapter recovers the base model exactly when the sheet is not in use.

arXiv abstract · PDF

Proof Assistants and Automated Reasoning · primary corpus · published 2026-11-03T19:32:16Z
Yutaka Nagashima
arXiv categories: cs.SE, cs.LO

Recent advances in AI-assisted proof automation are extending the use of proof assistants in software verification and mathematics. However, greater proof automation does not remove users' responsibility to assess whether formal statements capture their intended requirements, making education in formal specification and reasoning essential. To lower the installation and learning barriers associated with mature proof assistants, we present ProofStudio, a browser-based environment integrating Isabelle/HOL, Lean, Rocq, HOL4, and HOL Light with corresponding worked examples, preconfigured proof search, and contextual AI assistance. With ProofStudio, users can explore formal specifications and proofs across five systems without local installation, inspecting native prover feedback and experimenting with automation through a common interface.

arXiv abstract · PDF

Proof Assistants and Automated Reasoning · primary corpus · published 2026-11-03T20:56:53Z
Jesse Comer, Fangzhu Shen, Shuo Zhang, Mayur Naik, Sudeepa Roy, Val Tannen
arXiv categories: cs.DB, cs.AI, cs.LO

We present the Whiel (a contraction of Whi(le-R)el) system for Lean-certified reasoning about imperative relational programs. The system can encode containment and equivalence problems for Datalog, its extensions with negation, and the core fragment of graph query languages. It can also represent optimized or incremental evaluation algorithms that are not expressible in the original query language, as well as first-order specifications of integrity constraints, schema mappings, and views arising in data integration, exchange, and sharing. Whiel's program states are database instances, and its imperative structure enables compositional Hoare-style reasoning with first-order relational specifications, using prophecy variables and leveled invariants to support inductive arguments. Whiel supports neurosymbolic discovery of loop invariants whose verification conditions can be checked using the Vampire first-order theorem prover. Counterexamples are fed back into the neurosymbolic pipeline, while proposed solutions are translated into Lean proof certificates. To validate the Whiel system, we evaluate its performance on a curated benchmark suite. In summary, we envision the Whiel system as a tool for tackling mathematically demanding, typically undecidable problems involving complex query and constraint languages, with a high degree of trust in its output.

arXiv abstract · PDF

Proof Assistants and Automated Reasoning · primary corpus · published 2026-11-03T21:56:52Z
Amar Shah, Benjamin F. Jones, Can Cebeci, Jason Z. S. Hu, Lee A. Barnett, R\'emi Delmas, Marijn Heule, Bryan Parno, Bruno Dutertre
arXiv categories: cs.LO

We present Sundance, an SMT solver for program verification written in about 13,600 lines of Rust. Sundance combines the Cadical SAT solver with congruence closure, linear arithmetic, algebraic datatypes, and pattern-based quantifier instantiation. Sundance produces eDRAT proofs for every unsat answer. On 21,531 queries from Verus, Dafny, and F*, Sundance is comparable to existing solvers, with 26--38 times fewer lines of code than Z3 and cvc5. We further show that its components can be swapped for Z3's arithmetic solver, MiniSat, and the Semper e-graph. We have open sourced Sundance.

arXiv abstract · PDF

Proof Assistants and Automated Reasoning · cs.SE candidate · published 2026-11-04T22:34:57Z
\'Alvaro F. Silva, Martim Afonso, Nuno Saavedra, Emily First, Alexandra Mendes, Jo\~ao F. Ferreira
arXiv categories: cs.SE, cs.AI

Coding agents achieve high success rates on existing benchmarks for Verus, a verifier for Rust programs. These benchmarks typically provide the auxiliary lemmas needed to complete a proof. In practice, however, such lemmas must be discovered and proved. To capture this challenge, we present SEVERUS, a context-aware technique to generate Verus benchmarks that organizes verification tasks into quests, each divided into levelsin a gamified manner. Using the original proof dependencies in verified projects, SEVERUS constructs one quest per verification target and progressively removes proof context to create individual levels. These levels range from the easiest, requiring completing only a single missing lemma, to the hardest, requiring proving the target without any supporting lemmas. An independent checker rejects changes to executable code, weakened specifications, and unsound proof constructs. A noisy binary search estimates the highest level that an agent can solve reliably. Applied to six open-source Verus projects, SEVERUS generates 819 quests comprising 10,095 levels. Experiments with Codex using GPT-6 Sol and GPT-6 Luna, and with Claude Code using Sonnet 4.6, show that success decreases and cost increases as proof context is withdrawn. The strongest agent solves the final level of 52 of 60 sampled quests, yet can only reliably solve 35% of their levels, with failures concentrated in longer quests. Successful GPT-6 Sol proofs rarely reproduce the withheld lemmas, instead, using alternative proof decompositions. By systematically varying proof context, SEVERUS provides a foundation for constructing verification benchmarks that can continue to challenge increasingly capable coding agents.

arXiv abstract · PDF

Proof Assistants and Automated Reasoning · primary corpus · published 2026-11-05T12:43:10Z
Wyatt Benno (ICME Labs), Alberto Centelles (Imperial College London), Aman Goel (Amazon Web Services), Benjamin Kiesl-Reiter (Amazon Web Services)
arXiv categories: cs.CR, cs.AI, cs.CL, cs.LO

Autonomous agents increasingly execute consequential actions on behalf of users, but ordinary middleware guardrails do not provide cryptographic proof that a policy was actually enforced. Their verdicts leave counterparties dependent on the operator unless they repeat the checks themselves, potentially exposing sensitive policies and inputs. We present zkARc, a modular proof-carrying framework that wraps each stage of Automated Reasoning checks (ARc) in an independent, succinctly verifiable zero-knowledge proof. ARc is a neurosymbolic system that translates natural language policies into formal logic and verifies AI-generated content against them using SMT solvers. zkARc certifies the planner's output, the policy's formalization, the action's formalization and both solver queries. The receipt binds these computations to the exact action received and, under the stated assumptions, reveals no additional information about private policies and intermediate model values beyond the declared public information and verdict. This lets a third party check the claimed policy enforcement without re-running the pipeline or trusting the operator. We prove completeness, knowledge soundness and zero knowledge for the composed receipt under explicit assumptions. An implementation on Qwen2-0.5B enforces a spending policy end to end, approving two purchases and denying a third. A full receipt, which also proves model inference, takes about an hour to issue with CPU-only proving and verifies in under a minute, and the solver proof alone is 88 KiB and verifies in 0.3 seconds.

arXiv abstract · PDF

Proof Assistants and Automated Reasoning · primary corpus · published 2026-11-06T08:08:59Z
Guowei Dou, Wensheng Yu
arXiv categories: math.LO

This paper presents a formalization for a theory of constructing real numbers using concepts related to filters. The formalization is implemented using the Coq proof assistant and is grounded in axiomatic set theory. The theory encompasses various notions such as filters, ultrafilters, principal ultrafilters, and arithmetical ultrafilters. A special filter, namely the non-principal arithmetical ultrafilter, whose existence requires the Continuum Hypothesis to be proven, is employed to establish several non-standard number sets: *N, *Z and *Q. The set of real numbers, R, is subsequently derived by equivalently classifying a specific subset of *Q. The entire theory is thoroughly formalized, with each detail verified to ensure rigor and precision. This work contributes a new selection of foundational materials for the formalization of mathematical theories.

arXiv abstract · PDF

Proof Assistants and Automated Reasoning · primary corpus · published 2026-11-06T17:10:40Z
Jinho Kang, Jinsook Kim
arXiv categories: cs.LG, cs.AI, cs.CR, cs.LO

OpenAI's agents breached Hugging Face in July 2026, and the same company released more than seven hundred AI-generated manuscripts of mathematical proofs in October 2026. The first event is read as a failure in security, while the second is read as a success in mathematics. We read both through the hybrid framework of our paper (Kim and Kang, 2026, arXiv:2611.01914), in which coding, proving, and learning from data are derivations by one and the same deductive mechanism, distinguished by the kinds of premises from which they are derived. Under this framework, the AI systems behind the two events ran the same loop, in which a statistical proposer produces candidate exploits or proofs and a deductive verifier settles each one by a derivation. What separates the events is the logical form of the statement wanted by each of the two domains, security and mathematics. The safety of a program is a $\Pi_1$ statement, for it says that no exploit exists, which is not assured by any finite list of tests that have been passed by the program. By contrast, the provability of a sentence is a $\Sigma_1$ statement, for it says that a proof exists, which is assured by a single instance, namely a proof that has been checked by the deductive verifier. The theorem behind both is Turing's Undecidability Theorem: the halting set is $\Sigma_1$ but not decidable, so its complement is $\Pi_1$ and not $\Sigma_1$, which is to say that membership has a finite witness but non-membership has none. We prove that attaching a statistical proposer to a deductive verifier does not change this undecidability result, however good the proposer is. We then discuss what does assure safety and where the residual risk goes.

arXiv abstract · PDF

Proof Assistants and Automated Reasoning · primary corpus · published 2026-11-06T18:08:06Z
Sergey Shirobokov, Ben Jaderberg, Katerina Hristova, George Tsoukalas, Johannes Bausch, Eric Wieser, Francisco J. H. Heras, Nicholas C. Rubin, Guang Hao Low, S\'ebastien Racani\`ere, Nenad Toma\v{s}ev, Lei M. Zhang, James D. Watson, Tanuj Khattar, Aws Albarghouthi, Stavan Jain, Harun Khan, Leopoldo Sarra, Andrew W. Senior, Michael Broughton, Hussain Masoom, Sergio Boixo, Ryan Babbush, Swarat Chaudhuri, Pushmeet Kohli
arXiv categories: quant-ph, cs.AI, cs.PL

The timeline by which quantum computers can solve breakthrough problems in science depends on improved quantum algorithms as much as on better hardware. Such algorithmic advances are typically achieved through many years of expert human collaboration. In mathematics and computer science, large language models have accelerated progress through automated discovery loops. However, quantum algorithms can only be evaluated by classical computers on restricted or small instances. Here we demonstrate automated discovery of quantum programs beyond these regimes including order-of-magnitude improvements on scientific applications. To achieve this, we build a quantum program library in the Lean theorem prover in which Gemini 4 agents synthesize novel programs against formal problem specifications and verify their correctness and cost. Agent teams collaborate, sharing results and knowledge through wikis and discussing ideas at organized conferences. Our results improve on prior baselines for parallel search (up to 2.55x), quantum arithmetic (290x), and simulations relevant to fusion, photochemistry and drug-metabolism by 11x, 8x and 2.5x respectively. Combining human and artificial intelligence at scale, under the rigor of mathematical proof, lets researchers design algorithms that today's classical and quantum computers cannot test, shortening the path to practical quantum computation.

arXiv abstract · PDF

Proof Assistants and Automated Reasoning · primary corpus · published 2026-11-08T21:54:58Z
Volkan Da\u{g}l{\i}, Zerrin Da\u{g}l{\i}, Da\u{g}han Da\u{g}l{\i}, Emrah Yurtseven, Murat Emre \"Ozkaya
arXiv categories: cs.LO, cs.SC, math.CV, math.DS

We embed the Syracuse operator $T(n) = n/2$ (even $n$), $T(n) = (3n+1)/2$ (odd $n$) and the Collatz map $C(n)$ into $\mathbb{C}$ via entire functions of exponential type $\pi$: $f(z) = \frac{1}{4}(1 + 4z - (1 + 2z)\cos(\pi z))$ and $F(z) = \frac{1}{4}(2 + 7z - (2 + 5z)\cos(\pi z))$. We prove five results: (1) every integer periodic cycle $C \subset \mathbb{N}^+$ of $T$ is a strictly attracting Fatou cycle of $f$ with multiplier $\mu_f(C) = 3^{N_{\mathrm{odd}}}/2^N = \prod_{n \in C\text{ odd}} \frac{3n}{3n+1} \in (0,1)$, and $\mu_f(O_{1,2}) = \mu_F(O_{1,4,2}) = 3/4 < 1$; (2) on the Fatou basin $B(O_{1,2})$, $g = f^{\circ 2}$ conjugates to $\Phi_j(g(z)) = \frac{3}{4}\Phi_j(z)$ with Koenigs Taylor jets $c_2(1) = -\frac{13}{2}\pi^2$ and $d_2(2) = -\frac{9}{2}\pi^2$; (3) the Schwarzian derivative is strictly negative on $\mathbb{Z}$ ($S(f)(n) \le 3\pi^2 - \frac{3}{8}\pi^4 \approx -6.9196 < 0$), and a repelling Julia 2-cycle $O_{\mathrm{rep}} \subset J(f)$ ($\mu \approx 1.2148 > 1$) isolates $B(O_{1,2})$; (4) on $(\mathbb{Z}_2, \mu_{\mathrm{Haar}})$, the 2-adic Lyapunov exponent $\lambda_{\mathrm{Haar}} = \frac{1}{2}\ln(3/4) \approx -0.143841 < 0$ equals $\frac{1}{2}\ln|\mu_f(O_{1,2})|$; and (5) we certify 20 theorems in Lean 4 (anc/CollatzAttractor.lean, 0 sorry). These results establish local Fatou invariants and 2-adic ergodic averages for $f(z)$, leaving open whether every $n_0 \in \mathbb{N}^+$ lies in $\bigcup_{k \ge 0} f^{-k}(B(O_{1,2}))$.

arXiv abstract · PDF

Program Specification and Verification Methods · primary corpus · published 2026-11-02T11:39:14Z
Krishna Manoorkar, Wolfgang Poiger
arXiv categories: cs.LO, math.LO

We introduce $\mathbb{N}\mathtt{PDL}$, a resource-aware variant of Propositional Dynamic Logic ($\mathtt{PDL}$) capable of accounting for program costs measured by natural numbers (such as time or space in the sense of computability theory). In this framework, programs correspond to transition systems weighted by extended natural numbers, and the syntax of our logic includes formulas expressing which properties are reachable by program executions within specific cost constraints. First, we explain how the standard program constructs of non-deterministic choice, sequential composition, iteration, and tests are interpreted in this weighted setting and establish the validity of their corresponding reduction axioms. Using an appropriate adaptation of the (Fischer-Ladner) filtration technique, we proceed to prove decidability and completeness for $\mathbb{N}\mathtt{PDL}$ as our main results. We furthermore provide upper and lower complexity bounds for this logic using translations between standard $\mathtt{PDL}$ and $\mathbb{N}\mathtt{PDL}$.

arXiv abstract · PDF

Program Specification and Verification Methods · cs.SE candidate · published 2026-11-03T18:40:25Z
Yang Song
arXiv categories: cs.SE

Enterprise teams that deploy large language model (LLM) agents inherit a maintenance problem that traditional testing does not address. The model is non-deterministic, but the larger risk is that most of what changes an agent's behavior (a retired model version, a revised policy, an upstream schema change, a prompt edit meant to fix one case) originates outside the owning team and is discovered as a production defect rather than caught as a regression. This paper presents Agentic Behavior Engineering (ABE), a platform-agnostic methodology that treats observable agent behavior, rather than the prompt or the model, as the version-controlled engineering artifact. ABE adapts Design by Contract to non-deterministic systems. A specification-only behavior contract with stable rule identifiers states what the agent must do, must not do, and when it must abstain for lack of evidence; a lightweight scenario library turns each rule into concrete situations; and every engineering artifact (tests, runtime policies, telemetry) references the contract in one direction only, so that specification and implementation can change independently without drifting apart. The method organizes the work into five responsibilities (Specify, Ground, Control, Verify, Observe), treats missing evidence and a verified negative as different things, enforces authority outside the model, gates releases on per-scenario pass^k reliability rather than aggregate accuracy, and classifies every production run against the contract so that each finding routes to the asset that must change. We illustrate the method with an executable capacity-allocation boundary suite and a constructed worked example of a product-review approval workflow.

arXiv abstract · PDF

Program Specification and Verification Methods · primary corpus · published 2026-11-03T22:23:55Z
Suraaj Kanniwadi, Andrew C. Myers
arXiv categories: cs.PL, cs.CR

The real--ideal paradigm, an approach to security specification developed in the cryptography community, has the benefit that it can express sophisticated confidentiality and integrity requirements, even for decentralized systems. We show that this paradigm is the basis for a powerful and intuitive new semantic framework for language-based security. Our new framework cleanly and extensionally captures existing security definitions, including not only noninterference but also less understood information flow properties that involve downgrading, such as robust declassification and nonmalleable information flow. Past semantics for these properties have relied on intensional downgrading events. Further, we show that all of these properties can be enforced by a practical information-flow type system for a while-language that supports downgrading. Surprisingly, correctness of this type system is also characterized as a real--ideal simulation, with an important implication: the security of heterogeneous, decentralized systems with a strong (real) attacker can be understood by reasoning about a weak (ideal) attacker whose power is restricted to interaction with downgrading. This result explains the usefulness of nonmalleable information flow and related security properties. The results are fully formalized using the Rocq prover and are publicly available.

arXiv abstract · PDF

Program Specification and Verification Methods · primary corpus · published 2026-11-04T09:23:41Z
Daniel G\u{a}in\u{a}, Adri\'{a}n Riesco, Ionu\c{t} \c{T}u\c{t}u
arXiv categories: cs.LO

Transition Algebra can be viewed as an extension of many-sorted first-order logic by borrowing essential features from dynamic logic. This leads us to new, more expressive sentences that include transitions labelled with actions, which are built from terms using union, composition, and iteration operators. We define a suitable notion of Horn clause, develop a system of proof rules for reasoning about clauses, and subsequently show that the proof system is sound and complete. We then introduce a rewriting relation based on Horn clauses, capturing transitions along established paths expressed as actions. This rewriting relation is naturally extended to a narrowing procedure for solving queries, thereby laying foundation for logic programming in Transition Algebra. As usual, soundness for both rewriting and narrowing is straightforward, whereas completeness requires additional conditions. Finally, we provide a prototype tool that demonstrates the practical aspects and shows the effectiveness of the proposed method.

arXiv abstract · PDF

Program Specification and Verification Methods · cs.SE candidate · published 2026-11-04T19:04:09Z
Heba Jaradat, Mohammed-Khalil Ghali, Saurabh Kulkarni, Rohan Kulkarni, Sangwon Yoon
arXiv categories: cs.SE

Diagnostic Signal Reachability (DSR) captures whether board-level health signals are observable by management controllers, including baseboard management controllers (BMCs), complex programmable logic devices (CPLDs), and other smart controllers. Verifying DSR is essential for field diagnosability in datacenter fleets, where one design is deployed at massive scale, yet it remains largely manual, since each signal is traced by hand across schematic sheets, renamed nets, series components, and monitoring devices. Large language models (LLMs) are attractive but unreliable at structural connectivity reasoning, where over-claiming can silently hide a rare coverage gap. We present NetFlow-DSR, a neuro-symbolic framework in which an LLM orchestrates the DSR pipeline and resolves device roles mainly from part-name families and library pin names, consulting specifications only for ambiguous parts. Pin directionality is read from the design library, and deterministic graph engines verify connectivity over the authoritative netlist. The pipeline detects diagnostic nets, canonicalizes renamed net fragments, and performs controller-seeded, power-aware breadth-first search over an admissibility graph that credits device-mediated monitoring. Each verdict carries an auditable trace card whose proof path is the witness. Across five production boards from an AI platform, covering 421 expert-graded signals, a three-stage ablation improves pooled F1 from 0.578 to 0.944. Because a monitored verdict is emitted only with a proof path, the verifier is sound by construction, and precision and specificity were 100% in the evaluated data. In a cross-model study on the system-controller module, precision remained 100% across three LLMs while recall tracked each model's device-semantic extraction. Precision therefore depends on the netlist-grounded verifier and correct device semantics rather than on any single LLM.

arXiv abstract · PDF

Program Specification and Verification Methods · cs.SE candidate · published 2026-11-04T21:53:08Z
Paolo Modesti
arXiv categories: cs.CR, cs.SE

Global surveillance systems record large volumes of network traffic for retrospective analysis, but packet captures alone reveal little about protocol-level semantics. This paper presents an automated, specification-guided methodology for reconstructing passive Dolev-Yao intruder executions from captured network traffic and validating the reconstructed executions against a formal protocol specification. The framework takes a PCAP capture, an AnBx specification, and the associated deployment metadata; it extracts Java-serialised objects from TCP streams, reconstructs protocol sessions and channel-to-step assignments, and generates a passive intruder that evaluates the Dolev-Yao derived checks produced by the AnBx compiler. Three reconstruction challenges are addressed: multiple serialised objects and object references within a TCP stream, ambiguity in mapping interleaved connections to concurrent protocol sessions, and semantic validation of candidate reconstructions. We evaluate the methodology on 121 protocols from the AnBx test suite. For single-session captures, the standard JDK cryptographic provider recovers 97.8% of expected objects and achieves 94.2% successful reconstruction, where success requires complete object recovery and a clean passive-intruder execution. For the 112 parallel-capable protocols, the toolchain achieves 89.3% successful reconstruction for both two and three concurrent sessions, while recovering approximately 97.2% of expected objects. Experiments with mismatched protocol-role mappings and deliberately mutated traces show that the generated Dolev-Yao checks respond to semantic inconsistencies. By making the reconstruction step explicit, the solution produces protocol-level observations on which assessments of protocol resilience and the design of defensive countermeasures can be built.

arXiv abstract · PDF

Program Specification and Verification Methods · cs.SE candidate · published 2026-11-05T12:02:54Z
Mingxiu Wang, Jiawei Wang, Shuangxiang Kan, Angela Huo, Yuekang Li, Xi Zheng, Xiao Cheng
arXiv categories: cs.SE

Loop invariants are essential for deductive program verification, yet automatically inferring them for {multiphase programs}, whose loops contain conditional branches that induce multiple execution phases with distinct behaviors, remains an open problem. Existing LLM-based methods either reason about loops as a whole or use explicit branch information to generate atomic assertions jointly across branches, without maintaining complete candidate sub-invariants for independent generation and targeted repair. We present CLOVER, a structured neurosymbolic reasoning framework for multiphase invariant inference built on two interlinked mechanisms. First, compositional inference: CLOVER statically decomposes a loop into symbolic {loop branch sequences}, conjunctions of the loop guard and branch conditions that characterize distinct execution scenarios, and guides the LLM to generate candidate sub-invariants for each one independently, so that each LLM query focuses on a single execution scenario rather than the entire loop. Second, counterexample-guided localized refinement: when SMT verification rejects a composed disjunctive invariant, CLOVER traces the counterexample back through the branch structure to identify which specific loop branch sequence caused the failure and repairs only that sub-invariant, preserving all correct components. Both mechanisms are unified by a shared symbolic structure derived from the loop's branch semantics, which guides what the LLM generates, how candidates are composed, and where refinement is directed. We evaluate CLOVER on 316 linear arithmetic, 50 nonlinear arithmetic, and 54 multiphase benchmarks. CLOVER solves 35 of 54 multiphase benchmarks, outperforming the best LLM-based baseline (29) by 20.7\% and the best traditional method (22) by 59.1\%. On linear/nonlinear benchmarks, CLOVER remains competitive, solving 355 of 366 programs overall.

arXiv abstract · PDF

Program Specification and Verification Methods · primary corpus · published 2026-11-05T14:31:54Z
Christian Kuessner, Ragnar Mogk, Julian Haas, Annette Bieniusa, Mira Mezini
arXiv categories: cs.PL, cs.DC

Replicated data types providing strong eventual consistency offer a principled foundation for developing decentralized software. Yet existing approaches to programming such data types leave access control unresolved: they either provide none at all, delegate it to a trusted coordinator, reintroducing the centralization they were designed to avoid, or tie it to specific data-type constructions, while typically assuming non-Byzantine replicas and static policies. We present GUARDTs: Guarded Unforgeable Algebraic Replicated Data Types, which embed fine-grained permissions directly into the application data model, operate without a central authority, support dynamic policy evolution, and tolerate Byzantine replicas. We formally prove that GUARDTs guarantee confidentiality, integrity, and availability and show empirically that their access control adds negligible overhead on top of the cost of Byzantine-resilient replication itself.

arXiv abstract · PDF

Program Specification and Verification Methods · primary corpus · published 2026-11-05T20:43:57Z
John M. Li, Ryan Doenges, Pedro H. Azevedo de Amorim
arXiv categories: cs.PL, cs.LO

This paper introduces a categorical framework for models of higher-order separation logic including the weakest precondition modality. Weakest preconditions are interpreted by strong monads on a category fibered over a model of Moggi's computational lambda calculus. The fibered categories in question are termed bunched fibrations and shown to be equivalent to BI hyperdoctrines. Well-known heuristic techniques for obtaining weakest preconditions are shown to be expressible in categorical terms and are proved sound. The ``baking in the frame rule'' trick is shown to satisfy a universal property. Constructions are given for extending a program logic with cost credits. Our largest case study is parametrized by a category having local independent product (LIP) structure, a notion due to Simpson that axiomatizes name generation, randomness, and local state. From an LIP category, we construct an allocation monad, a bunched fibration, and a monad lifting. We instantiate our construction to obtain a novel probabilistic separation logic for measure-theoretic probability that both simplifies and clarifies prior work.

arXiv abstract · PDF

Program Specification and Verification Methods · primary corpus · published 2026-11-06T12:43:08Z
Luke Cheeseman, Elias Castegren, David Black-Schaffer, Erik \"Osterlund, Tobias Wrigstad
arXiv categories: cs.PL

In mainstream shared-memory languages, programmers use synchronisation mechanisms such as locks to isolate shared data accesses across threads to avoid data races. Yet synchronisation enforces only a temporal ordering, while shared memory still communicates updates between threads at every ordinary read and write. To achieve isolation, programmers therefore need to understand the connection between ordering and communication, and to apply synchronisation correctly and consistently, while compilers and hardware optimise assuming they have. When programmers synchronise incorrectly, they lose isolation, and the semantics of their programs change without notice. We propose Sync-as-Share, a memory model built on isolation and communication rather than on the ordering of accesses to shared memory. We start from thread isolation, where each thread reads and writes a private view of memory, and reinterpret programs' existing synchronisation actions to also communicate updates explicitly. As nothing is communicated outside synchronisation actions, data races become impossible by construction. Instead, conflicting updates are detected at synchronisation points. Viewing synchronisation as explicit communication exposes the design decisions of what should be communicated, to whom, and what counts as a conflict. We propose two communication topologies with different trade-offs. We instantiate Sync-as-Share for Java by making the synchronisation actions already defined by its memory model the only points at which threads communicate, so Java programs can adopt Sync-as-Share unmodified. We formalise this instantiation as version-controlled memory, in which synchronisation actions push and pull updates between private views, and mechanise it in Rocq. We show that Java programs that are correctly synchronised under the Java memory model behave identically under shared memory and Sync-as-Share.

arXiv abstract · PDF

Program Specification and Verification Methods · primary corpus · published 2026-11-07T15:43:02Z
Andreas Andreakis
arXiv categories: cs.DB, cs.DC, cs.LO

Applications use heterogeneous datastores where a source feeds sinks such as search indexes or data warehouses via change data capture (CDC). As transaction logs have limited retention, CDC alone cannot bootstrap sinks, and traditional approaches either stall source writes or hold back log events. DBLog-based incremental snapshots, adopted by Debezium and Flink CDC, read tables in chunks interleaved with the log without blocking writes or long log stalls and resume where they stopped. After the initial bootstrap, a sink can drift when losing change events or receiving unintended writes. Even a repeated bootstrap can leave orphan rows that exist in the sink and not at the source. A common remedy is to populate a new empty sink, but repairing an existing sink avoids parallel pipelines, a switch and serving traffic from a drifted sink until the new sink is ready. In DBLog's original design, each chunk only emits the latest state of the rows the table still contains, so it does not handle orphan rows. We extend DBLog to delete them using what a chunk read already knows, namely the keys that the range select did not return, emitting a new kind of event that sinks apply as deletes. We also add a repair request that an external process calls with orphan candidates, which the connector checks with its own read, emitting these events for keys confirmed absent. This enables three modes. In the fully integrated mode, every chunk pass removes the orphans it finds during full or periodic repairs. In the second mode, an external drift process hands suspected orphans to the connector. The third mode combines both and is what we recommend. Together, they turn DBLog into a complete data synchronization engine whether a sink catches up on live changes or missing rows, holds wrong column values, or contains orphan rows. Their safety and convergence are formally verified in Isabelle/HOL and Lean 4.

arXiv abstract · PDF

Program Specification and Verification Methods · primary corpus · published 2026-11-08T23:17:26Z
Felix Linker, Yue Huang, David Basin, Huayi Duan
arXiv categories: cs.LO, cs.NI

DNS zone configuration errors are a frequent source of outages and frustration, particularly in combination with DNSSEC. Research has attempted to address the problem of zone configuration errors using formal methods, but existing proposals (i) only verify the absence of specific, known configuration errors, and (ii) do not consider DNSSEC. We present a new formal model of the DNS that covers most of DNSSEC, making it one of the most complete DNS models to date. In addition, we present a new tool, DecDNS, that performs a resolvability change-impact analysis of zone configuration updates using our model. We show that such a change-impact analysis can identify configuration errors without explicitly searching for them. We evaluate DecDNS both formally and empirically. We prove that DecDNS is sound and complete and show that its results agree with widely used DNS software. Finally, we explain how our approach can be integrated into operational practice, helping guide zone management in the real world.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · primary corpus · published 2026-11-02T14:14:43Z
Michael Hanus
arXiv categories: cs.PL

Logic programming is based on defining relations. Functions are often considered as syntactic sugar which can be transformed into predicates so that their logic is not used for computational purposes. In this paper, we show that the use of functions improves the operational behavior of logic programs without loosing the flexibility of logic programming. For this purpose, we present a systematic transformation from predicates and goals into functions and nested expressions, respectively. By evaluating functions in a demand-driven manner and taking potential failures into account, it is ensured that the execution of the transformed programs will never require more steps than the original programs but can decrease the number of steps---in the best case reducing infinite search spaces to finite ones. Thus, functional logic programming provides an adequate basis to improve the operational behavior of logic programs without changing their semantics. This also shows that, from an operational point of view, functional logic programming has clear advantages compared to relation-based logic programming.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · primary corpus · published 2026-11-02T20:23:13Z
Oghenevwogaga Ebresafe, Daniel Zheng, Gordon Plotkin, Ningning Xie
arXiv categories: cs.PL

Languages that target hardware accelerators typically expose a restricted, first-order core without recursion or first-class functions, leaving programmers without a principled way to express computational effects. This paper presents a technique for compiling effect handlers to such a constrained target. We introduce a novel translation that statically eliminates effect handlers, and prove that it preserves both typing and semantics. Moreover, we address the challenges of integrating effect handlers with structured control flow, where continuations cannot be constructed statically. The calculus and all our results are fully mechanized in the Lean 4 proof assistant. Finally, we implement our design as a library for JAX, a Python domain-specific language for accelerator programming, and demonstrate its expressiveness through practical case studies.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · primary corpus · published 2026-11-03T11:22:45Z
Hui Xuan Tan, Stefanos Chaliasos, Alastair F. Donaldson
arXiv categories: cs.PL, cs.CR

A zero-knowledge virtual machine (zkVM) lets an untrusted prover convince a verifier that a program, typically Rust compiled to RISC-V, ran correctly. The proof covers the compiled binary, so a miscompilation can make a correct zkVM produce a valid proof of a computation that differs from the developer's source. We present the first empirical study of miscompilation as a threat to zkVM guarantees, on the production zkVMs SP1 and Jolt. We assemble 88 known rustc and LLVM miscompilations with Rust reproducers, using an LLM agent to recover Rust triggers for 60 of 124 LLVM bugs reported only as LLVM IR. Many of the bugs carry over to zkVMs: 48 of the 88 make a guest commit a wrong output on SP1 and 46 on Jolt, including the same 15 rustc bugs on both. Most bugs that do not reproduce never reach the faulty code on the zkVM's target, e.g. because they need an instruction-set extension. Existing guest programs are rarely affected by accident. Across 13 guests of 10 popular SP1 projects, the buggy and the fixed compiler produce byte-identical binaries in 447 of the 552 guest-bug pairs that build, and the other 105 have the same code or agree on every input we ran. An attacker who contributes code to a guest, however, can trigger these bugs on purpose. For about $40 per project, an LLM agent found patches that look like ordinary optimisations, preserve the behaviour of the guest's source, and expose a known bug in 12 of 366 project-bug pairs, across 11 of 20 projects. In four cases the guest commits a wrong output, including an Ethereum client that rejects a valid block, and in the other eight it fails on a valid input. Reviewing or formally verifying the zkVM or the guest's source cannot catch such a patch, because both are correct. zkVM projects should treat their compiler as part of their trusted base and track the known bugs of their toolchain.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · primary corpus · published 2026-11-03T14:02:24Z
Albert Schimpf, Stefan Wehr, Annette Bieniusa
arXiv categories: cs.PL

We define list types, distinguishing proper lists, which end in the empty list, from improper lists, which may end in any value. Both are encoded as recursive types of cons cells, implemented in etylizer. This work found one OTP compiler bug. We propose a one-line sound improvement to Dialyzer's list handling that finds six instances of dead code in the OTP code base. We compare BEAM VM type checkers and catalogue how other languages design lists and cons cells.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · primary corpus · published 2026-11-03T14:44:47Z
Jam Kabeer Ali Khan, Jinhao Tan, Bruno C. d. S. Oliveira
arXiv categories: cs.PL

Separate compilation is central to modular software: components are compiled independently and linked into an executable. Separate compilation is correct when a linked program behaves like the program formed by merging its sources. This property is less routine to prove than type soundness because it requires a formal account of linking. We present $\lambda_{\mathsf{SCE}}$, a simply typed calculus in which linking, modules, and environments are all first-class. Programmers control module linking through a link operator, which a type-directed elaboration translates into ordinary terms of a core calculus of first-class environments. The core calculus's existing evaluation rules then perform the linking: linking as evaluation. Linking independently compiled modules yields the same core term as elaborating their source link. Therefore, compilation and linking commute by construction. As a result, separate compilation correctness follows directly from the semantics preservation for both static and dynamic linking. All meta-theory is mechanized in Lean 4, and we implement a compiler to WebAssembly in OCaml.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · primary corpus · published 2026-11-04T10:52:22Z
Jinhua Wu, Yuting Wang, Zhemin Chen
arXiv categories: cs.PL

Borrow checking is a central mechanism for Rust to ensure temporal memory safety. Its correctness is based on the intuition that the Aliasing XOR Mutability discipline guarantees that programs without borrow errors inherently could not access invalid references (i.e., pointers). However, existing work on formalizing borrow checking treats it either as a component of type systems or as symbolic execution describing resource transfer. None provides a direct explanation of the correctness of borrow checking algorithms such as Non-Lexical Lifetimes (NLL) or Polonius in the official Rust compiler that function more like static pointer analysis. We take a first step toward solving this problem by formalizing Polonius, the next-generation borrow- checking algorithm for the Rust compiler, on a core subset of Rust. We prove its correctness by showing that any program accepted by Polonius does not access invalid references at runtime. The key observation is that, when borrow checking is performed lazily, Polonius could be treated as a forward abstract interpretation on abstract domains recording pointer aliasing (borrowing) relations. By providing a concrete semantics that formally describes the Aliasing XOR Mutability discipline, we prove the soundness of this abstract interpretation, from which we derive memory safety of checked programs. This formulation of Polonius is implemented and formally verified in the abstract interpretation framework of CompCert. The correctness proofs are generated by an agentic AI under human guidance using paper proofs as proof outline. To the best of our knowledge, this is the first comprehensive formalization and verification of a borrow checking algorithm as manifested in the Rust compiler.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · cs.SE candidate · published 2026-11-04T13:41:58Z
Ioanna Moraiti, Charalambos Mitropoulos, Artem Anchikov, Sotirios Ioannidis, Dimitris Mitropoulos, Thodoris Sotiropoulos
arXiv categories: cs.SE

Automated program reduction shrinks a program into a smaller one that preserves a property of interest. Language-agnostic grammar-based reducers are easy to retarget across languages, but because they reason only about syntax, they cannot perform the coupled edits needed to remove whole declarations, e.g., a method cannot be deleted while it is still called. As a result, they waste oracle calls on edits that cannot succeed and often leave irrelevant declarations behind. We present SCYTHE, a fast, semantic-aware pre-processing step that runs in front of any grammar-based reducer without modifying it. SCYTHE encodes the program as a typed declaration dependency graph and applies a set of semantic-aware operators that decouple declarations from their use sites, making them removable while keeping the program well-typed. Fine-grained token-level minimization is then left to the downstream reducer. On 73 benchmarks across C, Java, and Solidity, combining SCYTHE with PERSES never yields a larger result than PERSES alone, and a strictly smaller one on 70 of 73 cases. On average, the combination produces programs 55.6% smaller (up to 95.5%) and is 2.3$\times$ faster (up to 7.4$\times$). SCYTHE also boosts LATRA, a reducer that, unlike the purely syntactic PERSES, also applies language-specific transformations: the combination produces programs 10.6% smaller (up to 61.8%) and is 2.4$\times$ faster on average. Video: https://youtu.be/uEq_YYU0zZw

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · cs.SE candidate · published 2026-11-05T04:40:17Z
Shengbo Wang, Mingwei Liu, Yuwen Chen, Yanlin Wang
arXiv categories: cs.SE

Memory-safety concerns make Rust an attractive target for modernizing legacy C/C++ systems, yet project-level C++ migration must balance semantic fidelity with Rust-oriented reconstruction. Source-structure-preserving migration can track low-level behavior, but it can also carry source-language organization, unsafe idioms, and project assumptions into Rust. Direct agent-based translation gives the model more freedom to construct a Rust project, but semantic coverage depends on the model identifying the source behaviors that must be preserved. This problem is especially acute for C++, where source behaviors are often hidden in object models, destructor-driven lifetime protocols, and other hard-to-localize C++ semantics. This paper presents Req2Rust, the first project-level LLM-based C++-to-Rust migration harness. Req2Rust first derives an evidence-grounded Migration Requirements Specification (MRS) that records the behaviors and constraints that must be preserved. It then synthesizes a Rust Design Specification (RDS) and realizes it as an initial Rust project. Because real projects contain implementation details and idioms that only become visible during build and validation, Req2Rust treats the initial Rust project as an executable refinement state. Compiler, semantic, and unsafe-reduction validators produce validation reports for improving buildability, behavioral alignment, and unsafe usage. We evaluate Req2Rust on general C++ projects and modules from the large-scale Openharmony codebase against a ClaudeCode baseline. Req2Rust produces buildable Rust crates in both settings and improves test pass rate from 69.5% to 91.9% on general projects and from 45.4% to 87.9% on Openharmony modules.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · primary corpus · published 2026-11-05T12:29:23Z
Robin Webbers, Wind Wong, Klaus v. Gleissenthall
arXiv categories: cs.PL

Lightweight methods like QuickCheck have proven to be successful in functional languages and beyond, as they let users specify properties as Boolean functions directly in code. We can replicate some of their benefits for (bounded) proofs via symbolic execution. If we can execute arbitrary functions symbolically, we can specify properties just as easily. Unfortunately, existing symbolic execution tools for Haskell are restricted to a subset of the language that excludes many real-world applications like IO; they also have a hard time scaling to larger programs, making them a poor fit for general purpose lightweight verification. One reason behind these limitations is that existing techniques only offer fixed symbolic semantics for SMT base types. This makes it hard to cover more programming constructs and libraries; it also makes it difficult to fine-tune symbolic representations for better performance. We present SymFC, a new symbolic execution method for Haskell that offers configurable semantics via embeddings. An embedding of a function in SymFC is just another Haskell function that can use arbitrary code, as well as SMT primitives. Embeddings make it easy to support new programming constructs and fine-tune symbolic representations for speed. To integrate embeddings into Haskell's type system, we make use of Haskell's coercions, which let us transparently convert between a Haskell type and the type of its embedding. We realize embeddings in SymFC, an all-paths symbolic execution engine for Haskell, which lets us symbolically represent arbitrary types and values in GHC core. We implement SymFC as a GHC plugin, and evaluate it by checking properties of Haskell's container library, and the iproute library. We build embeddings for IORef, Haskell's Ptr/ForeignPtr interface, and the hardware library Clash, and our evaluation reports a 6.25x speedup on G2's own benchmarks.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · primary corpus · published 2026-11-07T02:00:16Z
Marius Momeu, Marius Arvinte, Cory Cornelius, Koushik Sen
arXiv categories: cs.PL, cs.AI, cs.CR, cs.SE

Wrapping C code in a safe Rust interface lets Rust applications use it without writing unsafe code, until the code itself is migrated to Rust. Such bindings are tedious and error-prone to write, however: their internals use unsafe code that the Rust compiler does not check, so a single mistake can introduce undefined behavior (UB), and they have so far been written mostly by hand. We present Crustify, an agentic co-translator that generates safe Rust bindings for repository-level C libraries. Crustify schedules a target's types and symbols into dependency-ordered waves of independent batches that agents bind concurrently. Its agents derive the ownership and lifecycle contract of every pointer and type they wrap, check each binding with coverage-guided equivalence and UB tests under sanitizers and Miri, and review every wave. They build on three tools that we contribute: (a) ffibox, Rust primitives for C/Rust interop that mirror Box, Arc, and Vec for C objects without ever forming a reference to memory that C may alias; (b) Wavefront, a neuro-symbolic static analyzer that orders a target's items by their dependencies, including those that casts and type-erased pointers hide; and (c) ffimap, a rustc-based analysis that maps the unsafe surface of bindings. On libgit2 and ffmpeg, with one developer in the loop, Crustify generated safe bindings for 41.9% and 42.8% of their public APIs in about 51.9 and 58.9 hours. On the interface consumers are expected to use, only 1.6% and 0.4% of the bindings' public functions are unsafe, and only 0.1% and 0.6% have a raw pointer in their signature. Their tests cover 98.92% and 99.07% of the Rust code and 45.95% and 67.20% of libgit2 and of ffmpeg's libavutil, and the reviewers fixed 8 and 13 defects that caused UB reachable from Rust. To our knowledge, this is the first work to automate the generation of safe Rust bindings for C libraries.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · primary corpus · published 2026-11-08T01:17:59Z
Derek Egolf, Stavros Tripakis
arXiv categories: cs.PL

We propose a synergistic combination of classical program synthesis techniques and contemporary large language models (LLMs) to solve the problem of recursive program synthesis from first-order logic specifications. Our approach leverages the strengths of both paradigms: we use LLMs as a source of statistical bias to guide the search for a correct program. At the same time we use techniques from classical synthesis to short-circuit on semantically incorrect prefixes and to avoid sampling semantically equivalent responses. The statistical bias is derived from the next-token distribution of an LLM, which is highly context-dependent. We operate with the understanding that (1) there is some class of synthesis instances that can be discharged by small models and symbolic tools, and (2) every other instance can be decomposed into these instances. Therefore, our intention is to expand the reach of small, open-weight LLMs and symbolic synthesis techniques, not to compete with proprietary frontier models on every possible instance. These are different tools for different jobs. In our experimental evaluation, we find that our method solves more benchmarks than either small LLMs or classical synthesis techniques alone. Our method solves 30/32 benchmarks using only a Qwen2.5 model with 32 billion parameters. Qwen2.5 solves 0 benchmarks on its own, and only solves a few additional benchmarks when combined with traditional constrained decoding techniques.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · primary corpus · published 2026-11-08T04:03:10Z
Yalu Cai, Tung-Che Chang, Santosh Nagarakatte
arXiv categories: cs.PL

Recent systems such as the eBPF Certificate Framework (BCF) and Proof-Carrying BPF address the imprecision in the Linux eBPF verifier with proof-carrying code. When the verifier's abstract domains cannot prove a safety condition, an in-kernel proof checker checks an untrusted user-space refutation proof. A single bug in this checker can compromise the security of the entire kernel. While formalizing BCF's in-kernel checker, we discovered 13 bugs such as unsound rewrite rules, silently unchecked proof steps, and memory safety errors. We demonstrate that forged certificates can trick the kernel to accept arbitrary unsafe eBPF programs. To address this problem, we propose Keel, a formally verified in-kernel proof checker for the Linux eBPF verifier. First, we specify the checker as a pure functional program in Lean and prove its soundness against bit-vector semantics. We decouple the steps of the proof certificate checker from the mathematical rewrite rules, which enables us to extend the rewrite rules without the need to change the checker. Second, we implement the checker in EmbC, a deeply embedded C fragment, and prove that our C implementation refines the functional specification without undefined behavior or memory leaks. Third, using an amortized potential argument, we prove linear time and memory bounds for the C checker. Keel is correct-by-construction while also being faster than the BCF checker inside the kernel, 1.3X in total and 2.0X on the slowest 1.4% of certificates.

arXiv abstract · PDF

Compilers Synthesis and Language Implementation · cs.SE candidate · published 2026-11-08T10:33:51Z
Philipp Vollmer
arXiv categories: cs.SE, cs.DC

The infrastructure definitions and the code for serverless applications are often only loosely connected. This yields a large error class: the referenced infrastructure components might not exist. It is also hard to keep the application and its permissions in sync. To address this problem we present an infrastructure from code solution where we provision cloud infrastructure from Wasm Interface Type (WIT) - the language defining the interface of WebAssembly components. We limit ourselves to the basic example of an AWS Lambda function accessing S3 buckets. We build two interpreters for the WIT language: one that derives the definition of S3 buckets as infrastructure as code and least-privilege IAM permissions, and a generic runtime that runs the component as a Lambda function and provides access to the S3 buckets as capabilities. We formulate consistency properties that ensure the existence of the S3 buckets and correct permissions of the Lambda, and provide evidence that our interpreters satisfy them. We show how selected failures for deployment of such cloud components can be prevented using our technique and how a baseline setup fails at this task. Together with the strict sandboxing of the WebAssembly runtime we achieve an instance of capability-based security for access to AWS infrastructure as a further result.

arXiv abstract · PDF

Compilers for Accelerators and Numerical Code · primary corpus · published 2026-11-02T03:14:28Z
Yihong Zhang, Bala Vinaithirthan, Karima Ma, Zachary Tatlock, Maaz Bin Safeer Ahmad, Andrew Adams
arXiv categories: cs.PL

Recurrences are ubiquitous in signal and image processing, bioinformatics, numerical computing, combinatorial optimization, and many other domains. Because recurrences seem inherently sequential, they are often implemented serially and thus do not leverage vector instructions in modern hardware. This leaves much of the available, often highly parallel, hardware underutilized. In this paper, we present an algebra of recurrences over semirings and study algebraic identities that enable vectorization. Using our algebraic framework, we present a number of vectorizing transformations that yield efficient, vectorized implementations across various settings. These transformations naturally extend to 2D recurrences and mutual recurrences. We implement the recurrence algebra and the vectorizing transformations in a compiler called VecRec.VecRec compiles recurrence programs to efficient vectorized C++ implementations. The generated kernels can achieve up to an order-of-magnitude speedup over serial implementations across a wide variety of recurrences. A case study in bioinformatics shows that they are competitive with, and in many cases better than, existing libraries with manually-crafted vectorization.

arXiv abstract · PDF

Compilers for Accelerators and Numerical Code · primary corpus · published 2026-11-02T20:22:41Z
Vaishnavi Kouru, Robert Chun
arXiv categories: cs.PL

Low-precision numeric types such as 8-bit integers, bfloat16, and half-precision floating point (fp16) are often used in AI inference workloads to reduce memory bandwidth, and RISC-V's openly specified Vector extension (RVV) is a natural target for compiling such workloads with auto-vectorization. This paper examines whether LLVM's RISC-V auto-vectorizer handles these narrow types equally well, using a multiply-accumulate loop written for fp32, int8, bf16, and fp16. Under a common baseline target (-march=rv64gcv), int8 and fp32 vectorize cleanly, while bf16 and fp16 degrade to increasingly scalar-heavy fallback code, with fp16 falling back to per-element software conversion calls, unless additional target-feature extensions (zvfbfmin/zvfbfwma, zvfhmin) are enabled. Under QEMU user-mode emulation, the baseline bf16 and fp16 kernels execute $17.0\times$ and $75.9\times$ as many dynamic instructions as their extension-enabled counterparts. Compiler diagnostics do report this degradation, but do not distinguish, in their wording, between a limitation that a compiler flag resolves entirely and one reflecting an inherent conversion cost, leaving no direct signal toward the fix. These results are supported by assembly-level instruction analysis, by direct inspection of LLVM's optimization remarks, and by dynamic instruction counts collected under emulation.

arXiv abstract · PDF

Compilers for Accelerators and Numerical Code · primary corpus · published 2026-11-03T05:15:32Z
Junyu Yin, Vinod Grover, Keren Zhou
arXiv categories: cs.PF, cs.PL

LLM agents are becoming GPU kernel engineers, but they still tune kernels without seeing where the time goes. Hardware profilers report how busy each unit was, not where each warp's time went; intra-kernel tracers can show it, but only with hand-placed probes and a recompilation that alters the very kernel being measured. We present Warpline, which gives agents this view automatically while leaving the kernel essentially unchanged. Warpline analyzes the binary to decide which events to record and inserts probes into the binary itself without recompilation or any manual step. It then aligns the trace with hardware profiling data on one unified timeline. Because it needs only the binary, it can regenerate this evidence for every new version of the kernel at whatever level the agent edits it (source, IR, or PTX), closing the optimization loop without human intervention. On NVIDIA B200, across 35 kernels in Triton, CuTe DSL, and CUDA C++, Warpline adds a median overhead of 1.2% and leaves a median 99.9% of executed instructions unchanged, whereas existing tracers have median overheads of 1.6% to 13.2% and leave only 4.6% to 32.7% unchanged. Warpline also traces closed-source kernels, which these tracers cannot. On 10 SOL-ExecBench problems, agents using Warpline spend less time and fewer model requests than a bare coding agent and NVIDIA's Kernel Design Agents (KDA), yet lead both after every round in geometric mean and reach a 7.69$\times$ geometric-mean speedup, against 6.94$\times$ and 6.13$\times$. Two case studies further demonstrate that Warpline reveals hidden bottlenecks and provides actionable optimization insights.

arXiv abstract · PDF

Compilers for Accelerators and Numerical Code · primary corpus · published 2026-11-03T16:09:26Z
Ravishka Rathnasuriya, Nidhi Majoju, Zihe Song, Wei Yang
arXiv categories: cs.SE, cs.DC, cs.PL

General-purpose graphics processing unit (GPU) computing has emerged as a leading parallel computing paradigm, offering significant performance gains in various domains such as scientific computing and deep learning. However, GPU programs are susceptible to numerical bugs, which can lead to incorrect results or crashes. These bugs are difficult to detect, debug, and fix due to their dependence on specific input values or types and the absence of reliable error-checking mechanisms and oracles. Additionally, the unique programming conventions of GPUs complicate identifying the root causes of bugs, while fixing them requires domain-specific knowledge of GPU computing and numerical libraries. Therefore, understanding the characteristics of GPU numerical bugs (GPU-NBs) is crucial for developing effective solutions. In this paper, we conduct a comprehensive study of GPU-NBs by analyzing 397 real-world bug samples from GitHub. We identify common root causes, symptoms, input patterns, test oracles that trigger these bugs and the strategies used to fix them. We also present GPU-NBDetect, a preliminary tool designed to detect numerical bugs across six distinct bug categories. GPU-NBDetect detected a total of 226 bugs across 186 mathematical functions in four libraries, with 60 of the bugs confirmed by developers. Our findings lay the groundwork for developing detection and prevention techniques for GPU-NBs and offer insights for building more effective debugging and auto-repair tool.

arXiv abstract · PDF

Compilers for Accelerators and Numerical Code · primary corpus · published 2026-11-04T07:21:03Z
Xuxiao Yang, Junchi Wu, Yuqi Peng, Feiyang Wu, Zhuoran Li, Wei Kong, Shuo Tao, Dongyi Fan, Yiming Zhang, Keqin Luo, Xingrui Gao, Hao Zhang, Xuehai Qian, Youwei Zhuo
arXiv categories: cs.PL, cs.AR

Statically scheduled accelerators such as Groq's Tensor Streaming Processor (TSP) achieve low-latency large language model inference by stripping dynamic synchronization hardware from the chip. With no caches, arbiters, or hardware schedulers, the compiler must fix the exact slice and issue cycle of every operation, so when an operation runs is a condition for correctness. Existing kernel languages cannot target such machines because they rely on hardware to resolve cycle timing and instead encode schedules implicitly in code structure. We present TauLang, a kernel language and compiler that makes time a first-class citizen of the program. The programmer schedules operations, loops, and composed kernels with parameterized explicit times, so exploring schedules means changing parameter values rather than rewriting code. TauLang validates explicit times algebraically in TauIR, its timed intermediate representation. It then solves tensor placement and cycle scheduling jointly in an integer linear program, using explicit times to group connected operations into timing clusters that prune the search space. On a cycleaccurate model of a TSP-like machine, joint search achieves a $1.40\times$ latency speedup across ten kernels over a space-first flow. A few explicit time pins keep latency within one cycle of the untimed schedules and scale joint search to 1,636 GEMM blocks, whereas untimed search finds no schedule at 32.

arXiv abstract · PDF

Compilers for Accelerators and Numerical Code · primary corpus · published 2026-11-04T20:17:40Z
Thisara Rathnayaka Weerakoon (1), Ishan Dewpura (1), Niman Ransindu (1), Shavin Anjitha (1), Tharindu R. Patabandi (2), Sanath Jayasena (1) ((1) Department of Computer Science & Engineering, University of Moratuwa, Sri Lanka, (2) Independent Researcher, San Jose, CA, USA)
arXiv categories: cs.DC, cs.PF, cs.PL

For sufficiently large transformer-based Large Language Models (LLMs), whose parameters cannot be retained in on-chip caches, prefill throughput on multi-socket CPUs is often limited by sustainable DRAM bandwidth rather than peak floating-point throughput. In the standard PyTorch compilation (i.e., TorchInductor) path, model weights are allocated without considering the Non-Uniform Memory Access (NUMA) topology: specifically, the affinity between memory banks and compute cores is disregarded. This causes a substantial fraction of weight accesses to traverse the inter-socket interconnect, severely degrading the effective memory bandwidth available to each socket. We address this bottleneck through a compiler-level solution that makes TorchInductor NUMA-aware. Treating each NUMA socket as an independent tensor-parallel partition, we introduce NUMA-aware Tensor Parallelism (NUMA-TP). This approach transparently shards weights across sockets and schedules compute kernels such that thread pools and memory allocations remain strictly local to their respective sockets using CPU affinity. We evaluate the approach on GPT-2 (117M, 345M, 762M) and BERT (Small, Large), which exercise standard multi-head attention and MLP, as well as Gemma 3 270M, which combines Multi-Query Attention with a GeGLU-gated MLP. By strictly enforcing data locality, our approach successfully mitigates cross-socket traffic, achieving prefill speedups of up to 2.63x on a dual-socket Haswell platform, up to 1.87x on a dual-socket Cascade Lake platform, and up to 2.27x on a four-socket Haswell-EX platform.

arXiv abstract · PDF

Compilers for Accelerators and Numerical Code · primary corpus · published 2026-11-07T17:09:25Z
Val\'erian Rey, Praneth Paruchuri
arXiv categories: cs.LG, cs.MS, cs.PL

We propose a new mathematical formalism in which all kinds of tensors and of operations on those tensors are represented as simple function compositions. Tensors are functions from indices to values. An element-wise operation (e.g. an activation function) is a composition with a function applied to values; re-indexing (e.g. reshape, transposition) is a composition with a function applied to indices; and a reduction is a composition with both an index function, mapping each index to several indices, and a reduction operation (e.g. product, sum, max). Combined with tensor stacking, these compositions can represent most interesting kinds of tensors (e.g. dense, jagged, all kinds of sparsity patterns, matrix factorizations), as well as lazy versions of almost every operation available in modern tensor computation frameworks, including einsums between tensors of any kind. Identities between compositions can then be used to rewrite such expressions into equivalent ones, without evaluating them. For instance, the product of two sparse matrices can be rewritten so that only products between non-zero values are computed, turning a sparse problem into a dense one. Using this algebra as the intermediate representation of a tensor computation engine would shift the focus from defining operations on tensors (e.g. einsum between sparse tensors) to defining an algebra on index functions. This should reduce the codebase complexity from $\mathcal{O}(mn^2)$, with $m$ the number of binary operations between tensors and $n$ the number of tensor types, to $\mathcal{O}(m + k^2)$, with $k$ the number of types of index functions. A draft implementation of a tensor computation framework based on this algebra is publicly available.

arXiv abstract · PDF

Quantum Programming and Circuit Semantics · primary corpus · published 2026-11-02T00:49:20Z
Shengyuan Yang, Charles Yuan
arXiv categories: cs.PL, quant-ph

Quantum programs that use temporary values, known as \emph{ancilla} qubits, must explicitly \emph{uncompute} each ancilla back to zero to ensure that the program produces correct outputs. Conventional uncomputation uses unitary quantum gates, whereas leading quantum algorithms now leverage \emph{measurement-based uncomputation} (MBU), which replaces costly unitary $T$ gates with cheaper measurements and phase corrections. Current quantum programming frameworks can use measurement to uncompute specific gates such as Toffoli. No automatic transformation, however, accepts an arbitrary circuit whose ancillas are computed and uncomputed via the standard approach and converts the circuit to use MBU\@. Researchers instead apply MBU to individual circuit designs by hand, which limits algorithm development and compiler optimization. Such a transformation has not existed due to two fundamental unknowns: where MBU applies and which gates realize MBU for an arbitrary computation. To solve these, we first present a static analysis that identifies, for each ancilla qubit, each circuit position where measurement is sound --- subsuming basic assumptions that MBU only applies at the end of a circuit. Next, we present circuit transformations that soundly turn unitary uncomputation gates into efficient phase corrections after measurement --- generalizing rewrite rules from prior literature that are either limited to a single gate or not applicable to a general circuit. We present \textsf{MBUndo}, an integrated compiler pass that automatically converts circuits to measurement-based uncomputation. It requires no user annotations other than which qubits are ancillas, the same as needed by existing uncomputation synthesizers, and can enhance their output circuits. We evaluate \textsf{MBUndo} on 22 benchmarks to reveal \emph{T} gate reductions of ${>}36.5\%$ over uncomputation synthesizers.

arXiv abstract · PDF

Quantum Programming and Circuit Semantics · primary corpus · published 2026-11-02T23:25:09Z
John van de Wetering, Ognyan Oreshkov, Ana Bel\'en Sainz
arXiv categories: cs.LO

This volume contains the proceedings of the 23rd International Conference on Quantum Physics and Logic (QPL 2026), which was held from August 17 to August 21 2026, in Amsterdam, The Netherlands, organized by the University of Amsterdam. QPL is an annual conference that brings together academic and industry researchers working on topics ranging from basic research in the foundations of physics to applications in quantum computing and communication, both for near-term quantum hardware and future large-scale, fault-tolerant devices. The conference places particular emphasis on the application of formal algebraic, logical, compositional, and categorical structures to quantum theory and related areas. Work applying quantum-inspired techniques and structures to other fields such as (classical) computation, linguistics, artificial intelligence, and causality is also welcome.

arXiv abstract · PDF

Quantum Programming and Circuit Semantics · primary corpus · published 2026-11-03T04:02:30Z
Mingsheng Ying
arXiv categories: quant-ph, cs.DC, cs.LO, cs.PL

In this paper, we develop a semantic model for the parallel execution of quantum circuits, providing a formal foundation for studying shared-qubit concurrency in quantum computing. As in classical shared-memory concurrency, parallel quantum circuits may interfere with one another through operations on shared qubits. However, quantum entanglement and the noncommutativity of quantum operations introduce additional challenges for reasoning about their correctness. To address these challenges, we generalise the classical Owicki-Gries method to quantum computing at the level of quantum circuits. Our approach enables compositional reasoning about parallel quantum circuits by separating the verification of individual components from the analysis of interference between them. We formulate proof rules for establishing the correctness of parallel quantum circuits and prove their soundness with respect to the proposed semantic model.

arXiv abstract · PDF

Quantum Programming and Circuit Semantics · primary corpus · published 2026-11-04T08:22:34Z
Samson Abramsky (University College London), Radha Jagadeesan (DePaul University)
arXiv categories: cs.LO

We develop a boundary-centric semantic framework for higher-order quantum computation, building on the Kelly-Laplaza description of compact closure and Abramsky's execution account. In the semantic carrier Perm(C), morphisms are complex-linear combinations of polarized boundary linkings, composed by execution. Finite-family addresses provide coherent control over finite-level quantum registers (qudits) while retaining the multiplicative boundary structure. We identify essential unitarity, a boundary condition extending ordinary unitarity to higher-order interfaces. On positive qudit registers it coincides with ordinary matrix unitarity; at higher order it expresses preservation of information across the full polarized boundary. We define a unit-free coherent quantum core generated bymultiplicative wiring, unitary gates on positive qudit registers, and contextual coherent control, and prove that every one of its morphisms is essentially unitary. The framework realizes an applied coherent quantum switch and the unitary stages of equal-ratio one-slot supermap dilations with explicit memory. Complete proofs appear in the full version of this paper.

arXiv abstract · PDF

Quantum Programming and Circuit Semantics · primary corpus · published 2026-11-04T22:55:58Z
William Schober (Universit\`a della Svizzera italiana), Scott Wesley (Dalhousie University)
arXiv categories: cs.LO, math.CT

Controlled subcircuits are commonplace in quantum algorithms as they represent the quantum analogue of branching statements (if then). We introduce a generalization of controlled subcircuits in the form of a binary operation which sends pairs of unitary quantum circuits to a generalized controlled operation, whose semantics are based on matrix exponentials and logarithms. The family of quantum circuits with generalized controlled operations and circuit exponentiation is denoted HQC for Hierarchical Quantum Circuits. We formalize HQC as a modified prop category using a novel category-theoretic construction, and provide a sound and complete equational theory for diagrammatic reasoning in HQC.

arXiv abstract · PDF

Quantum Programming and Circuit Semantics · cs.SE candidate · published 2026-11-05T01:36:54Z
Ragib Shahariar Ayon, Shibbir Ahmed
arXiv categories: cs.SE

Executable specifications make software assumptions explicit and checkable, yet their role in quantum information and machine learning (QIML) remains underexplored. We argue that executable specifications should be treated as first-class artifacts for independent verification and validation (IV&V) of QIML systems. Static analysis, testing, simulation, and runtime checking can provide evidence about QIML behavior, while Design by Contract shows that selected quantum-state, measurement, and statistical properties can be expressed as checkable conditions. However, adapting existing methods for specification inference and assessment from conventional and machine-learning software to QIML raises several challenges, notably limited evidence for deriving generalizable specifications, cross-stage and probabilistic behavior, repository-scale reasoning across hybrid workflows, and weak behavioral oracles. We characterize these challenges and identify research directions for QIML corpora, specification semantics, repository-level analysis, and specification assessment.

arXiv abstract · PDF

Quantum Programming and Circuit Semantics · cs.SE candidate · published 2026-11-05T16:08:19Z
Jiyuan Wang, Qian Zhang, Guoqing Harry Xu, Miryung Kim
arXiv categories: quant-ph, cs.SE

Over the past few years, several quantum software stacks (QSS) have been developed in response to rapid hardware advances in quantum computing. A QSS includes a quantum programming language, an optimizing compiler that translates a quantum algorithm written in a high-level language into quantum gate instructions, a quantum simulator that emulates these instructions on a classical device, and a software controller that sends analog signals to a very expensive quantum hardware based on quantum circuits. In comparison to traditional compilers and architecture simulators, QSSes are difficult to tests due to the probabilistic nature of results, the lack of clear hardware specifications, and quantum programming complexity. This work devises a novel differential testing approach for QSSes, named QDIFF with three major innovations: (1) We generate input programs to be tested via semantics-preserving, source to source transformation to explore program variants. (2) We speed up differential testing by filtering out quantum circuits that are not worthwhile to execute on quantum hardware by analyzing static characteristics such as a circuit depth, 2 qubit gate operations, gate error rates, and T1 relaxation time. (3) We design an extensible equivalence checking mechanism via distribution comparison functions such as Kolmogorov Smirnov test and cross entropy

arXiv abstract · PDF

Quantum Programming and Circuit Semantics · primary corpus · published 2026-11-05T20:30:24Z
Jacques Carette, Chris Heunen, Robin Kaarsgaard, Neil J. Ross, Amr Sabry
arXiv categories: cs.PL, quant-ph

Given the forces acting on a quantum particle, a Hamiltonian models its continuous evolution. Quantum computers evolve Hamiltonians to simulate physical systems, to solve optimisation problems, and to estimate eigenvalues, and even the popular circuit abstraction is compiled to Hamiltonians on the hardware. We introduce Hamilton, a process calculus whose parallel operator is the sum of interactions acting simultaneously. Its operational semantics is the Lie-Trotter product formula, which recovers a sum as the limit of ever finer sequential interleavings; compiling a program means halving it to a chosen precision and unrolling the interleaving into a circuit. The semantics is fully abstract, the expressible Hamiltonians are exactly those whose Pauli coefficients have the form $m/2^k$, the precision that successive halving reaches, and the equational theory is complete and decidable. A full implementation compiles Hamilton programs to circuits and decides their equivalence, and Agda proofs sanity-check the core metatheory.

arXiv abstract · PDF

Automata Games and Reactive Synthesis · primary corpus · published 2026-11-02T23:45:06Z
Michal Ajdarow
arXiv categories: cs.LO

Markov decision process over vector addition system with states (VASS MDP) is a finite state model combining non-deterministic and probabilistic behavior, augmented with non-negative integer counters that can be incremented or decremented during each state transition. VASS MDPs can serve as abstractions of probabilistic programs, offering many decidable properties. In this paper, we develop techniques for analyzing the polynomiality of asymptotic estimates for VASS MDPs. That is, for every initial configuration of size \(n\), we consider the number of transitions needed to reach a configuration with some counter negative. We show that for any VASS MDP, either for all \(\epsilon>0 \) and all sufficiently large \(n\) the number of transitions is at least \(2^{n^{\frac{1}{2}-\epsilon}} \) with probability at least \(1-\epsilon \), or for any superpolynomial function \(f \), all \(\epsilon>0 \) and all sufficiently large \(n\) the number of transitions is upper bounded by \(f(n) \) with probability at least \(1-\epsilon \). Furthermore, if the VASS MDP is DAG-like then we can replace \(f(n)\) with \(n^{k+\epsilon} \), where \(k=2\cdot 3^{w\cdot d+|T|} \) and \(w,d\) and \(T \) are the number of MECs, counters and transitions of the VASS MDP, respectively. It is decidable in polynomial time which case holds.

arXiv abstract · PDF

Automata Games and Reactive Synthesis · primary corpus · published 2026-11-03T03:44:01Z
Xinhao Yan, Kenji Kashima, Bo Chen, Hailong Huang
arXiv categories: eess.SY, cs.LO, cs.SY

This paper considers online intrusion-risk assessment and graded warning for unmanned aerial vehicles under bounded measurement attacks. To address this problem, we develop a monitoring framework that combines trusted state estimation, attack-aware risk assessment, and probabilistic signal temporal logic (PrSTL). Trusted observations support recursive state estimation, while potentially attacked observations inform integrity testing and intrusion-risk assessment. The key contribution is a confidence-set construction that combines normalized innovation statistics with physical attack bounds to characterize admissible measurement biases. The resulting family of bias-corrected Gaussian posteriors yields an upper bound on the probability of occupying a no-fly zone or its surrounding safety margin. Confidence guarantees and finite-cover numerical certificates quantify the reliability of this risk envelope, which is evaluated with or without an integrity alarm. The PrSTL monitor analyzes the resulting risk sequence to distinguish ordered, persistent, and repeated risk and produces graded warnings with explicit robustness margins and supporting windows. We validate the monitor in flight experiments with a Crazyflie quadrotor tracked by a Vicon motion capture system. Controlled comparisons quantify the contributions of individual monitoring components. Prescribed risk profiles verify the temporal semantics and illustrate how distinct risk patterns produce different warning levels.

arXiv abstract · PDF

Automata Games and Reactive Synthesis · primary corpus · published 2026-11-03T09:26:15Z
Benedikt Bollig, Patricia Bouyer-Decitre, Matthias F\"ugger, Dhrubajyoti Ghosh, Thomas Nowak, Nathalie Sznajder
arXiv categories: cs.DC, cs.FL, cs.LO, cs.SY, eess.SY

Reactive synthesis is the problem of generating a program that produces outputs satisfying a logical specification for every input stream. We study distributed synthesis for two processes communicating in rounds over unreliable links, with at least one message delivered in every round. Despite this delivery guarantee, we show that synthesis from linear temporal logic specifications is undecidable, even when messages carry the processes' complete causal histories. More generally, we give a complete characterization of the communication restrictions that make synthesis decidable. Restrictions are described by a message adversary $A$, a set of allowed infinite graph histories: sequences of communication graphs, each specifying which messages are delivered in a round. Iterated chromatic subdivision associates these histories with points in the unit interval, yielding an image $\pi(A) \subseteq [0,1]$. For every $\omega$-regular message adversary $A$, synthesis is decidable if and only if $\pi(A)$ is nowhere dense. In the decidable cases, our procedure takes a deterministic parity automaton for $A$ and a specification, decides realizability, and constructs a realizing distributed algorithm whenever one exists. Further, our topological arguments shed new light on the fundamental requirements of synthesis. They show that, for $\omega$-regular message adversaries, synthesis is decidable if and only if consensus is repeatedly solvable in bounded time. This links two previously unrelated problems from formal verification and distributed computing through the processes' uncertainty about communication.

arXiv abstract · PDF

Automata Games and Reactive Synthesis · primary corpus · published 2026-11-04T12:52:00Z
Andrea Manini, Matteo Rossi, Pierluigi San Pietro
arXiv categories: cs.LO

Classical Timed Games formulations may be unsuitable, or require substantial modeling effort, to capture complex interaction patterns between a controller and its surrounding environment, in which non-determinism must be resolved after the controller has chosen which action to perform. In this paper, we develop the theory of Timed CLTLoc Games (TCGs), a Timed Game variant designed to facilitate the modeling of such patterns. Unlike classical Timed Games formulations, TCGs partition locations rather than transitions, and use Constraint Linear Temporal Logic over clocks (CLTLoc) to specify the controller's objectives. We develop algorithms for solving TCGs and synthesizing winning controller strategies for games whose objectives include formal properties such as reachability and safety. For reachability objectives, our synthesis algorithm yields winning controller strategies that minimize the number of moves required to reach a goal state. Solving reachability TCGs is EXPTIME-complete, matching the complexity of solving reachability Timed Games. All of our algorithms operate backwards and are implemented in our C++ region-based library TARZAN, leveraging OpenMP for efficient parallelization. Experimental results demonstrate the feasibility of TARZAN.

arXiv abstract · PDF

Automata Games and Reactive Synthesis · primary corpus · published 2026-11-05T10:19:42Z
Sherzod Turaev, Nor Haniza Sarmin, Wan Heng Fong
arXiv categories: cs.FL, cs.LO

Fuzzy grammars and weighted automata usually attach to each word a single grade, which records how strongly the word is generated but not how far that record can be trusted. We study weighted grammars and finite automata whose weights are scalar grade-reliability pairs inspired by Z-numbers. Sequential composition multiplies both components, while aggregation selects a derivation by its credible grade, the product of grade and reliability, with ties resolved by grade. On the canonical carrier, in which the weights of zero grade or zero reliability are identified with zero, the resulting structure is a commutative selective semiring, isomorphic to a subsemiring of a lexicographically ordered product, and its credible-grade projection is a homomorphism onto the Viterbi semiring. We compare several alternative combination rules and identify the carriers on which the relevant algebraic laws hold. Standard results on weighted automata then yield a rational characterization and closure properties. We prove that positive credible-grade cuts and selected-run reliability filters of finite automata are regular and effectively constructible for rational weights and thresholds, and we exhibit distinctions that the scalar projection cannot see: a reliability filter that no scalar reweighting of the same one-state automaton implements, nonmonotonicity under the addition of runs, and an unambiguous automaton with no deterministic equivalent although its scalar projection is deterministic. A count-based example illustrates an attestation penalty for grammar rules. The construction concerns scalar pairs, and its extension to arbitrary fuzzy-valued Z-numbers remains open.

arXiv abstract · PDF

Automata Games and Reactive Synthesis · primary corpus · published 2026-11-06T10:06:52Z
Takuto Yamauchi (1, 2), Kenji Tei (2) ((1) Waseda University, (2) Institute of Science Tokyo)
arXiv categories: cs.GT, cs.LO

A game may have, for each target below its value, a finite controller meeting that target, yet no finite controller attaining the value itself. We study finite stochastic games with a hard specification that must hold on every supported execution, including paths of probability zero. Max uses a pure finite controller; Min may use any pure public-history strategy. We distinguish three numerical questions: can a supplied target be met, can the unspecified optimum be attained, and what is one exact value? For explicit hard and Boolean soft Streett conditions, the strict and non-strict supplied-threshold problems are coNP-complete, attainment of the unsupplied supremum is $\mathrm P^{\mathrm{NP}}$-complete, and one exact reduced fraction is $\mathrm{FP}^{\mathrm{NP}}$-complete under polynomial metric reductions. The proofs preserve both the value and its finite attainability when fixing a single opponent, and encode adaptive queries without computing unknown subgame values. The same construction yields matching value-comparison and exact-output lower bounds for ordinary stochastic Streett games with unrestricted randomized history strategies. We also bound the memory needed for optimal finite implementations for arbitrary Muller hard conditions and rational rewards in $[0,1]$ determined by infinitely recurring states. One controller is sure from the entire original sure region and attains at every finitely attained start, with no attainment premise on the other states. For $n$ states in that region it uses $2^{O(n\log(n+1))}Q(1+\log R)$ modes, where $Q$ is the product of the least common denominators of full original chance rows sourced in that sure region and $R$ clears all reward values. Its joint dependence on $Q$ and $R$ is worst-case sharp at each fixed $n\ge6$ when $Q,R\ge2$. Optimal dependence on arena size and efficient general synthesis are not resolved here.

arXiv abstract · PDF

Automata Games and Reactive Synthesis · primary corpus · published 2026-11-06T19:02:50Z
Miko{\l}aj Boja\'nczyk, Antonio Casares, Sven Manthe, Pawe{\l} Parys
arXiv categories: cs.FL, cs.LO

Rabin's Tree Theorem says that the MSO theory of the infinite binary tree $2^*$ is decidable. Shelah showed that MSO logic becomes undecidable if this tree is extended to $2^{\le \omega}$, i.e. by allowing quantification over sets of infinite branches. A longstanding open problem is whether the decidability can be recovered in $2^{\le \omega}$ by restricting set quantification to Borel sets. We make some progress in this direction, by identifying a suitable automaton model, and showing that most of the automata-theoretic approach to Rabin's Theorem can be extended to the new framework. The only missing part is a conjecture about finite-memory determinacy in certain games. This paper states and explores the conjecture. We prove it in some restricted cases, and give lower bounds on the memory required in those games.

arXiv abstract · PDF

Complexity Theory and Algorithmic Metatheorems · primary corpus · published 2026-11-02T09:41:46Z
Olivier Bournez, Johanne Cohen, Adrian Wurm
arXiv categories: cs.LG, cs.CC, cs.LO, cs.NE

We study the iterates of a fixed ReLU network $N$ of width 4, that is, the discrete-time system $x_{k+1} = N(x_k)$ on $[0,1]^4$. Equivalently, $x_k$ is the output of a weight-tied network made of $k$ copies of $N$, or of a recurrent network with no external input, started at $x_0$. We prove that every deterministic Turing machine $M$ admits such a network $N_M$. The network can be constructed in polynomial time from $M$. Each iteration has depth $\mathrm{poly}(|M|)$. The iterates of $N_M$ simulate $M$ exactly on every encoded tape. The number of iterations is proportional to the running time of $M$. Moreover, the fourth coordinate irreversibly flags every point of the convex cube $[0,1]^4$ whose simulation reads an invalid digit. This flag is the certificate that makes hardness reductions sound on convex input regions, the regime of practical verifiers. Convex regions were previously inaccessible because of a continuity obstruction inherent to ReLU networks. The correspondence has three consequences. First, reachability for iterated width-4 ReLU networks spans the full complexity hierarchy along the single axis of the time bound: it is NP-complete for a unary bound, NEXP-complete for a binary bound and RE-complete (undecidable) with no bound. Second, two extra neurons of width suffice to extend the hardness to every common smooth activation: at width 6, the robust verification problem (a promise problem with $\delta/2\delta$ gap) is NP-complete for $\tanh$, sigmoid, GELU, Swish, ELU, and any polynomial-time-computable continuous non-polynomial activation with a polynomial-time-computable Lipschitz constant. Third, the whole spectrum transfers to discretized Neural ODEs in dimension 5.

arXiv abstract · PDF

Complexity Theory and Algorithmic Metatheorems · primary corpus · published 2026-11-03T10:45:02Z
Benjamin Merlin Bumpus, Guilherme C. M. Gomes, Laura Larios-Jones, Will J. Turner
arXiv categories: math.CO, math.CT

Tree decompositions describe large graphs as gluings of smaller component parts. Here we study their categorical duals, tree co-decompositions, which construct large graphs via fibered products of small constituent parts. Co-decompositions are compressed representations of graphs or relational structures: the decomposed object can be exponentially larger than the space required to specify the co-decomposition. Our main contribution is an algorithmic meta-theorem for first order logic: given only a co-decomposition of a $\sigma$-structure $G$ with $b$ bags, each of size at most $w$ and an FO sentence $\phi$, there is an algorithm which, without ever constructing or inspecting $G$, operates on the co-decomposition and determines whether $G \models \phi$ in time $f_\sigma(w,|\varphi|)\cdot b$. We pair this algorithm with structural results on tree co-width, including its relationship to tree-width and a separation from twin-width. Furthermore, we characterize bounded path co-width using a graph grammar. In contrast to our logical meta-theorem, we prove that $(s,t)$-Path becomes NP-hard on co-decomposition inputs. These results demonstrate how categorical constructions can enable efficient computation on exponentially compressed structures.

arXiv abstract · PDF

Complexity Theory and Algorithmic Metatheorems · primary corpus · published 2026-11-03T20:59:00Z
Andrew Krapivin, Benjamin Przybocki, Bernardo Subercaseaux
arXiv categories: cs.CC, cs.LO

We study the minimum number of clauses required to encode a boolean function into a CNF formula with auxiliary variables. Our main result is that if a boolean function can be evaluated in nondeterministic time $t$ (in the RAM model) with $m$ bits of advice such that at most $b$ bits of advice are accessed for each input, then it admits a CNF encoding with $\widetilde{O}(t + \sqrt{mb})$ clauses. This constitutes a nonuniform generalization of Robson's (TCS'91) variant of the Cook--Levin theorem, for which a na\"ive generalization would yield $\widetilde{O}(t+m)$ clauses; our applications leverage $b = o(m)$ to obtain significantly better bounds. Since preprocessed data structures can be modeled as computation with advice, our result allows us to translate space- and time-efficient data structures to compact CNF encodings. As an application, we derandomize a data structure of Larsen and Williams (SODA'17) to show that every $k$-CNF function on $n$ inputs can be encoded with $n^k/2^{\Omega_k(\sqrt{\lg n})}$ clauses. Notably, despite encoding a $k$-CNF function, the encoding itself necessarily contains clauses of unbounded width, since an information-theoretic argument shows that the minimum number of bounded-width clauses to encode such functions is $\Omega_k(n^{k}/\lg n)$ in the worst case. In general terms, our results imply that for a wide variety of NP-complete problems, one can reduce to CNF-SAT in a way that results in asymptotically fewer clauses than previously known methods.

arXiv abstract · PDF

Complexity Theory and Algorithmic Metatheorems · primary corpus · published 2026-11-04T17:20:29Z
Jan Dreier, Nikolas M\"ahlmann, Micha{\l} Pilipczuk, Szymon Toru\'nczyk
arXiv categories: cs.DM, cs.DS, cs.LO, math.CO, math.LO

A graph class $\mathcal{C}$ is monadically dependent if one cannot interpret all graphs in vertex-colored graphs from $\mathcal{C}$ using a fixed formula of first-order logic. We prove that every monadically dependent graph class has almost bounded merge-width, thereby confirming a conjecture of the first and the last author [STOC '25]. Our proof is algorithmic and the witnessing decompositions in the form of merge sequences can be computed in nearly-cubic time. This is a step towards the proof of fixed-parameter tractability of model checking first-order logic on monadically dependent graph classes, which is achieved in a companion paper.

arXiv abstract · PDF

Complexity Theory and Algorithmic Metatheorems · primary corpus · published 2026-11-05T01:01:49Z
S{\o}ren Riis
arXiv categories: cs.CC, cs.LO, math.LO

This paper proves asymptotically optimal linear degree lower bounds for Nullstellensatz and Polynomial Calculus, yielding a four-way polynomial-versus-exponential proof-size classification for uniform polynomial consequences over fields of positive characteristic. The size bounds use full, explicit coefficient lists, including zeros. Apart from a fixed finite initial range, exactly one of four cases occurs: $\mathrm T_1$, bounded degree; $\mathrm T_2$, degree at least linear in the universe size $n$; $\mathrm T_3$, constant degree on some residue classes and at least linear degree on the others; or $\mathrm T_4$, infinitely many recurring finite degrees, with bounded-degree subsequences and finite $\Omega(n)$ peaks at arbitrarily large sizes. Thus the size patterns are polynomial bounds, exponential lower bounds, a periodic mixture, or polynomial subsequences with finite exponential peaks, respectively. Underivable targets have degree $\infty$, and both proof systems assign the same type. The result strengthens my 2008--2009 refutation classification and extends it to uniform consequences. The proof uses degree-preserving lifting with onset and period bounds linear in the degree. A common $p$-adic hardness spectrum describes the four types topologically. Distinguishing any two types is undecidable already for refutations. The linear degree bounds, four-way classification and pairwise undecidability results have been formalised and verified in Lean. The Lean formalisation, verification records and an accompanying tutorial are available in the supporting materials (https://doi.org/10.5281/zenodo.23965838).

arXiv abstract · PDF

Complexity Theory and Algorithmic Metatheorems · primary corpus · published 2026-11-05T15:04:35Z
Jan Dreier, Nikolas M\"ahlmann, Szymon Toru\'nczyk
arXiv categories: cs.LO, cs.DM, cs.DS, math.CO, math.LO

Monadically dependent graph classes are those in which first-order logic cannot encode all graphs. They include all nowhere dense classes and all classes of bounded twin-width. We show that first-order model checking is fixed-parameter tractable on every monadically dependent graph class. Together with the known hardness result for hereditary classes that are not monadically dependent, this gives a complete characterization of the hereditary graph classes with fixed-parameter tractable first-order model checking. This resolves a central open problem in algorithmic model theory. Our proof combines ideas from structural graph theory (graph decompositions), finite model theory (locality of first-order logic), and model theory (counting types). In particular, we show that in monadically dependent classes, tuples of fixed length have only $|U|^{O(1)}$ types of fixed quantifier rank over any set of parameters $U$.

arXiv abstract · PDF

Complexity Theory and Algorithmic Metatheorems · primary corpus · published 2026-11-06T15:43:30Z
Eduardo Skapinakis
arXiv categories: cs.CC, cs.LO

We introduce new notions of reducibility for monotone classes and show that a monotone version of Circuit Satisfiability and the Hamiltonian Cycle Problem are complete for $mNP$, even under positive reductions (which are not the same as monotone reductions). If this holds for all (monotone) $mNP$-complete problems - that they are also so complete for $mNP$ -, then $P\neq NP$. We introduce positive models of relativized computation and show that the separation $posP\subsetneq mNP$ does not relativize, even when oracles are restricted to monotone sets. Yet, there is a (weak) diagonalization proof that $posP\subsetneq mNP$.

arXiv abstract · PDF

Complexity Theory and Algorithmic Metatheorems · primary corpus · published 2026-11-07T13:05:30Z
Melissa Antonelli, Marcel Ertel, Eduardo Skapinakis
arXiv categories: cs.LO

Applicative theories offer a proof-theoretic framework for studying complexity. In this paper, we introduce a family of applicative theories to characterize classes ranging from constant-depth circuits to polynomial space. Our approach relies on a simple axiom scheme, the small variations of which allows to capture various forms of counting and alternation. This leads to highly uniform results. When applied on notation, the scheme captures bit counting, yielding a characterization of the functions computable by constant-depth, polynomial-size threshold circuits ($\textbf{FTC}^0$); when applied lexicographically, it allows for the counting of accepting computations, yielding a characterization of the functions in the counting hierarchy ($\textbf{FCH}$). Increasing the logical complexity of the induction formulas allowed in the scheme, we obtain characterizations of the functions computable by bounded Boolean circuits of logarithmic-depth and polynomial-size ($\textbf{FNC}^1$) and of the functions computable in polynomial space ($\textbf{FPSPACE}$). The latter characterization solves an open problem in the field. Finally, we investigate separation results. While it is unknown whether $\textbf{FNC}^1$ and $\textbf{FCH}$ are different, there is an oracle relative to which (relativized) $\textbf{FNC}^1$ is strictly contained in (relativized) $\textbf{FCH}$. We use this fact to separate the theories characterizing them, by exploring their ability to represent higher-order functionals.

arXiv abstract · PDF

Complexity Theory and Algorithmic Metatheorems · primary corpus · published 2026-11-07T16:39:50Z
Alexis de Colnet, Stefan Szeider
arXiv categories: cs.AI, cs.LO

Tree decision diagrams (TDDs), recently introduced by Capelli et al. (SAT 2026), are representations of Boolean functions. They generalize OBDDs by replacing variable orders with vtrees. The width of a TDD counts the distinct subfunctions across each vtree cut. Counting subfunctions is blind to linear structure. We introduce algebraic tree decision diagrams (ATDDs) by replacing this count with the rank of the cut matrix. The maximum of these ranks over all cuts, the factor rank, is exactly the width of the ATDD. Every TDD can be converted into an ATDD of no greater width. An ATDD is a tree tensor network in canonical form. ATDDs are exponentially more succinct than TDDs, and quasi-polynomially more succinct than structured deterministic DNNFs. Our main result is that this gain in succinctness does not cost canonicity. ATDDs are the first strict canonical form for a rank-based representation over arbitrary vtrees. For each function and vtree there is exactly one ATDD, over the rationals and without any genericity assumption. The canonicity admits a local characterization. Whether a tree tensor network is the ATDD of the Boolean function it computes can be checked in polynomial time from its tensors alone. Equivalence checking becomes a test of syntactic equality. The operation set includes polynomial-time model counting, weighted model counting, and a test whether a tree tensor network represents a Boolean function. Capelli et al. asked for the complexity of changing the vtree of a TDD and suggested local vtree changes. We answer the question. After a rotation of the vtree at one node, the new ATDD differs from the old one in two tensors only. Vtree change runs in output-polynomial time both for TDDs and for ATDDs. We formalize and verify our core results in Lean. We provide a prototype implementation of TDD and ATDD compilers as a first empirical validation.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-11-03T06:03:41Z
Xiaoyang Liu
arXiv categories: cs.CC, cs.LO

A closed path can return to its starting point while analytic continuation reaches another branch. We construct a finite computational calculus in which retained logarithmic branches supply memory, analytic observations select operations, and descent through a covering exposes deeper memory. Three branch coordinates suffice, and every finite observation uses the same cubic power covering. Each program defines a globally real analytic return map whose integer-lattice execution is realized by actual path lifting. Our first theorem simulates every finite-alphabet, finite-control Post--Turing machine, preserving complete configurations, halting, and divergence. Our second theorem identifies the partial numeric functions of the calculus, under fixed primitive-recursive input and output maps, with exactly the partial recursive functions. Deleting descent leaves a Forward language with a syntax-derived finite observation quotient and a primitive-recursive halting predicate. This yields a strict separation within the calculus and identifies access to deeper memory as its decisive additional operation. The constructions and semantic correspondences are formalized in Lean 4 with Mathlib.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-11-04T10:36:39Z
Sergey Salishev
arXiv categories: cs.CC, cs.AI, cs.FL, math.LO

The halting problem asks whether a program eventually halts, with unrestricted resources. Engineering systems instead certify bounded halting: given a program, an input, and a step budget T, decide whether the program halts within T steps. This paper studies two of its uses. First, it defines an exact finite-budget problem, placing the simulated program and the checker on the same unit-cost timescale, so the checker can be embedded in an adversarial program. A diagonal argument with explicit additive overhead shows that no fixed deterministic checker decides every instance within any fixed fraction of T below one, for large T. In the nondeterministic case, T bounds the branch depth allowed for a stable observable decision. Second, bounded-halting instances give adversarial tests for finitary universality, since a universal model must support arbitrary finite computations as T grows. The tests check resource growth with T, the absence of a fixed deliberation bound, and later access to intermediate data. They separate a fixed model with extendable external resources, a model family that grows with T, and a larger system built around a fixed component. For machine-learning systems, this identifies the resource growth a universality claim assumes and whether it fails for deployed models.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-11-04T12:43:01Z
Laurent Bienvenu, Noam Greenberg, Ludovic Patey, Dan Turetsky
arXiv categories: math.LO

We study the relation between the existence of escaping (or hyperimmune) functions and weak 1-genericity using computability over ideals. We prove in particular the existence of an $\mathcal{I}$-escaping function which does not $\mathcal{I}$-compute any weakly $\mathcal{I}$-generic set whenever $\mathcal{I}$ is a countable Turing ideal closed under the existence of diagonally non-computable functions.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-11-05T02:07:27Z
Mohammad Golshani
arXiv categories: math.LO

We give a true $\Pi^0_1$ sentence $\varphi$ which is independent of Peano Arithmetic. Moreover, if $\widehat{\phi}$ denotes its interpretation on $\omega$ as a sentence of set theory, then $\widehat{\phi}$ is a $\Pi^0_1$ sentence independent of ZFC.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-11-05T02:22:16Z
Naoto Shiraishi
arXiv categories: quant-ph, cond-mat.stat-mech, cond-mat.str-el, cs.LO

The frustration-free property is valuable in quantum many-body systems, which states that its ground states simultaneously minimize all local interaction terms, even when these terms act on overlapping degrees of freedom. Prominent examples include the AKLT model and Kitaev's toric code model, which serve as paradigmatic models of symmetry-protected topological phases and topological order, respectively. A fundamental question is whether a given Hamiltonian is frustration-free for all system sizes. Here we establish two seemingly contradictory results concerning this decision problem. First, we prove that frustration-freeness is decidable for any fixed local Hilbert space dimension. Specifically, there exists a finite, Hamiltonian-independent system-size cutoff such that frustration-freeness at this cutoff size guarantees frustration-freeness at all system sizes. Second, on the other hand, we also show that there exists a frustration-free Hamiltonian whose frustration-freeness cannot be proved within the standard axioms of mathematics (ZFC). We reconcile these seemingly contradictory results by showing that the cutoff, although finite for each local Hilbert space dimension, is uncomputable as a function of that dimension. Our findings reveal an unexpected fundamental distinction between decidability and provability arising in quantum many-body physics.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-11-05T17:15:44Z
Jean Abou Samra, David A. Madore
arXiv categories: math.LO, cs.LO

The Arthur-Nimue-Merlin degrees are a generalization of the Turing degrees introduced by Kihara as a tangible description of the partially ordered set of Lawvere-Tierney topologies on the effective topos (equivalently, subtoposes of the effective topos). They are defined in terms of a three-player game that introduces both angelic and demonic non-determinism into oracle queries. We construct an order embedding of the Turing degrees with their order reversed into the Arthur-Nimue-Merlin degrees, whose image we call the "co-Turing degrees"; we then study the order relationship of these co-Turing degrees with the (naturally embedded) Turing degrees within the Arthur-Nimue-Merlin degrees. This is a short version of arXiv:2603.19946, focused on the main results.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-11-07T05:07:46Z
Seth Douglas, Nidhal Mghirbi
arXiv categories: quant-ph, math.LO, math.OA

Given a finite nonlocal game, can the players win with certainty? We prove that the existence of a perfect normal spatial strategy is $\Sigma^0_2$-complete, even when restricted to games of value one, so it cannot be decided even with an oracle for the halting problem. This is strictly harder than perfect play in the finite-dimensional and commuting-operator models, which are $\Sigma^0_1$-complete and $\Pi^0_1$-complete. Within the commuting model, the existence of a perfect normal strategy with a finite or semifinite von Neumann host is $\Sigma^0_2$-complete, whereas for every fixed type $\mathrm{III}_\lambda$ subtype it has the same $\Pi^0_1$-complete language as unrestricted commuting play. A trace thus costs one existential number quantifier: the hardness constructions force every perfect strategy to choose a finite clock period or a finite tree depth. Spatial $\Sigma^0_2$-completeness also holds when finite entanglement entropy is required, and both forms are formally verified in Lean. For every computable $0<\alpha<1$, perfect spatial play with $\mathrm{Tr}\,h^\alpha<\infty$ for the reduced density $h$ is $\Sigma^0_2$-complete as well; these conditions form a strict ladder between finite rank and finite entropy. We also prove $\Sigma^0_2$-completeness for one-shot zero-error communication with normal entanglement, and construct a finite channel with zero-error codes of a given size each of which needs infinite entanglement entropy.

arXiv abstract · PDF

Nonclassical Logics and Proof Theory · primary corpus · published 2026-11-03T12:26:56Z
Stefano Berardi, Ugo de'Liguoro, Daniel Osorio-Valencia
arXiv categories: cs.LO

We formulate the global trace condition, GTC, for cyclic proofs as a particular case of the size-change termination condition, or SCT. We express cyclic proofs through a variant of size-change graphs, called transition graphs, whose edges are labelled by (finite) bipartite relations. We show that injective transition graphs suffice to encode cyclic pre-proofs for a variant of Brotherston and Simpson's sequent calculus with inductive definitions. The injectivity of transition graphs corresponds to restricting SCT to fan-in-free graphs. Then we prove that an essentially weaker condition implies SCT in this case, and hence GTC.

arXiv abstract · PDF

Nonclassical Logics and Proof Theory · primary corpus · published 2026-11-03T21:40:50Z
Olivia Aubone, Jos\'e Iovino
arXiv categories: math.LO

We prove that every obstruction to noncontextual hidden variables in quantum mechanics is finite, including the obstructions that rest on Gleason's hypothesis of countable additivity. Since Kochen and Specker, such obstructions have been certified by finite configurations of rays, at the level of propositional logic: once a configuration is fixed, the obstruction is the inconsistency of finitely many Boolean constraints. Compactness, the source of these configurations, cannot reach the obstructions that rest on countable additivity: in infinite dimension the finite-dimensional events admit a finitely additive noncontextual valuation, and countable additivity constrains infinitely many events at once. The tool is a theorem of infinitary real-valued logic that takes the place of compactness: every countable theory of closed conditions without models is refuted by a well-founded tree of finite contradictions, given by the winning strategies of a model existence game. Quantum probability is axiomatized by such a theory, whose standard models are exactly those of Gleason's theorem. In the strategy we construct, a hypothetical noncontextual measure is not refuted by a configuration fixed in advance: through countable additivity, the measure itself selects the four-dimensional subspace in which the measure fails. The same logic defines, in the standard models, exactly the $\sigma$-projective sets of probabilities. Statements about $\sigma$-projective sets often go beyond ZFC, as the measurability of all these sets does; our theorems are nevertheless proved in ZFC, since the only determinacy they use is that of open games.

arXiv abstract · PDF

Nonclassical Logics and Proof Theory · primary corpus · published 2026-11-04T00:50:34Z
Yifan Meng, Lili Shen, Dexue Zhang
arXiv categories: math.CT, math.GN, math.RA

We lift Mundici's equivalence between MV-algebras and abelian $\ell$-groups with a strong unit to the topological setting. To this end, we prove that, for every topological MV-algebra, the associated Mundici group can be endowed with a topology that extends the topology of the MV-algebra and makes it into an abelian topological $\ell$-group. Among such topologies there is a finest one; we identify this topology as the topological-group reflection of the bounded-stage final topology, and construct an explicit zero-neighbourhood base in terms of the original MV-algebra topology. Using this topology, we establish a topological Mundici adjunction that restricts to an equivalence between topological MV-algebras and Mundici-fine abelian topological $\ell$-groups with a strong unit. Here, Mundici-fine means that the group topology is the finest $\ell$-group extension of its unit-interval topology. We also identify extremal $\ell$-group extensions under additional hypotheses, and establish a quasitopological correspondence clarifying the distinction between separate and joint continuity.

arXiv abstract · PDF

Nonclassical Logics and Proof Theory · primary corpus · published 2026-11-04T04:17:52Z
Tomasz Kowalski, Katarzyna S{\l}omczy\'nska
arXiv categories: math.LO

We present an algebraic study of extensions of the implication--negation fragment $\mathrm{IPC}_{\to,\neg}$ of intuitionistic propositional logic. Such extensions by inference rules correspond to subquasivarieties of the variety $\var{Ho}$ of Hilbert algebras with zero. We describe the lattice of such extensions of $\mathrm{IPC}_{\to,\neg}$ by means of its generators: it is isomorphic to the lattice of upsets of a countable poset, and in particular it is completely distributive. Consequently, $\var{Ho}$ is not Q-universal, in contrast to several other varieties related to $\mathrm{IPC}$. Nevertheless, this lattice is very complex: at each suitably defined height it has intervals containing continuum many quasivarieties which are not varieties. To the best of our knowledge $\mathrm{IPC}_{\to,\neg}$ is the only natural fragment of intuitionistic logic known to combine a completely distributive lattice of extensions with continuum many non-axiomatic extensions.

arXiv abstract · PDF

Nonclassical Logics and Proof Theory · primary corpus · published 2026-11-05T12:29:00Z
Juan Manuel Cornejo, Andr\'es Gallardo, Paula Helt, Luiz Monteiro, Ignacio Viglizzo
arXiv categories: math.LO

${T}_n$-Heyting algebras form a subvariety of Heyting algebras and are characterized by the property that a chain of prime filters in such an algebra has at most $n-1$ elements. We study some basic properties of these algebras and determine the structure and number of elements of the free ${T}_n$-Heyting algebra with a finite number $r$ of free generators, $FT_n(r)$.

arXiv abstract · PDF

Nonclassical Logics and Proof Theory · primary corpus · published 2026-11-06T02:43:09Z
Jos\'e Iovino
arXiv categories: math.LO, math.FA, math.GN

The Stone-Weierstrass theorem obtains every continuous function on a compact space as a uniform limit of functions built from a separating family by finitely many operations, and Reggio proved the theorem equivalent to the Beth definability property of an infinitary equational logic. We extend both results beyond compactness: on every separable metric space, and in particular on every Polish space, every bounded uniformly continuous function is a uniform limit of functions built from countably many bounded separating functions by the connectives of infinitary real-valued logic, and an approximate Beth property of this logic is equivalent to the new theorem. The extension rests on a rule of syntax, which admits a countable supremum when its terms share an a priori bound and thereby makes the sentences define exactly the bounded Lipschitz functions, and on a model existence game that does the work of compactness in the proof of interpolation.

arXiv abstract · PDF

Nonclassical Logics and Proof Theory · primary corpus · published 2026-11-06T15:07:29Z
Stefano Bonzio, Gandolfo Vergottini, Nicol\`o Zamperlin
arXiv categories: math.LO

In this paper we continue the work started in [Bonzio & Zamperlin 2025] by investigating the algebraic semantics for modal external weak Kleene logics. In order to do so we study the global modal logics associated with the three-valued Kripke models introduced in the previous article, showing how these systems are algebraizable. We proceed by defining their algebraic counterparts, obtaining the classes of modal Bochvar and modal Halld\'{e}n algebras, whose structure theory we investigate via P\l onka sum decomposition. Of particular interested is the interaction of the modal operator with the homorphisms of the P\l onka decomposition. These results allow us to prove representation theorems for these expanded modal algebras in the style of the J\'onsson-Tarski representation for Boolean algebras with operators. As a consequence, we also obtain algebraic semnatics for the local modal logics from which the work originated.

arXiv abstract · PDF

Nonclassical Logics and Proof Theory · primary corpus · published 2026-11-06T15:33:13Z
Yanqiao Jia, Xueting Zhao, Yichuan Yang
arXiv categories: math.RA, math.DS, math.GN, math.LO

We establish a canonical topological lifting of Mundici equivalence, representing every topological MV-algebra as the unit interval of a topological $\ell$-group and extending the correspondence to a categorical adjunction. As applications, we give a direct group-theoretic proof of the equivalence of $T_0$ and $T_{3\frac12}$ and show that every topological MV-algebra is a retral space. We further extend the lifting to topological Riesz MV-algebras and identify the canonical topology with Wiweger's mixed topology under suitable assumptions, recovering the strict topology as a special case. Finally, we obtain a unit-interval formulation of Koopman representations for continuous-time dynamical systems.

arXiv abstract · PDF

Nonclassical Logics and Proof Theory · primary corpus · published 2026-11-06T16:23:19Z
Yanqiao Jia, Yichuan Yang
arXiv categories: math.RA, math.GN, math.LO

We prove that summability characterises precisely when a topological MV-algebra can be realized as the unit interval of a lattice-ordered topological abelian group, thereby providing a topological lifting of both Mundici equivalence and DiNola--Lettieri equivalence. Applications include a Birkhoff--Kakutani-type metrisation theorem, a second-countability criterion, and a topological extension of a key continuity lemma from the proof theory of first-order {\L}ukasiewicz logic---following Baaz--Metcalfe's hypersequent approach to approximate completenesss---and provides an $A$-valued topological semantics for the approximate strong completeness of~$\mathbf{G}\text{{\L}}\forall$, where $A$ ranges over summable topological MV-algebras.

arXiv abstract · PDF

Nonclassical Logics and Proof Theory · primary corpus · published 2026-11-08T07:27:35Z
Jakub Michaliszyn
arXiv categories: cs.LO

We study the decidability of modal satisfiability over classes of Kripke frames defined by universal first-order sentences. Although some such classes yield undecidable satisfiability problems, decidability is guaranteed for wide families of frame conditions, including universal Horn sentences and universal sentences implying transitivity. A more than decade-old open problem asks a natural question: can decidable and undecidable cases be distinguished algorithmically? We prove that this is impossible, already for equality-free universal frame conditions over a single binary relation. More precisely, there is no algorithm that, given such a condition, decides whether its associated local modal satisfiability problem is decidable. We first establish the result for conditions with equality and then eliminate equality by passing to quotients of worlds with identical incoming and outgoing edges.

arXiv abstract · PDF

Model Theory and Definable Structures · primary corpus · published 2026-11-03T17:32:21Z
Zixuan Zhu
arXiv categories: math.LO

In [Pil07], Pillay showed that every imaginary in a proper pair of algebraically closed fields is interalgebraic with an imaginary of a certain algebraic form. In this paper, we establish an analogue for lovely pairs of pseudofinite fields. After naming countably many constants, we prove that every imaginary in lovely pairs of pseudofinite fields is interalgebraic with an imaginary of the same algebraic form as [Pil07] in the corresponding pairs of finite extensions of pseudofinite fields.

arXiv abstract · PDF

Model Theory and Definable Structures · primary corpus · published 2026-11-03T22:19:16Z
Carlos Mart\'inez-Ranero
arXiv categories: math.NT, math.LO

Let $K$ be a number field, let $S$ be a finite set of places of $K$ containing the archimedean places, and let $\mathcal{O}_{K,S}$ denote the ring of $S$-integers of $K$. We prove that multiplication is positive-existentially definable in $(\mathcal{O}_{K,S},0,1,+,\mid)$ if and only if the unit group $\mathcal{O}_{K,S}^\times$ is infinite. This extends a 1977 theorem of Lipshitz for rings of integers to rings of $S$-integers. One of the key ingredients is a uniform bound for unit equations due to Evertse, Schlickewei and Schmidt, which we use to recover multiplication on the unit group.

arXiv abstract · PDF

Model Theory and Definable Structures · primary corpus · published 2026-11-04T12:13:38Z
Marcelo Fortmann
arXiv categories: math.LO

We show that, over a valued field $K$ with $1$-h-minimal theory $\operatorname{Th}(K)$, two Cartesian products of balls must be equal up to translation and coordinate permutation in order for there to exist a definable surjective isometry between them. For this purpose, we introduce a notion of relative dimension for cuboids in $K^n$ that is computed combinatorially and relates to the notion of dimension for definable sets in Hensel minimal theories when $K$ has infinite residue field.

arXiv abstract · PDF

Model Theory and Definable Structures · primary corpus · published 2026-11-04T13:46:24Z
Matthias Aschenbrenner, Lou van den Dries, Joris van der Hoeven
arXiv categories: math.LO, math.RA

We describe the group of strongly additive automorphisms of the differential field $\mathbb T$ of transseries as a non-trivial semidirect product. We show that this group is torsion-free and has trivial center, and that many naturally arising differential subfields of $\mathbb T$ are definably closed in $\mathbb T$.

arXiv abstract · PDF

Model Theory and Definable Structures · primary corpus · published 2026-11-05T01:13:48Z
Rob Sullivan
arXiv categories: math.LO, math.CO

A $k$-hypertournament is a higher-arity generalisation of a tournament, consisting of a set together with an irreflexive $k$-ary relation such that the automorphism group of each substructure of size $k$ is the alternating group $\mathrm{A}_k$. We show that, for each $k \geq 3$, there are continuum-many non-isomorphic countable ultrahomogeneous $k$-hypertournaments, answering a question of Cherlin.

arXiv abstract · PDF

Model Theory and Definable Structures · primary corpus · published 2026-11-05T16:00:54Z
Alessandro Vegnuti
arXiv categories: math.LO

Using techniques from model theory, we prove analogues of Rado's and S\'ark\"ozy's theorems on solutions to polynomial equations in dense sets of definable groups and fields equipped with well-behaved measures. As a special case, we adapt our results to pseudofinite structures, to deduce non-qualitative asymptotic results.

arXiv abstract · PDF

Model Theory and Definable Structures · primary corpus · published 2026-11-06T17:34:58Z
Daniel Max Hoffmann
arXiv categories: math.LO

Pym's theorem [Pym62] states that a regular Borel probability measure on a locally compact group is idempotent if and only if it is the normalized Haar measure of a compact subgroup. The Idempotent Measure Conjecture, the definable-group counterpart of [GHK25, Conjecture (A)], proposes an analogous characterization: a global fim Keisler measure on a definable group is idempotent if and only if it is the unique global Keisler measure concentrating on a type-definable subgroup and invariant under translation by elements of that subgroup. We prove this conjecture for virtually solvable definable groups in arbitrary theories. More generally, we establish it for definable groups admitting a finite series of definable normal subgroups whose successive quotients are either virtually solvable or stably embedded with stable induced structure. Finally, we disprove [GHK25, Conjecture (A)] in its automorphism-group formulation in the theory of dense linear orders without endpoints.

arXiv abstract · PDF

Model Theory and Definable Structures · primary corpus · published 2026-11-08T14:18:56Z
Paola D'Aquino, Sebastian Eterovi\'c
arXiv categories: math.NT, math.LO

We tackle Shapiro's conjecture for exponential polynomials where the coefficients are polynomials, and show that it follows from Schanuel's conjecture. More concretely, given exponential polynomials $f$ and $g$ with infinitely many common zeros, we show that Schanuel's conjecture implies that there is an exponential polynomial $h$ vanishing precisely at all the common zeros of $f$ and $g$.

arXiv abstract · PDF

Model Theory and Definable Structures · primary corpus · published 2026-11-08T18:31:09Z
Amador Martin-Pizarro, Daniel Palac\'in
arXiv categories: math.LO, math.CO

We prove versions of (variations of) Erd\H{o}s sumset and $B+B+t$ conjectures asked by Kra, Moreira, Richter and Robertson for semigroups equipped with pairwise commuting non-algebraic definable Keisler measures. Our results use model-theoretic methods involving the existence of \emph{many} coheir independent tuples in every definable relation of positive density.

arXiv abstract · PDF

Model Theory and Definable Structures · primary corpus · published 2026-11-08T20:17:58Z
John Harris
arXiv categories: math.PR, math.LO

We extend the discrete uniform, hypergeometric and binomial distributions to the surreal numbers, allowing infinitely many outcomes, chips and trials. A uniform distribution on $\mathbb{N}$ gives each outcome probability $1/\omega$; on the eventually periodic sets we define the needed sizes explicitly, obtaining a probability that is regular and strictly monotone. For an urn with infinitely many chips and finitely many draws, the hypergeometric distribution is within an infinitesimal of the binomial. With infinitely many trials, and under a hypothesis on factorials of omnific integers that we show can be satisfied, we prove a surreal de~Moivre--Laplace theorem, and we show that the hypergeometric distribution with infinitely many draws is locally normal with a finite-population correction. Near its center, it is relatively close to the binomial distribution if and only if the sampling fraction is infinitesimal, an exact form of a familiar rule of thumb. For rare successes we prove, without any hypothesis on factorials, a surreal Poisson limit theorem and describe urns with finitely many red chips, where the binomial approximation fails beyond the first success.

arXiv abstract · PDF

Large Cardinals Forcing and Cardinal Invariants · primary corpus · published 2026-11-02T08:20:51Z
Sviatoslav V. Dzhenzher
arXiv categories: math.FA, math.LO

We establish an extension theorem for kappa-additive probability measures, where kappa is an arbitrary uncountable cardinal. Starting from a <kappa-algebra, we define an outer measure using coverings of cardinality at most kappa and characterise measurable sets by approximation in outer measure of symmetric differences. We prove that these sets form a kappa-algebra carrying a complete kappa-additive extension of the original measure. The extension is unique on the generated kappa-algebra, and its completion is the minimal domain admitting a complete kappa-additive extension. We also establish attainment of the covering infimum and show why the closure assumption on the initial algebra is essential. Examples include a strict extension of classical Lebesgue measure under the additional hypothesis add N = aleph_1 < cov N.

arXiv abstract · PDF

Large Cardinals Forcing and Cardinal Invariants · primary corpus · published 2026-11-03T05:44:48Z
Hannes Jakob, John Krueger
arXiv categories: math.LO

We introduce a combinatorial principle $\textsf{SC}(\kappa)$, for any regular cardinal $\kappa \ge \omega_2$, which asserts the existence of a family $\mathcal{Y} \subseteq [H(\kappa)]^\omega$ of elementary substructures of $H(\kappa)$ which is closed under finite intersections and satisfies that for stationarily many $N \in \mathcal{Y}$, if $M \in \mathcal{Y}$ and $M \cap \omega_1 < N \cap \omega_1$, then $M \cap N \cap \kappa \in N$. We explore the idea of defining forcings with side conditions consisting of finite subsets of such a family $\mathcal{Y}$. If $\textsf{SC}(\omega_2)$ holds, then there exists a thin stationary subset of $[\omega_2]^\omega$, and consequently $\textsf{SC}(\omega_2)$ is independent of ZFC. Assuming that $\mu$ is a Mahlo cardinal, the L\'{e}vy collapse $\mathrm{Col}(\omega,<\mu)$ forces that $\textsf{SC}(\kappa)$ holds for all regular cardinals $\kappa \ge \omega_2$. Local instances of $\textsf{SC}$ can be forced using matrices of models or derived as consequences of square principles. We apply the principle $\textsf{SC}$ to define two kinds of forcings: a streamlined version of a strongly proper collapse, and a forcing which is strongly proper on a stationary set and adds arbitrarily many Baumgartner clubs. Finally, we prove two consistency results using forcings derived from $\textsf{SC}$ related to Aronszajn trees, the guessing model principle, strong failures of club guessing, and the higher dominating number.

arXiv abstract · PDF

Large Cardinals Forcing and Cardinal Invariants · primary corpus · published 2026-11-03T13:52:04Z
Evgenii Reznichenko
arXiv categories: math.GN, math.FA, math.LO

A space is ESLC if it contains neither an $S$-space nor an $L$-space, and NFS is the class of spaces containing no free sequences of length $\omega_1$. We prove that under $\mathrm{MA}(\omega_1)$, if all finite powers of $X$ belong to NFS, then $C_p(X)^\omega$ is ESLC; thus, for subspaces of $C_p(X)$, hereditary Lindel\"ofness, hereditary separability and countable spread coincide. This is derived from a dual form of a theorem of Todor\v{c}evi\'c. A Lindel\"of $\Sigma$-space belongs to NFS if and only if its compact subspaces have countable tightness. Hence $C_p(X)$ contains no $L$-spaces if $X$ is a Lindel\"of $\Sigma$-space of countable tightness and $\mathrm{MA}(\omega_1)$ holds, or if $X$ is any Lindel\"of $\Sigma$-space and PFA holds. Under $\mathrm{MA}(\omega_1)$, all iterated function spaces of Corson compact spaces are ESLC, and in ZFC the space $C_p(X,\{0,1\})$ is ESLC for every zero-dimensional Corson compact space $X$.

arXiv abstract · PDF

Large Cardinals Forcing and Cardinal Invariants · primary corpus · published 2026-11-03T14:21:57Z
Gervasio Figueroa, Joel Kuperman, Pedro S\'anchez Terraf
arXiv categories: math.LO

We prove that there is no sequence $\{ X_n \}_{n\in\omega}$ such that for all $n$, there is an injection from $\mathcal{P}(X_{n+1})$ to $X_n$ under a restricted set of axioms that conforms to the "working mathematician's" intuition (excluding Choice, Replacement, and Foundation). We also show such a sequence cannot be defined using a formula either. More precisely, it is inconsistent with Zermelo set theory minus Infinity to have a formula $\Phi(\cdot,\cdot)$ such that for each $n\in\omega$ there are $X$ and $Y$ with $\Phi(n,X)$, $\Phi(n+1,Y)$, and $\mathcal{P}(Y)$ being injectable into $X$. We finally show that the theorem fails if we allow infinitely many definitions, one for each term of the sequence, by using Hamkins, Linetsky, and Reitz's pointwise definable extensions of countable models of ZFC.

arXiv abstract · PDF

Large Cardinals Forcing and Cardinal Invariants · primary corpus · published 2026-11-03T16:19:53Z
Hope Duncan, Gabriel Goldberg, Asaf Karagila
arXiv categories: math.LO

We study the relationship between large cardinals and Blass' Small Violation of Choice ($\mathsf{SVC}$), which states that the Axiom of Choice holds in a set-generic extension of the universe. Our main theorem is that in the presence of a supercompact cardinal, either the Axiom of Choice fails significantly, or else $\mathsf{SVC}$ holds in $L(\mathcal P(\mathrm{Ord}))$. We show that a supercompact is not strong enough to reflect $\mathsf{SVC}$, while an extendible cardinal is. If we assume Usuba's Lo\'s Property holds for the supercompact, then we can outright derive $\mathsf{SVC}$ in the universe.

arXiv abstract · PDF

Large Cardinals Forcing and Cardinal Invariants · primary corpus · published 2026-11-03T16:49:01Z
Victor Torres-Perez, Liuzhen Wu
arXiv categories: math.LO

We prove that the $\mathrm{P}$-ideal dichotomy implies the negation of the square principle $\square(\lambda, \omega)$ for every regular cardinal $\lambda\geq\omega_2$.

arXiv abstract · PDF

Large Cardinals Forcing and Cardinal Invariants · primary corpus · published 2026-11-04T06:37:01Z
Farmer Schlutzenberg, Connor Watson
arXiv categories: math.LO

For a cone of reals $x$, the reals of $\mathrm{HOD}^{L[x]}$ are precisely the reals in $Q_3$, or equivalently, the set of reals in $M_1$, the minimal proper class mouse with a Woodin cardinal. We show that if $z$ is any real coding $M_1|\delta^{+M_1}$, then $z$ is the base of such a cone (so $M_1^{\#}$ is such a base). We also establish a kind of optimality for this result, by identifying a real $x$ such that $M_1\subseteq L[x]$ but $\mathbb{R}\cap\mathrm{HOD}^{L[x]}\not\subseteq M_1$, although there is a base for the cone in a generic extension of $L[x]$. We prove an analogous result for the reals of $\mathrm{HOD}^{M_{n}(x)}$ for even $n$, as well as an analogous optimality result which holds for all $n$.

arXiv abstract · PDF

Large Cardinals Forcing and Cardinal Invariants · primary corpus · published 2026-11-04T10:47:09Z
Alexander V. Osipov, Anton E. Lipin
arXiv categories: math.LO, math.GN

Under $\mathfrak p=\mathfrak c$, Cantor space contains a weak $\lambda$-set that is not a $\lambda$-set. This answers the consistency question of de Oliveira Rodrigues, dos Santos Ronchim, and Szeptycki. The hypothesis $\mathfrak p=\mathfrak c$ is compatible with the failure of the continuum hypothesis. The construction combines the finite-unions form of Hindman's theorem with Bell's characterization of $\mathfrak p$ in terms of $\sigma$-centered forcing. The increasing enumerations of the infinite members of the constructed space form an unbounded family under eventual domination. This makes the countable set of finite subsets of $\omega$ a witness to the failure of the $\lambda$-property.

arXiv abstract · PDF

Large Cardinals Forcing and Cardinal Invariants · primary corpus · published 2026-11-05T14:28:57Z
Thilo Weinert
arXiv categories: math.LO, math.CO

We prove equivalences of asymmetric partition relations involving natural numbers and products of weakly compact cardinals $\kappa$, infinite cardinals $\lambda<\kappa$ and natural numbers to certain classes of finitary problems in the theory of edge-coloured digraphs. We are able to determine three classes of Ramsey numbers exactly, typical examples in these classes are $r(\omega^2 2, 3)$, $r(\kappa\lambda 2, 3)$ and $r(\kappa\lambda 3, 3)$. We moreover provide general upper bounds for $r(\omega^2 m, 3)$ and $r(\kappa\lambda m, n)$.

arXiv abstract · PDF

Large Cardinals Forcing and Cardinal Invariants · primary corpus · published 2026-11-07T23:54:08Z
C\'esar Ismael Corral Rojas, Vinicius de Oliveira Rodrigues, Victor dos Santos Ronchim
arXiv categories: math.LO, math.GN

We determine the least cardinality of a set of reals that is not a weak $\lambda$-set, proving that it is $\max\{\mathfrak b,\mathfrak s\}$, where $\mathfrak b$ and $\mathfrak s$ are the bounding and splitting numbers. We prove that if $\mathfrak s<\mathfrak b$, then every first countable weak $\lambda$-space is a $\lambda$-space. We also show, relative to the consistency of $\mathsf{ZFC}$, that the existence of a weak $\lambda$-set that is not a $\lambda$-set is independent of $\mathsf{ZFC}+\mathfrak b=\mathfrak s$. In particular, we show that in the model obtained by adding $\omega_2$ Cohen reals over a model of $\mathsf{CH}$, every weak $\lambda$-set is a $\lambda$-set. Finally, we construct an almost-normal MAD family under $\mathsf{CH}$ and show that no such family exists under $\mathsf{OCA}_{\mathrm T}+\mathfrak{ap}>\omega_1$. Thus, the existence of an almost-normal MAD family is independent of $\mathsf{ZFC}$.

arXiv abstract · PDF

Descriptive Set Theory and Borel Combinatorics · primary corpus · published 2026-11-02T05:04:57Z
Ruijun Wang
arXiv categories: math.LO

We prove that the family of coset relations of $F_\sigma$ real linear subspaces of Banach space $\ell_1$ has no common upper bound among Borel equivalence relations in the sense of Borel reducibility. These relations are indexed by a well-founded tree. Consequently, on a Polish space, a universal $\Sigma^0_\alpha$ equivalence relation exists exactly when $\alpha=1$, and a universal $\Pi^0_\alpha$ equivalence relation exists exactly when $\alpha=1$ or $2$. This strengthens the earlier nonexistence theorem for a universal $F_\sigma$ equivalence relation. This also answers a question of Kanovei and Lyubetsky about universal equivalence relations in Borel classes.

arXiv abstract · PDF

Descriptive Set Theory and Borel Combinatorics · primary corpus · published 2026-11-02T15:45:23Z
Junhao Chen, Wei Dai
arXiv categories: math.LO

The 1-2-3 Conjecture asserts that every finite graph without isolated edges admits edge weights from $\{1,2,3\}$ such that the sum function forms a vertex coloring. We study its Borel analogue for locally finite Borel graphs without isolated edges, proving that five weights suffice in general and four suffice for regular graphs. We obtain three weights for acyclic graphs admitting a Borel selection of a nonempty finite set of ends from each component. We also obtain $\mu$-measurable and Baire measurable vertex-coloring $3$-edge weightings from $3$-colorings of the same definability, under probability measure-preserving and Baire quasi-invariance conditions, respectively.

arXiv abstract · PDF

Descriptive Set Theory and Borel Combinatorics · primary corpus · published 2026-11-02T16:53:10Z
Adam Kwela
arXiv categories: math.LO

An ideal $\mathcal{I}$ on $\omega$ is called Farah if there are hereditary closed subsets $C_n$ of $\mathcal{P}(\omega)$, for $n\in\omega$, such that $\mathcal{I}=\{A\subseteq\omega:\ \forall_{n\in\omega}\ \exists_{k\in\omega}\ A\setminus k\in C_n\}$. Farah asked in [Trans. Amer. Math. Soc. 356 (2004), no. 6] if every $\mathbf{F_{\sigma\delta}}$ ideal is a Farah ideal. We show that this is false by providing both tall and non-tall counterexamples. Moreover, we show that there is an antichain in the sense of Kat\v{e}tov order of length $\continuum$ consisting of $\mathbf{F_{\sigma\delta}}$ non-Farah ideals. We also investigate a closely related problem concerning sets of ideal limit points. We show that if $\mathcal{I}$ is an $\mathbf{G_{\delta\sigma\delta}}$ ideal on $\omega$ and $x\in X^\omega$ is a sequence in an uncountable Polish space $X$, then \[ \Lambda_x(\mathcal{I})=\left\{p\in X:\ \exists_{A\notin\mathcal{I}}\ x\restriction A\text{ converges to }p\right\} \] is $\mathbf{F_{\sigma}}$. This answers [Top. App. 312 (2022)] (partially) and [J. Symb. Logic, DOI: 10.1017/jsl.2026.10181]. Earlier it was known to be true only in the case of Farah ideals.

arXiv abstract · PDF

Descriptive Set Theory and Borel Combinatorics · primary corpus · published 2026-11-03T02:01:53Z
Ruijun Wang
arXiv categories: math.LO

Friedman and Stanley asked whether an invariant Borel class of countable structures must be Borel complete whenever every countable level of their hierarchy reduces to it. We construct a counterexample in one fixed countable language. The structural counterexample and its principal supporting results have been formalized in Lean~4 and it is available on github.

arXiv abstract · PDF

Descriptive Set Theory and Borel Combinatorics · primary corpus · published 2026-11-06T16:41:04Z
Filippo Calderoni, Danae Rupp
arXiv categories: math.LO

In this paper we focus on rigidity in descriptive set theory. Building on cocycle superrigidity results of Popa, Furman and Ioana, we prove rigidity in the purely Borel context for the orbit equivalence relations arising from the shift actions and translation actions of lattices in semisimple Lie groups with higher rank. Our results sharpen work of Adams and Kechris.

arXiv abstract · PDF

Descriptive Set Theory and Borel Combinatorics · primary corpus · published 2026-11-08T21:11:04Z
D\'aniel Heged\H{u}s, Benedek Kov\'acs
arXiv categories: math.CO, math.LO

We study infinite hat-guessing games indexed by linearly ordered sets $S\subseteq\mathbb R$, where players guess sequentially using information determined by the order. While well-ordered standing sets admit the naive, recursive definition of play, we found a surprising example showing that this approach fails for non-well-ordered ones, where local decision rules do not determine a unique global outcome. By requiring uniqueness of play, we aim to provide a natural framework for hat-guessing games on arbitrary standing sets. For the classical visibility model, it was previously known due to Glivick\'y that at most one incorrect guess can be guaranteed when $S$ is well-ordered. We prove the same result for backwards well-ordered sets, even in the case when $S$ has no first element. In the full-visibility version of the game, Glivick\'y proved that at most one incorrect guess can be guaranteed if the standing set has a first element. We extend this result to arbitrary nonempty standing sets.

arXiv abstract · PDF

Derived Categories and Homological Algebra · primary corpus · published 2026-11-02T14:28:21Z
Shantanu Sardar
arXiv categories: math.RT, math.CT, math.RA

We introduce hammock coordinates to study the combinatorial structure of partial silting configurations in the bounded derived category of a derived-discrete algebra $\Lambda(r,n,m)$. By extracting exact integer inequalities from the Bobi\'nski--Gei\ss{}--Skowro\'nski Hom-hammock formula, we establish a closed-form criterion for pairwise partial silting both within any $\mathcal Z$-component and across distinct components. Using this coordinate framework, we establish three primary results. First, we prove the universal upper bound $|S| \le n+m$ on the cardinality of any partial silting configuration $S$ of $\mathcal Z$-objects ---both globally via Bongartz completion in the silting-discrete setting, and combinatorially within a single component via a $\Sigma^r$-invariant staircase argument. Second, we prove that this bound is universally sharp by constructing an explicit L-shaped partial silting configuration of size $n+m$ for every $\Lambda(r,n,m)$, alongside specialized diagonal configurations. Third, we show that the configuration lattice carries a faithful action of the cyclic group $\mathbb Z/g$ where $g = \gcd(r+m, n-r)$. We conclude by showing a structural obstruction to local determination: pairwise partial silting of consecutive objects in the lattice ordering does not imply global partial silting, due to the strict additivity of a coordinate defect along chains.

arXiv abstract · PDF

Derived Categories and Homological Algebra · primary corpus · published 2026-11-03T01:59:07Z
Thomas Rush Brown
arXiv categories: math.CT, math.AT

We construct an endofunctor on (small) simplicial sets which freely adjoins a zero object to a (small) infinity-category, as the co-cone construction freely adjoins a terminal object. We then prove that this endofunctor induces a left adjoint to the inclusion of the infinity-category of (small) pointed infinity-categories and morphisms that preserve zero objects into the infinity-category of (small) infinity-categories. This adjunction, in turn, leads to the definition of a coherent choice of nullhomotopies on a pointed infinity-category. A coherent choice of nullhomotopies is a non-canonical, coherent choice of "higher zeroes" on a pointed infinity-category, mirroring the obvious definition of higher zeroes on the differential graded nerve of a differential graded category of chain complexes over an additive category. We then show that coherent choices of nullhomotopies give an alternate characterization of fiber sequences in pointed infinity-categories, generalizing the 1-categorical definition of kernels in terms of morphisms that compose to zero.

arXiv abstract · PDF

Derived Categories and Homological Algebra · primary corpus · published 2026-11-03T05:08:54Z
Shengyong Pan
arXiv categories: math.RT, math.CT

Let $\La_1$ and $\La_2$ be finite-dimensional $\ta_2$-finite complex algebras of global dimension at most two. We prove that, if they are cluster equivalent, then they admit $\bbZ$-gradings for which the bounded derived categories of graded modules are triangle equivalent. The equivalence is not required to commute with the internal grading shifts. The proof uses common multigraded dg models, relative gradings on two-term silting objects, and covering quotients. We also consider tilting lifts of cluster-tilting objects with endomorphism algebras of global dimension at most two. In acyclic cluster type, the existence of such a lift for every cluster-tilting object implies piecewise heredity. We construct a counterexample without this assumption using a surface algebra associated with a one-holed torus.

arXiv abstract · PDF

Derived Categories and Homological Algebra · primary corpus · published 2026-11-03T11:14:27Z
Liangyu Zhu
arXiv categories: math.AC, math.CT, math.RA, math.RT

Let $R$ be a commutative noetherian ring. We ask whether complexes with finitely generated cohomology and a fixed support can be generated by relatively compact objects, using coproducts which exist in the half-bounded derived category. We prove that $\mathbf D^+_{\mathrm{fg},W}(R)=\operatorname{Loc}_{\mathrm{ex}}(\mathbf D^b_{\mathrm{fg},W}(R))$ whenever $W\subseteq\operatorname{Spec} R$ is specialization closed and has finite dimension. The same equality holds for every specialization-closed subset of $\operatorname{Spec} B$ when $B$ is a finite-type algebra over a noetherian domain $A$ of finite character and either $A$ or $B$ is regular. These equalities classify the thick Hom-submodules closed under existing coproducts. We also prove the corresponding bounded-above statement from the support results of Matsui--Takahashi. For an arbitrary noetherian ring, the bounded-below generation conjecture reduces to torsion complexes over quotient domains, with their support unchanged. Finally, over a regular noetherian domain of infinite dimension, we give a bounded-below object which is generated by bounded objects with the same support but has no bounded-below representative by finitely generated modules. The comparison functor from the bounded-below derived category of finite modules is therefore neither full nor essentially surjective.

arXiv abstract · PDF

Derived Categories and Homological Algebra · primary corpus · published 2026-11-03T17:31:11Z
Jan \v{S}\v{t}ov\'i\v{c}ek, Florian Tecklenburg
arXiv categories: math.CT, math.AC

We characterise the commutative rings of weak global dimension at most one whose derived categories can be stratified by the Balmer-Favi support theory. For such rings, this yields a bijective correspondence between the class of localising subcategories of the derived category, and the subsets of the Zariski spectrum. For a large class of rings of weak global dimension at most one including all valuation domains, this occurs if and only if the ring is locally strongly discrete, if and only if the Telescope conjecture holds, and if and only if the module category has Gabriel dimension. However, we also give an example of a valuation domain where all these conditions fail, and yet the residue fields generate its derived category and we can classify all the localising subcategories of $D(R)$. Additionally, in the same example, we show that the Balchin-Stevenson smashing support cannot stratify $D(R)$ either.

arXiv abstract · PDF

Derived Categories and Homological Algebra · primary corpus · published 2026-11-03T18:11:56Z
Tobias Barthel, Drew Heard, Beren Sanders, Changhan Zou
arXiv categories: math.CT, math.AC, math.AT

We study the tensor triangular geometry of derived categories of valuation domains, obtaining complete ring-theoretic characterizations of their main structural properties. In particular, although valuation domains are almost always non-noetherian, their derived categories always satisfy the local-to-global principle and hence the detection property. We establish precise criteria for homological detection, stratification, and homological stratification, revealing a clear hierarchy among these properties. Notably, we obtain examples of derived categories of commutative rings that are homologically stratified and satisfy the local-to-global principle, but are not stratified. We also determine when the category of modules over a valuation domain has Gabriel dimension, and use this to provide a negative answer to a question of Balchin, G\'omez and Stevenson. Overall, valuation domains provide a rich class of non-noetherian rings whose derived categories can be understood in considerable depth.

arXiv abstract · PDF

Derived Categories and Homological Algebra · primary corpus · published 2026-11-04T08:47:31Z
Hang Yuan
arXiv categories: math.AT, math.CT, math.QA

For a quiver $Q$, we introduce and study $Q$-operads (or operads over $Q$), defined as a special sort of $\mathbf{fc}$-multicategories or virtual double categories, in which the directions of the arrows of $Q$ encode the permitted input orderings. In this higher operadic framework, we construct the bar--cobar adjunction and develop a theory of Koszul duality and homotopy algebras, together with compatibility results under changes of quiver. We treat dg categories and their left modules, right modules, and bimodules as algebras over quiver-operads. We prove that these operads are Koszul and that their resolutions govern the corresponding $A_\infty$ categories and modules. We also categorify Sagave's notion of derived $A_\infty$ algebras and introduce modules over derived $A_\infty$ algebras and categories. Finally, we explain that restriction along a folding of quivers constructs diagonal $A_\infty$ bimodules, while extension along an inclusion of quivers realizes two-sided bar models of derived tensor products.

arXiv abstract · PDF

Derived Categories and Homological Algebra · primary corpus · published 2026-11-05T00:30:16Z
Hisato Matsukawa
arXiv categories: math.KT, math.AT, math.CT

We construct higher additive noncommutative motives of stable $(\infty,n)$-categories, extending the additive motives of Blumberg, Gepner, and Tabuada and the secondary theory of Mazel-Gee and Stern. We formulate a notion of exact sequences and establish the universal property of the resulting additive motives. We give two equivalent constructions: a localization of enriched presheaves and a weighted Waldhausen $S$-construction on complete exact flags. We then compute their Hom objects, obtaining ordinary K-theory at the first level and lower additive motives recursively at higher levels. Our results recover the classical and secondary theories, provide coherent multiplicative structures, and yield an endofunctor on the category of Stefanich rings. In short, higher motives are higher K-theory.

arXiv abstract · PDF

Derived Categories and Homological Algebra · primary corpus · published 2026-11-05T06:10:19Z
Jing He, Yixia Zhang
arXiv categories: math.CT

We construct an idempotent complete Frobenius exact category with an idempotent complete stable category in which a complete ideal cotorsion pair of object ideals induces a cotorsion pair of objects that fails to be complete. This gives a negative answer to the question of Fu, Guil Asensio, Herzog and Torrecillas under idempotent completeness. The construction uses a lemma on dense triangulated subcategories and an example of Bondarko and Sosnilo in which a weight structure fails to extend to the idempotent completion. The induced cotorsion pair is hereditary, and every object admits an ordinary precover from its left class and an ordinary preenvelope into its right class. We characterize which objects admit special precovers and which admit special preenvelopes.

arXiv abstract · PDF

Tensor Categories and Hopf Algebras · primary corpus · published 2026-11-03T12:17:49Z
Chongying Dong, Xiangyu Jiao, Feng Xu
arXiv categories: math.QA, math.CT, math.RT

Three constructions of vertex operator algebras realizing the Haagerup center were announced independently and almost simultaneously. The relations between these constructions are studied in this paper. The generators are expressed in a common lattice basis for $E_6\oplus A_2$. It is proved that the constructions of Riesen and Huang give isomorphic vertex operator algebras, and that this algebra and the algebra constructed by Jiao have isomorphic fixed point subalgebras under automorphisms of order two. The isomorphisms are given explicitly on generators. The common fixed point subalgebra contains the parafermion vertex operator algebras $K(\mathfrak{sl}_2,3)$ and $K(\mathfrak{sl}_2,13)$. A general rationality criterion for unitary vertex operator algebras is given in terms of positive linear combinations of conformal vectors and is applied to these constructions. The two vertex operator algebras are simple current extensions of the common fixed point subalgebra and have equivalent module categories as ribbon categories. The equivalence follows from decomposition with respect to a nondegenerate pointed subcategory with four simple objects in the module category of the common fixed point subalgebra. It is also proved that the conformal nets associated with these unitary vertex operator algebras are completely rational.

arXiv abstract · PDF

Tensor Categories and Hopf Algebras · primary corpus · published 2026-11-03T16:44:02Z
Alexey Gordienko, Maria Morozova
arXiv categories: math.RA, math.CT, math.QA

Using Mac Lane's PROPs, one can introduce multilinear polynomial identities that involve all the operations of a Hopf algebra: the (co)multiplication, the (co)unit and the antipode. We find bases for polynomial identities and calculate their codimensions for the Sweedler algebra, treating it first as an ordinary associative algebra over a field and second as a Hopf algebra.

arXiv abstract · PDF

Tensor Categories and Hopf Algebras · primary corpus · published 2026-11-06T02:41:54Z
Bowen Li
arXiv categories: math.QA, math.CT

Let $\C$ be an essentially small abelian rigid braided monoidal category. We prove a reflection theorem for Nichols algebras in $\Ind(\C)$ and show that tuples admitting all reflections define connected semi-Cartan graphs. As applications, we prove that a finite Nichols algebra has a generating object of length at most one in $PSU(2)_k$ for odd $k\ge3$, in $SU(2)_{4m}$ for $m\ge1$, and in the representation categories of the Virasoro minimal models $\mathcal M(2,p)$ for odd $p\ge5$. In all three families, we prove that every finite pre-Nichols algebra is a Nichols algebra.

arXiv abstract · PDF

Tensor Categories and Hopf Algebras · primary corpus · published 2026-11-06T12:00:21Z
Emzar Khmaladze, Manuel Ladra, David Quiroga, Brais Ramos P\'erez
arXiv categories: math.RA, math.CT

In this paper, we define a Drinfeld-type center for an associative crossed module and prove that it is canonically the internal category of an explicit crossed module constructed from Mac Lane's bimultiplications. The resulting center carries a canonical multiplicative lifting, which induces a natural strict braiding, establishing its correspondence to a braided crossed module. We also examine the relationship between this center and Huq's categorical center. Finally, we obtain a canonical comparison morphism with Pirashvili's center of Lie crossed modules via the (braided) Liezation functors, which preserves braidings under an injectivity condition.

arXiv abstract · PDF

Tensor Categories and Hopf Algebras · primary corpus · published 2026-11-07T01:39:16Z
Inna Entova, Daniel Sebbag
arXiv categories: math.CT

Let $\mathcal{D}$ be a finite tensor category with exactly one isomorphism class of simple objects which are non-invertible. Semisimple tensor categories $\mathcal{D}$ with this property are called near-group categories, and have been studied by Evans, Gannon, Siehler and others. In this paper, we study such categories in the non-semisimple setting, with the additional assumption that the non-invertible simple object is projective. Specifically, we consider the case when $\mathcal{D}$ admits a fiber functor and has a unique semisimple abelian block (in the general case that $\D$ is not semisimple). We describe the structure of such categories and their corresponding Hopf algebras, and construct examples of such categories with a cyclic Picard group. We obtain additional results when the Frobenius-Perron dimension of the unique non-invertible simple object is a prime number.

arXiv abstract · PDF

Tensor Categories and Hopf Algebras · primary corpus · published 2026-11-08T08:54:10Z
Andrew Schopieray, Yilong Wang, Zhiqiang Yu
arXiv categories: math.QA, math.CT

We study stretched near-group fusion categories over $\mathbb{C}$ of type $G+k|G|$ for abelian groups $G$ and positive integers $k$, describing the structure of the double including fusion rules, modular data, and Frobenius--Schur indicators under a variety of assumptions. For cyclic $G$, when enough invertible objects exist in the double, we describe all associated de-equivariantizations which connect the existence of stretched near-group fusion categories to the existence of other stretched quadratic categories. All of our results apply to the case $k=1$. In particular, the known existence of $C_{m^2}+m^2$ near-group categories for all positive integers $m$ implies the existence of Haagerup--Izumi fusion categories for all cyclic groups. As a further application, we provide a general conductor bound severely restricting the existence of stretched near-group categories, and for infinitely many abelian groups $G$ of square order, among them $C_4\times C_2^{2j}$ with $j\geq2$, we show that a near-group fusion category $G+k|G|$ exists if and only if $k=0$.

arXiv abstract · PDF

Categorical Algebra and Higher Structures · primary corpus · published 2026-11-02T14:59:56Z
Maria Manuel Clementino, James Richard Andrew Gray
arXiv categories: math.CT

We show that the category of morphisms of topological groups admits split extension classifiers and hence the category of topological groups admits normalizers. We give explicit descriptions of both normalizers and of split extension classifiers of morphisms of topological groups in terms of split extension classifiers of topological groups.

arXiv abstract · PDF

Categorical Algebra and Higher Structures · primary corpus · published 2026-11-02T18:16:12Z
J. Climent Vidal, E. Cosme Ll\'opez, R. Ruiz Mora, M. Vago Marzal
arXiv categories: math.CT

Higher-order many-sorted categorial algebras are many-sorted algebras whose carriers are strict higher-order categories and whose operations are higher-order functors. They admit a homogeneous and a heterogeneous presentation, both by partial algebras whose operation domains are given by existence equations. To relate these presentations and their dimensions, we introduce generalized hep-derivors between hierarchical equationally partial signatures. A generalized hep-derivor selects carriers by existence equations in one variable and interprets operation symbols by terms, with operation domains evaluated recursively in the transformed algebra. Every generalized hep-derivor induces a functor between categories of many-sorted partial algebras. The values of this functor satisfy the domain conditions wherever their operations are defined, and we characterize when the operations are defined exactly where these conditions hold. The functor induced by a composite receives a natural inclusion from the composite of the induced functors; this inclusion, which can be strict, makes the induced functors a normal lax indexed category. In finite dimensions, generalized hep-derivors realize graduation and unification as an equivalence between the homogeneous and heterogeneous presentations, and discretization as a left adjoint to truncation. In dimension $\omega$, we reconstruct the categories of $\omega$-categorial algebras as projective limits of their finite-dimensional truncations and obtain unification by a quotient construction; we also establish algebraic squares and compatibility with change of signature. Finally, for nonempty sets of sorts, we show that the finite-dimension condition in the homogeneous $\omega$-presentation is not axiomatizable by quasi-existence equations on its fixed signature.

arXiv abstract · PDF

Categorical Algebra and Higher Structures · primary corpus · published 2026-11-03T06:31:50Z
Promit Mukherjee
arXiv categories: math.RA, math.CO, math.CT, math.GR

Given a finitely aligned higher-rank $k$-graph $\Lambda$, Farthing, Muhly and Yeend (Semigroup Forum 2005) constructed an inverse semigroup $S_\Lambda$ to provide a groupoid model for the $C^*$-algebra of $\Lambda$. In this paper, we extend some of the existing results related to the semigroup structure of a graph inverse semigroup to the more general setting of the inverse semigroup $S_\Lambda$. We obtain geometric descriptions of the Green's relations on $S_\Lambda$, which effectively generalize the existing characterization of Green's relations on a graph inverse semigroup. We provide a simple and useful description of the Cuntz-Krieger ideal of the Booleanization of $S_\Lambda$ and, based on this, identify a certain $X$-to-join Booleanization of $S_\Lambda$, where the abstract and concrete Cuntz-Krieger relations agree. Besides the natural partial order, $S_\Lambda$ is also ordered by set-inclusion. This helps us to realize $S_\Lambda$ as a semigroup \emph{graded-ordered} by $\mathbb{Z}^k$ and, subsequently, gives rise to a full inverse subsemigroup $S_\Lambda^h$ of $S_\Lambda$, which is graded by $\mathbb{Z}^k$ in the usual sense. We show that the Kumjian-Pask algebra of $\Lambda$ is graded isomorphic to the quotient of the contracted semigroup algebra of $S_\Lambda^h$ by the tight ideal. In the final part of the paper, we show that a $k$-graph morphism $p:\Lambda_1\longrightarrow \Lambda_2$ that is injective and satisfies a certain path lifting property induces, in a natural way, an injective $0$-preserving semigroup homomorphism from $S_{\Lambda_1}$ to $S_{\Lambda_2}$. In view of this, we build a suitable categorical setup to conclude that the isomorphism established between the Kumjian-Pask algebra of $\Lambda$ and the tight ideal quotient of the semigroup algebra of $S_\Lambda^h$ is natural.

arXiv abstract · PDF

Categorical Algebra and Higher Structures · primary corpus · published 2026-11-05T12:33:14Z
Lior Yanovski
arXiv categories: math.AT, math.CT

This is the first part of a series of expository notes on homotopical and categorical algebra. It charts a course from ordinary algebraic structures such as monoids, groups, and rings to their various homotopy-coherent generalizations and equivariant versions. The emphasis is on the ideas that lead to and connect the constructions, as well as where and how they appear in nature.

arXiv abstract · PDF

Categorical Algebra and Higher Structures · primary corpus · published 2026-11-05T14:16:18Z
Philip Hackney, Joachim Kock, Jan Steinebrunner
arXiv categories: math.CT, math.AT, math.CO

Aguiar, Bergeron, and Sottile showed that the coalgebra of quasisymmetric functions is terminal among connected graded coalgebras with a zeta function. After developing the notions of gradings and zeta functions for decomposition spaces, we establish an objective homotopic version of this result. Namely, the decomposition space $Q$ of quasisymmetric functions is terminal: for any conservatively graded decomposition space $X$ with zeta function $F$, there is a unique graded ikeo-culf span $X \leftarrow W \rightarrow Q$ inducing $F$ from the special zeta function on $Q$. More generally, for gradings in any complete decomposition space $M$ with indecomposable identities, the terminal object is $J(M)$, the free decomposition space on the nondegenerate simplices of $M$; the quasisymmetric case is $Q=J(B\mathbb{N})$.

arXiv abstract · PDF

Categorical Algebra and Higher Structures · primary corpus · published 2026-11-06T07:51:39Z
Aowen Fan
arXiv categories: math.AT, math.CT

We introduce an $\infty$-categorical model of operad pairs and their associated bimonoidal categories. We study the related concepts such as cocartesian-cartesian operad pairs, algebra pairs and the Day convolution. Using the Day convolution for operad pairs, we can define distributive functors between a symmetric bimonoidal category and a cartesian closed monoidal category. As an application, we show that for a finite group $G$, the operadic distributive functors from $\mathrm{Span}(\mathsf{Fin}_G)$ to any cartesian closed monoidal category coincides with the distributive functors defined by the distributive diagram. Therefore, we show that the connective $G$-equivariant $\mathbb{E}_{\infty}$-ring spectra are equivalently the spectral $G$-Tambara functors.

arXiv abstract · PDF

Categorical Algebra and Higher Structures · primary corpus · published 2026-11-06T13:44:11Z
Logan Geenis, Manfred Hartl, Tim Van der Linden
arXiv categories: math.CT, math.RA

We characterise the two-step nilpotent varieties of algebras: the semi-abelian varieties in which all ternary cosmash products vanish. Just as abelian varieties are the categories of modules over a ring, two-step nilpotent varieties are exactly the categories of modules over a square ring in the sense of Baues, Hartl and Pirashvili. We construct the square ring explicitly from the full subcategory on the free algebras on one and two generators, and give complete proofs. As consequences we obtain a description of any two-step nilpotent variety by generators and relations, an intrinsic characterisation in terms of quadratic term operations, and an account of its abelian core and of the lower central series of its objects in terms of the square ring. Along the way, we associate with any commutative ring $R$ a square ring whose modules, the two-step nilpotent $R$-groups, extend Hall's nilpotent $R$-groups of class two from $2$-binomial rings to arbitrary rings of coefficients.

arXiv abstract · PDF

Categorical Algebra and Higher Structures · primary corpus · published 2026-11-06T16:59:34Z
Isaac Carcac\'ia-Campos
arXiv categories: math.AT, math.CT

Every connected homotopy type is the classifying space of a small category, but this general result gives little control over the categories involved. We study finite acyclic categorical models and measure their complexity by the number of objects. Our main tool is the sink lemma, which describes the addition of a sink as the attachment of a cone along an explicit map. Using it, we determine the minimum number of objects required to model spheres, bouquets of spheres, Moore spaces of cyclic groups, real projective spaces, and lens spaces. We also exhibit infinitely many pairwise non-isomorphic rigid minimal models of the sphere. To include spaces admitting no finite model, we introduce a truncated invariant measuring the minimum number of objects required for a finite acyclic category to approximate a space through degree n. Spreading a finite monoid over n+1 objects produces such a category with an n-connected map to the monoid's classifying space. For every nontrivial finite group, this bound is optimal, although its classifying space admits no finite acyclic model.

arXiv abstract · PDF

Categorical Algebra and Higher Structures · primary corpus · published 2026-11-07T15:36:49Z
Martin Markl, Dominik Trnka
arXiv categories: math.CT

We show that an additive category is abelian if and only if its functorial nerve is a double d\'ecalage of a pseudo-simplicial object in Cat. In this characterization, the canonical isomorphism between the image and coimage is encoded by a coherent pseudo-simplicial identity.

arXiv abstract · PDF

Categorical Algebra and Higher Structures · primary corpus · published 2026-11-08T07:00:19Z
Kishan Dayaram, Zurab Janelidze, Ronald Kerario
arXiv categories: math.CT, math.GR

By a $\textit{proximity subgroup}$ of a group $G$ we mean a norm $\nu$ on $G$ valued in a complete lattice $L$ equipped with a binary sum (an additive counterpart of a multiplicative structure). The idea is that the smaller the value $\nu(y)$ is, the closer $y\in G$ is to the subgroup of $G$ defined by the equation $\nu(x)=\bot$, where $\bot$ is the bottom element of $L$. We test whether this notion is a suitable substitute for the usual notion of a subgroup (recovered by taking $L=\{\bot,\top\}$ with join as the sum), by showing that the form of proximity subgroups is noetherian. Intuitively, this means that proximity subgroups are as well suited for formulating and proving isomorphism theorems and homological diagram lemmas for groups as the usual subgroups are. We study several questions in relation to this, including what makes the noetherian form of usual subgroups special among all of these noetherian forms, and in fact, all noetherian forms of the category of groups.

arXiv abstract · PDF

Categorical Semantics Coalgebras and Convergence · primary corpus · published 2026-11-02T14:10:04Z
Ois\'{i}n Flynn-Connolly, Henning Basold, Chase Ford
arXiv categories: cs.LO, math.AC, math.CT

Final coalgebras and the coinduction principle for coalgebras over $R$-modules, where $R$ is a commutative ring, are essential in determining the denotational behaviour of various types of linear weighted automata. The goal of this paper is to provide lower and upper bounds on the ordinals that are needed to construct final coalgebras over $R$-modules as the limit of a transfinite sequence of functor iterations. We give an example of a binary intersection preserving finitary functor on the category of abelian groups, which is the category of modules over integers, that fails to converge in $\omega \cdot 2$ steps, thus settling an open problem of Ad\'{a}mek, Milius, and Moss. Then we relate this to the failure of the Artinian property of the integers and show that all finitary functors on $R$-modules for a Noetherian ring $R$ with Krull dimension $n$, which preserve countable directed intersections and a generalised notion of monomorphism, converge in $\omega \cdot (n + 2)$ steps. We also establish how the connection between Aczel-Mendler bisimulation and behavioural equivalence is mediated by the functor $\operatorname{Ext}^1$. These results show that homological algebra tools can play an important role in coalgebra.

arXiv abstract · PDF

Categorical Semantics Coalgebras and Convergence · primary corpus · published 2026-11-02T19:05:05Z
Kenichi Bannai, Masahiro Kurisaki
arXiv categories: math.PR, math.CT, math.ST, stat.TH

We extend the categorical treatment of Bayesian filters to models with feedback, whose transitions and observations may depend on the past observations. We work in the stochastic category, whose objects are measurable spaces and whose morphisms are Markov kernels, which we refer to as stochastic morphisms. We systematically parameterize stochastic morphisms by a measurable space, and develop the calculus of conditioning in a notation intuitively compatible with classical probability theory, requiring neither string diagrams nor densities. A stochastic morphism into a product space is regarded as a parameterized family of joint laws, and its conditional law is again a stochastic morphism, so that the rules of conditioning become equalities of stochastic morphisms. We define the Bayesian inverse with respect to a parameterized prior and prove Bayesian coherence. A model with feedback is then a model whose parameter space grows with the observations, and we derive the Bayesian filter, prediction and smoothing for such models, with standard Borel hidden states and countably generated observation spaces. The affine Gaussian stochastic morphisms parameterized by a measurable space form a family strictly larger than the Markov category $\mathbf{Gauss}$, closed under composition and Bayesian inversion, in which we obtain the Kalman filter and the Rauch-Tung-Striebel smoother with feedback.

arXiv abstract · PDF

Categorical Semantics Coalgebras and Convergence · primary corpus · published 2026-11-03T21:07:34Z
Emilio Angulo-Perkins, Fr\'ed\'eric Mynard
arXiv categories: math.GN, math.CT

Given a category $\mathsf{C}$ of lattices, we introduce the category $\mathsf{C^{Cap}}$, a pointfree version of the category $\Cap$ of convergence approach spaces, that contains $\Cap$ coreflectively, as well as the category $\mathsf{C^{Conv}}$, of pointfree convergence spaces introduced by Goubault-Larrecq and Mynard, both reflectively and coreflectively. We investigate pointfree counterparts of pseudo-approach, pre-approach, and approach spaces along two natural axes---depth and adherence-determinedness---which coincide in the spatial case but diverge in general lattices, and we determine when the point--powerset adjunction restricts to these subcategories. Unlike in $\mathsf{C^{Conv}}$, the category $\mathsf{Ap}$ of approach spaces finds a natural analog $\mathsf{C^{Ap}}$ in $\mathsf{C^{Cap}}$ and "index theory" translating traditional topological or metric results into generalizing inequalities can be conducted. We illustrate this with a result involving measure of continuity and measure of compactness.

arXiv abstract · PDF

Categorical Semantics Coalgebras and Convergence · primary corpus · published 2026-11-04T04:15:37Z
Evan Patterson
arXiv categories: math.CT, cs.LO

E-graphs are a powerful algorithmic technique for automated equational reasoning but have resisted a conceptual understanding independent of issues of presentation and implementation. We propose an operational semantics for e-graphs based on the fundamental category-theoretic concepts of diagrams, limits, and initial functors. We illustrate the formalism through numerous example calculations and establish its soundness and completeness. Technical prerequisites are kept to a minimum in the main text; less standard elements of the mathematical theory are developed in two appendices.

arXiv abstract · PDF

Categorical Semantics Coalgebras and Convergence · primary corpus · published 2026-11-05T07:37:24Z
Jayampathy Ratnayake, Annanthakrishna Manokaran
arXiv categories: math.CT

We study self-similar spaces obtained by repeatedly gluing finitely many scaled copies of a pointed metric space along prescribed boundary points. A finite gluing specification defines endofunctors on suitable categories of pointed sets and pointed metric spaces. Under non-degeneracy and metric admissibility assumptions, the initial algebra of the set functor carries a canonical metric. Its Cauchy completion is a final coalgebra for the metric functor and, after forgetting the metric, also for the underlying set functor. We compare this construction with Iterated Function Systems. When the orbit algebra is injective and its comparison with the initial algebra is bi-Lipschitz, the attractor is isomorphic to the completed final coalgebra. This gives a categorical analogue of Hutchinson's theorem for overlaps captured by finitely many distinguished points. Examples include the unit interval, Cantor spaces, the Sierpi\'nski gasket and $p$-adic integers.

arXiv abstract · PDF

Categorical Semantics Coalgebras and Convergence · primary corpus · published 2026-11-05T14:56:38Z
Gabriel Saadia, Umberto Tarantino
arXiv categories: math.CT, math.GN

Virtual ultracategories are a recent categorification of topological spaces seen as sets of points together with a convergence relation between points and ultrafilters. However, a topology can also be described in terms of convergence of filters: in this paper, we thus introduce an analogue of virtual ultracategories based on filters rather than ultrafilters. At the topological level, convergence of filters is completely determined by its restriction to ultrafilters. Our main result shows that, under the assumption of tautness, the same phenomenon holds at the categorified level, thereby offering a non-ultra-biased perspective on virtual ultracategories.

arXiv abstract · PDF

Categorical Semantics Coalgebras and Convergence · primary corpus · published 2026-11-07T03:32:41Z
J. Rogelio P\'erez-Buend\'ia
arXiv categories: math.DS, math.CT, math.NT

We formulate discrete dynamics internally in the topos Cond of condensed sets. For an endomorphism $f\colon X\to X$, we construct orbit quotients, backward histories, preimage trees, and periodic loci as objects evaluated on profinite parameter spaces. The framework recovers global-section dynamics, fully faithfully embeds compact Hausdorff systems, characterizes the invertible extension, and is compatible with inverse limits. It organizes $p$-adic congruence towers and shows, for a Cantor-type non-Archimedean Julia set, that classical periodic points can be dense although the internal periodic locus is not isomorphic to the compact condensed Julia set.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-11-03T06:25:06Z
Yeonseok Lee
arXiv categories: cs.LO, cs.LG, cs.RO

Vision-Language-Action (VLA) models generalize across tasks, but their autoregressive decoders need sequential forward passes in proportion to the action horizon, each bounded below on embedded aerial platforms by streaming billions of parameters from memory. We present Aero-VPA, a lightweight Vision-Predictor-Action architecture for 3D navigation on edge hardware. A compact RGB-D Vision Transformer and a five-head ensemble predictor, trained without pixel reconstruction, forecast the next latent state; a Conditional Flow Matching solver generates a velocity and yaw-rate chunk in two Euler steps, so each decision takes five sequential network evaluations; and the ensemble dispersion drives an uncertainty fallback. Version 1 specified the architecture, deployment and protocol without results. This version reports the first closed-loop evaluation: PX4 software-in-the-loop simulation of quadrotor missions in procedurally generated forests. Behaviour cloning failed on all 60 missions despite open-loop errors of 0.02-0.04 m/s: the policy copies its last command, a copycat form of causal confusion. DAgger with a privileged, safety-gated supervisor gave the first successes but plateaued at 11.1-21.1% across six checkpoints. A map-free runtime shield with a 15 s depth memory, barrier constraints, a cap on motion outside the 73-degree field of view and backoff along the flown path raised the first DAgger policy's success on 180 paired missions from 21.1% to 52.2% (95% CI [45.0, 59.4]; exact McNemar p = 1.2 x 10^-10) and cut its crashes from 72.2% to 22.2%, while timeouts rose from 2.8% to 23.3%. All six checkpoints gained 30.0-34.4 percentage points, at mean speeds of 1.16-1.36 m/s. The code (https://github.com/ylee-sling/Aero-VPA), the trained policy (72.6 MB, https://huggingface.co/ylee-sling/aero-vpa) and the full benchmark dataset are public.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-11-04T15:12:05Z
Fabio Rovai
arXiv categories: cs.AI, cs.DB, cs.LO

A national digital twin was conceived as an ecosystem of twins connected through mappings to a common foundation, but the roadmap that promises to confirm those mappings are valid never says what valid means. We give the test a precise form, coherence and conservativity of the merged ontology, borrowed from logic-based alignment repair, and apply it to the Information Exchange Standard (IES), first pair by pair and then to whole hubs. Crosswalks from IES into thirteen ontologies across seven sector groups, anchored on the building ontologies BOT, Brick, and SAREF4BLDG, pass through separate stages of matching, human review, certification of each SKOS correspondence against the two class hierarchies, and reasoning with HermiT. Pair by pair, the stages catch different failures: certification alone removed all 526 conservativity violations of the raw crosswalks, review alone left 73, and together they made eleven of twelve overlapping pairs coherent and conservative. Pairwise certification does not compose. Merging the three certified building crosswalks into one hub made five Brick classes unsatisfiable, through a homonym between the IES and Brick notions of a floor that only BOT's disjointness axioms expose; rejecting that one row gave a coherent and conservative hub that entails 290 cross-ontology links nobody wrote down. The core hub is inconsistent before any crosswalk is added, because two published standards, the Open Energy Ontology and BFO 2020, contradict each other; with either one left out it is coherent and conservative. A hub, not a pair, is the unit an ecosystem of twins has to certify.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-11-04T15:20:35Z
David H. Wolpert, David C. Krakauer
arXiv categories: math.LO, cs.LO, physics.hist-ph

``Emergence'' refers to the fact that different mathematical languages and theories seem to be required to describe scientific theories that operate at different spatial and temporal scales. Highly circumscribed, special cases of emergence have been investigated using many different formal tools, including coarse-graining (over space and / or time), renormalization, dimension reduction, broken symmetry, and various formulations of causality. Here we extend the mathematics of model theory to unify and extend these earlier investigations. As a preliminary application of our framework, we investigate canonical examples of emergence, including the emergence of genetics from chemistry, of psychology from neurobiology, and of different forms of collective behavior from the laws governing their constituent parts. By exploiting the power of model theory we also uncover many aspects of emergence that were previously obscured. In particular, we uncover some of the rich hierarchical structure that relates different scientific fields. For example, we show that scientific fields can be related via a collection of multiple partial orders, all defined over the same set. On the other hand, under an alternative relation among scientific fields, one which allows cycles, we show that it is possible that the set of all of scientific fields must collapse into a single scientific field. Going forward, these investigations point to the formal tools that might need to be developed in order to arrive at a deeper understanding of this emergent hierarchy of scientific reality.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-11-05T04:28:30Z
Hans-Martin Will
arXiv categories: cs.LO, cs.AI, cs.DB

Type theories designed for mathematics or program verification need only that a proposition holds; proof irrelevance in conversion erases, at the kernel level, how a claim was established. A persistent knowledge store, by contrast, must retain that record: who established a claim, by which derivation or external tool, and under which assumptions. This volume presents the theory of Eigenius---a store of typed knowledge over constructive institutions---and develops its metatheory from that requirement. The kernel theory is a dependent type theory with cumulative universes, an impredicative universe of propositions, inductive families, and an intensional identity type. Proof irrelevance is an axiom with an explicit witness rather than a conversion rule, so proofs of a proposition are provably equal yet remain distinct terms. Definitional equality is joinability under an orthogonal rewriting system---confluent, injective on type formers, and decidable by a type-free test---while a separate subsumption judgment covers universe cumulativity, codomain-covariant function types, and declared class inclusions. We prove consistency via a set-theoretic model; develop a justification logic over the kernel's propositions to track evidence and support; organize environments as an institution so that store extensions are signature morphisms and external verdicts enter via comorphisms; formulate a typed knowledge-graph theory with records, classes, and refinements; and prove the correctness of conversion, normalization by evaluation, and bidirectional type checking relative to termination. A Lean 4 formalization accompanies the volume.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-11-06T05:53:00Z
Damiano Azzolini, Giuseppe Mazzotta, Francesco Ricca, Fabrizio Riguzzi
arXiv categories: cs.LO, cs.AI

Probabilistic Answer Set Programming (PASP) extends Answer Set Programming with the possibility of representing uncertain data. Among the possible available semantics, we focus here on the credal semantics. In this setting, prior work has focused exclusively on plain ASP programs, i.e., programs without optimization constructs. However, many real world tasks define optimality criteria over the possible solutions, which cannot be conveniently modeled with existing probabilistic ASP frameworks. In this paper, we close this gap and propose optimal Probabilistic Answer Set Programming, which extends PASP by also allowing weak constraints, which are the standard optimization construct of ASP. We define the semantics of such programs, study the computational complexity of the inference and most probable explanation tasks, and propose practical implementations based on Algebraic Model Counting and Answer Set Programming with Quantifiers. An empirical evaluation of the proposed approach on three real world tasks confirms the applicability of our framework.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-11-06T18:29:48Z
Marco Colombo, Balaji A Jayaram, Sowmyakumari Selvaraj, Sumit Tokkar, Animesh Kumar, Aravinda Prasad Sistla, Ravishankar Shetty, Rigel Gjomemo
arXiv categories: cs.AI, cs.PL

This paper describes an approach and use case to estimate the correctness of LLM-generated COBOL summaries without access to human-authored references. The core intuition is that inter-model agreement on semantics is informative about truth, and that an LLM-as-judge can provide higher-fidelity pairwise assessments than traditional string- or embedding-based metrics. We operationalise this intuition with (i) controlled summary generation from diverse models; (ii) a LLM evaluator that compares pairs of summaries and emits structured judgments; and (iii) a calibrated aggregation rule that combines supportive evidence while penalising only corroborated contradictions.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-11-08T18:20:46Z
Isabel Amaya-Rodr\'iguez, Cristina Martin, Nekane Larburu, Teresa Garcia-Navarro, Roberto Gonz\'alez Novas, Alberto Rodr\'iguez Taboada, Maite Garc\'ia-Sebastian, Ainara Estanga, Mirian Ecay-Torres, Pablo Mart\'inez-Lage, Miguel A. Armengol de la Hoz, Cristina Rubio-Escudero, Iv\'an Mac\'ia
arXiv categories: cs.LO, stat.OT

Fairness in clinical artificial intelligence (AI) is usually evaluated after model training, yet bias can enter earlier in the AI lifecycle, during data collection and labelling. When routine clinical assessments serve as target variables, systematic differences in these labels across sociodemographic groups are carried into model development, validation and updating. This study addresses this early lifecycle stage by auditing labels from three standardised instruments used in residential care: the Barthel Index (BI), the Mini-Mental State Examination (MMSE) and the Global Deterioration Scale (GDS). Using electronic health records of 2,407 residents from 12 nursing homes in the Basque Country, Spain (2011-2021), we assessed four social determinants of health (SDoH) - sex, educational attainment, lifetime work activity and marital status - with two group fairness metrics, Disparate Impact (DI) and Statistical Parity Difference (SPD), computed for each outcome category with bootstrap confidence intervals. Disparities were found for all four attributes and across the three instruments: men, residents with intermediate education and never-partnered residents were more frequently classified in categories indicating preserved function or cognition. These disparities may reflect genuine differences in health status, measurement properties of the instruments, assessment practices or selective admission to residential care, and cannot be attributed to a single cause with the present design. Regardless of their origin, any model trained on these labels would inherit them, and they could persist through later lifecycle stages unless explicitly examined. These findings support pre-training label auditing as the first step of a continuous fairness assessment spanning model development, validation, deployment and updating.

arXiv abstract · PDF