arXiv weekly literature review

Proof assistants and mechanized formalization · primary corpus · published 2026-09-03T18:37:50Z
František Farka, Carmine Abate, Sven Linker, Sebastian Ertel
arXiv categories: cs.PL

We present Corten, a foundational verification framework for Rust programs in the Rocq theorem prover, built on the Iris separation logic framework. Corten provides the first semantics of surface-level Rust mechanized in a proof assistant with an attached program logic, directly grounded in the Rust Reference: it deeply embeds the Typed High-level Intermediate Representation (THIR) into Rocq and formalises Rust's dynamic semantics as a weakest-precondition predicate transformer calculus. By operating at THIR rather than on internal compiler representations, Corten proof goals display the THIR AST, which pretty-prints to surface Rust, keeping verification close to the source code and facilitating maintainability as code evolves. Atop this semantics, Corten develops a program logic and a syntax-directed proof automation layer; the program logic includes defunctionalized continuation stacks that keep proof goals first-order and compact. Soundness is established incrementally, construct by construct, against an interaction-trees denotation. A synthetic test suite demonstrates a two-to-four times reduction in proof size compared to raw semantic proofs. We further showcase Corten on a buddy allocator case study, verifying memory safety of the allocation and deallocation functions, laying the groundwork for end-to-end verification in a shared Rocq semantic foundation spanning hardware-software boundaries.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-09-03T07:35:29Z
Ján Pastorek
arXiv categories: cs.AI, cs.LO, math.CO

We report on our ongoing project to develop a computational pipeline, AutoGraphForge, for an automated graph-theoretic conjecturing-refuting-formalizing-proving system. Conjecture generation is counterexample-guided and runs in rounds: a Graffiti3 generator proposes conjectures over a small, evolving snapshot table $T$ (initially a few hundred graphs with their computed invariants) that grows only by counterexamples to its own conjectures. A novelty filter of $559$ classical and folklore relations, closed under transitive composition and linear identity substitution, decides via a linear program whether a candidate is already implied by known results. Surviving candidates are tested against a dataset of about $348,000$ graphs, unioning the complete House of Graphs invariant export, the exhaustive census of all connected graphs on at most nine vertices, several extremal families (strongly regular, minimal Ramsey, Cayley, cages, barbells, lollipops, spiders), and random models. Counterexample-search algorithms then attack the remainder. Run for several rounds on an HPC cluster, the loop yields $6,522$ conjectures that survived the refutation dataset, the novelty filter and every active-search run -- among them nontrivial relations between the annihilation number and the edge-cover number for bipartite and regular graphs, which we prove by hand. A subsequent formalization and proving stage deterministically translates each surviving conjecture into a Lean 4 statement skeleton; every candidate proof is kernel-verified against a pinned mathlib4 and our custom invariant preamble. This stage integrates two neural provers -- DeepSeek-Prover-V2-671B (served with vLLM) and the Lean-specialised OProver-32B -- behind the independent kernel check. It is implemented end-to-end and passes initial sanity checks, with the full pipeline currently running on the cluster.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-09-04T13:58:19Z
Weichen Winston Yin, Jacob M. Taylor, Dirk R. Englund, Frank H. L. Koppens
arXiv categories: quant-ph, cs.AI, cs.LO

Formalizing mathematics in a proof assistant, where a machine checks every definition, statement and proof, has set a new standard of rigor. Large language models are now capable of formalizing autonomously, even at the scale of whole textbooks. We bring this standard of rigor to physics, where theoretical arguments carry idealizations that are rarely stated fully, and any logical gaps could have a cascading effect on interdependent results. Recognizing the need to evaluate autoformalization systems for physics, we release AxQM, 1,019 kernel-checkable proof-synthesis tasks over 479 items drawn from the textbook Quantum Computation and Quantum Information by Nielsen and Chuang. The tasks are stated in a custom Lean library of finite-dimensional quantum mechanics. By task count, it is the largest proof-synthesis benchmark in physics by a factor of four. AxQM is derived from a near-complete formalization of the formal portions of the textbook, so every task is guaranteed a solution, which we keep private. Grading of the benchmark is done deterministically by the Lean kernel, which checks that the proof compiles, that no sorry appears in it or in any declaration it depends on, and that it introduces no new axioms.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-31T18:47:23Z
Daniel Bund, Julian Erhard, Michael Petter, Michael Schwarz
arXiv categories: cs.PL, cs.SE

Maintaining an abstraction of the execution history of threads can improve the precision of data race detection in static analysis. Here, we extend the digest framework to handle concurrency constructs and synchronization mechanisms that have been ignored in static race detection. We introduce mechanisms for the commonly used thread barriers, as well as pthread_once, which allows to ensure that an action is executed only once. We also instantiate the framework with an abstraction of locksets held by ancestor threads. We propose a suite of litmus tests to evaluate analyses for these features and compare our implementation to state-of-the-art tools, finding that they lack support.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-09-01T11:50:45Z
June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal
arXiv categories: cs.PL, cs.CR

CHERIoT is a novel hardware-software co-design that leverages hardware capabilities to define a notion of compartment, in a minimalistic capability-based OS, CHERIoT RTOS. By default, compartments are isolated to limit damage in case of bugs or malicious behaviour. To allow cross-compartment communication, the OS provides a privileged component, called the switcher. The switcher provides an interface for cross-compartment calls, while enforcing isolation between compartments and guaranteeing stack safety. Together with hardware capabilities, the switcher is critical to enforce the security guarantees of the CHERIoT compartment model. The design of CHERIoT raises two questions: First, how can one formalise the informal notion of compartmentalisation that CHERIoT compartments are designed to provide? And second, given that the safety properties of CHERIoT hinge on the complementary roles of the capability machine and of the switcher, does the design of CHERIoT enforce the desired security properties? In this paper, we introduce Griotte and Griotte OS, idealised but faithful versions of the CHERIoT machine and the CHERIoT RTOS, which we use to answer these two questions: First, we formally capture the aforementioned security guarantees in the form of a continuation-based logical relation which captures the combined behaviour of the switcher and of the capability machine. And second, we define a specification for the Griotte switcher that enforces those guarantees, and prove that the implementation meets the specification. We demonstrate Griotte on a range of key scenarios illustrating different aspects of CHERIoT, including integrity of the local state in the presence of memory sharing with unknown code. Our approach is modular: we verify compartments individually, and then compose their specifications. Together, our contributions give a solid formal foundation to the design of CHERIoT.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-09-02T03:25:29Z
Wesley B. Nuzzo, Samuel Dodson, Benjamin Houle, Tarakaram Gollamudi, Anitha Gollamudi
arXiv categories: cs.CR, cs.PL

Trusted Execution Environments (TEEs) provide hardware-supported isolation through enclaves that protect code and data independently of software abstractions. However, TEEs alone cannot enforce information-flow security. This problem is further aggravated in LLVM-like low-level languages that allow unrestricted pointer manipulation and unstructured control flow. Moreover, using TEEs effectively typically requires manually partitioning applications into enclave and non-enclave components, a process that is labor-intensive, error-prone, and lacks fine-grained control. We address these challenges with a three-step approach. First, we formalize SIR, an enclave-oblivious calculus based on LLVM IR, equipped with a novel permissive type system that enforces security against low-level attackers. To obtain meaningful guarantees, SIR combines information-flow control with security-aware coarse-grained memory safety. Second, we extend SIR to SIREN, an enclave-aware calculus that enforces noninterference against stronger attackers capable of observing arbitrary non-enclave memory. Third, we develop a type-driven, type-preserving compilation from SIR to SIREN that automatically produces secure enclave-aware programs, eliminating manual partitioning while providing fine-grained control over host-enclave boundaries. We implement and evaluate SPLITR on thirteen microbenchmarks and real-world workloads, including applications from SGXGauge, on Intel SGX hardware. SPLITR scales to OpenSSL (425,953 LLVM IR instructions) and supports multiple objectives that expose trade-offs among enclave TCB size, host-enclave transitions, and boundary data movement. For OpenSSL, optimizing for transitions reduces them from 393 to 187. Runtime overhead is dominated by fixed enclave costs for short-running workloads, whereas long-running applications better amortize these costs and approach native performance.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-09-03T16:17:47Z
M. Frans Kaashoek, Nickolai Zeldovich
arXiv categories: cs.LO

MachCSL is a framework for verifying systems software, such as an OS kernel, on top of low-level semantics of a RISC-V computer, based on the Sail RISC-V semantics. The key idea behind MachCSL is to adapt concurrent separation logic, based on Iris, to reasoning about low-level hardware execution at the sub-instruction level: page-table translation, TLB, privilege levels, configuration registers, instruction fetch/decode/execute, traps and interrupts, DMA, shared memory, power failures, etc. Reasoning at this level of detail ensures that the system software correctly manages all of the hardware details. Verifying software at this low level of abstraction is tedious, but LLM-based agents are capable of reasoning about such low-level details. As a case study, we verify the xv6 OS kernel (6,593 lines of C and assembly code), which provides a traditional Unix system call interface (processes, file system, file descriptors, and preemptive scheduling) and has substantial internal concurrency (multi-core support with fine-grained locking, shared memory, interrupts, DMA, etc.). In the verification process, we uncovered nine bugs in the xv6 implementation, as well as one bug in the Sail RISC-V semantics. The verification effort took us 77 days, including the time to develop the MachCSL framework.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-09-03T22:48:21Z
Amirali Sajadi, Saikat Dutta, Preetha Chatterjee
arXiv categories: cs.SE, cs.CR, cs.PL

Static application security testing (SAST) tools help developers find vulnerabilities before deployment, but false positives create substantial triage effort. We study whether CodeQL false positives in Java security analysis form recurring, explainable patterns that can be reduced by refining the analysis. We run CodeQL's Java security query suite on 167 CVE instances from 110 projects, focusing on the ten queries with the highest false positive rates. We manually review 500 sampled false positive paths and locations and construct a source-level taxonomy. The five categories are Missed Path Constraint or Sanitization (36.6%), Benign Execution Context (29.4%), Missing Trust Boundary Modeling (27.6%), Imprecise Concurrency Modeling (5%), and Imprecise Sink Modeling (1.4%). Guided by these findings, we implement CodeQL refinements that detect and filter recurring false positive patterns at the query level. The refinements remove 81.8% of reviewed false positives. Across the full selected-query dataset, they remove 15.8% of reported paths and locations while retaining 7 of 8 true positives. This shows that many false positives can be reduced in the analysis, although fixed refinements often depend on project-specific context. To address this generalization gap, we evaluate whether agentic coding tools can adapt refinement patterns to new projects. Given our patterns as templates, the two tools succeed on 56% and 62% of tasks, with query compile-pass rates above 90%. Without this guidance, both succeed on only 28%, while compile rates fall to 30-36%. These results support a refinement-oriented SAST workflow in which recurring false positives are modeled in CodeQL queries and automatically adapted to different project contexts, reducing repeated triage.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-09-04T15:42:57Z
Chujun Geng, Noah Charlton, Spyros Blanas, Michael D. Bond, Yang Wang
arXiv categories: cs.PL

Data stores are widely used because they provide persistence, scalability, and fault tolerance with a simple interface. However, most data store applications configure the data store to use weak isolation to achieve scalable performance, resulting in sporadic unserializable executions that are incorrect or fail. Prior work uses dynamic predictive analysis to infer violations from execution traces, but it cannot handle relational (i.e., SQL) queries with complex predicates, and it predicts executions that do not violate View Serializability. This paper introduces Augur, the first dynamic predictive program analysis that (1) supports data store applications with complex relational queries and (2) reports only executions that violate View Serializability. The evaluation demonstrates that Augur finds feasible, unserializable executions in the widely used OLTP-Bench programs and in the widely used e-commerce application Spree.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-09-01T14:27:06Z
Oleksii Kolesnichenko, Jakub Peleška, Gustav Šír
arXiv categories: cs.PL, cs.DB, cs.LG

