nLab Sandbox

It occurs to me that there is the following interesting application of the dependent-type-theoretic formulation of the possibility/necessity modalities that, years ago, we wrote down in this entry (here).

Namely, to point out that when applied to linear dependent types, then the counit of the necessity modality as defined here embodies what in quantum information theory is a “measurement gate”.

Like so:

Let \mathscr{H} be a linear type in the empty context, which is to be regarded as the Hlbert space of states that some quantum protocol is operating on. Think of the quantum teleportation-protocol as a good illustration in the following.

Now consider that in the process of the protocol, a measurement(-gate) is to be performed. Unwinding what the traditional song-and-dance boils down to, this means that

  1. a set (a non-linear type) RR of measurement results is chosen.

  2. a direct sum-decomposition

    r:R r \mathscr{H} \simeq \underset{r : R}{\oplus} \mathscr{H}_r

    for an indexed set of direct summands =(r r)\mathscr{H}_\bullet = (r \mapsto \mathscr{H}_r)

    is chosen (with r\mathscr{H}_r consisting of those quantum states that one may find the system to have “collapsed” to after the result rr has been measured)

  3. a quantum circuit is drawn whose gates may depend on r:Rr : R (in the quantum teleportation protocol as shown here, this dependency is through the variable called σ\sigma there)

As a result, quantum circuits that include measurement gates are actually fiberwise morphisms in a category of bundles of Hilbert spaces over finite sets of (potential) classical outcomes.

Traditional literature never puts it this way (some texts on Quipper get close, but I haven’t seen it stated real clearly there, either), but it is clear from inspection that this is what happens.

Now one should ask: In this dependent-linear-typed picture of quantum information protocols: What is a measurement gate itself?

To see this, observe that for a finite index set of results RR, the direct sum of result Hilbert space is equivalently their categorical product, hence their limit, hence their right base change along R*R \to \ast:

r:R r. \mathscr{H} \;\simeq\; \underset{r : R}{\prod} \mathscr{H}_r \,.

To put this into the context of possible measurement results, context-extent it to RR (which I’ll denote by R *R^\ast, if you allow) to get

R *R *r:R r. R^\ast \mathscr{H} \;\simeq\; R^\ast \underset{r : R}{\prod} \mathscr{H}_r \,.

Now the collapse postulate of quantum physics says that if we are in context rr then a measurement operates on quantum states as the linear projection p r: rp_{r} \colon \mathscr{H} \xrightarrow{\;} \mathscr{H}_r on its rrth direct summand.

But, as a linear map dependent on rr, this is just the (R *r:R)(R^\ast \dashv \underset{r : R}{\prod})-counit

R *R *r:R rϵ R^\ast \mathscr{H} \;\simeq\; R^\ast \underset{r : R}{\prod} \mathscr{H}_r \xrightarrow{\phantom{--} \epsilon \phantom{--}} \mathscr{H}_\bullet


So if :=R *r:R\Box \,:=\, R^\ast \circ \underset{r : R}{\prod} denotes the corresponding comonadic modility (“necessarily so in possible worlds RR”), then we discover that a quantum measurement gate with possible outcomes \mathscr{H}_\bullet indexed by RR, understood as an RR-dependent linear map, is the necessity counit

meas: ϵ . meas \;\colon\; \Box \mathscr{H}_\bullet \xrightarrow{\phantom{--} \epsilon \phantom{--}} \mathscr{H}_\bullet \,.

That seems kind of cute.

For example, in the quantum teleportation protocol, this would be Alice’s measurement, and then Bob would go and do r:Rσ r: r rr : R \;\vdash\; \sigma_r : \mathscr{H}_r \xrightarrow{\;\;} \mathscr{H}_r to get

meas σ \Box \mathscr{H}_\bullet \xrightarrow{\phantom{-} meas \phantom{-}} \mathscr{H}_\bullet \xrightarrow{\phantom{-} \sigma_\bullet \phantom{-}} \mathscr{H}_\bullet

As it goes with these Yoneda-like insights, it’s all locally trivial, but this looks like the right picture to make explicit:

Q: What is a quantum measurement gate seen in dependent linearly typed quantum programming languages?

A: The necessity counit on the dependent type of possible outcomes.

Last revised on September 28, 2022 at 08:00:28. See the history of this page for a list of all contributions to it.