Quantum Control and General Recursion beyond the Unitary Case

TL;DR

This paper introduces the first quantum programming language with recursion that supports coherent control of arbitrary quantum operations, addressing fundamental challenges in quantum software semantics.

Contribution

It develops both operational and denotational semantics for this language, incorporating measurement, recursion, and coherent control in a unified framework.

Findings

First language with recursion and coherent control of quantum operations

Operational semantics accounts for default evolution branches

Denotational semantics based on vacuum extensions and fully abstract

Abstract

Coherent control, aka quantum control, is a central concept in quantum computing that is attracting increasing attention from both the quantum foundations and quantum software communities. Defining coherent control in the presence of recursion and measurement has long been known to be a major challenge. In particular, no-go results have been established for standard semantical domains like completely positive maps. We address this problem by introducing the first quantum programming language with recursion that allows for the coherent control of arbitrary quantum operations. We equip this language with both an operational and a denotational semantics that we prove to be adequate. To design these semantics, we show that combining coherent control, recursion, and measurement crucially requires describing the evolution of subprograms in the absence of input. To address this, the operational semantics takes into account a default evolution branch, while the denotational semantics uses the concept of coherent quantum operation, based on vacuum extensions. We strengthen the validity of our approach by developing an observational equivalence: two programs are equivalent if their probability of termination is the same in any context. The denotational semantics is shown to be fully abstract with respect to this observational equivalence.