Relational Deep Learning (RDL) has become a powerful paradigm for learning from multi-tabular data. However, manually defining RDL prediction tasks is a laborious process that frequently results in data leakage. To address this issue, we introduce Relational Task Generation Language (RTGL) - an open-source declarative language that streamlines RDL task formulation by abstracting away low-level SQL details. We showcase RTGL by reconstructing existing RDL benchmark tasks and uncovering their inconsistencies stemming from manually crafted SQL definitions of RDL prediction targets, thereby underscoring the value of a dedicated declarative language. In addition, we demonstrate the practical utility of RTGL by designing various new tasks with diverse forms and target types. Our experiments confirm the robustness and usability of RTGL, as well as its seamless integration with the existing RDL frameworks, making it widely accessible to the community.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-09-02T02:30:20Z
Takuma Yoshioka, Taro Sekiyama, Atsushi Igarashi
arXiv categories: cs.PL

Bidirectional typing mixes type synthesis and type checking into a single process. Existing bidirectional type systems can be classified into two styles based on whether, given a function application, a bidirectional typing algorithm synthesizes the function's type first and typechecks the argument against the synthesized argument type, or it synthesizes the arguments' types first and typechecks the function against the synthesized arguments' types. We call the former _function-first_ and the latter _argument-first_. Not only do the two styles significantly differ in how the type systems and typing algorithms are formalized, but also they lead to incompatible typeabilities, forcing a language designer to select one style and to give up the other's typeabilities. In this paper, we unify the two styles and develop \lang with a new bidirectional type system for higher-rank polymorphism. Key ideas of the unification are twofold. Each function application is annotated with a bit of information to represent whether function- or argument-first typing is used, to allow a language designer (or even a programmer) to switch between the two styles at their discretion. We reformulate the function- and argument-first type systems by using ideas from colored types and boxy types, which can specify which part of a type should be synthesized or used for checking in a flexible manner. We also develop a typing algorithm based on the worklist approach by Zhao et al. The (declarative) type system of $λ^{BH}$ is shown to be sound and to subsume two representative function- and argument-first systems. Our typing algorithm is shown to be sound with respect to the type system of $λ^{BH}$ and complete with respect to representative function- and argument-first systems. We mechanically prove the metatheorems using the Abella theorem prover.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-09-03T14:25:42Z
Isolde Adler, Carsten Lutz, Quentin Manière, Marcin Przybyłko, Lukas Schulze
arXiv categories: cs.DB, cs.LO

In the context of database querying, property testing provides a framework for testing query answers with high confidence while inspecting only a sublinear part of the database, through completion queries and size queries. A fundamental result of Chen and Yoshida (2019) states that non-satisfaction of a Boolean conjunctive query $q$ is testable with a constant number of such queries and one-sided error if and only if $q$ is equivalent to an $α$-acyclic query. In this article, we initiate the study of property testing for recursive query languages, focusing on two-way regular path queries (2RPQs) and monadic Datalog. One of our main results is positive: non-answers to any 2RPQ are constant query testable with one-sided error. We extend this slightly to a certain class of monadic Datalog programs in which recursion is restricted to be linear and rule bodies must be $α$-acyclic. Turning towards unrestricted monadic Datalog, we next show that if a monadic Datalog program $Π$ is not equivalent to an $α$-acyclic program, then falsity of $Π$ is not constant query testable with one-sided error. This is under the assumption that all rule-bodies are self-join free. We leave open the case of monadic Datalog programs with $α$-acyclic rule bodies that are not restricted to linear recursion, but observe as a first step that there exist $α$-acyclic programs that are mildly non-linear and constant query testable with one-sided error.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-09-03T15:38:56Z
Guanxuan Wu, Allison Sullivan
arXiv categories: cs.PL, cs.LO

Slotted e-graphs represent open terms modulo consistent renaming, while algebraic operators benefit from canonical sequence, bag, or set children. We compose the two at a specification level: typed slot-mapped invocations inhabit operator-declared ports whose sibling quotient and recursive flattening licenses are certified separately. A generic finite quotient presentation proves exactness of its least-orbit normal form, while certified records specify effective-support kernel extraction and collision. For abstract obligation traces carrying local endpoint certificates, we prove finite-unfolding equational soundness. An Alloy case study compares seven related pipeline arms on a frozen corpus and a controlled transformation suite. Its measurements characterize bounded capability and structural consolidation; they do not establish refinement of the Java artifact or experimental replay against the formal model.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-09-04T09:07:15Z
Nikolay Fot, Alexander Vinarsky
arXiv categories: cs.PL, cs.SE

This paper presents Cordell Programming Language (CPL), a compact C-like systems language that retains C's direct access to memory, layout, and machine interfaces while experimenting with a smaller grammar and selected conveniences from newer languages. Also this paper studies whether C-like are more convenient to use for compiler experiments than modern approaches and paradigms. While the language and compiler provide primitive values, pointers, arrays, containers with methods, unions, generic functions, overloads, entry-point and section control, system calls, and inline assembly, they do not provide high-level constructs such as classes, built-in methods, a standard library, or memory protection. The article describes the language design, compiler pipeline, target backends, static-analysis architecture, and OS-facing use cases, then evaluates the prototype backend with reproducible x86_64 and i386 microbenchmarks against C compiler baselines. The obtained results suggest that the compiler can produce code comparable to that produced by production compilers such as GCC and Clang, as well as by small compilers such as TinyC and SmallerC.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-09-01T10:35:46Z
Alex Rice, Chris Heunen, Tobias Grosser
arXiv categories: cs.PL, quant-ph

Quantum compilers typically follow the circuit model, representing programs as fixed sequences of gates. This static view breaks down in hybrid quantum-classical applications, where gate choices depend on runtime data or measurement results. We introduce a new Intermediate Representation (IR) that elevates gates to first-class values, enabling their dynamic creation, composition, and control. This unified representation allows classical computation to steer quantum behaviour, capturing phenomena including stochastic gate selection, adaptive error correction, and measurement-driven computation within a single framework. Case studies in noise modelling, randomised compilation, error correction, and measurement-based quantum computing show that our IR expresses these programs compactly and supports optimisations that were not possible in the circuit model. Evaluation on a benchmark suite of hybrid quantum-classical programs indicates that our IR represents programs compactly and facilitates compiler analysis and transformation.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-09-01T16:32:46Z
Maxwell Bernstein, Takashi Kokubun, Aaron Patterson, Si Xing "Alan" Wu, Kevin Menard
arXiv categories: cs.PL

Ruby is a dynamically typed and object-oriented programming language. Its primary implementation, CRuby, contains a bytecode virtual machine and a mature lazy basic block versioning (LBBV) just-in-time (JIT) compiler called YJIT. In order to both implement more advanced optimizations than YJIT supports and also encourage more outside contributions, we present a new method-based JIT called ZJIT. Like YJIT, ZJIT compiles from bytecode to machine code. Unlike YJIT, ZJIT has multiple global and local optimization passes. ZJIT's high-level intermediate representation is in static single assignment (SSA) form. In order to optimize Ruby's local variables, ZJIT lifts local variables into SSA values. This is a departure from how other Ruby compilers handle locals: other JIT compilers either leave local variables as memory loads and stores or do advanced partial evaluation to recover SSA values from memory. While implementing locals, we (re-)discovered what features make local variables in Ruby especially challenging to compile correctly and efficiently. We demonstrate these features and illustrate how we solved these problems in ZJIT.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-09-01T16:55:11Z
Gene Zhang
arXiv categories: cs.DB, cs.AI, cs.PL

A durable assumption holds that graph analytics requires a purpose-built graph engine, and that relational systems are ill-suited to connected data. We argue the opposite for the workloads enterprises actually run. A columnar relational engine fronted by a graph query language matches or exceeds native graph engines on analytical graph queries, and - decisively - scales past the point where in-memory graph engines fail. We further argue that the node/edge property graph is not a more faithful model of connected data but a re-encoding of relationships that already exist explicitly in relational tables; reconstructing them at query time is pure overhead. We present ClickGraph and its Databricks-dialect sibling DeltaGraph, systems that translate Cypher directly onto the native relational schema - the tables, columns, and foreign keys as they already exist - and execute in place on ClickHouse, Databricks, or in-process on lakehouse files, with no import and no separate cluster. Because the output is ordinary SQL, an underperforming query is an open optimization surface: it can be rewritten, and the engine itself extended. We support the argument with a peer system's own published benchmark, in which a columnar engine outruns Neo4j by two-to-four orders of magnitude, and with reproducible measurements across the LDBC Social Network Benchmark suite.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-09-01T18:29:11Z
Wei Qiang, Ronghui Gu
arXiv categories: cs.PL

Today's quantum devices are noisy, so reducing circuit size is critical for reliable execution. Existing rule-based optimizers often rely on large rule sets that are difficult to manage and still miss long-distance transformations. We present QSymb, a framework for synthesizing compact and expressive quantum-circuit rewrite rules with formal guarantees. We formalize symbolic rewrite rules in which a symbolic gate represents infinitely many subcircuits. We then define canonical symbolic rules of the form $L;S = S;R$ and prove that they constitute a compact generative core from which general symbolic rules can be derived. On top of this formal foundation, given a gate set, QSymb synthesizes (1) a small, non-derivable concrete rule set that is complete up to chosen size and qubit bounds, and (2) a small but expressive canonical symbolic rule set that captures transformations beyond finite or monomial-only patterns. We further present rule anchoring to derive optimization-effective rules from canonical symbolic rules. Together, these results provide both expressiveness and guarantees: soundness of synthesized rules via validation, non-derivability, and bounded completeness. On the IBM-Eagle gate set, QSymb strictly outperforms state-of-the-art rewrite-based optimizers (Qiskit, Guoq, Quartz, TKET, and Queso) in two-qubit-gate reduction on 90%, 67%, 82%, 85%, and 83% of standard quantum algorithm benchmarks, respectively; on Nam gate set, the corresponding rates are 88%, 74%, 81%, 86%, and 82.9%. It achieves final average two-qubit-gate reductions of 27.44% and 29.95%, respectively.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-09-01T18:42:13Z
Xiangyu Ren, Yuexun Huang, Zhaohui Yang, Yuchen Zhu, Tsung-Wei Huang, Tsung-Yi Ho, Zhiding Liang, Antonio Barbalace
arXiv categories: quant-ph, cs.AR, cs.PL

Simulating quantum many-body systems has been one of the most important applications of quantum computation. For simulation, the Hamiltonian of a physical system is compiled into quantum programs with native instructions for quantum hardware. In previous works, the Hamiltonian is represented as Pauli strings, then compiled and optimized based on the quantum circuit model. Such representation paradigm neglects the spatial topology of original physical models, which is vital information to reducing the overhead of compiling many-body systems Hamiltonians. To address such neglect, we introduce a spatial-topology preserving compiler for quantum many-body simulation. Using Pauli gadgets as the representations of the Hamiltonian, we introduce our intermediate representation -- GadIR, to preserve the spatial-topology information of original physical models. Our compiler frontend performs the group reduction algorithm based on Pauli gadget model, which is a hardware-independent optimization. Our compiler backend performs trotterization and scheduling on Pauli gadgets, then synthesizes the Pauli gadgets into hardware-native quantum programs. We evaluate our compiler on all the canonical quantum many-body system models, while achieving a significant reduction on compilation overhead regarding four major quantum architectures. Overall, our spatial-topology preserving IR exploits the compilation optimization space for quantum many-body systems Hamiltonian.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-09-02T19:50:00Z
Gaurav Verma, Michael Canesche, Fernando Magno Quintão Pereira
arXiv categories: cs.PL

This paper describes our experience extending the polyhedral compiler Pluto with a lightweight, coordinate-wise hill-climbing tuner that adjusts numeric transformation parameters, such as tile sizes and thread-block dimensions, after Pluto selects the kernel's loop structure. To ensure fast convergence and escape local minima, hill climbing is augmented with two techniques: expanded neighborhood exploration and a shortest-hop refinement phase. On x86 and ARM CPUs, tuned kernels outperform Pluto's default configuration (1.06-1.28x geometric mean speedup across 11 benchmarks) and static optimizers (Clang -O3, Polly, IOOpt), reaching performance competitive with the AutoTVM autotuner at substantially lower search cost. Applying the same technique to GPU thread-block allocation on an NVIDIA A100 yields 5.5-8.5% improvement over default configurations. These results position post-optimization parameter tuning as a practical middle ground between fixed-cost-model polyhedral compilation and full autotuning.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-09-04T00:35:54Z
Narasinga Rao Miniskar, Seyong Lee, Keita Teranishi, Jeffrey S Vetter
arXiv categories: cs.PL, cs.CL

