Denotational Semantics · Quantum PL Wiki

Denotational semantics assigns a mathematical object to each program construct. Composition in the program corresponds to composition in the model. For finite-dimensional quantum registers, commands are often interpreted as completely positive, trace-nonincreasing maps on density operators. Subnormalized states $\rho\succeq0$ with $\mathrm{tr}(\rho)\leq1$ record probability mass as well as quantum information.

When the semantics collects terminating executions, output trace represents termination probability for a normalized input. A deterministic command that terminates on every input has a trace-preserving denotation. Trace loss can also represent a selected measurement branch, but its meaning must be stated explicitly.

Basic constructs and composition

The command skip denotes the identity map. A unitary command has meaning $\llbracket U\rrbracket(\rho)=U\rho U^\dagger$ . If $C_1;C_2$ means execute $C_1$ first and then $C_2$ , the order is

\llbracket C_1;C_2\rrbracket =\llbracket C_2\rrbracket\circ\llbracket C_1\rrbracket.

Independent operations on separate registers combine by tensor product. Their joint input may still be entangled; independence of operations does not imply independence of states.

For measurement operators $M_m$ and subsequent branch commands with meanings $\mathcal E_m$ , discarding the outcome gives

\rho\longmapsto\sum_m\mathcal E_m(M_m\rho M_m^\dagger).

Keeping the outcome instead uses a classical register, for example $\sum_m\lvert m\rangle\langle m\rvert\otimes M_m\rho M_m^\dagger$ before further branch processing.

Example: a measurement changes composition

Consider H; measure_z, with the measurement result forgotten. On input $\lvert0\rangle\langle0\rvert$ , the output is

\sum_{m=0}^1P_mH\lvert0\rangle\langle0\rvert H^\dagger P_m=I/2.

Reversing the commands gives $\lvert+\rangle\langle+\rvert$ : the initial measurement leaves $\lvert0\rangle$ unchanged, and the Hadamard then creates coherence. Thus these programs have different denotations even though both return unbiased computational-basis outcomes on that input.

This example links circuit descriptions to mathematical program meanings. The adjoint of a command's map also yields its weakest-precondition transformer.

Limitations

Loops and recursion require suitable fixed points or limits of finite unfoldings. Classical stores, allocation, and deallocation require additional state-space structure. Operational adequacy connects the denotation to observable execution behavior; full abstraction is a stronger correspondence with contextual equivalence and is not automatic.

The introductory model does not establish a semantics theorem for any particular implementation. Noise can be represented by channels, but the chosen channels, timing assumptions, and approximation bounds must be justified separately.

References

Peter Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527-586 (2004). DOI: 10.1017/S0960129504004256.
Samson Abramsky and Bob Coecke. A categorical semantics of quantum protocols. LICS (2004). arXiv:quant-ph/0402130.