Feynman Meets Turing: The Curse of Quantum Universality
Formal Languages and Automata Theory
Summary
The authors study programming languages designed to describe quantum circuits, which must represent certain special mathematical objects called unitary matrices. They show that any language capable of describing all these quantum circuits cannot have a compiler that always reliably recognizes which programs make sense. This is different from classical programming languages, where you can always list out valid programs because they describe functions that don't have this constraint. Their work points out a fundamental difference between classical and quantum computing languages from a theoretical perspective.
Authors
Yannik N. Böck, Holger Boche, Frank H. P. Fitzek
Abstract
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.