Quantum Loop Programs
Quantum Loop Programs
Ying and Feng study the denotational behavior, termination, and almost termination of quantum loops, with applications to quantum walks.
Paper information (formal version: 2010, Acta Informatica 47(4):221–250; preprint: 2006) — Mingsheng Ying and Yuan Feng. arXiv:quant-ph/0605218
Work
The paper treats loops as first-class quantum-program constructs and studies their iteration semantics, termination, and almost termination. An iteration may contain quantum operations and measurement branches, so it cannot be reduced to ordinary matrix multiplication for a finite circuit. The paper develops a corresponding functional semantics and uses quantum walks to illustrate the expressive setting.
Contributions
- A systematic account of the computation and functional semantics of quantum loops.
- An analysis of termination and almost-termination behavior.
- A treatment of probabilistic effects from measurement branches and repeated iteration.
- Applications of the loop framework to examples such as quantum walks.
Limits
Loop semantics depends on the chosen state space, measurement rules, and definition of termination probability; it does not automatically provide invariants or decidability results for every loop. The model is idealized and omits device noise, runtime scheduling, and hardware resource costs. Turning a termination result into a proof for a concrete program still needs specifications and reasoning tools.
Connections
The paper fills in the fixed-point and recursion issues mentioned by Denotational Semantics and supplies loop-semantic background for Quantum Weakest Preconditions and Floyd–Hoare Logic for Quantum Programs. Compared with the finite static model of Quantum Circuits, quantum loop programs express dynamic iteration and termination behavior.
Original paper
Mingsheng Ying and Yuan Feng, Quantum Loop Programs, Acta Informatica 47(4), 221–250 (2010). arXiv:quant-ph/0605218