Quantum While Programs: Syntax and Execution

This page uses a sequential language over finite-dimensional quantum registers. Measurement outcomes control execution; no additional classical store is returned. It presents a finite-dimensional account of the language discussed in Chapter 5; infinite-dimensional integer variables require additional operator and convergence conditions. Syntax, initialization, and small-step rules correspond to Definitions 5.1–5.4 and Figure 5.1; loop unfoldings correspond to Proposition 5.2.

States, registers, and program syntax

A register $q$ has Hilbert space $\mathcal H_q$ ; spaces for several registers combine by tensor product. Inputs are partial density operators: $\rho\succeq0$ and $\mathrm{tr}(\rho)\leq1$ . The trace records the probability mass of an execution branch, without renormalizing after each measurement. A finite-dimensional core language is

S ::= \mathbf{skip}\mid q:=0\mid \bar q:=U[\bar q]\mid S_1;S_2 \mid \mathbf{if}\ (\square_m\ M[\bar q]=m\to S_m)\ \mathbf{fi} \mid \mathbf{while}\ M[\bar q]=1\ \mathbf{do}\ S\ \mathbf{od}.

$U$ is a unitary on the listed registers. A case command uses one measurement $\{M_m\}$ satisfying $\sum_mM_m^\dagger M_m=I$ . It is not a sequence of Boolean guard tests, and its operators need not be mutually orthogonal projectors. A while command uses a two-outcome measurement $\{M_0,M_1\}$ : 0 exits and 1 continues. All local operators implicitly extend by the identity on other registers.

Initialization resets a register

The command $q:=0$ discards the previous information in $q$ and prepares $\lvert0\rangle$ . For an orthonormal basis $\{\lvert i\rangle\}$ of $q$ , define $A_i=\lvert0\rangle\langle i\rvert\otimes I_{\mathrm{rest}}$ . Then

\mathcal R_q(\rho)=\sum_i A_i\rho A_i^\dagger =\lvert0\rangle\langle0\rvert_q\otimes\mathrm{tr}_q(\rho).

The last expression uses tensor order with $q$ first. Initialization can destroy existing entanglement while preserving the reduced state of the other registers. It is a completely positive, trace-preserving map, and is generally not unitary.

One-step operational semantics

A configuration is written $\langle S,\rho\rangle$ , and $\downarrow$ marks termination. Every measurement branch below carries an unnormalized state. Its weight is already included in its trace, so no additional probability factor is applied.

\langle\mathbf{skip},\rho\rangle\to\langle\downarrow,\rho\rangle, \qquad \langle q:=0,\rho\rangle\to\langle\downarrow,\mathcal R_q(\rho)\rangle.

\langle\bar q:=U[\bar q],\rho\rangle\to\langle\downarrow,U\rho U^\dagger\rangle.

Sequential composition has two lifting rules:

\frac{\langle S_1,\rho\rangle\to\langle S_1',\rho'\rangle} {\langle S_1;S_2,\rho\rangle\to\langle S_1';S_2,\rho'\rangle},\qquad \frac{\langle S_1,\rho\rangle\to\langle\downarrow,\rho'\rangle} {\langle S_1;S_2,\rho\rangle\to\langle S_2,\rho'\rangle}.

In the first rule, $S_1'$ is a residual command rather than the termination marker. A case command has one rule for each outcome $m$ :

\langle\mathbf{if}\ (\square_m M=m\to S_m)\ \mathbf{fi},\rho\rangle \to\langle S_m,M_m\rho M_m^\dagger\rangle.

Writing $W$ for the loop, its exit and continuation rules are

\langle W,\rho\rangle\to\langle\downarrow,M_0\rho M_0^\dagger\rangle, \qquad \langle W,\rho\rangle\to\langle S;W,M_1\rho M_1^\dagger\rangle.

If distinct paths reach the same terminal configuration, their contributions must still be counted separately. Deduplicating them as a set would lose probability mass.

