Foundations of Quantum Programming

$\begin{array}{l}\hfill \begin{array}{cc}t{r}_{{\mathcal{H}}_{qvar(S)}}& (〚X;Q〛(|\mathrm{\Psi }\rangle \langle \mathrm{\Psi }|))\\ =t{r}_{{\mathcal{H}}_{qvar(S)}}\left[\sum _{\{{\sigma }_i\},\delta }\sum _{i,j}{\mathrm{\Lambda }}_i{\mathrm{\Lambda }}_j\cdot |i\rangle \langle j|(F_{\delta }{E}_{i{\sigma }_i}|{\psi }_i\rangle \langle {\psi }_j|E_{j{\sigma }_j}^{†}{F}_{\delta }^{†})\right]\\ =\sum _{\{{\sigma }_i\},\delta }\sum _i{\mathrm{\Lambda }}_i^2\cdot F_{\delta }{E}_{i{\sigma }_i}|{\psi }_i\rangle \langle {\psi }_i|E_{i{\sigma }_i}^{†}{F}_{\delta }^{†}.\end{array}\end{array}$

  (6.55)

On the other hand, we can compute the semi-classical semantics of Y:

$\begin{array}{l}\hfill \begin{array}{cc}╙Y╜({\oplus }_{i=1}^n{\sigma }_i{\delta }_i)|\mathrm{\Psi }\rangle & =\sum _{i=1}^n{\alpha }_{{\{{\sigma }_k,{\delta }_k\}}_{k\ne i}}^{(i)}\cdot |i\rangle (╙S_i;Q╜({\sigma }_i{\delta }_i)|{\psi }_i\rangle )\\ =\sum _{i=1}^n{\alpha }_{{\{{\sigma }_k,{\delta }_k\}}_{k\ne i}}^{(i)}\cdot |i\rangle (F_{{\delta }_i}{E}_{{\sigma }_i}|{\psi }_i\rangle ).\end{array}\end{array}$

Furthermore, we obtain:

$\begin{array}{l}\hfill \begin{array}{c}t{r}_{{\mathcal{H}}_{qvar(S)}}(〚Y〛(|\mathrm{\Psi }\rangle \langle \mathrm{\Psi }|))\\ =t{r}_{{\mathcal{H}}_{qvar(S)}}\left[\sum _{\{{\sigma }_i,{\delta }_i\}}\sum _{i,j}{\alpha }_{{\{{\sigma }_k,{\delta }_k\}}_{k\ne i}}^{(i)}{({\alpha }_{{\{{\sigma }_l,{\delta }_l\}}_{l\ne j}}^{(j)})}^{*}\cdot |i\rangle \langle j|(F_{{\delta }_i}{E}_{i{\sigma }_i}|{\psi }_i\rangle \langle {\psi }_j|E_{j{\sigma }_j}^{†}{F}_{{\delta }_j}^{†})\right]\\ =\sum _{\{{\sigma }_i\},\delta }\sum _i{\left|{\alpha }_{{\{{\sigma }_k,{\delta }_k\}}_{k\ne i}}^{(i)}\right|}^2\cdot F_{{\delta }_i}{E}_{i{\sigma }_i}|{\psi }_i\rangle \langle {\psi }_i|E_{i{\sigma }_i}^{†}{F}_{{\delta }_i}^{†}.\end{array}\end{array}$

  (6.56)

Comparing equations (6.55) and (6.56), we see that

$\begin{array}{l}\hfill t\end{array}$