arXiv subjects

Louis Lemonnier

Publications and source records attributed to Louis Lemonnier.

10 recordsLinked to original sources

arXiv2025

A programming language combining quantum and classical control

The two main notions of control in quantum programming languages are often referred to as "quantum" control and "classical" control. With the latter, the control flow is based on classical information, potentially resulting from a quantum measurement, and this paradigm is well-suited to mixed state quantum computation. Whereas with quantum control, we are primarily focused on pure quantum computation and there the "control" is based on superposition. The two paradigms have not mixed well traditionally and they are almost always treated separately. In this work, we show that the paradigms may be combined within the same system. The key ingredients for achieving this are: (1) syntactically: a modality for incorporating pure quantum types into a mixed state quantum type system; (2) operationally: an adaptation of the notion of "quantum configuration" from quantum lambda-calculi, where the quantum data is replaced with pure quantum primitives; (3) denotationally: suitable (sub)categories of Hilbert spaces, for pure computation and von Neumann algebras, for mixed state computation in the Heisenberg picture of quantum mechanics.

cs.LO↗

arXiv2025

One rig to control them all

Controlled commands -- computations whose execution depends on a separate input -- play a central role in reversible Boolean circuits and quantum circuits. However, existing formalisms typically treat control only implicitly, entangled with other aspects of computation. From a semantic perspective, control is most naturally expressed in semisimple rig categories, which -- unlike standard circuit models such as props -- support both parallel and conditional composition. We present a construction that freely adjoins an explicit syntactic notion of control to a circuit theory specified as a suitable prop, subject to eight universally quantified equations. Our main result is that these equations are sound and complete for the intended semantics of control: the resulting theory satisfies a universal property, identifying it exactly as the circuit subtheory of the free semisimple rig completion. The proof combines coherence for rig categories with a new method based on induction over Gray codes. We illustrate the usefulness of the framework by showing that it simplifies several existing sound and complete axiomatisations of quantum circuits, isolating a small and conceptually clean set of generators and equations. In addition, the same equations yield a sound and complete axiomatisation of the multiply controlled Toffoli gate set, that is universal for reversible Boolean circuits.

cs.LO↗

arXiv2025

Quantum Circuits Are Just a Phase

Quantum programs today are written at a low level of abstraction - quantum circuits akin to assembly languages - and the unitary parts of even advanced quantum programming languages essentially function as circuit description languages. This state of affairs impedes scalability, clarity, and support for higher-level reasoning. More abstract and expressive quantum programming constructs are needed. To this end, we introduce a simple syntax for generating unitaries from "just a phase"; we combine a (global) phase operation that captures phase shifts with a quantum analogue of the "if let" construct that captures subspace selection via pattern matching. This minimal language lifts the focus from gates to eigendecomposition, conjugation, and controlled unitaries; common building blocks in quantum algorithm design. We demonstrate several aspects of the expressive power of our language in several ways. Firstly, we establish that our representation is universal by deriving a universal quantum gate set. Secondly, we show that important quantum algorithms can be expressed naturally and concisely, including Grover's search algorithm, Hamiltonian simulation, Quantum Fourier Transform, Quantum Signal Processing, and the Quantum Eigenvalue Transformation. Furthermore, we give clean denotational semantics grounded in categorical quantum mechanics. Finally, we implement a prototype compiler that efficiently translates terms of our language to quantum circuits, and prove that it is sound with respect to these semantics. Collectively, these contributions show that this construct offers a principled and practical step toward more abstract and structured quantum programming.

cs.PL↗

arXiv2024

Non-Cartesian Guarded Recursion with Daggers

Guarded recursion is a framework allowing for a formalisation of streams in classical (as opposed to concurrent, probabilistic, quantum) programming languages. The latter take their semantics in cartesian closed categories. However, some programming paradigms do not take their semantics in a cartesian setting; this is the case for concurrency, reversible and quantum programming for example. In this paper, we focus on reversible programming through its categorical model in dagger categories, which are categories that contain an involutive operator on morphisms. We show how to introduce the framework of guarded recursion into dagger categories with sufficient structure for data types, also called dagger rig categories. First, given an arbitrary category, we build another category shown to be suitable for guarded recursion in multiple ways, via enrichment and fixed point theorems. We then study the interaction between this construction and the structure of dagger rig categories, aiming for reversible programming. Finally, we show that our construction is suitable as a model of higher-order reversible programming languages, such as symmetric pattern matching, to which we add guarded recursion features.