From the execution tree to a denotational map

Write $\mathcal E_m(\rho)=M_m\rho M_m^\dagger$ and $\mathcal B=\llbracket S\rrbracket$ . The basic denotations satisfy

\llbracket S_1;S_2\rrbracket=\llbracket S_2\rrbracket\circ\llbracket S_1\rrbracket, \qquad \llbracket\mathbf{if}\rrbracket=\sum_m\llbracket S_m\rrbracket\circ\mathcal E_m.

The contribution from exiting after exactly $n$ completed body executions is $\mathcal E_0\circ(\mathcal B\circ\mathcal E_1)^n$ . Hence

\llbracket W\rrbracket(\rho)=\sum_{n=0}^{\infty} \mathcal E_0\big((\mathcal B\circ\mathcal E_1)^n(\rho)\big).

The finite partial sums increase monotonically and have trace at most the input trace, so they converge in finite dimensions. Set $F_0=0$ and $F_{k+1}=\mathcal E_0+F_k\circ\mathcal B\circ\mathcal E_1$ . Their limit is the least solution of $F=\mathcal E_0+F\circ\mathcal B\circ\mathcal E_1$ . The zero map denotes a program that never terminates; it does not denote an immediate normal return.

For a normalized input, $\mathrm{tr}(\llbracket S\rrbracket(\rho))$ is the eventual termination probability. Missing mass is the probability of divergence, including possible divergence inside the body. Termination with probability one does not imply a uniform finite bound on the number of steps.

Example: measure, flip, and test again

Take computational-basis measurement $M_i=\lvert i\rangle\langle i\rvert$ and body $X$ . Outcome 0 exits immediately. Outcome 1 is flipped to the zero state by $X$ and exits at the next test. Thus

\llbracket W\rrbracket(\rho)=M_0\rho M_0+M_0XM_1\rho M_1X^\dagger M_0 =\mathrm{tr}(\rho)\lvert0\rangle\langle0\rvert.

The loop terminates with probability one on every input. If the body is replaced by skip, input $\lvert1\rangle$ never exits and has zero output denotation, whereas input $\lvert0\rangle$ exits immediately.

Infinite-dimensional integer variables in the textbook

The type definitions appear on printed page 64, and initialization and transition rules in Figure 5.1 on page 67. The textbook allows both Boolean type $\mathcal H_2$ and integer type $\mathcal H_\infty$ . The latter has computational basis $\{\lvert n\rangle:n\in\mathbb Z\}$ and can be represented as $\ell^2(\mathbb Z)$ . A quantum register is a finite sequence of distinct variables, so even finitely many registers may have an infinite-dimensional state space.

The textbook's initialization rule for an integer variable is

\mathcal R_q(\rho)=\sum_{n=-\infty}^{\infty} (\lvert0\rangle_q\langle n\rvert\otimes I)\rho (\lvert n\rangle_q\langle0\rvert\otimes I).

Here the input is a positive trace-class operator. The finite partial sums are positive with bounded trace, and their convergence can be interpreted in trace norm. This is not a formal series of arbitrary unbounded matrices. Dual assertions are bounded effects, and local unitaries and measurement operators must be well-defined on the relevant Hilbert spaces. Unbounded position or momentum operators cannot directly serve as effects. Finite-dimensional matrix enumeration and numerical eigenvalue methods do not automatically extend to this setting.

Figure 5.1 defines a configuration as a pair consisting of a program and a partial density operator, without an additional general classical store; this page uses the same convention. Figure 5.2 on printed page 68 (PDF page 6) gives a separate pure-state probabilistic transition semantics: it normalizes the conditional state and labels the transition arrow with its probability. That differs from absorbing probabilities into partial density operators as above; the two conventions must not be combined in a way that counts a branch weight twice. Initialization can turn a globally pure entangled state into a mixed state, so Figure 5.2 has no general pure-state initialization rule.