Recursive Quantum Programs with Classical Control

Syntax, declarations, and scope

This entry follows Chapter 5, Section 5.5 (printed pp. 82–90). Recursion here has classical control determined by measurement outcomes. It is distinct from recursion with coherent quantum control in Chapter 12. Prerequisites are denotational semantics and quantum languages.

Definitions 5.14–5.16 add procedure identifiers $X$ to the while language. A program scheme may contain calls. A declaration $D=\{X_i\Leftarrow S_i\}_{i=1}^n$ assigns bodies to distinct procedure names; bodies can call any of these names. A recursive program consists of a main statement $S$ and a declaration $D$ , allowing direct and mutual recursion. The formal development concerns parameterless procedures. Classical and quantum parameters are further extension questions, not features already covered by these results.

Operational meaning of a call

In a configuration $\langle S,\rho\rangle$ , the state is a partial density operator. The REC rule in Figure 5.6 (p. 84) is

\frac{X_i\Leftarrow S_i\in D}{\langle X_i,\rho\rangle\longrightarrow_D\langle S_i,\rho\rangle}.

A call unfolds to its body without changing the quantum state. The copy rule copies program syntax, not an unknown quantum state. Existing while-language rules remain, using transitions relative to the declaration.

Definition 5.19 defines $\llbracket S\mid D\rrbracket(\rho)$ by summing outputs of all finite terminating executions, with multiplicity when distinct paths yield the same output. Infinite executions contribute no terminating output. For normalized input, the output trace is the termination probability; individual branches must not first be normalized.

While loops as recursion

On p. 85, while M[q]=1 do B od is represented by

X\Leftarrow\mathbf{if}\ M[q]=0\to\mathbf{skip}\;\square\;1\to B;X\ \mathbf{fi}.

Using $X$ as the main statement gives the same denotation as the loop. Outcome 0 terminates; outcome 1 executes the body and calls again. General mutual recursion goes beyond this single-loop pattern.

Sequential composition still satisfies $\llbracket T_1;T_2\mid D\rrbracket=\llbracket T_2\mid D\rrbracket\circ\llbracket T_1\mid D\rrbracket$ : the order of function composition must not be reversed.

Finite unfolding and the supremum

Definition 5.20 and Eq. (5.16), p. 85, define approximations uniformly for arbitrary program schemes:

S_D^{(0)}\equiv\mathbf{abort},\qquad S_D^{(k+1)}\equiv S[S_{1D}^{(k)}/X_1,\ldots,S_{nD}^{(k)}/X_n].

Substitution is simultaneous. The initial approximation is abort, producing no terminating output, not skip. Approximants contain no procedure calls but may retain while constructs, so finite unfolding does not mean every execution terminates.

Proposition 5.8 (p. 86) states

\llbracket S\mid D\rrbracket=\bigsqcup_{k\geq0}\llbracket S_D^{(k)}\rrbracket.

This is the supremum of an increasing semantic chain, not a sum of approximants, which would double-count terminating paths. The proof establishes that every finite terminating execution appears in some unfolding and every terminating execution of an unfolding corresponds to one of the original program.

Least fixed points

Write $F_S$ for the semantic functional interpreting procedure names as quantum operations. The declaration induces

F_D(\mathcal E_1,\ldots,\mathcal E_n)= (F_{S_1}(\mathcal E_1,\ldots,\mathcal E_n),\ldots,F_{S_n}(\mathcal E_1,\ldots,\mathcal E_n)).

Section 5.5.4 works in the domain of quantum operations with componentwise order. Continuity allows iteration from the tuple of zero operations to yield the least fixed point. Theorem 5.2 (p. 88) gives

\mu F_D=\bigsqcup_{k\geq0}F_D^k(\mathbf0),\qquad \llbracket S\mid D\rrbracket=F_S(\mu F_D).

Leastness excludes extra output unsupported by finite terminating executions. For $X\Leftarrow X$ , the fixed-point equation alone permits many solutions, but iteration from zero remains zero, correctly representing nontermination. Existence of a least fixed point does not imply almost-sure termination.

Source verification

Chapter 5, Section 5.5: Definitions 5.14–5.21, Figure 5.6, Proposition 5.8, and Theorem 5.2. PDF images of printed pp. 84, 85, 86, and 88 were inspected for REC, simultaneous substitution, the supremum, and fixed-point formulas; surrounding scope was checked against page-separated text. This entry explains the semantics without claiming to reproduce every proof in the chapter.