The Multi-Level Intermediate Representation (MLIR) has made reusable compiler infrastructure practical for domain-specific computation. However, MLIR's strong compile-time type requirements and low-level (C++) extension model can be a poor match for high-level, dynamically specialized languages such as Julia. MLIR has several drawbacks for dynamic programming languages in terms of the type system and level of abstraction. It is thus extremely challenging for non-compiler or scientific computing users to introduce new programming abstractions and express algorithm implementations in a form that remains both natural and optimizable. As a result, library interfaces for linear algebra, mesh processing, partial differential equations, and related domains often sit outside the compiler optimization path. We present JLIR (Julia-native Level Intermediate Representation), a Julia-native intermediate representation framework that brings the main benefits of MLIR-style multi-level, dialect-oriented compilation into the Julia ecosystem while remaining usable as ordinary Julia code. JLIR represents Julia programs before low-level lowering, supports extensible operations and transformation passes through Julia's language mechanisms, and allows partially typed programs to remain transformable until concrete types are known. The framework includes built-in dialects for arithmetic, control flow, functions, structured loops, and memory operations, and it also includes a lightweight mechanism for adding new domain operations without modifying the core system. To demonstrate JLIR's capabilities, we applied it to automatic Julia for Accelerators (JACC) kernel generation.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-31T13:54:48Z
Jingyu Ke, Ling-I Wu, Guoqiang Li
arXiv categories: cs.LO, cs.SE

Agentic verification systems can often generate source-level specifications that look plausible, but plausibility is not enough: the verifier must still turn those specifications into SMT obligations that the solver can prove. When this step fails, current LLM-driven loops usually expose only a coarse verifier error, timeout, or unknown solver result. The model cannot tell whether the specification is wrong, a helper lemma is missing, the proof context contains irrelevant facts, or the obligation needs a different theory view. This paper presents Schwarz, an agentic verification harness that makes SMT-backed proof failure local, checkable, and repairable. Schwarz turns failed verification into obligation-local repair tasks: program-point snapshots expose checked facts at a boundary, local lemmas let the agent propose missing proof steps, and theory-aware solver policies guide the agent toward solver-friendly formulations for numeric, quantified, memory, and floating-point obligations. We implement Schwarz for C and Rust/Verus and evaluate it on 1,475 tasks. On 475 benchmarks from recent agentic verification tools, Schwarz solves 95.2% of the tasks. On 1,000 tasks from the SV-COMP 2026 ReachSafety track, averaging 1,427 LOC, Schwarz solves 91.5% of the tasks, compared with 60.1% for CPAchecker. Ablations and comparison with a pure-agent baseline show that solver-aware repair is effective and scalable.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-09-01T02:18:20Z
Lara Marinov, Aditya Thimmaiah, Jayanth Srinivasa, Junyi Jessy Li, Milos Gligoric
arXiv categories: cs.PL, cs.AI, cs.CL, cs.SE

Large language models (LLMs) have shown proficiency in various software engineering tasks, such as code generation and translation. However, a key limitation in their performance may be their (lack of) understanding of programming-language semantics. Even when explicit semantics are given, it remains unclear whether LLMs apply those rules or lean on priors learned during pre-training instead. We study if LLMs lean on priors or given semantics with a novel task--Program Executability Prediction (PrEx)--that asks models to predict whether a program is semantically valid or invalid (and, if invalid, which formal rule it violates) given the program's syntax and operational semantics. Because PrEx requires both valid and invalid programs, we build a dataset with systematically generated invalid transformations derived from valid programs. We evaluate open-source coding LLMs under two semantic formalisms and two semantic shifts across Human-Written, LLM-Translated, and Fuzzer-Generated program splits. Our findings show that LLMs lean on pre-training priors rather than systematically applying the given rules, performing especially poorly on modified semantics and degrading further as program complexity increases. PrEx is available at https://github.com/EngineeringSoftware/prex.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-09-03T04:49:02Z
Zikai Zhou, Yufei Jin, Yilin Xu, Yu-Chiang Wang, Chieh-Ju Chao, Monica S. Lam
arXiv categories: cs.CL, cs.CY, cs.LO

Accountability means a decision can be examined, justified, and contested. LLMs make this hard: fluent output may be ungrounded, incomplete, or unfaithful to the decision process. Achieving accountability requires verified rationales (how was the decision reached), assumptions (what was assumed rather than known), policy consistency (the same treatment for the same facts), and pivotal conditions (what would change the outcome). We introduce self-faithfulness as an automatic test of accountability: changing the pivotal conditions should change the decision. We examine accountable AI through clinical trial matching, a high-stakes task central to evidence-based medicine. Although LLM-based matchers match patients to trials reasonably accurately, they apply decision policies inconsistently and produce rationales that are unfaithful to their own decisions. We introduce VERDICT, an LLM-based agent that translates a decision task, its constraints, and its policy into Satisfiability Modulo Theories (SMT), then derives the decision with SMT and MaxSMT solvers -- so policies are applied consistently and decisions are accountable by construction. Across a SIGIR 2016-derived dataset and TREC 2021, VERDICT achieves the strongest decision accuracy among LLM-only and neurosymbolic baselines, applies policies with perfect consistency, and produces clinician-preferred rationales grounded in explicit assumptions and pivotal conditions, with improved counterfactual self-faithfulness.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-09-03T22:22:37Z
Shangkun Wang, Nina Cai, Charles Hoong, Julian Walker, Gerson Kroiz, George Vanica, Deepak Patil, Andi Gavrilescu, Hassan Sipra, Sethu Sankaran
arXiv categories: cs.AI, cs.PF, cs.PL

Designing and authoring high-performance custom kernels for accelerators is a complex task that requires deep hardware-level expertise. Large Language Models (LLM) can be leveraged together with real-time compiler feedback to build agentic systems for kernel generation. In this work, we present MaxKernel, a multi-agent system that implements three distinct paradigms for TPU kernel development: (1) a Human-in-the-Loop (HITL) agent for collaborative, step-by-step design; (2) an Autonomous (Auto) agent that executes a fully automated, metric/trace-driven optimization loop; and (3) a Graph-Based Autonomous Search that scales the Auto agent for global exploration of the design space. All three paradigms leverage a shared pool of specialized sub-agents to handle planning, implementation, self-debugging, testing, and hardware profiling. We evaluate MaxKernel on JaxBench, a comprehensive suite of 50 diverse kernel tasks for TPUs, alongside complex, real-world workloads from state-of-the-art open-source models. We demonstrate that MaxKernel consistently generates highly optimized implementations, matching expert hand-tuned baselines and delivering significant performance across the benchmark. Our agent is open-sourced and available https://github.com/AI-Hypercomputer/accelerator-agents/tree/main/MaxKernel.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-09-04T17:08:51Z
Samuel Kushnir, Kimia Noorbakhsh, Kavya Sreedhar, Liqun Cheng, Ming Liu, Parthasarathy Ranganathan, Mohammad Alizadeh, Fred Kjolstad, Suvinay Subramanian
arXiv categories: cs.PL, cs.AI

Machine-learning performance modeling is a uniquely hostile terrain for long-lived software: the assumptions baked into today's abstractions are invalidated by tomorrow's models and systems, forcing perpetual refactoring of performance-modeling frameworks. Meanwhile, AI coding agents have become fast and capable enough that regenerating an entire library is cheaper than paying down the tech debt of incrementally patching it. We describe SMART, a rigorous symbolic performance-modeling library for ML systems whose main branch contains almost no code: the repository is a DAG of self-contained natural-language design docs, coding sub-agents regenerate the implementation from only the docs on new version updates, and every human change is a natural-language edit to a doc--self-documenting by construction. Two ingredients make regeneration reliable: (i) a design-doc style built around step-by-step worked examples that act as in-context demonstrations for the generating agents, and (ii) a minimal, recursively defined operator IR with symbolic (SymPy) cost expressions, a fast analytical roll-up mode for large sweeps, and a slow modulo-scheduling mode for fine-grained schedule studies. Regenerated implementations reproduce hand-audited reference models--including DeepSeek-V3 serving on a TPU pod slice--to round-off precision, suggesting that design docs--not code--can be the durable artifact for ML-systems co-design tools.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-31T21:11:22Z
Alexandre Duret-Lutz
arXiv categories: cs.FL, cs.LO

