arXiv subjects

Henning Basold

Publications and source records attributed to Henning Basold.

15 recordsLinked to original sources

arXiv2026

Central Limits via Dilated Categories

The Central Limit Theorem (CLT) establishes that sufficiently large sequences of independent and identically distributed random variables converge in probability to a normal distribution. This makes the CLT a fundamental building block of statistical reasoning and, by extension, in reasoning about computing systems that are based on statistical inference such as probabilistic programing languages, programs with optimisation, and machine learning components. However, there is no general theory of CLT-like results currently, which forces practitioners to redo proofs without having a good handle on the essential ingredients of CLT-type results. In this paper, we introduce dilated seminorm-enriched category theory as a unifying framework for central limits, and we establish an abstract central limit theorem within that framework. We illustrate how a strengthened version of the classical CLT and the law of large numbers can be obtained as instances of our framework. Moreover, we derive from our framework a novel central limit theorem for symplectic manifolds, the CLT for observables, which finds applications in statistical mechanics.

cs.LO↗

arXiv2025

Quantum Physics using Weighted Model Counting

Weighted model counting (WMC) has proven effective at a range of tasks within computer science, physics, and beyond. However, existing approaches for using WMC in quantum physics only target specific problem instances, lacking a general framework for expressing problems using WMC. This limits the reusability of these approaches in other applications and risks a lack of mathematical rigor on a per-instance basis. We present an approach for expressing linear algebraic problems, specifically those present in physics and quantum computing, as WMC instances. We do this by introducing a framework that converts Dirac notation to WMC problems. We build up this framework theoretically, using a type system and denotational semantics, and provide an implementation in Python. We demonstrate the effectiveness of our framework in calculating the partition functions of several physical models: The transverse-field Ising model (quantum) and the Potts model (classical). The results suggest that heuristics developed in automated reasoning can be systematically applied to a wide class of problems in quantum physics through our framework.

quant-ph↗

arXiv2025

Separation Logic of Generic Resources via Sheafeology

Separation logic was conceived in order to make the verification of pointer programs scalable to large systems and it has proven extremely effective. The key idea is that programs typically access only small parts of memory, allowing for local reasoning. This idea is implemented in separation logic by extending first-order logic with separating connectives, which inspect local regions of memory. It turns that this approach not only applies to pointer programs, but also to programs involving other resource structures. Various theories have been put forward to extract and apply the ideas of separation logic more broadly. This resulted in algebraic abstractions of memory and many variants of separation logic for, e.g., concurrent programs and stochastic processes. However, none of the existing approaches formulate the combination of first-order logic with separating connectives in a theory that could immediately yield program logics for different resources. In this paper, we propose a framework based on the idea that separation logic can obtained by making first-order logic resource-aware. First-order logic can be understood in terms of categorical logic, specifically fibrations. Our contribution is to make these resource-aware by developing categorical logic internally in categories of sheaves, which is what we call sheafeology. The role of sheaves is to model views on resources, through which resources can be localised and combined, which enables the scalability promised by separation logic. We contribute constructions of an internal fibration in sheaf categories that models predicates on resources, and that admits first-order and separating connectives. Thereby, we attain a general framework of separation logic for generic resources, a claim we substantiate by instantiating our framework to various memory models and random variables.

cs.LO↗

arXiv2025

Optimization and Synthesis of Quantum Circuits with Global Gates

Compiling quantum circuits to account for hardware restrictions is an essential part of the quantum computing stack. Circuit compilation allows us to adapt algorithm descriptions into a sequence of operations supported by real quantum hardware, and has the potential to significantly improve their performance when optimization techniques are added to the process. One such optimization technique is reducing the number of quantum gates that are needed to execute a circuit. For instance, methods for reducing the number of non-Clifford gates or CNOT gates from a circuit is an extensive research area that has gathered significant interest over the years. For certain hardware platforms such as ion trap quantum computers, we can leverage some of their special properties to further reduce the cost of executing a quantum circuit in them. In this work we use global interactions, such as the Global M{\o}lmer-S{\o}rensen gate present in ion trap hardware, to optimize and synthesize quantum circuits. We design and implement an algorithm that is able to compile an arbitrary quantum circuit into another circuit that uses global gates as the entangling operation, while optimizing the number of global interactions needed. The algorithm is based on the ZX-calculus and uses an specialized circuit extraction routine that groups entangling gates into Global M{\o}lmer-S{\o}rensen gates. We benchmark the algorithm in a variety of circuits, and show how it improves their performance under state-of-the-art hardware considerations in comparison to a naive algorithm and the Qiskit optimizer.

