Quantum Predicate Connectives and Noncommutativity

An effect is a bounded Hermitian operator $0\preceq A\preceq I$. Its satisfaction value $\mathrm{tr}(A\rho)$ need not be Boolean. This entry follows §6.1 and §6.1.2; printed pages 94 and 100 (PDF pages 4 and 10) were checked visually. See Quantum Hoare Logic.

Four connective constructions

Negation is $I-A$. For normalized states its value is $1-\mathrm{tr}(A\rho)$; for partial density operators replace 1 by $\mathrm{tr}(\rho)$.

Assertions on separate registers combine as $A\otimes B$. On product input their value factors as $\mathrm{tr}(A\rho_1)\mathrm{tr}(B\rho_2)$. Entangled input need not factor. On overlapping spaces, $AB$ need not even be Hermitian. Commuting effects do have an effect product, but that product should not be identified with every proposed logical intersection operation.

Convex combinations $\sum_i p_iA_i$ remain effects for $p_i\geq0$, $\sum_i p_i\leq1$. Measurement-conditioned combination is $\sum_mM_m^\dagger A_mM_m$, where $\sum_mM_m^\dagger M_m=I$. It combines assertions selected by measurement outcomes rather than applying Boolean disjunction to an unchanged input. These constructions support auxiliary rules and case reasoning.

A noncommuting example

For $A=|0\rangle\langle0|$ and $B=|+\rangle\langle+|$,

They differ, and $AB$ is not Hermitian. Legal assertions do not make every combination legal.

Weakest preconditions and commutativity

Although $\mathrm{wp}_{\mathcal E}(A)=\mathcal E^*(A)$, an adjoint completely positive map is generally not multiplicative. Proposition 6.5 distinguishes:

• Unitaries: $[U^\dagger AU,U^\dagger BU]=U^\dagger[A,B]U$, so commutativity is preserved in both directions.
• Projective measurement with forgotten outcomes: $\mathcal E^*(A)=\sum_kP_kAP_k$. The transformed assertions commute exactly when $P_kAP_k$ and $P_kBP_k$ commute within every block.
• Rank-one basis measurement: all transformed assertions are diagonal in the same basis, even when their original assertions did not commute.

The preceding example becomes $A$ and $I/2$ after computational-basis dephasing. Higher-rank measurement blocks retain room for noncommutativity.

Sufficient conditions for general operations

Section 6.1.2 studies Kraus and system–environment representations. If $A,B$ commute with each other and both commute with every Kraus operator, their weakest preconditions commute (Proposition 6.8). The property of commuting with every Kraus operator is representation-independent (Lemma 6.5): equivalent lists, padded with zeros, are related by unitary linear combinations.

These are sufficient conditions, not necessary conditions for arbitrary operations. Other spectral and environment-compression criteria in the chapter retain their finite-dimensional or operator assumptions. They do not establish universal preservation of simultaneous observability.

Source

Mingsheng Ying, Foundations of Quantum Programming, second edition, §6.1 and §6.1.2, Example 6.1, Proposition 6.5, Lemma 6.5 and Proposition 6.8. Chapter DOI.