LTLf, a finite word variant of LTL, can be reduced to LTL by introducing a new atomic proposition indicating the prefix of the infinite words that correspond to the finite words that the original LTLf formula was considering. Such a reduction was originally proposed by De Giacomo and Vardi (IJCAI'13). However, while any LTL formula reduced from LTLf describes an obligation property in the hierarchy of Manna and Pnueli (PODC'90), the aforementioned reduction does not provide an LTL formula that belongs to the syntactic obligation fragment of LTL. This note shows how the reduction was fixed in Spot in order to ensure that the resulting LTL formula is always a syntactic obligation. Doing so allows algorithms specialized to syntactic obligation to be used on LTLf formulas. For instance, in previous work (CAV'26) we described a specialized translation from syntactic obligations to minimal, weak, deterministic Büchi automata that would not be usable with the original reduction.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-09-01T10:30:46Z
Hsi-Ming Ho, Shankaranarayanan Krishna, Khushraj Madnani
arXiv categories: cs.LO, cs.AI

Automated mining of formal specifications is vital for verifying real-time systems. However, existing passive learning approaches remain restricted to deterministic specifications or limited fragments of Timed Regular Expressions (TRE). To our knowledge, this paper presents the first framework to tackle \emph{precise} passive learning for an expressive timed logic, \emph{Metric Interval Temporal Logic} (MITL) without relying on predefined templates or restricted logic fragments. Our approach formally reduces the timed learning problem into a scalable untimed one. By identifying quantitative timing differences between positive and negative traces, we synthesise precise timed constraints and inject them as new Boolean atomic propositions. This embeds timing into the alphabet, delegating the complex formula evaluation to highly optimised, off-the-shelf untimed LTL tools. Crucially, our framework is complete, guaranteeing a separating specification can always be found. We evaluate our implementation across several benchmarks, demonstrating the effectiveness of our approach.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-09-02T11:10:04Z
Anne Schreuder, Lorenz Winkler, Laura Kovács, C. -H. Luke Ong
arXiv categories: cs.LO

We study the synthesis of polynomial invariants for probabilistic transition systems (PTS) based on martingale theory. We present tractable methods to verify that such polynomials are indeed invariants, in the sense that their expected value upon termination is the same as their value at the start of the computation. We do this by applying the Optional Stopping Theorem (OST) in the form of a specific precondition. This precondition requires the existence of an integrable dominating function for the martingale expression, which implies uniform integrability; we refer to this condition as dui. For linear PTS we simplify the dui property to proving finiteness of the expected value of an expression depending on the update matrix, the degree of the martingale expression, and the stopping time. Specifically, if all random samples have finite moments and we can verify a moment bound on the runtime of a linear loop, then we can automatically synthesise polynomial loop invariants that satisfy the OST. Notably, dui allows for the sampled distributions to have unbounded support, which is a novel contribution to the field.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-09-02T11:29:22Z
Tsubasa Matsumoto, Kazuki Watanabe, Masaki Waga
arXiv categories: cs.LO

Given the safety-critical nature of many embedded systems, their safety assurance is essential. Because such systems are typically stochastic, probabilistic model checking is a particularly important technique. However, there is a well-known scalability issue due to state-space explosion, especially when verifying complex properties. To mitigate this issue, we propose specification-guided path shortcutting for probabilistic systems, focusing on Markov chains (MCs) and $ω$-regular properties. The key idea is that, when the verified property is fixed, certain sequences of transitions in an MC can be replaced with a single transition without changing the satisfaction probability, and thus, we can reduce the state space of the MC. We implement the proposed path shortcutting and evaluate its contribution to the performance of probabilistic model checking, using Storm as the baseline model checker. The results suggest that our approach often outperforms the baseline, particularly on benchmark instances with complex specifications.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-09-03T11:05:43Z
Nathalie Bertrand, Pranav Ghorpade, Senthil Rajasekaran, Sasha Rubin, Moshe Y. Vardi
arXiv categories: cs.LO, cs.FL

The discounted sum is a way to aggregate a sequence of weights from a finite alphabet $Σ$, i.e., for a discount factor $λ$, the discounted sum of a sequence $w_0 w_1 w_2 \cdots$ over $Σ$ is $\sum_{i \in \mathbb{N}} w_i λ^i$. The target discounted-sum problem, which is currently open, asks, given $λ,Σ$ and a target $t$, whether there exists an infinite sequence over $Σ$ whose discounted sum is equal to $t$. We study and solve a probabilistic variant of this problem, i.e., the target discounted-sum problem on Markov chains. To do this, we prove that the event consisting of paths whose discounted sum is equal to the target and has infinitely many distinct suffix sums has probability zero. This structural property allows us to solve the target discounted-sum problem on Markov chains using an automata-theoretic technique. We apply our technical results to Markov decision processes with target discounted-sum objectives: we show that the infimum value and the finite-memory supremum value are computable in pseudo-polynomial time and are attained by deterministic finite-memory strategies.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-09-03T11:36:45Z
Vladimir Krsmanovic, Florian Kohn, Bernd Finkbeiner, Milan Simovic
arXiv categories: cs.RO, cs.LO, eess.SY

Robots operating in physical environments make control decisions based on uncertain sensor measurements, which can lead to unsafe or suboptimal actions. Runtime monitors that check their behavior against safety specifications must represent this uncertainty soundly. Zonotopes are a widely used representation, but continuously incorporating new measurements grows their order unboundedly, so monitors must periodically apply an over-approximating reduction. The choice of the reduction method substantially affects the zonotope's precision, yet existing approaches typically utilize a fixed method throughout the run, even though the optimal choice depends on the current state. This paper presents a Predictive Zonotope Reduction (PZR) approach, which frames reducer selection as an optimal control problem and solves it using beam-search model predictive control. Policy distillation into a small neural policy further provides substantially higher execution speed than model predictive control while maintaining improved performance, enabling uncertainty-aware runtime monitoring on resource-constrained real-time systems. We implement our approach in the RLola runtime monitoring framework and evaluate it on a 5-degree-of-freedom robotic arm simulated in MuJoCo, with sensor uncertainty modeled according to ISO 5725. Experiments on a Raspberry Pi 5 show that dynamic reduction significantly lowers false-positive rates in monitoring compared with static reduction strategies.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-09-03T17:58:57Z
Angel Y. He, David Parker
arXiv categories: cs.LG, cs.GT, cs.LO, cs.MA

We introduce the first Probably Approximately Correct (PAC) learning framework for general-sum concurrent stochastic games (CSGs) with transition uncertainty, while addressing the challenge of Nash equilibrium (NE) existence. Our algorithm maintains data-driven $L^1$ confidence sets over transition kernels and solves a robust CSG to compute a social-welfare optimal $\varepsilon$-NE, using a robust MDP-based exploration mechanism to drive joint state-action coverage. Crucially, we introduce a Nash margin characterisation that enables principled reasoning about equilibrium existence: the framework either returns an $\varepsilon$-approximate NE whose social-welfare value is $\varepsilon$-close to optimal, or provides a sound certificate that no exact NE exists. Under a minimum reachability condition $p_{\mathrm{reach}}>0$ over relevant state-action pairs, the algorithm terminates after a polynomial number of trajectory samples, with sample complexity $\widetilde{O}\left( {R_{\max}^2 H^4 |S|^2 |A| / (p_{\mathrm{reach}} \varepsilon^2)} \right)$. Empirical results on benchmark CSGs demonstrate near-optimal performance, correct handling of equilibrium (non-)existence, and sample complexity consistent with theory.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-31T09:02:37Z
Michael Hoefnagel, Giuseppe Metere, Danielle Kleyn
arXiv categories: math.CT, math.LO

The main aim of this note is to provide a characterisation of coextensive morphisms in the category of bounded hoops. This characterisation is then used to show that several categories of bounded hoops are coextensive as categories. Among these are the variety of bounded Wajsberg hoops, or more generally the variety of bounded $\vee$-hoops. Our characterisation also yields the coextensivity of the category $\mathbf{Heyt}$ of Heyting algebras and recovers the known coextensivity of the category $\mathbf{MV}$ of MV-algebras.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-31T14:00:09Z
Qian Chen, Tenyo Takahashi
arXiv categories: math.LO

We investigate decidability of properties in the lattice $\mathop{\mathsf{NExt}} \mathsf{Grz}_t$ of extensions of the Grzegorczyk tense logic $\mathsf{Grz}_t$ and the lattice $\mathop{\mathsf{NExt}} \mathsf{S4}_t$ of reflexive and transitive tense logics, with applications to the lattice $\mathop{\mathsf{Ext}} \mathsf{biIPC}$ of bi-superintuitionistic logics. We prove that a broad class of properties is undecidable in $\mathop{\mathsf{NExt}} \mathsf{Grz}_t$, including tabularity, Kripke completeness, the finite model property, and decidability, which also yields their undecidability in $\mathop{\mathsf{NExt}} \mathsf{S4}_t$. We also construct infinitely many tabular extensions of $\mathsf{Grz}_t$ (and thus of $\mathsf{S4}_t$) whose coincidence problems are undecidable, while presenting one tabular extension of $\mathsf{Grz}_t$ and infinitely many ones of $\mathsf{S4}_t$ with a decidable coincidence problem. As a consequence, we obtain that the finite model property and tabularity are undecidable in $\mathop{\mathsf{Ext}} \mathsf{biIPC}$, and that there are infinitely many tabular extensions of $\mathsf{biIPC}$ whose coincidence problems are undecidable. These results clarify some similarities and differences between $\mathop{\mathsf{NExt}} \mathsf{Grz}_t$ and $\mathop{\mathsf{NExt}} \mathsf{Grz}$, $\mathop{\mathsf{NExt}} \mathsf{S4}_t$ and $\mathop{\mathsf{NExt}} \mathsf{S4}$, as well as $\mathop{\mathsf{Ext}} \mathsf{biIPC}$ and $\mathop{\mathsf{Ext}} \mathsf{IPC}$. The proofs adapt Chagrov's method of reducing from an undecidable problem for Minsky machines. We isolate and explicitly formulate the method of good valuations, a recurring technique underlying several proofs in the literature that use large frames, making it available for further applications.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-31T21:59:35Z
Amirhossein Akbar Tabatabai
arXiv categories: cs.LO, math.LO

In this paper, we establish exponential separations between Extended Frege systems for a range of intuitionistic substructural and linear logics. More precisely, for any logic $L$ below the intuitionistic logic obtained by extending $\mathbf{ILL}$ with structural rules, and any logic $M$ not contained in $L$, we construct a family of $\mathsf{FL_e}$-provable formulas that have short proofs in $M$-Frege but require proofs of exponential size in $L$-Extended Frege. The same result holds in the $!$-free settings, using $\mathbf{IMALL}$ and $\mathbf{FL_e}$ in place of $\mathbf{ILL}$. The key ingredient in proving these separations is a variant of the feasible disjunction property for $L$-Frege, which may be of independent interest.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-09-01T05:15:11Z
Leonardo Pacheco
arXiv categories: math.LO, cs.LO

A classical result in modal logic states that $\mathsf{S4}$ has $14$ modalities, that is, every sequence of negations, boxes, and diamonds is equivalent to one in a set of $14$ such sequences. We study analogous results for the non-classical analogues $\mathsf{CS4}$, $\mathsf{IS4}$, $\mathsf{GS4}$, and $\mathsf{GS4^c}$ of $\mathsf{S4}$. First, we show that, while all these logics have finitely many $\{\Box,\Diamond\}$- and $\{\neg,\Box\}$-modalities, the logic $\mathsf{CS4}$ has infinitely many $\{\neg,\Diamond\}$-modalities. Second, we show that $\mathsf{IS4}$ and $\mathsf{GS4}$ have finitely many $\{\neg,\Diamond\}$-modalities, but they have infinitely many $\{\neg,\Box,\Diamond\}$-modalities. At last, we show that $\mathsf{GS4^c}$ has finitely many $\{\neg,\Box,\Diamond\}$-modalities.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-09-03T21:54:01Z
Zalán Gyenis, Krzysztof Krawczyk
arXiv categories: math.LO

We solve an open problem posed by Peter Fritz in \cite{Fritz} by proving that there are uncountably many C-Post complete congruential modal logics which are neighborhood complete. The method is algebraic: we construct an uncountable sequence of varieties of modal algebras which are minimal in the lattice of all subvarieties of modal algebras and are generated by a single complete and atomic modal algebra.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-31T10:53:52Z
Ondřej Kuželka
arXiv categories: cs.LO, cs.DM

Every fixed first-order sentence $\varphi$ determines an enumerative sequence $n\mapsto\mathrm{FOMC}(\varphi,n)$, counting its models on the labeled domain $[n]$. We study the complexity of these sequences when logical specifications may use genuine unary function symbols and hence nested terms $x,f(x),f^2(x),\ldots$. We first prove that, for every fixed sentence $\varphi\in\mathrm{C}^1_{=}[f]$, with one unary function and an arbitrary finite relational vocabulary, $\mathrm{FOMC}(\varphi,n)$ is computable in time polynomial in $n$. By contrast, permitting either a second variable or a second unary function already yields hardness. Without counting quantifiers, there is a fixed sentence in $\mathrm{FO}^2_{=}[f]$ whose model-counting function is $\#\mathrm{P}_1$-complete. With one variable and two unary functions, there is a fixed constant-free universal sentence in $\mathrm{FO}^1_{=}[f,g]$, using only unary predicates besides $f$ and $g$, whose model-counting function is again $\#\mathrm{P}_1$-complete. We also relate labeled and unlabeled enumeration exactly. For every relational sentence $\varphi$, we construct an extension $\varphi_{\mathrm{aut}}$ in which a unary function records an automorphism and $\mathrm{FOMC}(\varphi_{\mathrm{aut}},n)=n!\cdot\mathrm{UFOMC}(\varphi,n)$, where $\mathrm{UFOMC}(\varphi,n)$ denotes the number of $n$-element models of $\varphi$ up to isomorphism. Thus automorphism marking gives a one-query exact reduction from unlabeled to labeled model counting at the same domain size. Over relational vocabularies of maximum arity at most $k$, where $k\geq2$, eliminating the auxiliary function yields single-query reductions from unlabeled $\mathrm{FO}^k_{=}$ and $\mathrm{C}^k$ model counting to labeled $\mathrm{FO}^{k+1}_{=}$ and $\mathrm{C}^{k+1}$ model counting, respectively.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-31T22:17:36Z
James Freitag, Scott Mutchnik
arXiv categories: math.LO, math.QA

Using ChatGPT 5.6, we find a counterexample to the stable forking conjecture. This answers a long-standing open question of Hart, Kim and Pillay (1996).

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-31T23:58:47Z
Anatole Dahan
arXiv categories: cs.LO, cs.CC, math.LO

We investigate the expressive power of fixed-point logics (FP) and their extensions in defining generating sets for accessible subgroups of definable permutation groups. This operation, computable in polynomial time via the Schreier-Sims algorithm, plays a central role in the group-theoretic approach to Graph Isomorphism and Graph Canonisation. In particular, it underpins polynomial-time canonisation for bounded colour-class graphs--a class for which no natural logic capturing P is currently known. We first show that this operation cannot, in general, be expressed in any logic for P. This limitation arises from the fact that accessible subgroups need not admit symmetric generating sets of polynomial size. However, we prove that when the base group admits a definable ordered generating set, the accessible subgroup operation becomes definable in fixed-point logic with the group order operator (FP + ord). This is achieved by partially simulating the Schreier-Sims algorithm within FP + ord. As a corollary, we show that fixed-point logic with counting (FPC) can also define the operation when the base group is abelian. In particular, FPC can define the automorphism group of any graph with abelian colours--despite being unable to canonise such graphs.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-09-01T13:32:07Z
Artem Chernikov, Yuyan He
arXiv categories: math.LO, math.CO

We prove that a relation obtained by composing arbitrary functions of arity $\leq k$ with a relation definable in an $n$-dependent structure is $kn$-dependent. This confirms a conjecture of Chernikov and Hempel. We also demonstrate optimality of the result.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-09-02T02:06:21Z
Makoto Yanagawa
arXiv categories: math.LO, math.GR

We prove that if a group $G$ contains a Baumslag-Solitar group $\mathrm{BS}(m,n)$, with $mn\neq0$, then the theory of fields with a $G$-action has no model companion. In particular, every group containing $\mathbb{Z}^2\cong\mathrm{BS}(1,1)$ has no model companion for its field actions, resolving a conjecture of Beyarslan and Kowalski. Consequently, there are no model companions for field actions of $\mathbb{Q}^2$, Thompson's groups $F,T,V$, or Higman's group. Our argument adapts Hrushovski's method for two commuting automorphisms. The key modification is the cyclotomic condition $θ_q$, which removes the need to prescribe a non-trivial action on a root of unity and thereby makes Hrushovski's method applicable after passing from a subgroup to an ambient group.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-09-02T07:06:41Z
Ulla Karhumäki, Nicholas Ramsey
arXiv categories: math.GR, math.AG, math.LO

We show that every faithful, transitive, and generically $(n+2)$-transitive action of a connected group $G$ on an irreducible variety $X$ of dimension $n > 0$, all defined over an algebraically closed field $F$, is isomorphic to the natural action of the projective linear group $PGL_{n+1}(F)$ on the projective space $\mathbb{P}^n(F)$. More precisely, we establish the Borovik-Cherlin conjecture for permutation groups $(G,X)$ definable in models of $ACF$.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-09-02T10:44:36Z
Zahra Mohammadi Khangheshlaghi, Rizos Sklinos
arXiv categories: math.LO

We show that the first-order theory of the Farey graph is $1$-ample but not $2$-ample. Along the way, we prove that it weakly eliminates imaginaries and observe that forking is trivial.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-09-03T14:01:46Z
Zhentao Zhang
arXiv categories: math.LO

Let $G$ be a definable group in an NIP theory. We prove that every minimal proximal definable $G$-flow is strongly proximal. Consequently, the universal minimal proximal definable $G$-flow $Π^{\mathrm{def}}(G)$ coincides with the minimal strongly proximal definable $G$-flow $Π^{\mathrm{def}}_{\mathrm{s}}(G)$. Furthermore, for a $p$-adic definable group $G$, we can compute $Π^{\mathrm{def}}(G)$ explicitly. We show that $Π^{\mathrm{def}}(G)$ is exactly $Π^{\mathrm{def}}(S)$ where $S$ is the semisimple part of the definably amenable-semisimple decomposition of $G$. In addition, $Π^{\mathrm{def}}(S)\cong S^*_\mathcal{F}(\mathbb{Q}_p)$, the space of types of full dimension on $\mathbf{F}$, where $\mathcal{F}=\mathbf{F}(\mathbb{Q}_p)$ for a flag variety $\mathbf{F}$ constructed from $S$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-31T04:56:40Z
Mateus Jesus de Arruda Campos, Gabriel Fernandes, Vinicius de Oliveira Rodrigues
arXiv categories: math.LO, cs.LG, math.PR

The fundamental theorem of statistical learning states that, under suitable measurability assumptions, finite Vapnik--Chervonenkis (VC) dimension guarantees that every proper consistent learning rule is probably approximately correct (PAC). Blumer, Ehrenfeucht, Haussler, and Warmuth showed, assuming the Continuum Hypothesis, that the "well-behavedness" condition of the concept class cannot be omitted: they constructed a concept class of Borel sets of VC dimension one admitting a consistent learning rule that is not PAC. We show that the Continuum Hypothesis is unnecessary. Working in Zermelo--Fraenkel set theory with the Axiom of Choice (ZFC) alone, we construct a concept class of Borel sets on $[0,1]$ of VC dimension one and a proper consistent learning rule that is not PAC. More precisely, for a suitable Borel probability measure and target concept, the rule has true risk one at every sample size on a set of samples of outer probability one. Consequently, finite VC dimension and Borel measurability of the individual concepts do not suffice to guarantee that every proper consistent learning rule is PAC. The result shows, with no need of extra set-theoretical assumptions, that the additional regularity assumption in the fundamental theorem cannot in general be omitted.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-31T07:43:13Z
Geng-Rui Zhang
arXiv categories: math.NT, math.LO

For every quadratic number field $K$, we prove a uniform $3$-unknown Diophantine definition of integer tuples in $\mathcal{O}_K$, allowing finitely many polynomial nonvanishing conditions. This yields an effective $+3$ transfer principle and a $13$-unknown representation of every recursively enumerable integer relation. Consequently, there exists an absolute degree bound $D_0\geq1$ such that for every quadratic number field $K$, there is no algorithm that, given \[ P(Y_1,\ldots,Y_{13})\in\mathbb{Z}[Y_1,\ldots,Y_{13}],\quad \mathrm{deg}\ P\leq D_0, \] decides whether $P=0$ has a solution in $\mathcal{O}_K^{13}$. The arithmetic input is a fourth-order Pell--Lucas congruence. It is a specialization of the norm-one Lucas multiplication formula, which yields exact valuations for the deviation of a Lucas quotient from its linear term, together with deviation criteria for Lucas--Wieferich and Wall--Sun--Sun primes. We also establish local surjectivity and $\ell$-adic density for second-order correction terms for norm-one Lucas sequences.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-31T08:19:32Z
Bokai Yao
arXiv categories: math.LO

We investigate the iterative conception of set in its most general form, allowing urelements without assuming that they form a set. We formulate this conception in two ways, as stage theory and as level theory, and develop a general theory of levels with urelements. Unlike their pure-set counterparts, the resulting stage and level theories are not set-theoretically equivalent; moreover, second-order level theory with urelements is not weakly quasi-categorical. We then consider further principles governing stages and levels, motivated by directedness, unboundedness, and reflection. Some of these principles restore set-theoretic equivalence between the corresponding theories, while their level-theoretic versions yield forms of quasi-categoricity. These principles form strict implication hierarchies, thereby revealing distinct stronger conceptions of set beyond the basic iterative conception.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-31T13:50:39Z
Jerome Clech
arXiv categories: cs.LO

We formalise computational free will by separating locally constrained admissibility from the selection of one global continuation. Global sections of a finite choice presheaf form an admissible set, GLUE; SELECT singles out the continuation realised at a pre-identified occurrence. A uniform trace relation certifies that continuation efficiently after the act, although it is assumed not to be uniformly anticipable in polynomial time from the prior occurrence input. Under explicit uniformity, balance, historical-completeness, and unique-projection assumptions, this trace defines a total FNP search relation with no deterministic polynomial-time selector. Thus existence of computational free will in the stated sense implies a separation between polynomially verifiable and polynomially solvable search, and hence that P differs from NP. The result is conditional and gives no unconditional class separation.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-31T21:57:33Z
Patrizio Cintioli
arXiv categories: math.LO

This paper proves that every nonrecursive many-one degree contains either exactly one or infinitely many finite-one degrees. This gives a negative answer to Open Question 2 of Richter, Stephan, and Zhang~\cite[p.~17]{RSZ}. Earlier work established that, for almost every $A\subseteq\N$ with respect to the standard product measure on $2^\N$, the degree $[A]_{\m}$ contains an infinite antichain of finite-one degrees~\cite{Cintioli}. Thus the question had already received an almost-sure negative answer; the present theorem settles it for every nonrecursive many-one degree.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-09-01T03:10:46Z
Evan Leach
arXiv categories: math.LO

We characterize the Borel sets with an infinite version of Karchmer and Wigderson's game linking finite circuit complexity to communication complexity. To this end, we formulate an infinite version of communication complexity and prove that a given subset of the Cantor space is Borel if and only if a certain infinite communication game is solvable. We utilize this connection to provide new elementary and purely combinatorial proofs of some classical results in descriptive set theory, including the analytic separation theorem and the equivalence of monotone and positive Borel sets. Another consequence is a characterization of Borel separability via the winner of a certain "cut-and-choose" game, which we use to obtain new combinatorial proofs that neither the set of ill-founded trees nor any infinite parity function is Borel.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-09-01T05:24:12Z
Mohamed Amine Bergach
arXiv categories: cs.PF, cs.AR, cs.LO

Where does a computer's energy go? Mostly into keeping, not into computing. A bit held in fast storage draws power for every second it stays there, and it costs energy again each time it moves between storage levels. We call the first cost \emph{rent} and the second \emph{fare}, and we state one law: the energy of a computation is at least its operations, plus rent on every live bit for as long as it lives, plus fare on every bit moved. The model under the law prices control as well as data. There is no free clock, and any unpriced register would make the theorems false. One lemma does most of the work: every use of a value is paid for by rent, by fare, or by computing the value again. Three things follow. Exact attention brings every past token back for every new one, so its energy grows with the square of the context length, while a recurrent model with a fixed state grows linearly. The square is a theorem for machines that never re-read past tokens. Under a stated serving hypothesis it is the fare on every past token, which passes the model's own arithmetic near ten thousand tokens, the point where long-context serving becomes bandwidth-bound today. Known bounds on memory over time become joule floors: on any sequential machine with volatile working storage, sorting $n$ items pays rent proportional to $n^2/\log n$ bit-steps on most inputs, and the bound for scrypt makes every password guess cost joules that no amount of parallel hardware reduces.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-09-01T08:17:19Z
Eric P. Astor, Laurent Bienvenu, Damir Dzhafarov, Ludovic Patey, Paul Shafer, Reed Solomon, Linda Westrick
arXiv categories: math.LO

Many statements studied in reverse mathematics can be seen as mathematical problems, formulated in terms of instances and solutions. We develop a framework of typicality encompassing measure and genericity, and we classify the reverse mathematics zoo in terms of which problems admit typical solutions. It turns out that even very weak problems do not admit typical solutions.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-09-01T17:56:48Z
Zhi-Wei Sun
arXiv categories: math.NT, math.LO

Hilbert's Tenth Problem over the integers was solved negatively by Y. Matiyasevich in 1970. In this paper, we prove that there is no algorithm to determine for any polynomial equation $P(z_1,\ldots,z_{10})=0$ (with integer coefficients and ten unknowns) whether it has integer solutions. This improves the previous 11 unknowns theorem.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-09-02T15:06:55Z
Guozhen Shen
arXiv categories: math.LO

The Erdős--Dushnik--Miller theorem states that for every aleph $κ$, \[ κ\to(κ,ω); \] that is, every coloring $c:[κ]^2\to2$ has either a $0$-homogeneous set of cardinality $κ$ or a $1$-homogeneous set of cardinality $ω$. In this article, we present a purely combinatorial proof of this theorem in $\mathsf{ZF}$ (i.e., Zermelo--Fraenkel set theory without the axiom of choice), avoiding any metamathematical considerations.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-09-02T18:09:45Z
Matteo Casarosa
arXiv categories: math.LO, math.CO

Combinatorial set theory provides several tools to study derived limits of certain inverse systems of abelian groups. Most known nonvanishing results for $\lim^n$ with $n>1$ depend on some guessing principles of the form $\mathrm{w}\lozenge(S)$ called weak diamonds. In this paper, we explore some applications of the guessing principle $\clubsuit(S)$ and its weakenings instead.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-09-03T14:32:06Z
Heng Li, Xizhi Liu
arXiv categories: math.CO, math.LO

Given a finite family $\mathcal F$ of forbidden $r$-graphs, the Turán problem asks for the maximum asymptotic edge density of $\mathcal F$-free $r$-graphs and the structure of near-extremal examples. We show that both questions can encode arbitrary computation. Fix a universal Turing machine $\mathsf U$. For every sufficiently large fixed $r$, there is a rational $τ_r\in(0,1)$ such that, from each binary word $β$, one can construct a finite family $\mathcal F_{r,β}$ with $π(\mathcal F_{r,β})=τ_r$ if $\mathsf U$ does not halt on $β$, and $π(\mathcal F_{r,β})>τ_r$ otherwise. The same dichotomy governs extremal structure. We construct finite families $\mathcal G_{r,β}$ such that nonhalting gives a unique extremal limit and Erdős--Simonovits stability, whereas halting gives two nonempty compact extremal phases separated by the sign of a fixed continuous statistic. Hence uniqueness and connectedness of the extremal space, symmetry breaking, two-phase behavior, and stability are all undecidable. The reductions are effective and verifiable in ZFC by finite certificates. Consequently, for every consistent computably axiomatized extension of ZFC and every sufficiently large fixed $r$, there is a finite family $\mathcal F$ for which the true equality $π(\mathcal F)=τ_r$ is neither provable nor refutable; analogous independence holds for the five structural properties above. We also obtain effective approximation, classify exact comparison complexity, and show that the smallest improvement witnesses have Busy-Beaver growth, with no uniform computable positive lower bound on the density gain.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-09-03T16:53:22Z
Fabio F. G. Buono
arXiv categories: cs.CR, cs.AI, cs.LO

For every coherent and sufficiently expressive finite syntactic system S, we prove the existence of at least one theorem that S cannot produce autonomously. The result is a metatheorem: it proves the existence of a theorem, and applies to every finite syntactic system - security mechanisms, AI systems, formal verifiers, legal systems, economic models, and the formal system in which it is itself proved.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-09-03T18:16:41Z
Sebastián Barbieri, Nicanor Carrasco-Vargas, Paul Toussaint
arXiv categories: math.DS, math.GR, math.LO

We prove that for any cocompact Fuchsian group the class of Medvedev degrees attained by subshifts of finite type is the class of $Π_1^0$ degrees. This result relies on the construction of a rigid hierarchical structure in a graph model of the hyperbolic plane, and on the fact that every such group admits a representation in $\operatorname{PSL}_2(\mathbb{R})$ such that the matrices in the image have coefficients that are computable real numbers.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-09-04T02:24:40Z
Tatsuji Kawai
arXiv categories: math.LO

In the context of constructive reverse mathematics, we show that Brouwer's fixed-point theorem and weak König's lemma (WKL) are equivalent. To derive WKL from Brouwer's fixed-point theorem, the construction of a continuous function on the unit square without fixed points due to Orevkov [Soviet Math. Doklady (1963), 1253--1256] is generalised to yield a uniformly continuous function on the unit square whose fixed points encode information about infinite paths of a given infinite tree.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-31T19:44:57Z
Alain Connes, Caterina Consani
arXiv categories: math.AG, math.CT

We construct the absolute algebraic geometry of the compactification $\overline{\text{Spec}\, \mathbf Z}$ by amalgamating the affine absolute curve $(\text{Spec}\, \mathbf Z)_{\mathbf{F}_{1}}$ with an archimedean component defined over the signed extension $\mathbf{F}_{1^2}$ of $\mathbf{F}_1$. By adjoining a formal imaginary unit to the absolute projective line, we obtain an equivariant topos endowed with a canonical geometric inversion symmetry, which induces the twistor real structure on its complex points. This archimedean geometry is incorporated into a global absolute curve defined as an internal object of the odd arithmetic topos, dual to the multiplicative monoid of odd positive integers, and governed by the intrinsic Hopf structure of spherical $\mathbf{F}_{1^2}$-algebras. The restriction of the absolute Frobenius action to odd integers is forced arithmetically by the extension of scalars to $\mathbf{F}_{1^2}$. On complex points, the resulting dynamics simultaneously generates the Adams operations and complex conjugation on real Hodge structures. At the categorical level, the odd arithmetic topos originates in the pericyclic category, whose $λ$-operations provide a conceptual interpretation of the local factors of geometric L-functions.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-09-01T05:57:40Z
Masai Noda
arXiv categories: math.CT, math.DG

There exists an adjoint pair (D, C) of functors between the category of diffeological spaces and that of topological spaces. In this article, by using the functors, we introduce two pairs of functors between the categories of sheaves on a diffeological space and on a topological space. Then, the adjointness of the novel functors up to the functors induced by the unit and counit of C and D is clarified. There is no natural functor between sites obtained by a diffeological space and a topological space. Therefore, the adjunctions on the categories of sheaves are elaborated without applying the general theory of topoi.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-09-03T05:16:21Z
Jiacheng Liang
arXiv categories: math.AT, math.AG, math.CT

We introduce the atomic smashing frame, extending the Balmer spectrum from tensor-triangular geometry to an arbitrary presentably symmetric monoidal $\infty$-category $\mathcal{V}$. This yields a formulation of the telescope conjecture for $\mathcal{V}$ and recovers the classical Balmer spectrum in the stable compactly-rigidly generated case. Exploiting dualizable and rigid $\infty$-categories, we establish a correspondence between smashing ideals and locally rigid localizations. This leads to a recollement theorem for smashing frames in the (pre)stable setting, together with an atomic refinement in the stable compactly-rigidly generated case. As a major application to chromatic homotopy theory, we show that the natural projections induce an embedding of the smashing frame of $\mathrm{Sp}$ into the product of the smashing frames of the monochromatic layers $\mathrm{Sp}_{T(n)}$, over all primes and heights. In particular, the spatiality of the smashing frame of $\mathrm{Sp}$ reduces entirely to that of $\mathrm{Sp}_{T(n)}$. In the unstable setting, we characterize the telescope conjecture for $\infty$-topoi in terms of smashing fields, and for connective module categories and hypercomplete connective sheaves in terms of Pierce-type conditions. Finally, we introduce the Serre smashing frame. Over a connective $\mathbb{E}_\infty$-ring $R$, this frame sits between the atomic and usual smashing frames, providing an intermediate structural layer in the study of the telescope conjecture for the connective $R$-module category.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-09-03T07:48:57Z
Kevin Coulembier
arXiv categories: math.CT

In [B2] Balmer introduced the homological spectrum of a rigid tensor-triangulated category, and had the ``nerves of steel'' not to conjecture that it was in bijection with the prime spectrum, despite an ``avalanche of examples''. Naturally, the statement came to be known as Balmer's Nerves of Steel Conjecture. More recently, in [NVY] the conjecture was stated explicitly and extended to a more general non-symmetric context. In this paper we provide a counterexample to the original suggestion in [B2], so also to the conjecture from [NVY]. A first counterexample was recently constructed in [BHR].

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-09-03T08:14:37Z
Peng Xu
arXiv categories: math.CT, math.AG

Let k be a field of characteristic p>0. We prove that for every p-decomposition group P, the tensor-triangulated category \operatorname{DPerm}(P;k) is stratified and its Balmer spectrum is generically noetherian. As an arithmetic application, we show that for a nonarchimedean local field F with residue characteristic \ell, the category \(\operatorname{DAM}(F;k)\) of derived Artin motives is stratified if and only if \ell\neq p. In the stratified case its Balmer spectrum is generically noetherian; consequently, \operatorname{DAM}(F;k) satisfies the telescope conjecture.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-09-04T02:47:02Z
Zhonghui Sun
arXiv categories: math.AT, math.CT, math.KT

Bicategorical shadows provide a categorical framework that encompasses Hochschild homology and topological Hochschild homology (THH), encodes their Morita invariance, and extends the notion of trace from symmetric monoidal categories to bicategories. Certain equivariant variants, such as $C_n$-twisted THH, do not fit into the ordinary shadow framework. We introduce bicategories with $G$-twisting data and show that every ordinary shadow on such a bicategory induces, for each $g\in G$, a $g$-twisted shadow on the associated bicategory of $G$-twists. These $g$-twisted shadows are invariant under $G$-Morita equivalence; examples include $C_n$-twisted THH and twisted Hochschild homology of $C_n$-Green functors. We further define a $g$-twisted bicategorical trace that recovers the $g$-twisted Hattori--Stallings trace. For $C_n$-Green functors, the orbitwise $g$-twisted Hattori--Stallings traces assemble into a morphism of $C_n$-Mackey functors that, at the orbit $C_n/C_n$, recovers the degree-zero twisted Dennis trace.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-09-04T09:39:23Z
Roberto Tellez-Dominguez
arXiv categories: math.DG, math-ph, math.AT, math.CT

We construct a weak Lie 3-group $T_2 \mathbb B^{F_1}_n$ from the 2-category of gerbes over $\mathbb R^n / \mathbb Z^n$ and the $\mathbb R^n/ \mathbb Z^n$-action on it by pullback along translations. We also construct a homotopy equivalence between $T_2 \mathbb B^{F_1}_n$ and a different Lie 3-group $T_2 \mathbb D^{F_1}_n$, which admits a dimensional reduction to the homotopy equivalence of Lie 2-groups introduced by Nikolaus and Waldorf to model half-geometric T-duality. This is a first step towards establishing a higher form of T-duality for 2-gerbes over torus fibrations, relevant to supergravity and M-theory.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-31T13:09:15Z
Ryu Tomonaga
arXiv categories: math.RT, math.CT, math.RA

The notion of $d$-stable dg categories axiomatizes $d$-cluster tilting subcategories of stable dg categories. We establish an Auslander correspondence for $d$-stable dg categories: we characterize the $d$-stability of an additive connective dg category in terms of coherence, weak global dimension, and a duality on finitely presented modules. This gives a homological characterization of $d$-stability and reveals it as a twisted form of $(d+1)$-Calabi--Yau duality. For locally finite connective dg algebras, this interpretation becomes particularly transparent under Koszul duality, where $d$-stability corresponds to a shifted self-injectivity condition on the Koszul dual. Following the constructions of Amiot, Guo and Keller, for a $d$-stable dg category $M$, we introduce its $d$-cluster dg category $\mathcal C_{d,{\rm dg}}(M):=\operatorname{per}_{\rm dg}M/^\mathbb{L}\mathcal D^b_{\rm fp, dg}(M)$. Using our Auslander correspondence, we show that $\mathcal C_{d,{\rm dg}}(M)$ contains $M$ as a $d$-cluster tilting subcategory. In particular, every $d$-stable dg category can be realized as a $d$-cluster tilting subcategory of a stable dg category. We then develop cluster Morita theory: a pretriangulated dg category equipped with a $d$-cluster tilting subcategory $M$ is quasi-equivalent to $\mathcal C_{d,{\rm dg}}(M)$. Thus the connective dg structure of a cluster tilting subcategory determines its ambient dg category up to quasi-equivalence. As an application of cluster Morita theory, we prove a Morita-theoretic variant of Amiot's conjecture. More precisely, we establish a Calabi--Yau correspondence: for a locally finite $d$-stable dg category $M$ over a field, right $(d+1)$-Calabi--Yau structures on $\mathcal D^b_{\rm fp, dg}(M)$ are in bijection with right $d$-Calabi--Yau structures on $\mathcal C_{d,{\rm dg}}(M)$.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-31T16:03:01Z
Rio Haeussler Albi
arXiv categories: math.AG, math.CT

We define semiorthogonal decompositions of stable $\infty$-categories of length $n$, extending the theory of semiorthogonal decompositions presented in arXiv:2106.02873. Prior to this, we explicitly construct an equivalence of $\infty$-categories relating Waldhausen diagrams to coherent complexes in stable $\infty$-categories. This allows us to view semiorthogonal decompositions from two different perspectives, each of which has its unique advantages and disadvantages. Under mild conditions, we prove a reconstruction theorem for semiorthogonal decompositions, recovering a stable $\infty$-category as the (op)lax limit of a diagram formed by the subcategories constituting its decomposition. We apply this reconstruction in the case of Beilinson's exceptional collection, to obtain a reconstruction of $D^b(\text{Coh}(\mathbb{P}^n))$.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-31T19:54:08Z
Zaqueu Cristiano, Wellington Marques de Souza, Javier Sánchez
arXiv categories: math.RA, math.CT, math.RT

We continue the study of the basic theory of object-unital groupoid graded rings. In this work, we are especially interested in nilpotency conditions on the graded Jacobson radical. We introduce the concept of left/right objectwise nilpotency of graded ideals, and prove that this condition is appropriate for obtaining graded generalizations of the Hopkins--Levitzki theorem. Although this condition is not symmetric, we show that its two-sided version is suitable for defining gr-semiprimary rings. It is known that one-sided $Γ_0$-artinian rings need not be $Γ_0$-noetherian, but using our tools we prove that one-sided gr-hereditary $Γ_0$-artinian rings, two-sided $Γ_0$-artinian rings, and $d$-finitely generated one-sided $Γ_0$-artinian rings are $Γ_0$-noetherian. However, the first class need not be gr-semiprimary, whereas the other two always are. We illustrate our results with several (counter)examples, especially involving graded upper triangular matrices.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-09-01T02:42:18Z
Jing He, Panyue Zhou
arXiv categories: math.RT, math.CT

Chen, Liu, Lu, and Zhang recently constructed a pretriangulated category with invertible suspension in which Verdier's octahedral axiom fails. We introduce a general enlargement construction for right pretriangulated categories and show that it preserves axioms (RTR1)-(RTR3), while failure of (RTR4) is detected by the forgetful functor. Applied to their type $A_5$ example, the construction yields a right pretriangulated category that is not right triangulated. In this example, the suspension is faithful but not essentially surjective.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-09-01T15:26:42Z
Antonio Del Donno, Giovanni Gava, Emanuele Latini, Thomas Weber
arXiv categories: math.QA, math.CT, math.DG, math.RA

We develop a theory of first order differential calculi in braided monoidal categories and classify braided covariant and bicovariant calculi on braided Hopf algebras. We show that, under certain conditions, bicovariant calculi can be transmuted to braided bicovariant calculi. For Radford--Majid biproducts, we combine bicovariant calculi on a Hopf algebra and braided bicovariant calculi on the corresponding braided Hopf algebra to covariant smash product calculi. The associated Maurer--Cartan form is shown to decompose into a direct sum of the Maurer--Cartan forms of the structure Hopf algebra of the quantum principal bundle and the braided Hopf algebra on the base. Geometrically, this construction realises the quantum affine extension of a given Hopf algebra, and we prove that the resulting quantum principal bundle is equipped with a frame resolution induced by the quantum Maurer--Cartan form. Building on this correspondence, we introduce and develop the notion of quantum $\textrm{G}$-structure, proving that quantum $\textrm{G}$-structures are quantum frame resolutions on the reduction. The theory is illustrated by examples based on transmutations of higher analogues of Sweedler's Hopf algebra and on the braided quantum plane, seen as a Yetter--Drinfeld module of $O_q(\mathrm{GL}_2)$.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-09-01T17:07:17Z
Alexandru Chirvasitu
arXiv categories: math.QA, math.CT, math.RA

We prove that a coaction of a Hopf algebra on another preserving the latter's associative-algebra structure and comultiplication automatically also preserves the counit, antipode, and tensor-interchange map and in fact factors through the coaction dual to an action of an affine group scheme by Hopf-algebra automorphisms. This generalizes and unifies a number of results to the effect that quantum groups have only classical symmetries, due to Kasprzak et al., Budziński-Kasprzak and Brannan et al. The stated automatic classicality follows from the fact that the antipode, counit and tensorand-interchange of a Hopf algebra internal to any symmetric monoidal category are contained in the (non-symmetric) monoidal subcategory generated by the associative-algebra structure and the comultiplication, assuming a weak form of arrow-retraction invariance.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-09-02T02:53:02Z
Jing He, Panyue Zhou
arXiv categories: math.RT, math.CT

Let $M$ be a silting object in an idempotent complete algebraic triangulated category $\mathcal T$. Put $B={\rm End}_{\mathcal T}(M)$, and let $\mathbb{P}_M\colon {\rm pr}(M)\to K^{[-1,0]}({\rm proj}B)$ be the presentation functor associated with $M$. It was recently asked whether $\mathbb{P}_M(T)$ must be tilting whenever $T\in{\rm pr}(M)$ is a tilting object. We answer this question in the negative by giving an explicit finite-dimensional example. Namely, for $$ Λ=k(1\xrightarrowα2\xrightarrowβ3\xrightarrowγ4)/(αβγ),$$ we construct a silting object $M\in K^b({\rm proj}Λ)$ and a tilting object $T=ΣΛ\in{\rm pr}(M)$ for which $$ {\rm dim}_k{\rm Hom}_{K^b({\rm proj}B)}\bigl(\mathbb{P}_M(T),Σ^{-1}\mathbb{P}_M(T)\bigr)=1.$$ Thus $\mathbb{P}_M(T)$ is a two-term silting complex but not a tilting complex.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-09-03T07:05:33Z
Marcello Lanfranchi
arXiv categories: math.CT, math.AG, math.DG

Classic Lie theory establishes a correspondence between Lie groups, which are internal group objects in the category of smooth manifolds, and Lie algebras. An analogous correspondence also exists for group objects in affine schemes. Both smooth manifolds and affine schemes form tangent categories, which provide a categorical context for differential geometry. Therefore, it is natural to ask whether the Lie correspondence can be constructed entirely from the tangent structure. Building on work of Cockett and Schwarz, we develop an internal Lie group-Lie algebra correspondence in tangent categories. We introduce Lie group objects as group objects in a tangent category which admit a tangent space at the unit. For any group object, we construct a Lie functor and show it is tangentially representable exactly when the group object is a Lie group. Representability then yields an internal Lie algebra whose underlying object is the tangent space at the unit. We prove this Lie algebra is a differential Lie algebra, with a bilinear Lie bracket induced by the adjoint representation, and we extend the construction to a functor from Lie groups to differential Lie algebras. Finally, we recover the usual Lie correspondences in both differential and algebraic geometry.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-09-03T09:47:35Z
Ivan Di Liberti, Luca Reggio
arXiv categories: math.CT, math.LO, math.RA

For categories, being balanced (meaning that every arrow that is both epic and monic is an isomorphism) can be regarded as a strong tameness property which plays an important role, for example, in algebra and logic. We study the problem of associating a balanced companion category, called \emph{Beth companion}, to a locally finitely presentable category (equivalently, the category of models of a finitary essentially algebraic theory). We show that, if it exists, the Beth companion is unique and can be described in terms of \emph{saturated} objects. Under some additional assumptions, we prove that Beth companions can be computed as orthogonality classes, and admit a syntactic presentation via Gabriel--Ulmer duality. Finally, we establish conditions for the transfer of properties, ensuring, for instance, that if the original category is equivalent to a (quasi)variety, its Beth companion is too.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-09-03T16:44:05Z
Kenichi Shimizu, Harshit Yadav
arXiv categories: math.QA, math.CT

Let $\mathcal{B}$ be a braided finite tensor category and let $A$ be a simple commutative algebra in $\mathcal{B}$. We construct an order-reversing Galois connection between subalgebras of $A$ and tensor subcategories of $\mathcal{B}_A$. Let $\mathcal{B}'$ denote the Müger center and set $A':=A\cap\mathcal{B}'$. The closure operators are $B\mapsto\langle B,A'\rangle_{\mathrm{alg}}$ and $\mathcal{E}\mapsto\langle\mathcal{E},\mathcal{B}_A^{\mathrm{loc}}\rangle_{\otimes}$. Thus the closed subalgebras are those containing $A'$, while the closed tensor subcategories are those containing $\mathcal{B}_A^{\mathrm{loc}}$; equivalently, the fixed-point intervals $[A',A]_{\mathrm{alg}}$ and $[\mathcal{B}_A^{\mathrm{loc}},\mathcal{B}_A]_{\otimes}$ are anti-isomorphic as lattices. For a finite tensor category $\mathcal{C}$, the canonical algebra in $\mathcal{Z}(\mathcal{C})$ yields an anti-isomorphism between its subalgebras and tensor subcategories of $\mathcal{C}$. When $\mathcal{B}$ is nondegenerate, Frobenius extensions correspond to unimodular tensor subcategories. For a Hopf algebra in $\mathcal{B}$, the correspondence specializes to an order-preserving bijection between Hopf ideals and normal left coideal subalgebras.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-09-03T18:10:30Z
Harsh Beohar, Mike Cruchten, Georg Struth
arXiv categories: cs.FL, cs.LO