cs.LO↗

arXiv2024

The Semantics of Effects: Centrality, Quantum Control and Reversible Recursion

This thesis revolves around an area of computer science called "semantics". We work with operational semantics, equational theories, and denotational semantics. The first contribution of this thesis is a study of the commutativity of effects through the prism of monads. Monads are the generalisation of algebraic structures such as monoids, which have a notion of centre: the centre of a monoid is made of elements which commute with all others. We provide the necessary and sufficient conditions for a monad to have a centre. We also detail the semantics of a language with effects that carry information on which effects are central. Moreover, we provide a strong link between its equational theories and its denotational semantics. The second focus of the thesis is quantum computing, seen as a reversible effect. Physically permissible quantum operations are all reversible, except measurement; however, measurement can be deferred at the end of the computation, allowing us to focus on the reversible part first. We define a simply-typed reversible programming language performing quantum operations called "unitaries". A denotational semantics and an equational theory adapted to the language are presented, and we prove that the former is complete. Furthermore, we study recursion in reversible programming, providing adequate operational and denotational semantics to a Turing-complete, reversible, functional programming language. The denotational semantics uses the dcpo enrichment of rig join inverse categories. This mathematical account of higher-order reasoning on reversible computing does not directly generalise to its quantum counterpart. In the conclusion, we detail the limitations and possible future for higher-order quantum control through guarded recursion.

cs.LO↗

arXiv2023

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

Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages

Monads in category theory are algebraic structures that can be used to model computational effects in programming languages. We show how the notion of "centre", and more generally "centrality", i.e. the property for an effect to commute with all other effects, may be formulated for strong monads acting on symmetric monoidal categories. We identify three equivalent conditions which characterise the existence of the centre of a strong monad (some of which relate it to the premonoidal centre of Power and Robinson) and we show that every strong monad on many well-known naturally occurring categories does admit a centre, thereby showing that this new notion is ubiquitous. More generally, we study central submonads, which are necessarily commutative, just like the centre of a strong monad. We provide a computational interpretation by formulating equational theories of lambda calculi equipped with central submonads, we describe categorical models for these theories and prove soundness, completeness and internal language results for our semantics.

cs.LO↗

arXiv2022

Large-scale quantum diagrammatic reasoning tools, !-boxes vs. scalable notations

The application of diagrammatic reasoning techniques to large-scale quantum processes needs specific tools to describe families of diagrams of arbitrary size. For now, large-scale diagrammatic reasoning tools in ZH-calculus come in two flavours, !-boxes and scalable notations. This paper investigates the interactions between the two approaches by exhibiting correspondences through various examples from the literature, focusing on (hyper)graph states and diagrammatic transforms. In doing so, we set up a path toward a neat and tidy large-scale diagrammatic reasoning toolbox.

quant-ph↗

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↗

arXiv2021

Hypergraph Simplification: Linking the Path-sum Approach to the ZH-calculus

The ZH-calculus is a complete graphical calculus for linear maps between qubits that admits a straightforward encoding of hypergraph states and circuits arising from the Toffoli+Hadamard gate set. In this paper, we establish a correspondence between the ZH-calculus and the path-sum formalism, a technique recently introduced by Amy to verify quantum circuits. In particular, we find a bijection between certain canonical forms of ZH-diagrams and path-sum expressions. We then introduce and prove several new simplification rules for the ZH-calculus, which are in direct correspondence to the simplification rules of the path-sum formalism. The relatively opaque path-sum rules are shown to arise naturally from two powerful families of rewrite rules in the ZH-calculus. The first is the extension of the familiar graph-theoretic simplifications based on local complementation and pivoting to their hypergraph-theoretic analogues: hyper-local complementation and hyper-pivoting. The second is the graphical Fourier transform introduced by Kuijpers et al., which enables effective simplification of ZH-diagrams encoding multi-linear phase polynomials with arbitrary real coefficients.

quant-ph↗