Pith. sign in

REVIEW 5 minor 2 references

Qif resolves the correspondence problem and makes the quantum SWITCH definable for measurement-containing programs.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 22:04 UTC pith:3BYINH3G

load-bearing objection A serious, well-crafted PL paper that makes a credible case for a linear-type design letting quantum SWITCH be defined for arbitrary measurement-containing programs; the main caveat is the load-bearing strong monoidal embedding, but it is explicit and defended, so I'd send it out.

arxiv 2607.15873 v1 pith:3BYINH3G submitted 2026-07-17 cs.PL cs.LOquant-ph

Programming with Quantum-Controlled Quantum Channels

Kengo Hirata , Takeshi Tsukada This is my paper
classification cs.PL cs.LOquant-ph
keywords quantum programming languagesquantum SWITCHindefinite causal orderlinear type systemdenotational semanticsoperational semanticsquantum channelsprogram transformation
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Qif is a two-layer quantum programming language built to prove that quantum control of general quantum channels can be given a well-defined semantics. The paper's central claim is that the quantum SWITCH—the operation that superposes the two orders F∘G and G∘F—should be treated as a different kind of quantum control from a controlled operation, and that the right constraint is linearity: in a quantum conditional, each channel variable must be used exactly once in each branch. Under this constraint, the term qif x then F(G(y)) else G(F(y)) really does denote the quantum SWITCH, even when F and G contain measurements, and the denotation is independent of the choice of operator-sum decompositions. The paper backs this with a denotational semantics (a Hilb/CPM two-layer model), an operational semantics that compiles every well-typed program to a quantum circuit in the white-box setting, and soundness, adequacy, and full abstraction results. The payoff would be a programming language in which indefinite causal order is expressible and executable, not merely a physical curiosity.

Core claim

On the paper's own terms, the discovery is that the semantic ill-definedness of quantum conditional branching over channels has a precise cause—the correspondence problem: the then- and else-branches of qif contain measurements whose outcomes must be paired, and there is no canonical pairing in general. The authors show that if both branches use each higher-order channel variable exactly once (linearity), a canonical pairing exists, because each hidden measurement in F has a twin in the other branch. Interpreting qif in the Hilbert-space layer while classical constructs live in the completely-positive layer, with a structure-preserving embedding between them, then makes the defining equation

What carries the argument

The central machinery is the two-layer categorical model: the quantum sublanguage lives in Hilb (finite-dimensional Hilbert spaces and linear maps), the classical sublanguage lives in CPM (completely positive maps), and an embedding functor ι from Hilb to CPM connects them, preserving the compact closed structure exactly. The qif construct is interpreted using the biproduct in Hilb, not in CPM, which is what lets a pure superposition of two programs lift to a genuine superposition of channel orders. Around this sits a linear type system: in Hilb terms every variable is used exactly once, so the two branches of qif are forced to contain matching uses of the same function variables. The operat

Load-bearing premise

The load-bearing premise is that the denotational model—two layers, Hilb for pure quantum programs and CPM for classical/measurement programs, connected by an embedding that preserves the compact closed structure exactly—is the correct semantics for quantum control; if that embedding preserved structure only in a weaker (lax) sense, the coercion that lets a higher-order quantum operation be applied to a measurement-based channel would not exist, and the definability of the SW

What would settle it