Language recognition by homomorphisms is a central construction of algebraic language theory. Initially studied for monoids and semigroups, it has subsequently been expanded to other algebraic structures. Our new categorical account is based on fibrations, which have already seen other applications in automata theory. Languages and surjective homomorphisms give indeed rise to two fibrations, and the notion of language recognition is stable under reindexing. We develop this framework in a category with a factorisation system and address two main technical questions in the fibrational setting. First, we provide sufficient conditions under which languages have syntactic quotients (which is a generalisation of syntactic congruences) and we show how such quotients can be described in some concrete cases using a result by Slomiński. Second, we introduce sufficient conditions under which (regular) languages are closed under certain J-limits and J-colimits.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-09-03T19:50:56Z
Juan Antonio Vega Coso
arXiv categories: math.CT, math.PR

This paper establishes the algebraic and categorical foundations of spectral duality structures (SDS). We show that the class of all SDS admits the structure of a graded monoidal category, in which the degree K is the fundamental invariant indexing the strata. We define the Cartesian product and the disjoint union of structures, together with morphisms preserving the involution and the weights, and we prove that C* = 1/(1+sqrt(K)) is a functor constant on each stratum. Objects are classified up to isomorphism by the combinatorial type (k,f), the degree K, and a multiset of inversion classes [r] = {r, 1/r}. We further prove that the response rank equals exactly the number of non-trivial pairs k, and we connect the categorical structure with the Fisher-Rao geometry developed in a companion paper. The SDS, originally identified in problems of stochastic resetting, thus emerges as an autonomous mathematical object with a rich algebraic structure and a natural geometric realisation.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-09-01T21:04:18Z
Luis Gambarte
arXiv categories: math.CT

