arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2507.11676

Quantum Circuits Are Just a Phase

Chris Heunen·Louis Lemonnier·Christopher McNally·Alex Rice
View original source ↗Read source document ↗Export metadata ↓

Abstract

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.

Explore related subjects

cs.PLcs.LOquant-ph

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Chris Heunen, Louis Lemonnier, Christopher McNally, Alex Rice. 2025-12-01. Quantum Circuits Are Just a Phase. https://doi.org/10.1145/3776731

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A Rig of Transformations

In high-level functional languages, the compiler often gives users little control over the runtime representation of data types. Yet how we model data structures at the program level can be different to how we want to represent them at the binary level, for efficiency or legacy reasons. Hence being able to describe data layouts and their transformations for data types is a useful and necessary part of programming, but difficult to do correctly, efficiently and ergonomically. We present a model of finite algebraic data types as a commutative rig (a ring without additive inverses), where the rig-equalities are modelled by isomorphisms between data. Using this approach, we can also model embedding a data type into a larger type (e.g. bit-padding) as a partial isomorphism.

cs.PL↗
arXiv2026

Certified Panic Mode: Repair-Invariant Error Recovery for Maximal-Munch Lexing

Classical panic-mode recovery skips a failed scan forward by convention: it promises progress, and membership in a designated set where one is found, but no repair-universal boundary guarantee for the position it lands on. This paper chooses the resume position by theorem: a position is a sound recovery point when every prefix repair whose scan commits through the certificate's returned evidence places a token boundary there, complete repairs the special case, by a committed-prefix lemma over certificates posted for a different purpose (arXiv:2608.03473, arXiv:2608.09761). The quantifier is strictly the stronger one, and a dichotomy locates the difference exactly: the inclusion is strict precisely when no repair completes while some scan still commits through the evidence, a two-token witness realizing the case. The evidence-returning form pairs each answer with the interval it rests on, which is what makes the guarantee deployable: a caller who knows what the scanner cannot check decides whether the certified boundary transfers to the clean input it intended. The search is one forward walk in evidence order and provably terminates; the guarantee is per-automaton, relative to the active mode. The procedure ships in the munch lexing library, and a deterministic corruption study measures its recovery quality beside the classical skip-one and delimiter conventions. Every certified answer whose evidence survives the damage passes its executable landing check on every recovery move, 40,885 of 40,885; among first answers, the 5,595 resting on evidence the damage reached land 1,589 times, reported and never asserted. On 13,522 of the 16,808 trials the shipped repair routine labels beyond repair, the resumed suffix tokenizes whole and the two quantifiers provably coincide, so both are empty there if those negative labels are exact; 3,286 stay undetermined.

cs.PL↗
arXiv2026

Behavioral Analysis of Timed Actors using Syntactic Slice Equivalence

Tiny twins are compact behavioral models derived from timed actor models for selected observable messages. When a source model evolves, regenerating its tiny twin requires state-space exploration and reduction even if the relevant behavior is unchanged. We present a static analysis for Timed Rebeca that compares backward slices of Rebeca dependence graphs for a given set of observable message names. For the Zeno-free fragment with after annotations and no delay statements, we prove that slice equivalence implies weak timed bisimulation under the selected observations. This preserves observable actions and total elapsed time across internal transitions, allowing the existing tiny twin to be reused. We evaluate the implementation on ten benchmark models paired with revisions that preserve their observable slices. The cost of static comparison depends on the size of the graphs representing source statements and their dependencies, while tiny-twin generation depends on the number of reachable states and transitions. This difference is reflected in the measurements: static comparison takes less than one second using tens of megabytes of memory, while tiny-twin generation can take over an hour and use hundreds of gigabytes.

cs.PL↗