https://arxiv.org/api/13J3PG5XR3eoUFOIWH4kbIb94HA 2026-07-22T00:35:09Z 19781 165 15 http://arxiv.org/abs/2607.04015v1 2026-07-04T20:21:27Z

Many stabilizer quantum error-correcting codes are built from a finite pattern repeated across space or time, such as lattice codes, translation-invariant graph states, and quantum convolutional codes. Ordinary stabilizer ZX-diagrams capture only finite truncations of such systems, obscuring the repeated structure that defines them. We introduce the delayed stabilizer ZX-calculus, a finite graphical language for these infinite, translation-invariant processes. It extends the odd-prime-dimensional stabilizer ZX-calculus with a single new generator, the delay, which feeds data from one time step to the next. We equip the calculus with two semantics. In the first semantics, we interpret the behaviour of a delayed ZX-diagram as an equivalence class of sequences of quantum channels; where two sequences are identified if they have the same information content. We show that the behaviour of a delayed ZX-diagram uniquely determines an infinite stabilizer group. In the second semantics, we interpret the delay as a formal variable, encoding the translation-invariant families of Pauli operators as generating functions. This allows us to represent a delayed ZX-diagram in terms of a tableau of generating functions, from which the infinite stabilizer group can be recovered. Finally, we give a complete axiomatization of the delayed stabilizer ZX-calculus, featuring generalised Euler decomposition and colour change rules. Using generalised forms of local complementation and pivoting, we reduce every diagram to a unique normal form. This establishes soundness, universality, and completeness for the generating tableau semantics.

2026-07-04T20:21:27Z Cole Comfort Giovanni de Felice http://arxiv.org/abs/2602.06934v5 2026-07-04T19:51:52Z

