Termination of Nondeterministic Quantum Programs

TL;DR

This paper introduces a model for nondeterministic quantum programs, providing conditions and algorithms to determine their termination behavior, highlighting fundamental differences from classical programs due to quantum interference effects.

Contribution

It defines a quantum nondeterministic program model, characterizes termination conditions, and presents an algorithm for checking termination in finite-dimensional spaces.

Findings

A zero-one law for termination probability is established.

A necessary and sufficient condition for program termination is derived.

Quantum interference can cause nondeterministic programs to terminate with probability zero.

Abstract

We define a language-independent model of nondeterministic quantum programs in which a quantum program consists of a finite set of quantum processes. These processes are represented by quantum Markov chains over the common state space. An execution of a nondeterministic quantum program is modeled by a sequence of actions of individual processes. These actions are described by super-operators on the state Hilbert space. At each step of an execution, a process is chosen nondeterministically to perform the next action. A characterization of reachable space and a characterization of diverging states of a nondeterministic quantum program are presented. We establish a zero-one law for termination probability of the states in the reachable space of a nondeterministic quantum program. A combination of these results leads to a necessary and sufficient condition for termination of nondeterministic quantum programs. Based on this condition, an algorithm is found for checking termination of nondeterministic quantum programs within a fixed finite-dimensional state space. A striking difference between nondeterministic classical and quantum programs is shown by example: it is possible that each of several quantum programs simulates the same classical program which terminates with probability 1, but the nondeterministic program consisting of them terminates with probability 0 due to the interference carried in the execution of them.