A Complete Calculus for Hamiltonian Quantum Programming

Jacques Carette, Chris Heunen, Robin Kaarsgaard, Neil J. Ross, Amr Sabry

Given the forces acting on a quantum particle, a Hamiltonian models its continuous evolution. Quantum computers evolve Hamiltonians to simulate physical systems, to solve optimisation problems, and to estimate eigenvalues, and even the popular circuit abstraction is compiled to Hamiltonians on the hardware. We introduce Hamilton, a process calculus whose parallel operator is the sum of interactions acting simultaneously. Its operational semantics is the Lie-Trotter product formula, which recovers a sum as the limit of ever finer sequential interleavings; compiling a program means halving it to a chosen precision and unrolling the interleaving into a circuit. The semantics is fully abstract, the expressible Hamiltonians are exactly those whose Pauli coefficients have the form $m/2^k$, the precision that successive halving reaches, and the equational theory is complete and decidable. A full implementation compiles Hamilton programs to circuits and decides their equivalence, and Agda proofs sanity-check the core metatheory.