Foundations of Quantum Programming

Proof

We only prove (ii), and the proof of (i) is similar and easier. For every $ρ \in D (H_{all})$ , by Proposition 4.2.3 (iv) we observe:

$\begin{array}{l} \begin{array}{l} t r [(M_{0}^{†} P M_{0} & + M_{1}^{†} (w l p . S . (w l p . while . P)) M_{1}) ρ] \\ = t r (P M_{0} ρ M_{0}^{†}) + t r [(w l p . S . (w l p . while . P)) M_{1} ρ M_{1}^{†}] \\ = t r (P M_{0} ρ M_{0}^{†}) + t r [(w l p . while . P) ⟦ S ⟧ (M_{1} ρ M_{1}^{†})] \\ + [t r (M_{1} ρ M_{1}^{†}) - t r (⟦ S ⟧ (M_{1} ρ M_{1}^{†}))] \\ = t r (P M_{0} ρ M_{0}^{†}) + t r [P ⟦ while ⟧ (⟦ S ⟧ (M_{1} ρ M_{1}^{†}))] + [t r (⟦ S ⟧ (M_{1} ρ M_{1}^{†}) \\ - t r (⟦ while ⟧ (⟦ S ⟧ (M_{1} ρ M_{1}^{†}))] + [t r (M_{1} ρ M_{1}^{†}) - t r (⟦ S ⟧ (M_{1} ρ M_{1}^{†}))] \\ = t r [P (M_{0} ρ M_{0}^{†} + ⟦ while ⟧ (⟦ S ⟧ (M_{1} ρ M_{1}^{†})))] \\ + [t r (M_{1} ρ M_{1}^{†}) - t r (⟦ while ⟧ (⟦ S ⟧ (M_{1} ρ M_{1}^{†}))] \\ = t r (P ⟦ while ⟧ (ρ)) + [t r (ρ M_{1}^{†} M_{1}) - t r (⟦ while ⟧ (⟦ S ⟧ (M_{1} ρ M_{1}^{†})))] \\ = t r (P ⟦ while ⟧ (ρ)) + [t r (ρ (I - M_{0}^{†} M_{0})) - t r (⟦ while ⟧ (⟦ S ⟧ (M_{1} ρ M_{1}^{†})))] \\ = t r (P ⟦ while ⟧ (ρ)) + [t r (ρ) - t r (M_{0} ρ M_{0}^{†} + ⟦ while ⟧ (⟦ S ⟧ (M_{1} ρ M_{1}^{†})))] \\ = t r (P ⟦ while ⟧ (ρ)) \end{array} \end{array}$

Get Foundations of Quantum Programming now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.

Start your free trial

Foundations of Quantum Programming by Mingsheng Ying

Don’t leave empty-handed

It’s yours, free.

Check it out now on O’Reilly