Take F=G=D, where D is the measure-then-flip channel D(ρ)=|1⟩⟨0|ρ|0⟩⟨1|+|0⟩⟨1|ρ|1⟩⟨0|. Compute the syntactic dilation of qif x then F(G(y)) else G(F(y)) with x=|+⟩ and compare the final state on the control and target qubits with the quantum SWITCH's output, which retains entanglement between them. If the compiled circuit ever yields |+⟩⊗D(D(y))—the output of the non-switched composition—then the claimed equality fails; conversely, direct state tomography of the compiled circuit on this example settles the claim.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • The equation SWITCH(x,y,F,G) = qif x then F(G(y)) else G(F(y)) is valid for arbitrary quantum operations F and G, including programs that branch on measurement outcomes; this is the first such definability result.
  • Because the denotational semantics is independent of the choice of operator-sum decompositions, programs have a unique observational meaning even when F and G are given as black-box channels.
  • Every well-typed Qif program can be compiled to a quantum circuit by syntactic dilation; the compilation is white-box, so it does not contradict the impossibility of a black-box circuit for the quantum SWITCH with opaque holes.
  • The language distinguishes SWITCH from the superficially similar qif x then F(G(y)) else F(G(y)); the latter is rejected by linearity or denotes a different operation, resolving the apparent paradox that SWITCH(F,F) beats the composition F∘F.
  • Adding divergence yields a fully abstract semantics, so program equivalence in the language coincides with contextual equivalence at first-order types.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Our inference: the paper's linearity diagnosis suggests a general design principle for indefinite-causal-order languages—any construct that duplicates a channel inside the branches of quantum control is likely to reintroduce the correspondence ambiguity, so non-linear control of general channels may be intrinsically underdetermined.
  • Our inference: since compilation is white-box and depends on the chosen dilations of F and G, the practical cost of running a Qif program is sensitive to how F and G are implemented; the language itself does not provide a black-box realization of the SWITCH.
  • Our inference: the paper notes that one well-known indefinite-causal-order protocol is probably not expressible in Qif and that adding general recursion blocks a simple syntactic dilation. A testable extension is to apply the dilation dynamically, one loop iteration at a time, which the paper sketches but does not formalize.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

0 major / 5 minor

Summary. This paper presents Qif, a linear functional quantum programming language designed around the thesis that quantum-controlled operations and the quantum SWITCH are different mechanisms. The language has a quantum sublanguage (modelled in Hilb, with qif) and a classical sublanguage (modelled in CPM, with measurement and if), connected by a strong monoidal embedding ι:Hilb→CPM. The central claim is that the term SWITCH(x,y,F,G) = qif x then F(G(y)) else G(F(y)) defines the quantum SWITCH even when F,G are arbitrary quantum channels containing measurement, and that this is the first language with this property. The paper diagnoses the correspondence problem in earlier semantics and enforces a linear type discipline to solve it. It supplies a denotational semantics that is shown independent of Kraus decompositions, and an operational semantics obtained by syntactic dilation to a measurement-free language QifUnitary, which yields concrete white-box circuit synthesis. Theorems prove type safety, progress, termination, soundness, adequacy, and full abstraction with divergence.

Significance. Assuming the proofs are correct, this is a substantial contribution to quantum programming language semantics. It gives the first fully worked-out language in which the quantum SWITCH is definable for general quantum channels, with both a concise categorical model and an executable compilation strategy. The contrast with Dave et al.'s lax-monoidal model is illuminating and makes the source of the extra expressiveness precise. The paper's main theorems are formal, and the appendix contains detailed proofs; in particular, the semantic independence from Kraus decompositions is a strong correctness property. The white-box compilation theorem is a concrete algorithmic achievement. The main caveat is that the central claim is conditioned on the choice of a strong monoidal embedding; this is a design decision rather than a physical axiom, but it is supported by the operational 'no dummy values' analysis and is not an internal inconsistency. I found no error that would invalidate the central claim.

minor comments (5)
  1. [Section 3.1, Eq. (2)] The association of control states with the two causal orders is inconsistent with Eq. (1) and the qif semantics in Fig. 8. Eq. (1) gives |0⟩ -> G(F) and |1⟩ -> F(G) under Fig. 8, while Eq. (2) and the surrounding text say |0⟩ -> F(G) and |1⟩ -> G(F). The proof of Theorem 5.2 (Appendix C.12) computes |1⟩⊗F(G)+|0⟩⊗G(F), which matches Eq. (1), not Eq. (2). Since the two conventions differ by a NOT on the control qubit, this is a presentation bug, but it should be fixed for consistency, e.g. by swapping |0⟩ and |1⟩ in Eq. (2).
  2. [Section 4.1] The FO(A) restriction on qif/if results is justified only by a pointer to prior work (Hirata & Tsukada 2026). Please include a short explanation or a precise theorem statement, since this restriction also limits the expressiveness of the language and is not self-contained.
  3. [Appendix C.8] The 'abort' constant is described as causing divergence, but its syntactic dilation (κ≔α);() is a normal form in QifUnitary. The intended interpretation is that output test channels are projected onto ⟨0|, so the program has zero probability of producing an observable output. This should be stated explicitly to avoid confusion about the operational meaning of divergence.
  4. [Appendix C.9] In the full abstraction proof for the Hilb case, the construction of a unit-type context that distinguishes two terms differing by a global phase is only sketched. Please expand this step, e.g. by explaining how the qbit output is embedded into CPM and measured to produce a unit-type observation.
  5. [Section 5.1, Remark 5.1] The dependence of the central expressivity claim on the strong monoidal embedding is a design assumption. The paper should state this more prominently, e.g. in the introduction, so that the 'first language' claim is understood as relative to this semantic choice.