Grassroots Logic Programs (GLP) is a concurrent logic programming language in which logic variables are partitioned into paired readers and writers. An assignment is produced at most once via a writer and consumed at most once via its paired reader, and may contain additional readers and/or writers. This enables the concise expression of rich multidirectional communication modalities. The language was introduced together with concurrent (cGLP) and multiagent (maGLP) operational semantics. Here, we derive from these (\ia)~dGLP, a deterministic counterpart of cGLP, and (\ib)~madGLP, a counterpart of maGLP in which deterministic agents communicate solely by asynchronous message passing, and prove them correct against their abstract counterparts. maGLP shared variable pairs spanning agents can be implemented as local variables paired by \emph{global links}, with correctness following from disjoint substitution commutativity (a consequence of GLP's single-occurrence invariant). We further prove that madGLP is grassroots. Both dGLP and madGLP serve as formal specifications for an AI-driven implementation discipline (math $\to$ informal spec $\to$ Dart) employed and described here: from dGLP, AI (Claude) developed a workstation-based GLP implementation in Dart, and from madGLP it is developing a smartphone-based multiagent one.

2026-02-06T18:30:11Z arXiv admin note: text overlap with arXiv:2510.15747 Ehud Shapiro http://arxiv.org/abs/2607.03996v1 2026-07-04T19:38:03Z

Time-dependent processes are often described by machines with an internal state which is updated as time evolves. An external observer cannot see this state and learns about a process only through finite observations of its inputs and outputs, each of which imposes a constraint on the trajectories the process can exhibit. We introduce a semantic construction in which two stateful processes have the same behaviour when they have the same constraints, as determined by finite observations, independent of their internal state. The construction is defined over any preorder-enriched monoidal category with a compatible notion of discarding, which we call a discard bicategory, capturing partial, non-deterministic, probabilistic, and quantum processes. The resulting category of behaviours provides a functorial semantics for free feedback categories in the sense of Katis, Sabadini, and Walters. For non-deterministic systems, we prove a categorified compactness theorem: every compatible family of finite observations between compact Hausdorff spaces extends uniquely and functorially to an infinite closed relation. Restricted to affine relations over finite fields, the compactness theorem recovers Willems' notion of behaviour for linear time-invariant systems.

2026-07-04T19:38:03Z Cole Comfort Giovanni de Felice http://arxiv.org/abs/2607.07723v1 2026-07-04T18:17:36Z

This paper does not address the mathematical truth of P versus NP. Instead, it identifies a structural limitation of uniform proof-generation methods in the standard Turing model. The observation is model-theoretic: it concerns the interaction between semantic invariants and syntactic verification, not the provability of complexity statements. We formalise an admissible method as a generator-verifier pair that produces, for each program, a finite certificate establishing a semantic property. Admissibility forces the generator-verifier composition to behave uniformly with respect to the invariant being certified. In the standard model, such uniform semantic certification implicitly induces a decision procedure for the property. Rice's theorem shows that this implicit behaviour cannot be realised for non-trivial semantic invariants, revealing a structural constraint on formal certification. Understanding this requires a meta-computational perspective: the obstruction arises from the computational behaviour induced by certification, not from the complexity-theoretic status of the property. We apply this framework to two semantic invariants naturally associated with formal certification of P vs. NP and with cryptographic hardness assumptions (in particular, one-way functions). Both fall under the same limitation: no uniform admissible method can certify them in the standard model. A complete Coq formalisation is provided, capturing the extensional structure of admissible methods and the semantic-syntactic interaction underlying the result.

2026-07-04T18:17:36Z Fabio F. G. Buono http://arxiv.org/abs/2607.03951v1 2026-07-04T16:53:39Z

The reproducibility crisis in scientific research has received widespread recognition, thereby increasing the importance of meta-analyses that integrate statistical analyses from multiple studies. However, statistical methods often have ambiguous and implicit underlying assumptions, which can lead to their erroneous applications and interpretations. To address this issue, we propose a formal verification framework for statistical programs written in Python. Specifically, we present Why3-py, a Python front-end for the Why3 verification platform that transforms Python programs into verification-oriented WhyML representations suitable for formal verification, addressing the challenges arising from Python's dynamic typing and runtime polymorphism. Furthermore, we extend the StatWhy tool to support the verification of meta-analysis methods. These tools enable users to identify overlooked assumptions and misuse of analyses, and to verify the correctness of Python programs for hypothesis testing and for meta-analyses.

2026-07-04T16:53:39Z Akira Tanaka Yusuke Kawamoto http://arxiv.org/abs/2607.07722v1 2026-07-04T15:49:36Z

The first part of this paper provides an experience report, recounting the design and long-term maintenance of the Carnap proof assistant framework used cumulatively by over 45,000 students worldwide over the last decade. We cover the good, the bad, and the ugly: what worked well, what didn't work, and what added friction to development and maintenance over time. These insights motivate a bottom-up redesign of the Carnap framework, which is the topic of the paper's second part. Briefly, the new design combines a new high-performance verifier kernel (mm0-zig) targeting Mario Carneiro's metamath zero format, and the Aufbau Bytecode Compiler, (abc), a new proof compiler that can serve as a backend for richly interactive proof-authoring experiences on the web.

2026-07-04T15:49:36Z 11 pages, 2 figures, 1 table. Accepted for publication at TEAL Graham Leach-Krouse http://arxiv.org/abs/2410.24053v4 2026-07-04T08:15:44Z

We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for Gödel-Löb provability logic. In particular, we consider Sambin and Valentini's sequent system GLseq, Shamkanov's non-wellfounded and cyclic sequent systems GL$\infty$ and GLcirc, Poggiolesi's tree-hypersequent system CSGL$^{*}$, and Negri's labeled sequent system G3KGL. Shamkanov provided proof-theoretic correspondences between GLseq, GL$\infty$, and GLcirc, and Goré and Ramanayake showed how proofs could be transformed between CSGL$^{*}$ and G3KGL; however, the exact nature of proof transformations between the former three systems and the latter two systems has remained an open problem. We solve this open problem by showing how to restructure tree-hypersequent proofs into an end-active form and introduce a novel 'linearization technique' that transforms such proofs into linear nested sequent proofs. As a result, we obtain a new proof-theoretic tool for extracting linear nested sequent systems from tree-hypersequent systems, which yields the first cut-free linear nested sequent calculus LNGL for Gödel-Löb provability logic. We show how to transform proofs in LNGL into a certain normal form, where proofs repeat in stages of modal and local rule applications, and which are translatable into GLseq and G3KGL proofs. These new syntactic transformations, together with those mentioned above, establish full proof-theoretic correspondences between GLseq, GL$\infty$, GLcirc, CSGL$^{*}$, G3KGL, and LNGL while also giving (to the best of the author's knowledge) the first constructive proof mappings between structural (viz. labeled, tree-hypersequent, and linear nested sequent) systems and a cyclic sequent system.

2024-10-31T15:47:59Z Accepted to CSL 2025 Tim S. Lyon http://arxiv.org/abs/2606.22908v3 2026-07-04T05:01:48Z

Purely functional programming makes immutability and non-strict evaluation its defaults; we push further, making interning and memoization the defaults of computation. In prior operational semantics for the pure $λ$-calculus, representing and transforming cyclic and infinite data requires an added recursion construct, a $\texttt{letrec}$, a $μ$-binder, or a built-in $Y$ for graph reduction, and sharing the repeated work of a memoized or dynamic-programming function requires an impure cache. We show that no extension is needed. We apply tabling, the standard method for solving a least-fixpoint equation, to weak-head reduction; this defines a new operational semantics for the pure $λ$-calculus that keeps each term's standard lazy meaning. A term that reaches finitely many distinct states, each solved in finitely many steps, comes out as a finite graph, possibly cyclic; the calculus stays pure, and the graph is sound and independent of reduction order. We implemented this operational semantics as a $λ$-calculus interpreter. It does dynamic programming automatically, sharing repeated subproblems with no memoization table. It creates and transforms cyclic graphs with no added recursion construct. And it decides an unproductive loop, returning $\bot$ for $Ω$ in finite time. What the evaluator returns is a graph, so the $λ$-calculus becomes a DSL for graph computation: the memo table of dynamic programming, the transposition table of game search, and the derived-fact table of Datalog reachability and points-to analysis are all tabling on state identity, and none of them is written by hand. Compilation is one more such problem: we write a bootstrap compiler that compiles its own source, all as a pure $λ$-term.

2026-06-22T06:46:37Z Bo Yang http://arxiv.org/abs/2607.03645v1 2026-07-03T23:58:21Z

We consider and extend results on basic path logic and the ordered fragment of first-order logic, both of which originate from the functional translation of modal logic. Basic path logic is a subclass of the clausal class for the $\exists^*\forall^*$-fragment and has the remarkable property that binary resolution decides it. This decidability result and the consequence finding completeness of binary resolution allows us to observe that binary resolution also decides uniform interpolation and computes uniform interpolants for basic path logic. By introducing constant Skolemisation, we show that sentences of the ordered fragment can be transformed into basic path logic, and this transformation preserves logical consequences in the ordered fragment. We characterise the search space of the SCAN algorithm on the clausal form of the ordered fragment by a variation of basic path logic and prove that SCAN terminates on this class, and therefore it decides second-order quantifier elimination for this class. It remains unclear whether uniform interpolants in the ordered fragment can be extracted from the output of SCAN.

2026-07-03T23:58:21Z Submitted for publication in a journal Renate A. Schmidt Hongkai Yin http://arxiv.org/abs/2505.12024v2 2026-07-03T22:42:49Z

A residuated semigroup is a structure $\langle A,\le,\cdot,\backslash,/ \rangle$ where $\langle A,\le \rangle$ is a poset and $\langle A,\cdot \rangle$ is a semigroup such that the residuation law $x\cdot y\le z\iff x\le z/y\iff y\le x \backslash z$ holds. An element $p$ is positive if $a\le pa$ and $a \le ap$ for all $a$. A residuated semigroup is called balanced if it satisfies the equation $x \backslash x \approx x / x$ and moreover each element of the form $a \backslash a = a / a$ is positive, and it is called integrally closed if it satisfies the same equation and moreover each element of this form is a global identity. We show how a wide class of balanced residuated semigroups (so-called steady residuated semigroups) can be decomposed into integrally closed pieces, using a generalization of the classical Plonka sum construction. This generalization involves gluing a disjoint family of ordered algebras together using multiple families of maps, rather than a single family as in ordinary Plonka sums.

2025-05-17T14:28:12Z Stefano Bonzio José Gil-Férez Peter Jipsen Adam Přenosil Melissa Sugimoto http://arxiv.org/abs/2607.09748v1 2026-07-03T19:59:03Z

In distributed systems, the classical State Machine Replication (SMR) model assumes that correct replicas execute deterministic transitions to yield identical bitwise states. However, the rise of agentic distributed systems -- where autonomous, stochastic, and model-driven agents orchestrate infrastructure -- presents scenarios where deterministic, bitwise replication is insufficient. Replicas operating with generative models may exhibit divergent reasoning paths, summaries, and token boundaries, yet reach semantically equivalent and correct operational decisions. Forcing bitwise agreement across these stochastic participants degrades execution flexibility, induces context amnesia, and limits performance. We argue that in such settings replicas should agree on belief, not bits. We propose Epistemic State Replication (ESR), a belief-replication layer for agentic distributed systems that shifts the replication boundary from data visibility to knowledge visibility. We formalize the epistemic node state as a pair K = (L, B) separating the deterministic, immutable evidence log (L) from the stochastic, evolving belief lineage (B). To govern execution safety, we define Semantic Linearizability, which requires operations to reflect the latest committed operational meaning within a verifier-bounded semantic compatibility metric, and Bounded Eventual Coherence, which bounds expected semantic divergence under fair delivery, monotonic evidence, bounded verifier disturbance, and a contractive graft operator. We outline protocols for propagating derived insights using structured epistemic deltas, and formalize Verifiable Semantic Rollbacks to prune faulty premises from belief lineages without inducing context amnesia. We prototype ESR and report preliminary simulation results that show feasibility under the stated assumptions and illustrate reductions in secondary cognitive faults.

2026-07-03T19:59:03Z 16 pages, 4 tables Jun He Deying Yu http://arxiv.org/abs/2508.20054v2 2026-07-03T17:04:39Z

The study of categories abstracting the structural properties of relations has been extensively developed over the years, resulting in a rich and diverse body of work. In a previous paper we offered a survey providing a modern presentation of these ``categories for relations'' as instances of gs-monoidal categories, showing how they arise as Kleisli categories of suitable symmetric monoidal monads. The end result was a taxonomy that organised numerous related concepts in the literature, including in particular Markov and restriction categories. This paper further enriches the taxonomy: it proposes two categories that are once more instances of gs-monoidal categories, yet more abstract than Markov and restriction categories. They are characterised by an axiomatic notion of mass and domain of an arrow, the latter one of the key ingredients of restriction categories, which generalises the domain of partial functions. The paper then introduces mass and domain preserving monads, proving that the associated Kleisli categories in fact preserve the corresponding equations and that these monads arise naturally for the categories of semiring-weighted relations.

2025-08-27T17:06:57Z MFPS 2026 Proceedings version Cipriano Junior Cioffo Fabio Gadducci Davide Trotta http://arxiv.org/abs/2607.16266v1 2026-07-03T15:37:04Z

Existing approaches for reasoning about action and change provide expressive semantics for modeling dynamic systems, in most cases built on top of logic programming systems. We introduce a modular framework for transition and trajectory verification based on Tiles and implemented in Soda, which is an efficient functional programming language. The framework operationalizes action language semantics through executable verification pipelines that process states, actions, transitions, and rules as compositional functional components. Verification procedures are represented as typed functional pipelines, enabling modular specifications, reusable reasoning components, and transparent execution workflows with guaranteed pipeline termination. The framework includes an executable specification layer that allows users to define domain descriptions in YAML, which are operationalized into the underlying verification model and executable pipeline structure. We provide an open-source implementation and illustrate the framework through examples that involve misinformation and emotional reasoning.

2026-07-03T15:37:04Z Julian Alfredo Mendez Andreas Brännström http://arxiv.org/abs/2607.03405v1 2026-07-03T15:11:19Z

We show that the existence of an oddomorphism from a graph $F$ to a graph $G$ does not imply that $G$ is a minor of $F$. This answers a question posed by Roberson (2022) and shows that the CFI graphs cannot be used to prove the Strong Roberson Conjecture. Additionally, we introduce the concept of a split-off minor and show that the existence of an oddomorphism from $F$ to $G$ implies that $G$ is a split-off minor of $F$. Consequently, every class that is closed under taking split-off minors and disjoint unions is homomorphism distinguishing closed. The split-off minor relation is the first minor-like structural relation shown to have this property, marking a meaningful advancement in our understanding of the interaction between structural graph containment and homomorphism indistinguishability relations.

2026-07-03T15:11:19Z 22 pages Arnar Á. Kristjánsson http://arxiv.org/abs/2508.06918v2 2026-07-03T13:48:09Z

We classify all Mal'cev clones over a three-element set up to minion homomorphisms. This is another step toward the complete classification of three-element relational structures up to pp-constructability. We furthermore provide an alternative proof of Bulatov's result that all Mal'cev clones over a three-element set have an at most 4-ary relational basis.

2025-08-09T10:14:42Z 36 pages, 4 figures; appendix contains a github link with additional material Stefano Fioravanti Michael Kompatscher Bernardo Rossi Albert Vucaj