The notion of a generalised category with families, introduced by Coraglia and Emmenegger is one of the most general notions introduced to capture categorically the notion of dependent typing. It is shown that these generalised categories with families are biequivalent to comprehension categories. We will show that the notion of a (2-dep,$Σ$)-category, an extension of the notion of a (dep,$Σ$)-category, introduced by Petrakis, is not biequivalent to generalised categories with families, but instead is equivalent to a direct generalisation of that notion.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-09-02T13:39:42Z
Francesco Dagnino, Amin Farjudian, Eugenio Moggi
arXiv categories: math.GN, cs.LO

We study the relationship between quasi-uniform spaces, topological spaces, and quantale-valued metric spaces. Our main result is a metrization theorem establishing an equivalence between the category of quasi-uniform spaces and a category of quantale-valued metric spaces. We also obtain a quantale-based metrization theorem for arbitrary topological spaces that refines existing constructions. These results identify quasi-uniformities as the appropriate qualitative counterpart of quantale-valued metrics. Building on this correspondence, we show that the Hausdorff-Smyth monad on quantale-valued metric spaces, which is used in quantitative robustness analysis, arises as a lifting of a corresponding monad on quasi-uniform spaces along the equivalence. This provides a unified categorical framework connecting topology, quasi-uniformity, and quantitative robustness analysis.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-09-02T14:35:26Z
Julien Lamiroy, Benoît Valiron, Renaud Vilmart
arXiv categories: cs.LO

