A Semantics for Quantum Loops
summary
Defines two precise semantics for quantum-controlled loops: a circuit-style unitary semantics built by copying the quantum guard into a growing temporary ancilla pool and compiling k iterations into a finite unitary, and a convergent linear semantics that uses the null base case to collect only terminated branches so the operator sequence is Cauchy and has a limit. Shows the unitary version lacks a general infinite limit while the linear version yields a usable denotation.
AI-written summary · about
chapters (11)
- 0:00Quantum loop semantics intro
- 1:03Quantum control flow loops
- 2:05Modeling quantum loops
- 3:07Math representation of loops
- 5:55Unitary limits for loops
- 8:26Classical semantics challenges
- 10:28Linear semantics unbounded
- 13:00Unitary vs linear semantics
- 15:45Loop semantics implications
- 16:26Conclusion future research
- 16:49Q&A
related talks
14mDenotational semantics for stabiliser quantum programs
21mQuantum and Classical Control (work-in-progress)
24mSemantics for Variational Quantum Programming
18mFormalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
18mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
24mQuantum Control Machine: The Limits of Control Flow in Quantum Programming
28mA type-theoretic account of quantum computation (Extended Abstract)
15mToward A Quantum Programming Language for Higher Level Formal Verification