Foundations of Quantum Programming

6.4.5 An Example

To close out this section, we present a simple example that helps us to understand the semantic notions introduced here.

Example 6.4.1

Let q be a qubit variable and x,y two classical variables. Consider the QuGCL program

$\begin{array}{l}\begin{array}{ccc}P\equiv \hfill & \mathbf{qif}|0\rangle \to \hfill & H[q];\hfill \\ \mathbf{if}{M}^{(0)}[q:x]=\hfill & 0\to X[q];\hfill \\ \square \hfill & 1\to Y[q]\hfill \\ \mathbf{fi}\hfill \\ \square |1\rangle \to \hfill & S[q];\hfill \\ \mathbf{if}{M}^{(1)}[q:x]=\hfill & 0\to Y[q]\hfill \\ \square \hfill & 1\to Z[q]\hfill \\ \mathbf{fi};\hfill \\ X[q];\hfill \\ \mathbf{if}{M}^{(0)}[q:y]=\hfill & 0\to Z[q]\hfill \\ \square \hfill & 1\to X[q]\hfill \\ \mathbf{fi}\hfill \\ \mathbf{fiq}\hfill \end{array}\hfill \end{array}$

where M⁽⁰⁾,M⁽¹⁾ are the measurements on a qubit in computational basis |0〉,|1〉 and basis |±〉, respectively (see Example 6.3.3), H is the Hadamard gate, X,Y,Z are the Pauli matrices, and S is the phase gate (see Examples 2.2.1 and 2.2.2). The program P is a quantum case statement between two subprograms ...