Circularity Check

0 steps flagged

No significant circularity; the SWITCH claim is derived from the model, with one minor non-load-bearing self-citation.

full rationale

The central derivation is self-contained rather than circular. The denotational semantics is defined compositionally in Hilb and CPM, and Theorem 5.2 is proved by computing the denotation of the SWITCH term from the qif rule and the strong monoidal embedding, then comparing the result with the external definition of the quantum SWITCH [Chiribella et al. 2013]. Proposition C.36 is a substitution lemma proved from the model, not an assumed instance of the target theorem. The operational semantics and its soundness/adequacy/full-abstraction results are proved relative to that denotational semantics. The only self-citation is the restriction forbidding function types as qif results, attributed to Hirata and Tsukada [2026]; that restriction is orthogonal to the first-order SWITCH example and does not carry the paper's central claim. The choice of a strong rather than lax embedding is an explicitly disclosed modeling assumption, not a circular one, and it is contrasted with Dave et al. 2025a. No prediction or theorem reduces by construction to its own input.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 1 invented entities

No free parameters fitted to data. The central claim rests on standard quantum-information and category-theoretic background: finite-dimensional Hilbert spaces, CPTP maps, Stinespring dilation, compact-closed categories with biproducts. The main domain assumption is that the two-layer Hilb/CPM model with the strong embedding ι is the right formalization of quantum control; this is a design choice, but the paper verifies its consequences thoroughly.

axioms (5)
  • domain assumption Quantum systems are finite-dimensional Hilbert spaces; states are density operators; operations are completely positive trace-preserving maps (quantum channels).
    Section 2 preliminaries; this is the standard quantum-information model the entire semantics is built on.
  • standard math Hilb and CPM are compact closed categories with biproducts, and the embedding functor ι: Hilb → CPM preserves the compact closed structure on the nose.
    Section 5.1; Theorem 5.2 and the lifting of higher-order operations depend on ι being strong monoidal and compact-closed preserving.
  • standard math Stinespring's dilation theorem: every quantum channel arises as a unitary on a dilated system followed by partial trace.
    Section 3.4 motivates the syntactic dilation; the paper explicitly notes the language-level transformation is not a direct corollary (footnote 7), but the technique is inspired by it.
  • domain assumption Measurements are modeled by the map m: (2) → (1,1) in CPM, and booleans are the biproduct (1,1); the semantics of if and qif uses the biproducts in CPM and Hilb respectively.
    Fig. 8; this modeling choice distinguishes classical and quantum control and is the formal locus of the correspondence problem.
  • ad hoc to paper Qif forbids function types in the results of qif and if (the FO(A) restriction), justified only by a technical reason in the authors' prior work (Hirata & Tsukada 2026).
    Section 4.1, typing rules in Fig. 7; this restriction is needed for the operational semantics' normal forms and may limit expressiveness of the language.
invented entities (1)
  • Output test channels κ in QifUnitary-with-divergence no independent evidence
    purpose: Device for proving full abstraction of the language with divergence (abort): they project measurement outcomes to ⟨0| and thereby distinguish semantic maps.
    Appendix C.1, C.8. Introduced solely for the proof; no external physical realization.

pith-pipeline@v1.3.0-alltime-deepseek · 61678 in / 12651 out tokens · 129143 ms · 2026-08-01T22:04:35.535889+00:00 · methodology

0 comments
read the original abstract

