\(
\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}}
\)
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].
Problems
- 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.
- 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?
- (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}\).
Aochu Dai (dac22@mails.tsinghua.edu.cn)
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.