Although the circuit model for quantum computation is well established, it is incapable of representing non-causal higher-order quantum processes such as the quantum switch. If several models of non-causal quantum computation have been considered in the literature, the approaches have so far only been focusing on the physicality of such processes, using matrices and other techniques from linear algebra. If these approaches are expressive, they however only provide a static and monolithic understanding of these processes. In this article, we propose a new formalism for non-causal, higher-order quantum processes. Based on a Curry-Howard interpetation, our proposal offers a computational interpretation that is both compositional and modular. In particular, we present Intuitionistic Unitary Linear Logic (IULL), a logic based on linear logic focusing on conservation of unitarity for higher order terms. We prove the coherence of IULLL, its completeness with regard to unitaries, and the admissibility of its cut rules. We finally discuss the validity of our approach by revisiting known non-causal quantum processes with IULL.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-09-02T17:54:57Z
Mario Román
arXiv categories: cs.PL, cs.LO

We introduce a do-notation metalanguage for causal probabilistic programming. The metalanguage is based on magmads: non-associative monads. We derive causal probabilistic programming constructs from non-associativity and the primitives of probabilistic programming.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-09-03T07:29:09Z
Jean-Simon Pacaud Lemay, Chad Nester
arXiv categories: math.CT, cs.LO

We study the override and update operators on partial functions from the perspective of restriction categories. We propose a definition of override restriction categories, in which both of the operators in question exist. We prove a number of results concerning these operators and their relationship to the structure of the ambient restriction category, as well as relating them to the existing literature on the override and update operators. We provide various examples of override restriction categories and in particular show that every classical restriction category is an override restriction category.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-09-03T12:51:10Z
Mingsheng Ying, Zhicheng Zhang, Kean Chen
arXiv categories: quant-ph, cs.PL, cs.SE