In contrast to a classical bit, which can only take the value $0$ or $1$, its quantum counterpart -- a qubit -- can exist in a superposition of $0$ and $1$. This is a superposition of data values, naturally raising the question of whether one can superpose not only data but also programs. For example, a particular superposition of programs, known as the quantum SWITCH, has attracted much attention, and its implementations and computational advantages have been studied extensively within the physics community. A naive way to control a program by a qubit is by means of a controlled operation. Given an operation $F$, this amounts to considering an operation that behaves as $F$ when the control qubit is $|1\rangle$, and as the identity operation when the control qubit is $|0\rangle$. This idea works well when $F$ is a unitary operation, but it is not well-defined for a general quantum channel. By contrast, the quantum SWITCH is free from the well-definedness issue. This contrast leads to the key insight of this paper: controlled operations and the quantum SWITCH should be regarded as different kinds of quantum control mechanisms. Building on this insight, we develop a novel quantum programming language with quantum control and measurement that can express the quantum SWITCH over quantum channels. Using a semantic analysis based on program transformations, we identify the source of the ill-behavedness of controlled operations as the \emph{correspondence problem}: a lack of coordination between the measurements performed in the then- and else-branches of quantum conditional branching. We address this problem with a linear type system that enforces alignment of the quantum operations used in the two branches, yielding a well-behaved language capable of expressing the quantum SWITCH.

Figures

Figures reproduced from arXiv: 2607.15873 by Kengo Hirata, Takeshi Tsukada.

