\( \newcommand{\ket}[1]{\vert#1\rangle} \newcommand{\bra}[1]{\langle#1\vert} \newcommand{\bigket}[1]{\bigl\vert#1\bigr\rangle} \newcommand{\bigbra}[1]{\bigl\langle#1\bigr\vert} \newcommand{\class}[1]{\mathrm{#1}} \newcommand{\problem}[1]{\mathrm{#1}} \renewcommand{\natural}{\mathbb{N}} \newcommand{\real}{\mathbb{R}} \newcommand{\complex}{\mathbb{C}} \newcommand{\ip}[2]{\left\langle#1, #2 \right\rangle} \newcommand{\Tr}{\mathop{\mathrm{Tr}}\nolimits} \newcommand{\tr}{\mathop{\mathrm{tr}}\nolimits} \newcommand{\abs}[1]{\left\lvert#1 \right\rvert} \newcommand{\norm}[1]{\left\lVert#1 \right\rVert} \newcommand{\floor}[1]{\left\lfloor#1 \right\rfloor} \newcommand{\X}{\mathcal{X}} \newcommand{\Y}{\mathcal{Y}} \newcommand{\A}{\mathcal{A}} \newcommand{\B}{\mathcal{B}} \newcommand{\E}{\mathop{\mathbb{E}}} \newcommand{\Var}{\mathop{\mathrm{Var}}} \newcommand{\dif}{\mathrm{d}} \newcommand{\eps}{\epsilon} \newcommand{\sign}{\mathrm{sign}} \newcommand{\poly}{\mathrm{poly}} \newcommand{\polylog}{\mathrm{polylog}} \newcommand{\negl}{\mathrm{negl}} \newcommand{\church}[1]{\overline{#1}} \newcommand{\defeq}{\stackrel{\text{def}}{=}} \newcommand{\pair}[2]{\langle#1, #2\rangle} \newcommand{\tuple}[1]{\langle#1\rangle} \newcommand{\red}{\rightarrow} \newcommand{\reds}{\twoheadrightarrow} \newcommand{\betared}{\rightarrow_{\beta}} \newcommand{\betareds}{\twoheadrightarrow_{\beta}} \newcommand{\betaeq}{=_{\beta}} \newcommand{\betaetared}{\rightarrow_{\beta\eta}} \newcommand{\betaetareds}{\twoheadrightarrow_{\beta\eta}} \newcommand{\parared}{\rightarrow_{\|}} \newcommand{\parareds}{\twoheadrightarrow_{\|}} \newcommand{\desc}[1]{\langle#1 \rangle} \newcommand{\adv}{\mathcal{A}} \newcommand{\dis}{\mathcal{D}} \newcommand{\labelsty}[1]{\mathrm{#1}} \newcommand{\Enc}{\labelsty{Enc}} \newcommand{\Dec}{\labelsty{Dec}} \newcommand{\plain}{\labelsty{p}} \newcommand{\cipher}{\labelsty{c}} \newcommand{\PRG}{\labelsty{PRG}} \newcommand{\Commit}{\labelsty{Com}} \newcommand{\oracle}{\mathcal{O}} \newcommand{\Sim}{\labelsty{Sim}} \newcommand{\comp}{\labelsty{c}} \newcommand{\view}{\labelsty{view}} \newcommand\TIME{\class{TIME}} \newcommand\SPACE{\class{SPACE}} \newcommand\SIZE{\class{SIZE}} \newcommand\NTIME{\class{NTIME}} \newcommand\NSPACE{\class{NSPACE}} \newcommand\BQP{\class{BQP}} \newcommand\BPP{\class{BPP}} \newcommand\QMA{\class{QMA}} \renewcommand\P{\class{P}} \newcommand\Ppoly{\class{P{/}poly}} \newcommand\NP{\class{NP}} \newcommand\NPC{\class{NP}\text{-complete}} \newcommand\coNP{\class{coNP}} \newcommand\MA{\class{MA}} \newcommand\AM{\class{AM}} \newcommand\QCMA{\class{QCMA}} \newcommand\EXP{\class{EXP}} \newcommand\NEXP{\class{NEXP}} \newcommand\PP{\class{PP}} \newcommand\GapP{\class{GapP}} \newcommand\IP{\class{IP}} \newcommand\QIP{\class{QIP}} \newcommand\PSPACE{\class{PSPACE}} \newcommand\NPSPACE{\class{NPSPACE}} \newcommand\MIP{\class{MIP}} \newcommand\RE{\class{RE}} \newcommand\QMAM{\class{QMAM}} \newcommand\PH{\class{PH}} \renewcommand\L{\class{L}} \newcommand\NL{\class{NL}} \newcommand\coNL{\class{coNL}} \newcommand\NLC{\class{NL}\text{-complete}} \newcommand\PPAD{\class{PPAD}} \newcommand\SharpP{\#\class{P}} \newcommand\HVPZK{\class{HVPZK}} \newcommand\HVSZK{\class{HVSZK}} \newcommand\PZK{\class{PZK}} \newcommand\SZK{\class{SZK}} \newcommand\CZK{\class{CZK}} \newcommand\val{\mathrm{val}} \newcommand\vale{\mathrm{val}^*} \newcommand\perm{\mathop{\mathrm{perm}}\nolimits} \newcommand\pathfunc{\mathrm{path}} \newcommand\SELF{\problem{SELF}} \newcommand\HALT{\problem{HALT}} \newcommand\MINTM{\problem{MIN}_\text{TM}} \newcommand\ACCTM{\problem{ACC}_\text{TM}} \newcommand\TQBF{\problem{TQBF}} \newcommand\PAL{\problem{PAL}} \newcommand\PATH{\problem{PATH}} \newcommand\LONGPATH{\problem{LONGEST\text{-}PATH}} \newcommand\SHORTPATH{\problem{SHORTEST\text{-}PATH}} \newcommand\HAMPATH{\problem{HAM\text{-}PATH}} \newcommand\HAMCYCLE{\problem{HAM\text{-}CYCLE}} \newcommand\INDSET{\problem{IND\text{-}SET}} \newcommand\MINCUT{\problem{MIN\text{-}CUT}} \newcommand\MAXFLOW{\problem{MAX\text{-}FLOW}} \newcommand\MAXCUT{\problem{MAX\text{-}CUT}} \newcommand\MAXCUTAPP{\problem{MAX\text{-}CUT\text{-}APPROX}} \newcommand\SAT{\problem{SAT}} \newcommand\PERM{\problem{PERMANENT}} \newcommand\THREESAT{3\text{-}\problem{SAT}} \newcommand\TWOSAT{2\text{-}\problem{SAT}} \newcommand\TWOUNSAT{2\text{-}\problem{UNSAT}} \newcommand\NAESAT{\problem{NAESAT}} \newcommand\REACHABILITY{\problem{REACHABILITY}} \newcommand\THREECOL{3\text{-}\problem{COLORING}} \newcommand\CLIQUE{\problem{CLIQUE}} \newcommand\COL{\problem{COLORING}} \newcommand\COMPOSITE{\problem{COMPOSITE}} \newcommand\PRIME{\problem{PRIME}} \newcommand\TSP{\problem{TSP}} \newcommand\VC{\problem{VERTEX\text{-}COVER}} \newcommand\FACTOR{\problem{FACTOR}} \newcommand\GI{\problem{GRAPH\text{-}ISO}} \newcommand\GNI{\problem{GRAPH\text{-}NONISO}} \newcommand\SHORTPROOF{\problem{SHORT\text{-}PROOF}} \newcommand\UHALT{\problem{UNARY\text{-}HALT}} \newcommand\GG{\problem{GENERAL\text{-}GEOGRAPHY}} \newcommand\FG{\problem{FORMULA\text{-}GAME}} \)

Birkhoff-von Neumann Quantum Logic

Aochu Dai

1 Background

Verification and analysis are very important topics in quantum programs and circuits. To formally verify the characteristics of a quantum system, we can represent properties of a quantum state by identifying some linear subspace of the total space \(\mathcal{H}\) containing the state. When the vector of the quantum state is in the subspace, we say the state satisfies the subspace. This idea can be generalized to a well-defined orthomodular lattice logic system, called Birkhoff-von Neumann quantum logic. We write \(\mathcal{S}(\mathcal{H})\) for the set of subspaces of \(\mathcal{H}\), then \((\mathcal{S}(\mathcal{H}), \cap, \lor, \neg)\) forms an orthomodular lattice. The logic connectives conjunction and negation means the intersection and orthocomplement of subspaces. The disjunction of two subspaces stands for the larger subspace spanned by them. Unlike Boolean logic, the quantum logic is not distributive between conjunction and disjunction.

You can find a detailed introduction and some examples in Section 5.1 of [4].

2 Problems

  1. In \(2^n\)-dimensional Hilbert space \(\mathcal{H}\), \(V_1, V_2\) are subspaces stabilized by Pauli subgroups \(\langle g_1,g_2,\cdots,g_l\rangle\) and \(\langle g_1',\cdots,g_m'\rangle\). Treat \(V_1\) and \(V_2\) as propositions of Birkhoff-von Neumann quantum logic, please give algorithms to compute the stabilizer groups (if there are) of \(V_1\cap V_2\), \(V_1\lor V_2\), and \(\neg V_1\), represented in the form of generators.
  2. In Problem 1, we have found that \(V_1\lor V_2\) is not always legal for stabilizer formalism. That is, The disjunction of two stabilizer subspaces may be not a stabilizer subspace, which always has \(2^k\) dimensions. Alternatively, we have some other methods to represent a quantum logic proposition by recording a set of orthonormal basis of the subspace. In this formalism, please give an algorithm to compute \(V_1\lor V_2\). What are the disadvantages of this method compared with the previous stabilizer-based method?
  3. (Research level, optional) Chapter 6 of [2] gives some notions about quantum precondition. Using Birkhoff-von Neumann logic as the assertion logic, could you specify the weakest precondition of \(A\) with respect to program statements: (1) \(q:= Uq\); (2) \(\text{if} (\square m\cdot M[q] = m \rightarrow S_m) \text{fi}\).

3 Contacts

Aochu Dai (dac22@mails.tsinghua.edu.cn)

4 References

[1] Ying, Mingsheng. “Floyd–hoare logic for quantum programs.” ACM Transactions on Programming Languages and Systems (TOPLAS) 33.6 (2012): 1-49.

[2] Mingsheng Ying. Foundations of Quantum Programming (Second Edition) 2024, Chapter 5, 6

[3] Fang, Wang, and Mingsheng Ying. “Symbolic execution for quantum error correction programs.” Proceedings of the ACM on Programming Languages 8.PLDI (2024): 1040-1065.

[4] Ying, Mingsheng. “Model checking for verification of quantum circuits.” Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings 24. Springer International Publishing, 2021.