In this paper, we introduce a notion of abstract quantum data type within the framework of universal algebra. This notion provides an algebraic foundation for describing data abstraction in quantum programming. We formally define a quantisation of classical data types and show that their equational specifications can be soundly lifted to the quantum setting. Two standard quantisation methods for classical functions, namely the bit oracle and the phase oracle, arise as special cases of this general construction. We illustrate the framework with applications to quantum arrays and quantum error-correcting codes, showing how they can be understood through the lens of data-type quantisation. We further establish conditions under which quantisation preserves structural relationships and constructions of classical data types, including embeddings, isomorphisms, and products.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-09-04T10:35:28Z
Nelson Martins-Ferreira
arXiv categories: math.CT

This article develops the notion of a computational category, motivated by the observation that many mathematical structures occurring in scientific computing already admit concrete algorithmic representations. Finite sets, finite-dimensional vector spaces, relations, and graphs may all be represented through elementary MATLAB and Octave data structures such as indexing vectors, matrices, logical arrays, and sparse matrices. The central idea is that a category may often be described through a category of canonical representatives indexed by the natural numbers. This viewpoint leads naturally to representative categories whose objects are dimensions and whose morphisms are finite computational data structures. The resulting framework unifies several examples, including matrix categories, index categories, categories of column spaces, row-based models of finite sets, and categories combining finite subsets with finite-dimensional vector spaces through mixed morphisms. The paper also introduces computational categories with distinguished non-finite representatives, extending the finite setting while retaining concrete coordinate descriptions. Throughout, categorical constructions are interpreted algorithmically and implemented using standard MATLAB and Octave operations. The work contributes to a computational perspective on category theory and, conversely, to a categorical understanding of matrix-oriented scientific computing.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-31T07:03:44Z
Michal Hevessy, Benjamin Vejnar
arXiv categories: math.LO, math.DS

In this paper, we study how the classification complexity of natural orbit equivalence relations changes when the full homeomorphism group of a compact metrizable space is replaced by a dense non-closed subgroup. For a compact space $X$ and a subgroup $G \leq \mathcal{H}(X)$, we consider three canonical actions: the left shift action on $\mathcal{H}(X)$, the induced hyperspace action on $\mathcal{F}(X)$, and the conjugation action on $G$ We first analyze subgroups of the group $\mathcal{H}^+([0,1])$ of increasing interval homeomorphisms, focusing on bi-Lipschitz homeomorphisms, diffeomorphisms, and bi-absolutely continuous homeomorphisms. We show that, in contrast to the behavior of closed subgroups, passing to these subgroups strictly increases the complexities of the associated classification problems or makes them incomparable with the corresponding full-group relations. In the second part, we investigate hyperspace actions of bi-absolutely continuous homeomorphisms on the Cantor space and the Hilbert cube with respect to some Borel probability measure and show that a similar behavior occurs on these spaces as well.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-31T18:00:04Z
Yu-Zhe Liu
arXiv categories: math.RA, math.CT, math.FA, math.RT

We define the integral profiles of all modules and introduce integral coefficient rings ${^{\mathscr{P}}\mkern-6.5mu\text{\&}\mkern-5.5mu{_\mathscr{I}}}(A)$ for all finite-dimensional complex algebras $A$. The integral profile of a module is a matrix with parameters. We provide a classification theorem for modules, to be precise, (1) two modules $M\cong N$ are isomorphic if and only if their integral profiles are similar, i.e., $M\cong N$ if and only if $\displaystyle \int M \sim \int N$. That is, the integral profile is a complete invariant of finite-dimensional modules. Furthermore, we show the following results in this paper: (2) we introduce the central integrals of algebras and show that it is isomorphic to the center of algebras; (3) we provide a descriptions for some special modules; (4) integral coefficient ring of $A$ (with a compatible orthogonal fixed embedding system) has Morita invariance; (5) the global dimension of $A$ is finite if and only if the embedded integral profile of $\mathrm{top}(A)$ lies in ${^{\mathscr{P}}\mkern-6.5mu\text{\&}\mkern-5.5mu{_\mathscr{I}}}(A)[x]$; (6) the finitistic dimension of $A$ is finite if and only if each embedded integral profile of $M$ lying in ${^{\mathscr{P}}\mkern-6.5mu\text{\&}\mkern-5.5mu{_\mathscr{I}}}(A)[x]$ implies that its degree is less than or equal to a fixing integer $d\in\mathbb{N}^+$.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-09-01T00:29:20Z
B. Miller
arXiv categories: math.DS, math.LO

For all $d \ge 3$, we provide an example of a homeomorphism of Cantor space that has an uncountable $d$-scrambled set but no $d$-scrambled Cantor set.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-09-01T02:39:34Z
Gabriel Fernandes, João Marcelo Maciel Messias
arXiv categories: math.GN, math.LO

We establish the cardinal inequality \(|X|\leq 2^{t(X)Hψ(X)}\) for every Hausdorff SDL space \(X\), where \(t(X)\) and \(Hψ(X)\) denote the tightness and the Hausdorff pseudocharacter of \(X\), respectively. Since both invariants are bounded by \(χ(X)\), this yields \(|X|\leq 2^{χ(X)}\). As a consequence, every first-countable Hausdorff strongly cellular--Lindelöf space has cardinality at most the continuum. These results answer Questions~2.1 and~2.2 of Bella and Spadaro. An intermediate result is a uniform bounded-decomposition property for SDL spaces; in particular, their strict quasi--Lindelöf number satisfies \(\sqL(X)\leq t(X)\).

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-09-01T08:22:16Z
Noa Lavi
arXiv categories: math.AC, math.LO

Factorization in rings of the form $K((G^{\le 0} )) $ exhibits pathological behavior due to divisibility by monomials. It remains open whether this is the only obstruction and whether the quotient by the ideal generated by all monomials is a unique factorization domain. Prior to this work, the only instances of unique factorization beyond the irreducible elements followed directly from the primality of elements which aren't divisible by any monomial and whose support has order type $ω$ or $ω+1$. Using the $RV$ tool from valuation theory as a key ingredient, we establish unique factorization for elements of $ K((\mathbb{R}^{\le 0}))$ which aren't divisible by any monomial and whose support has order type $ω^α $ or $ω^α+1 $ for a large class of non additively principal ordinals $α$.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-09-01T15:53:04Z
Miguel Campercholi
arXiv categories: math.RA, math.LO

Global representations are subdirect representations satisfying a sheaf-like local-to-global patching principle. We develop a unified and simplified theory of such representations. For quasivarieties with a near-unanimity term, this framework recovers the main classical representation theorems through a common argument and yields a general representation by factors of bounded subdirect width. When the relatively subdirectly irreducible members form a universal class, we obtain an optimal result: every relatively congruence-distributive algebra admits a global representation by relatively globally indecomposable factors, which we characterize explicitly. We also provide a converse: global representations by factors of bounded relative subdirect width force the existence of a near-unanimity term. Adding semisimplicity to the hypotheses of the main theorem yields optimal representation results for filtral quasivarieties and dual discriminator varieties, together with a simple description of the globally indecomposable algebras. The technical engine behind these results is a new infinitary extension of the congruence-system component of the Baker--Pixley theorem.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-09-01T21:31:22Z
Sam Whitmire
arXiv categories: math.FA, math.GN, math.LO

In his 1994 doctoral thesis, Bossard introduced the notion of the non-universal tree $T_{NU}(X)$ associated with each separable Banach space $X$ which does not contain an isomorphic copy of $C(2^\mathbb{N})$. Together with the order operation defined on well-founded trees, we obtain a method of classifying the complexity of separable Banach spaces by the degree of isomorphism of finite-dimensional subspaces of $C(2^\mathbb{N})$. Despite further refinement of this concept in later years, we are unaware of any specific instances of direct exhibitions of the order of the non-universal tree for a concrete space and basis. We show that if $H$ is any separable Hilbert space, then $o(T_{NU}(H)) = ω + 1$ when taken with respect to the Haar basis for $C(2^\mathbb{N})$, demonstrating that the class of Hilbert spaces is the least complex class with respect to this measurement when considering this basis.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-09-02T17:16:54Z
Jason Zesheng Chen
arXiv categories: math.LO

Kechris asked whether essential freeness of countable Borel equivalence relations is preserved under extensions of finite index. Kaya proved that every such extension of a relation $E$ is Borel reducible to the equivalence relation $E^{\mathrm{fin}}$ on nonempty finite subsets which records the $E$-classes met by the subset. We show that $E^{\mathrm{fin}}$ is essentially free whenever $E$ is. This gives an affirmative answer to Kechris's question.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-09-02T20:02:15Z
Ruiwen Dong, Doron Shafrir
arXiv categories: math.NT, cs.LO

Let $R$ be a commutative ring and $f(a_1, \ldots, a_n) = \sum_{i=1}^k r_{i1}^{a_1} \cdots r_{in}^{a_n} m_i$ be a linear-exponential map over an $R$-module $M$. Dong and Shafrir (2026) showed that, when $\ell M = 0$ for some $\ell \in \mathbb{N}_{>0}$, the zero set of $f$ is the intersection of effectively computable $p$-normal sets, where $p$ ranges over the prime divisors of $\ell$. This generalizes an earlier theorem of Derksen and Masser (2012) on the solution set of $S$-unit equations over fields of positive characteristic. The purpose of this paper is twofold. First, we give a shorter proof of Dong and Shafrir's result, using the theorem of Derksen-Masser as a blackbox. Our proof also yields a decomposition of the zero set as a positive Boolean combination of affine transformations of zero sets of linear-exponential equations over fields. Second, we prove a multi-dimensional generalization of the Skolem-Mahler-Lech theorem over rings of finite characteristic. Specifically, we show that the zero set of every $n$-dimensional linear recurrence sequence over an $R$-module $M$ satisfying $\ell M = 0$ is the intersection of effectively computable $p$-normal sets (in $\mathbb{N}^n$), where $p$ ranges over the prime divisors of $\ell$. For example, this gives a decision procedure for whether two classical linear recurrence sequences have a common value over a ring of characteristic $p^a$ or $p^a q^b$, where $p$ and $q$ are primes.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-09-03T22:37:04Z
Aishni Parab
arXiv categories: cs.AI, cs.PL, cs.SC

Humans can learn and generalize novel concepts from sparse data because they express knowledge in rich structural formats. In this paper, we propose that programs are a strong candidate for universal representation of concepts. We review computational models of concept learning that use programs as their concept representation and evaluate their contribution toward a universal representational language.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-09-04T11:16:34Z
Jineon Baek, Byung-Hak Hwang, Joonhyun La, Hongseok Yang
arXiv categories: math.CO, cs.CC, cs.FL, cs.LO

Algebraic combinatorics often seeks bijections that explain identities between distributions object by object. Encoding combinatorial objects as words lets automata theory study such a bijection as a word-to-word computation and measure its memory, input access, and control of output order. This refines existence questions by asking which computational mechanisms a bijection requires. We develop this viewpoint for Dyck paths. Our motivating example is the $q,t$-Catalan polynomial. Let $D_n$ be the set of Dyck paths of semilength $n$, let $D=\bigcup_{n\ge 0}D_n$, and let $area, dinv, bounce \colon D\to\mathbb{N}$ be the standard statistics. Then, \[ C_n(q,t)=\sum_{P\in D_n}q^{area(P)}t^{bounce(P)} =\sum_{P\in D_n}q^{dinv(P)}t^{area(P)}. \] Haglund's zeta map $ζ\colon D\to D$ gives a bijective proof: it preserves semilength and sends $(dinv,area)$ to $(area,bounce)$. By contrast, the full symmetry $C_n(q,t)=C_n(t,q)$ still lacks a direct explanation: no explicit, uniform, semilength-preserving bijection is known that swaps area and dinv on every Dyck path. Polyregular maps from automata theory provide a natural computational starting point, but we prove that neither $ζ$ nor the classical height-sweep bijection witnessing Narayana symmetry is polyregular. The missing mechanism is global ordering by numerical levels whose range grows with the input. We call this a \emph{rank sort} and introduce \emph{weighted-rank polyregular maps} (WRP), extending polyregular maps by one such sort and containing both bijections. Nevertheless, WRP is a proper subclass of deterministic logspace. We prove that $ζ^{-1}$ lies outside WRP and that no WRP map can realise a semilength-preserving area-dinv swap. Thus the rank-sorting strategy behind $ζ$ cannot be extended within WRP to exchange the two statistics.

arXiv abstract · PDF