Figure 1
Figure 1. Figure 1: Definition and implementation of a controlled [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Dilation of a program with no qif. (a) Source program. (b) Deferring the measurement. (c) Moving the qubit creation operations |0⟩ and |1⟩ to the beginning. Here CX is the controlled X gate. Source Programming Language. Before proceeding to the discussion, we briefly describe the programming language used here. The language has two types, bool and qubit. The qubit type is subject to the linearity constrain… view at source ↗
Figure 3
Figure 3. Figure 3: An example of the program transformation. (a) Source program. (b) Hoisting the measurement [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Comparison between the previous and new transformations. The previous transformation introduces [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Correspondence of measurements affects the translation. [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Syntax of QIF. Here, 𝑈 is a n-qubit unitary operator, and ℱ is a name for globally defined term. This observation leads to the following language design. We divide the language into two sublanguages: a classical sublanguage in which measurements are available, and a quantum sublan￾guage in which quantum conditional branching is available. In the classical sublanguage, quantum branching is not directly perm… view at source ↗
Figure 7
Figure 7. Figure 7: Typing rules for QIF. The rules labelled ⊢E are shared between ⊢Hilb and ⊢CPM. We omit the exchange rule, which permutes the order of elements in Δ. type is purely quantum if it does not involve bool, and we write Quantum(𝐴) to indicate that 𝐴 is purely quantum. The boolean type bool is not available in the quantum sublanguage. Most term constructors are from the standard linear lambda calculus or from qua… view at source ↗
Figure 8
Figure 8. Figure 8: Categorical semantics for QIF. Here, ev: (𝐴 ⊸ 𝐵) ⊗𝐴 → 𝐵 is the evaluation map, 𝜎𝐴,𝐵 : 𝐴⊗𝐵  𝐵⊗𝐴 is the braiding, swap: (1, 1) → (1, 1) is the swapping morphism, 𝑑⊕E : 𝐴⊗ (1⊕E 1)  𝐴⊕E𝐴 is the distribution isomorphism, 𝑚: (2) → (1, 1) is the measurement map, : 𝐼 ⊕ 𝐼 → 𝐼 is the discard map, and Λ𝑌 (−) maps a morphism 𝑓 : 𝑋 ⊗ 𝑌 → 𝑍 to a morphism 𝑋 → 𝑌 ⊸ 𝑍. • Each object 𝑛® = (𝑛0, . . . , 𝑛𝑘−1) in CPM is a ret… view at source ↗
Figure 9
Figure 9. Figure 9: Syntax of QIFUNITARY. The table shows the differences from QIF (red: deleted, blue: added). We can prove that the SWITCH term does actually define the quantum SWITCH. Theorem 5.2. The categorical semantics of SWITCH coincides with the quantum SWITCH. ⋄ The fact that we can define a natural semantics without making any arbitrary choices demon￾strates that there is no remaining ambiguity and that the corresp… view at source ↗
Figure 10
Figure 10. Figure 10: Selected typing rules for QIFUNITARY. meas ⇝ 𝜆𝑥qbit . let𝑦 ⊗ 𝑧 = CX(𝑥 ⊗ 𝛼) in (𝜉 ≔ 𝑧;𝑦) |1⟩ ⇝ 𝛼 true ⇝ 𝛼 not ⇝ X 𝑀 ⇝ 𝑀 ′ @ ( ®𝛼, ®𝜉) 𝑁𝑖 ⇝ 𝑁 ′ 𝑖 @ ( ®𝛽𝑖 , ®𝜁𝑖) | ®𝛽1 | − | ®𝜁1 | = | ®𝛽2 | − | ®𝜁2 | = | ®𝜂| − |®𝛾 | if 𝑀 then 𝑁1 else 𝑁2 ⇝ let 𝑥 ⊗ 𝑦 = [PITH_FULL_IMAGE:figures/full_fig_p020_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Selected rules for syntactic dilation for terms, types and non-linear contexts. [PITH_FULL_IMAGE:figures/full_fig_p020_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Evaluation contexts of QIFUNITARY. Here, 𝑐 is an assignment of 0 or 1 to a finite set of input channels 𝛼®. Theorem 6.1 (Type preservation for Syntactic Dilation). Assume Γ ⇝ bΓ, Δ ⇝ Δ ′ and 𝐴 ⇝ 𝐴 ′ . Then, for any term Γ; Δ ⊢CPM 𝑀 : 𝐴 in Qif, there exists a QifUnitary term 𝑀′ and ( ®𝛼, ®𝜉) such that 𝑀 ⇝ 𝑀′ and bΓ; Δ ′ ⊢ 𝑀′ : 𝐴 ′ @ ( ®𝛼, ®𝜉). ⋄ Remark 6.2. We can define translations into QifUnitary from t… view at source ↗
Figure 13
Figure 13. Figure 13: Selected reduction rules for QIFUNITARY. We implicitly assume a well-typed definition D. The state 𝛼® ↦→ |𝜑⟩ is omitted for rules that does not change it. Here 𝐶𝑐𝑈𝛼® denotes the unitary 𝑈 applied to qubits 𝛼® controlled by 𝑐. For a permutation 𝜎 : {1, . . . ,𝑚} → {1, . . . ,𝑚}, ⌈𝜎⌉ denotes the permutation unitary, i.e., it maps |𝑖1 · · ·𝑖𝑚⟩ to [PITH_FULL_IMAGE:figures/full_fig_p022_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Visualisation of syntactic dilation in a string diagram [PITH_FULL_IMAGE:figures/full_fig_p023_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: A toy example in QIF. originally proposed in Ying et al. [2012], also employs a unitary operator 𝑉 that generates an entangled state, whilst respecting the norm of the Kraus operator. In Ying et al. [2014], they introduced generalised semantics with arbitral choice of coefficients, whose degree of freedom corresponds to the freedom of the choice of 𝑉 ; see Appendix E. Quantum Conditional on Pure Quantum C… view at source ↗
Figure 16
Figure 16. Figure 16: Exhaustive typing rules for QIFUNITARY. The set of input channels 𝛼® and ®𝛽, or the output channels ®𝜉 and ®𝜁 are disjoint. B Definition of Language B.1 Exhaustive definitions The complete collection of typing rules for QifUnitary appears in [PITH_FULL_IMAGE:figures/full_fig_p031_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Exhaustive rules for syntactic dilation. [PITH_FULL_IMAGE:figures/full_fig_p032_17.png] view at source ↗
Figure 19
Figure 19. Figure 19: Exhaustive rules for small step semantics for Q [PITH_FULL_IMAGE:figures/full_fig_p033_19.png] view at source ↗
Figure 20
Figure 20. Figure 20: Additional rules for QIF with divergence. (Left): new syntax, (Middle): new typing rule, (Right): its categorical semantics. Output test channels 𝜅, 𝜆, 𝜇, . . . Terms 𝑀, 𝑁 F · · · | (𝜅 ≔ 𝑀); 𝑁 Type Judgements bΓ; Δ ⊢ 𝑀 : 𝐴 @ ( ®𝛼, ®𝜉, 𝜅®) bΓ; Δ ⊢ 𝑀 : qbit @ ( ®𝛼, ®𝜉, ®𝜆) bΓ; Δ ′ ⊢ 𝑁 : 𝐴 @ ( ®𝛽, ®𝜁 , 𝜇®) bΓ; Δ, Δ ′ ⊢ (𝜅 ≔ 𝑀); 𝑁 : 𝐴 @ ( ®𝛼 ®𝛽, ®𝜉 ®𝜁 , 𝜅 ®𝜆𝜇®) abort ⇝ (𝜅 ≔ 𝛼); () LbΓ; Δ ⊢ 𝑀 : 𝐴 @ 𝛼, ® ®𝜉, 𝜅®… view at source ↗
Figure 21
Figure 21. Figure 21: Additional rules for QIFUNITARY extended with output test channels. Theorem C.5 (Progress). For each configuration 𝐶 := ( ®𝛼 ↦→ |𝜓⟩, 𝑀) such that bΓ; ⊢ 𝑀 : 𝐴 @ ( ®𝛽, ®𝜉) and definitions D : Γ, there exists a configuration 𝐶 ′ such that 𝐶 −→D 𝐶 ′ , or 𝑀 is of the form ( ®𝜉 ≔ 𝛼®);𝑉 . ⋄ Theorem C.6 (Termination). There is no infinite sequence of −→D reductions, and it terminates with the normal form ( ®𝜉 ≔ 𝛼… view at source ↗
Figure 22
Figure 22. Figure 22: Second projection to CPM of the categorical semantics of QIF in 𝑇 (A). Let 𝑐𝐴 = {(𝑥𝐴, 𝑠𝐴 ◦ 𝑥𝐴) | 𝑥𝐴 ∈ CPM(𝐼, 𝑛®)} and 𝑐𝐵 = {(𝑥𝐵, 𝑠𝐴 ◦ 𝑥𝐵) | 𝑥𝐵 ∈ CPM(𝐼,𝑚®)} for some objects 𝐴 and 𝐵. Then (𝑦, 𝑦′ ) ∈ 𝑐 ∗ 𝐴⊗𝐵 if and only if 𝑦 ◦ (𝑥𝐴 ⊗ 𝑥𝐵) = 𝑦 ′ ◦ 𝑠𝐴⊗𝐵 ◦ (𝑥𝐴 ⊗ 𝑥𝐵). Since 𝑥𝐴 ⊗ 𝑥𝐵 are jointly epic in CPM, 𝑦 = 𝑦 ′ ◦ 𝑠. Therefore,𝑐 ∗ 𝐴⊗𝐵 = {(𝑦 ′ ◦ 𝑠𝐴, 𝑦′ ) | 𝑦 ′ : ( Í 𝑛® ⊗ Í 𝑚®) → 𝐼 }. Since bool and qbit satisfy … view at source ↗
Figure 23
Figure 23. Figure 23: Syntax and derivation rules of VAC = Í 𝑖∈𝐼 Í 𝑗 ∈𝐽 𝜄  |1⟩⟨1| ⊗ (𝑉𝑖 ◦𝑊𝑗) + |0⟩⟨0| ⊗ (𝑊𝑗 ◦ 𝑉𝑖)  . This is the same as the definition of the quantum SWITCH [Chiribella et al. 2013], as expected. □ D Vacuum Extensions and the Ill-Definedness Issue Barsse et al. [2026] also defined a programming language in which arbitrary quantum channels may appear under quantum control. Their language has classical recursi… view at source ↗
Figure 24
Figure 24. Figure 24: Categorical semantics of VAC in CQC 𝐾 : C 𝑛 −→ C 𝑚 is a linear map such that the following map Mat𝑛+1 (C) −→ Mat𝑚+1 (C)  𝜌 𝑣 𝑤 † 𝛼  ↦−→  𝐹 (𝜌) 𝐾𝑣 𝑤 †𝐾 † 𝛼  defines another completely positive trace preserving map. The composition is defined component￾wise, i.e., (𝐺, 𝐿) ◦ (𝐹, 𝐾) = (𝐺𝐹, 𝐿𝐾). ⋄ The semantics of qif is defined via the following vacuum-control operation, which makes use of the linear maps … view at source ↗
Figure 25
Figure 25. Figure 25: Kraus semantics of VAC the end. In particular, a channel represented by Kraus operators {𝐾𝑖 }𝑖∈𝐼 admits such a purification in which, if the auxiliary qubits are measured in the computational basis rather than discarded, the possible outcomes are {𝑜𝑖 }𝑖∈𝐼 and the branch with outcome 𝑜𝑖 implements 𝐾𝑖 . Since the Kraus semantics of Vac selects one Kraus operator 𝐾0 from the Kraus decomposition {𝐾𝑖 } 𝑛 𝑖=0 ,… view at source ↗
Figure 26
Figure 26. Figure 26: Syntactic dilation for VAC Theorem D.4. The syntactic dilation preserves the semantics. That is, if J𝑆K = (𝐹, 𝐾) and 𝑆 ⇝ 𝑀, then L𝑀M = 𝐹 . Moreover, 𝐾 can be recovered as follows: 𝐾 = (idΓ ′ ⊗ ⟨1| ®𝜉 ) ◦ J𝑀K ◦ (idΓ ⊗ |1⟩𝛼® ). Proof. By induction on the structure of 𝑆. The only non-trivial case is qif. Let {|𝑆1 |} = {𝐾0, . . . , 𝐾𝑛}, {|𝑆2 |} = {𝐿0, . . . , 𝐿𝑛} and let qif 𝑞 then 𝑆1 else 𝑆2  ⇝ 𝑀 @ ( ®𝛼1𝛼®2… view at source ↗
Figure 27
Figure 27. Figure 27: Syntax of QUGCL’. chooses an arbitrary unitary 𝑈 . We show that this freedom of choice coincides with the freedom of choice in the generalized semantics. More concretely, we establish a two-way correspondence between these choices: for every choice of coefficients in QuGCL’, a suitable choice of 𝑈 yields a semantics-preserving translation into QifUnitary; conversely, every choice of 𝑈 determines coefficie… view at source ↗
Figure 28
Figure 28. Figure 28: Syntactic dilation from QUGCL’ to QIFUNITARY. TabortU∅ = 0, T𝑈 [®𝑞]U∅ = 𝑈𝑞® ⊗ id, Tqif 𝑞 then 𝑆1 else 𝑆2U𝑓 ⊔𝑔 = 𝛼𝑆1,𝑓 |0⟩⟨0| ⊗ T𝑆2U𝑔 + 𝛼𝑆2,𝑔 |1⟩⟨1| ⊗ T𝑆1U𝑓 , Tif(𝑥 ← meas(𝑞)) then 𝑆1 else 𝑆2U(𝑥↦→𝑖)⊔𝑓 = |𝑖⟩⟨𝑖| ⊗ T𝑆𝑖U𝑓 where the coefficients 𝛼𝑆𝑖 ,𝑓 are any complex numbers satisfying Í 𝑓 ∈Δ𝑆1 |𝛼𝑆1,𝑓 | 2 = Í 𝑔∈Δ𝑆2 |𝛼𝑆2,𝑔 | 2 = 1. In the canonical semantics of Ying [2016] these coefficients are instantiated as… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

2 extracted references · 1 linked inside Pith

  1. [2]

    implements

    has the type qbit⊗𝐴 ′ @(®𝛼®𝛽1,®𝜉®𝜉1) inQifUnitary. □ C.3 Proof of Semantic Preservation of Syntactic Dilation For the proof, we define another category𝑇(A) . We first define a compact closed categoryA, and obtain𝑇(A)usingfocussed orthogonalityby Hyland and Schalk [2003]. Definition C.14.The category A consists of the following: An object ofA is a sequence...

    2003

  2. [2024]

    https://doi.org/10.48550/ARXIV.2409.18420 Hlér Kristjánsson, Giulio Chiribella, Sina Salek, Daniel Ebler, and Matthew Wilson

    Exponential separation in quantum query complexity of the quantum switch with respect to simulations with standard quantum circuits. https://doi.org/10.48550/ARXIV.2409.18420 Hlér Kristjánsson, Giulio Chiribella, Sina Salek, Daniel Ebler, and Matthew Wilson. 2020. Resource theories of communication. New Journal of Physics22, 7 (jul 2020), 073014. https://...

    Pith/arXiv arXiv doi:10.48550/arxiv.2409.18420 2020