arXiv subjects

Kostia Chardonnet

Publications and source records attributed to Kostia Chardonnet.

10 recordsLinked to original sources

arXiv2026

Quantum Term Rewrite Systems: Applications to Complexity Analysis

Term Rewrite Systems (TRS) is a computational model offering a level of abstraction well-suited towards static analysis, e.g., termination or complexity analyses. In this paper, we introduce Quantum Term Rewrite Systems (QTRS), an extension of TRS to quantum computing, thus allowing to benefit from quantum advantage while being able to certify the complexity. We ensure that QTRS correspond to physically realizable processes and adapt techniques to obtain termination certificates or generic bounds on the reduction length. We delineate a class of terminating QTRS that can be compiled to uniform families of quantum circuits of size bounded by the reduction length. Conversely, this class is universal for quantum circuits. In particular, we show a characterization of the class of functions computable in quantum polynomial time, known as $\mathtt{FBQP}$.

cs.LO↗

arXiv2026

Compiling Quantum Lambda-Terms into Circuits via the Geometry of Interaction

We present an algorithm turning any term of a linear quantum $\lambda$-calculus into a quantum circuit. The essential ingredient behind the proposed algorithm is Girard's geometry of interaction, which, differently from its well-known uses from the literature, is here leveraged to perform as much of the classical computation as possible, at the same time producing a circuit that, when evaluated, performs all the quantum operations in the underlying $\lambda$-term. We identify higher-order control flow as the primary obstacle towards efficient solutions to the problem at hand. Notably, geometry of interaction proves sufficiently flexible to enable efficient compilation in many cases, while still supporting a total compilation procedure. Finally, we characterize through a type system those $\lambda$-terms for which compilation can be performed efficiently.

cs.LO↗

arXiv2026

Approximation theory for distant Bang calculus

Approximation semantics capture the observable behaviour of {\lambda}-terms, with B\"ohm Trees and Taylor Expansion standing as two central paradigms. Although conceptually different, these notions are related via the Commutation Theorem, which links the Taylor expansion of a term to that of its B\"ohm tree. These notions are well understood in Call-by-Name {\lambda}-calculus and have been more recently introduced in Call-by-Value settings. Since these two evaluation strategies traditionally require separate theories, a natural next step is to seek a unified setting for approximation semantics. The Bang-calculus offers exactly such a framework, subsuming both CbN and CbV through linear-logic translations while providing robust rewriting properties. However, its approximation semantics is yet to be fully developed. In this work, we develop the approximation semantics for dBang, the Bang-calculus with explicit substitutions and distant reductions. We define B\"ohm trees and Taylor expansion within dBang and establish their fundamental properties. Our results subsume and generalize Call-By-Name and Call-By-Value through their translations into Bang, offering a single framework that uniformly captures infinitary and resource-sensitive semantics across evaluation strategies.

cs.LO↗

arXiv2025

The Tensor-Plus Calculus

We propose a graphical language that accommodates two monoidal structures: a multiplicative one for pairing and an additional one for branching. In this colored PROP, whether wires in parallel are linked through the multiplicative structure or the additive structure is implicit and determined contextually rather than explicitly through tapes, world annotations, or other techniques, as is usually the case in the literature. The diagrams are used as parameter elements of a commutative semiring, whose choice is determined by the kind of computation we want to model, such as non-deterministic, probabilistic, or quantum. Given such a semiring, we provide a categorical semantics of diagrams and show the language as universal for it. We also provide an equational theory to identify diagrams that share the same semantics and show that the theory is sound and complete and captures semantical equivalence. In categorical terms, we design an internal language for semiadditive categories (C,+,0) with a symmetric monoidal structure (C,x,1) distributive over it, and such that the homset C(1,1) is isomorphic to a given commutative semiring, e.g., the semiring of non-negative real numbers for the probabilistic case.

cs.LO↗

arXiv2025

Resource-Aware Quantum Programming with General Recursion and Quantum Control

This paper introduces the hybrid quantum language with general recursion $\mathtt{Hyrql}$, driven towards resource-analysis. By design, $\mathtt{Hyrql}$ does not require the specification of an initial set of quantum gates. Hence, it is well amenable towards a generic cost analysis, unlike languages that use different sets of quantum gates, which yield quantum circuits of distinct complexity. Regarding resource-analysis, we show how to relate the runtime of an expressive fragment of $\mathtt{Hyrql}$ programs with the size of the corresponding quantum circuits. We also manage to capture the class of functions computable in quantum polynomial time, which, by Yao's Theorem, corresponds to families of circuits of polynomial size. Consequently, this result paves the way for the use of termination and runtime-analysis techniques designed for classical programs to guarantee bounds on the size of quantum circuits.

cs.LO↗

arXiv2025

A Curry-Howard Correspondence for Linear, Reversible Computation

In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic $μ$MALL: linear logic extended with least fixed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy $μ$MALL validity criterion and how the language simulates the cut-elimination procedure of $μ$MALL.

cs.LO↗

arXiv2025

The Many-Worlds Calculus

In this paper, we explore the interaction between two monoidal structures: a multiplicative one, for the encoding of pairing, and an additive one, for the encoding of choice. We propose a colored PROP to model computation in this framework, where the choice is parameterized by an algebraic side effect: the model can support regular tests, probabilistic and non-deterministic branching, as well as quantum branching, i.e. superposition. The graphical language comes equipped with a denotational semantics based on linear applications, and an equational theory. We prove the language to be universal, and the equational theory to be complete with respect to this semantics.

cs.LO↗

arXiv2024

Semantics for a Turing-complete Reversible Programming Language with Inductive Types

This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, pattern-matching is used to ensure the reversibility of functions. We show how one can encode any Reversible Turing Machine in said language. We then build a sound and adequate categorical semantics based on join inverse categories, with additional structures to capture pattern-matching. We then derive a full completeness result, stating that any computable, partial injective function is the image of a term in the language.

cs.LO↗

arXiv2022

Geometry of Interaction for ZX-Diagrams

ZX-Calculus is a versatile graphical language for quantum computation equipped with an equational theory. Getting inspiration from Geometry of Interaction, in this paper we propose a token-machine-based asynchronous model of both pure ZX-Calculus and its extension to mixed processes. We also show how to connect this new semantics to the usual standard interpretation of ZX-diagrams. This model allows us to have a new look at what ZX-diagrams compute, and give a more local, operational view of the semantics of ZX-diagrams.

cs.LO↗

arXiv2021

Categorical Semantics of Reversible Pattern-Matching

This paper is concerned with categorical structures for reversible computation. In particular, we focus on a typed, functional reversible language based on Theseus. We discuss how join inverse rig categories do not in general capture pattern-matching, the core construct Theseus uses to enforce reversibility. We then derive a categorical structure to add to join inverse rig categories in order to capture pattern-matching. We show how such a structure makes an adequate model for reversible pattern-matching.

cs.LO↗