quant-ph↗

arXiv2025

An Expressive Coalgebraic Modal Logic for Cellular Automata

Cellular automata provide models of parallel computation based on cells, whose connectivity is given by an action of a monoid on the cells. At each step in the computation, every cell is decorated with a state that evolves in discrete steps according to a local update rule, which determines the next state of a cell based on its neighbour's states. In this paper, we consider a coalgebraic view on cellular automata, which does not require typical restrictions, such as uniform neighbourhood connectivity and uniform local rules. Using the coalgebraic view, we devise a behavioural equivalence for cellular automata and a modal logic to reason about their behaviour. We then prove a Hennessy-Milner style theorem, which states that pairs of cells satisfy the same modal formulas exactly if they are identified under cellular behavioural equivalence.

cs.LO↗

arXiv2023

The Directed Van Kampen Theorem in Lean

Directed topology is an area of mathematics with applications in concurrency. It extends the concept of a topological space by adding a notion of directedness, which restricts how paths can evolve through a space and enables thereby a faithful representation of computation with their direction. In this paper, we present a Lean formalisation of directed spaces and a Van Kampen theorem for them. This theorem allows the calculation of the homotopy type of a space by combining local knowledge the homotopy type of subspaces. With this theorem, the reasoning about spaces can be reduced to subspaces and, by representing concurrent systems as directed spaces, we can reduce the deduction of properties of a composed system to that of subsystems. The formalisation in Lean can serve to support computer-assisted reasoning about the behaviour of concurrent systems.

cs.LO↗

arXiv2023

Enriching Diagrams with Algebraic Operations

In this paper, we extend diagrammatic reasoning in monoidal categories with algebraic operations and equations. We achieve this by considering monoidal categories that are enriched in the category of Eilenberg-Moore algebras for a monad. Under the condition that this monad is monoidal and affine, we construct an adjunction between symmetric monoidal categories and symmetric monoidal categories enriched over algebras for the monad. This allows us to devise an extension, and its semantics, of the ZX-calculus with probabilistic choices by freely enriching over convex algebras, which are the algebras of the finite distribution monad. We show how this construction can be used for diagrammatic reasoning of noise in quantum systems.

cs.LO↗

arXiv2023

Finitely Presentable Higher-Dimensional Automata and the Irrationality of Process Replication

Higher-dimensional automata (HDA) are a formalism to faithfully model the behaviour of concurrent systems. For ordinary automata, there is a correspondence between regular expressions, regular languages and finite automata, which provides a powerful link between algebraic proofs and operational behaviour. It has been shown by Fahrenberg et al. that finite HDA correspond with interfaced interval pomset languages generated by sequential and parallel composition and non-empty iteration, and thereby to a variant of Kleene algebras (KA) with parallel composition. It is known that this correspondence cannot be extended to concurrent KA, which additionally have process replication. An alternative to finite HDA are locally finite HDA, in which every state can only reach finitely many other states, and finitely branching HDA. In this paper, we show that both classes of HDA are closed under process replication and thus models of concurrent KA. To achieve this, we prove that the category of HDA is locally finitely presentable, where the finite HDA generate all other HDA. We then prove that this has the unfortunate side-effect that all HDA are locally finite, which means that the correspondence with concurrent KA trivialises. Similarly, we also show that, even though finitely branching HDA are closed under process replication, the resulting HDA necessarily have infinitely many initial states.

cs.FL↗

arXiv2020

Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols

Compositional methods are central to the development and verification of software systems. They allow to break down large systems into smaller components, while enabling reasoning about the behaviour of the composed system. For concurrent and communicating systems, compositional techniques based on behavioural type systems have received much attention. By abstracting communication protocols as types, these type systems can statically check that programs interact with channels according to a certain protocol, whether the intended messages are exchanged in a certain order. In this paper, we put on our coalgebraic spectacles to investigate session types, a widely studied class of behavioural type systems. We provide a syntax-free description of session-based concurrency as states of coalgebras. As a result, we rediscover type equivalence, duality, and subtyping relations in terms of canonical coinductive presentations. In turn, this coinductive presentation makes it possible to elegantly derive a decidable type system with subtyping for $\pi$-calculus processes, in which the states of a coalgebra will serve as channel protocols. Going full circle, we exhibit a coalgebra structure on an existing session type system, and show that the relations and type system resulting from our coalgebraic perspective agree with the existing ones.

cs.LO↗

arXiv2020

The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them

In sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen's classical and intuitionistic calculi LK and LJ enjoy cut elimination. The property is less studied in coinductive extensions of sequent calculi. In this paper, we use coinductive Horn clause theories to show that cut is not eliminable in a coinductive extension of LJ, a system we call CLJ. We derive two further practical results from this study. We show that CoLP by Gupta et al. gives rise to cut-free proofs in CLJ with fixpoint terms, and we formulate and implement a novel method of coinductive theory exploration that provides several heuristics for discovery of cut formulae in CLJ.

cs.LO↗

arXiv2018

Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses

We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive uniform proofs; its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality; and soundness of both proof systems is proven relative to a novel coalgebraic description of complete Herbrand models.

cs.LO↗

arXiv2018

Breaking the Loop: Recursive Proofs for Coinductive Predicates in Fibrations

The purpose of this paper is to develop and study recursive proofs of coinductive predicates. Such recursive proofs allow one to discover proof goals in the construction of a proof of a coinductive predicate, while still allowing the use of up-to techniques. This approach lifts the burden to guess invariants, like bisimulation relations, beforehand. Rather, they allow one to start with the sought-after proof goal and develop the proof from there until a point is reached, at which the proof can be closed through a recursion step. Proofs given in this way are both easier to construct and to understand, similarly to proofs given in cyclic proof systems or by appealing parameterised coinduction. In this paper, we develop a framework for recursive proofs of coinductive predicates that are given through fibrational predicate liftings. This framework is built on the so-called later modality, which has made its appearance in type theoretic settings before. In particular, we show the soundness and completeness of recursive proofs, we prove that compatible up-to techniques can be used as inference rules in recursive proofs, and provide some illustrating examples.

cs.LO↗

arXiv2016

Type Theory based on Dependent Inductive and Coinductive Types

We develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theory with a small set of rules, while still being fairly expressive. For example, all well-known basic types and type formers that are needed for using this type theory as a logic are definable: propositional connectives, like falsity, conjunction, disjunction, and function space, dependent function space, existential quantification, equality, natural numbers, vectors etc. The reduction relation on terms consists solely of a rule for recursion and a rule for corecursion. The reduction relations for well-known types arise from that. To further support the introduction of this new type theory, we also prove fundamental properties of its term calculus. Most importantly, we prove subject reduction and strong normalisation of the reduction relation, which gives computational meaning to the terms. The presented type theory is based on ideas from categorical logic that have been investigated before by the first author, and it extends Hagino's categorical data types to a dependently typed setting. By basing the type theory on concepts from category theory we maintain the duality between inductive and coinductive types, and it allows us to describe, for example, the function space as a coinductive type.

cs.LO↗

arXiv2015

Dependent Inductive and Coinductive Types are Fibrational Dialgebras

In this paper, I establish the categorical structure necessary to interpret dependent inductive and coinductive types. It is well-known that dependent type theories \`a la Martin-L\"of can be interpreted using fibrations. Modern theorem provers, however, are based on more sophisticated type systems that allow the definition of powerful inductive dependent types (known as inductive families) and, somewhat limited, coinductive dependent types. I define a class of functors on fibrations and show how data type definitions correspond to initial and final dialgebras for these functors. This description is also a proposal of how coinductive types should be treated in type theories, as they appear here simply as dual of inductive types. Finally, I show how dependent data types correspond to algebras and coalgebras, and give the correspondence to dependent polynomial functors.

cs.LO↗

arXiv2014

Transformation von Scade-Modellen zur SMT-basierten Verifikation

In this work we develop a fully automatic verification procedure of safety properties of Scade programs. We transform each such program into an SMT instance (Satisfiability Modulo Theories) and feed this to a solver. The goal is to have a publicly accessible experimentation platform for the verification of Scade programs. The choice of SMT is determined by the fact that it offers more expressive logics than propositional logic, yet their solvers have been shown to perform very well. The expressiveness of SMT logics allows us to implement symbolic model checking thus avoiding the expansion of the complete state space of the models during the verification. In order to reduce the complexity we transform the Scade programs into SMT instances in two steps. First they are reduced to programs of a synchronous data flow language Lama. This language has simpler semantics than Scade while still preserving some of the programmer's abstractions. Next we interpret such a Lama program as a system of quantifier free first-order formulas. The remaining abstractions in Lama can be used to simplify these systems. This in turn could lead to speeding up the verification process and allowing more properties to be verifiable. We implemented these transformations successfully in a software using Haskell. This work is concluded by a comparison of this software to the existing verification software "Scade Design Verifier" which comes with the Scade Suite.

cs.LO↗