We consider a formal model of quantum circuit description languages (QCDLs) in which semantically meaningful programs correspond to computable unitary matrices. We show that any semantically universal QCDL -- that is, any QCDL able to describe all computable unitary matrices, which in turn form the set of matrices we can meaningfully represent on digital hardware -- cannot have a semi-decidable set of semantically meaningful descriptions. In particular, no such language admits a compiler that reliably recognizes all valid program descriptions. This result stands in contrast to classical programming languages. While compilation in languages such as C or C++ may itself involve non-terminating computations, the set of semantically meaningful programs remains recursively enumerable, since successful compilation provides a witness of validity. The essential difference lies in the nature of the semantic domains: classical languages describe partial recursive functions, whereas QCDLs describe total unitary operators. Our analysis establishes a fundamental limitation of quantum circuit description languages and highlights a structural distinction between classical and quantum models of computation at the level of formal language theory.
We consider a formal model of quantum circuit description languages (QCDLs) in which semantically meaningful programs correspond to computable unitary matrices. We show that any semantically universal QCDL -- that is, any QCDL able to describe all computable unitary matrices, which in turn form the set of matrices we can meaningfully represent on digital hardware -- cannot have a semi-decidable set of semantically meaningful descriptions. In particular, no such language admits a compiler that reliably recognizes all valid program descriptions. This result stands in contrast to classical programming languages. While compilation in languages such as C or C++ may itself involve non-terminating computations, the set of semantically meaningful programs remains recursively enumerable, since successful compilation provides a witness of validity. The essential difference lies in the nature of the semantic domains: classical languages describe partial recursive functions, whereas QCDLs describe total unitary operators. Our analysis establishes a fundamental limitation of quantum circuit description languages and highlights a structural distinction between classical and quantum models of computation at the level of formal language theory.
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.
We consider a formalism ofquantum compiler functions– functions that map unitary matrices to corresponding gate-circuit approximations – and prove the infeasibility of digitally computing such functions. Since the gate-circuit model of quantum computing emerged, much research has been conducted to find algorithmic solutions to thequantum compiler problem. The renownedSolovay-Kitaev theoremproves the existence of quantum compiler functions that provide low-complexity gatecircuit approximations to arbitrary unitary matrices, which is indispensable for the practical feasibility of gate-based quantum computing. However, the mere existence of such functions does not imply theirrealizabilityby means of analgorithm– a constructive procedure executed by aTuring machine. In fact, no algorithm for computing any quantum compiler function is known today. The present article demonstrates that no such algorithm can exist. We prove that no quantum compiler function can satisfyBanach-Mazur computability, which is a formalization of algorithmic feasibility with (mathematically) weak requirements. In consequence, there definitely does not exist a Turing machine that computes any quantum compiler function in the above sense, nor can there exist aconstructive proofof the existence of any such function. Furthermore, we discuss proposed methods of quantum compiling and analyze them in the context of our results.
We propose the design of a programming language for quantum computing. Traditionally, quantum algorithms are frequently expressed at the hardware level, for instance in terms of the quantum circuit model or quantum Turing machines. These approaches do not encourage structured programming or abstractions such as data types. In this paper, we describe the syntax and semantics of a simple quantum programming language with high-level features such as loops, recursive procedures, and structured data types. The language is functional in nature, statically typed, free of run-time errors, and has an interesting denotational semantics in terms of complete partial orders of superoperators.
We consider the problem of computing gate-circuit approximations of quantum algorithms, i.e., unitary operators, from the perspective of computable (effective) analysis. The scientific community thinks the Solovay-Kitaev theorem a mile-stone in quantum compiling - the task of computing gate-circuit approximations - because it proves the existence of efficient quantum compilers in an analytic sense. However, since we cannot represent unitary operators in a mere analytical way on digital computers, contemporary digital implementations of quantum compiling resort to heuristic numerics and remain below the computational performance engineers hope to realize using the result of Solovay and Kitaev. This paper discusses quantum compiling within a framework of computable analysis, establishing a concept of computable unitary operators for digital computing based on the theory of Turing machines. Particularly, we prove that digital quantum compiling is uncomputable due to the underlying algebraic structure. Finally, we discuss several implications of our findings for heuristic digital implementations of quantum compiling, hinting toward possible research directions to thoroughly understand the relevant bottlenecks.
Many quantum programming languages have been recently introduced to create a new tool for expressing quantum algorithms. However, many have failed to formally express \nthemselves as a universal programming language for quantum computation. In this dissertation, the SequenceL language is shown to be universal in two models of quantum computation, the circuit and machine models. A SequenceL quantum interpreter is developed to show universality in the circuit model. A universal quantum Turing machine (UQTM) is introduced using non-recursive computational laws of the functional language, SequenceL with no explicit recursion. The SequenceL UQTM is implemented \nbased on the rules of Bernstein and Vasari’s UQTM. Bernstein and Vasari’s UQTM definition is expanded to include quantum Turing machine with arbitrary run times. \nFinally, postselection is introduced as a halting scheme for quantum Turing machines.
Many production quantum programming languages represent hybrid quantum computations by extending a classical base language with a quantum effect, where qubits are addressed by reference, and quantum operations are understood to mutate some external quantum state. However, the semantics of this view of quantum computation remains underdeveloped, especially when the language allows mid-circuit measurements and non-termination.
In this work, we provide a general method for building denotational semantics for such languages, by defining the quantum orchestra monad, which precisely captures this style of quantum effect. The monad has a concrete presentation, being based on the formalism of quantum instruments, a common tool in quantum information theory for capturing the action of a quantum process along with its classical outcomes. It acts on the category DCPO, and so enables the interpretation of divergent hybrid programs.
The quantum orchestra monad serves as a natural extension of both the classical state monad and the probabilistic powerdomain monad. We investigate some of the subtleties present when trying to naïvely extend these definitions to the quantum non-commutative case.