Best wishes to your son!

Regarding the modalities: There would probably be more to say on such interactions, but right now I can’t help with any particular insight along the lines you seem to have in mind.

Just to point out that non-isomorphic measurement bases on a single Hilbert $\mathscr{H}$ space won’t be reflected in maps of the underlying basis sets. Instead, for a single abstract basis set $B$ (characterized just by its cardinality, such as $card(B) = 2$ in the QBit case) its comes from two distinct linear isomorphisms $\mathscr{H} \overset{\sim}{\to} \mathbb{C}[B]$.

]]>Somewhere in Asia?

Yes, my son got married in Singapore, and we extended the trip for a few days to Malaysia.

In quantum systems, we are certainly interested in different measurement bases.

Of course, famously giving rise to the uncertainty principle for position and momentum measurements. But then if the span is $X \leftarrow X \times Z \to Z$, say, for finite sets of measurement outcomes, the ’modalities’ would just be basis change operators, no?

I was led to the morning thought by the ideas of the *free energy principle* program which looks to understand self-sustaining entities in terms of the Markov blankets that screen them off from their environment. There’s a quantum version of this (discussed in that paper I sent to you some days back, perhaps this one: A free energy principle for generic quantum systems) which looks at quantum systems which may be decomposed as two weakly-interacting systems interacting through their shared boundary. Maybe more like the Fong et al. situation.

Morning thought:

Hm, which time zone are you in. Somewhere in Asia?

In quantum systems, we are certainly interested in different measurement bases. For instance the ZX-calculus derives its name from the fact that it models QBit measurements in the “X-basis” and the “Z-basis”.

]]>Morning thought: I wonder if quantumly recapitulating further steps of the path we took with classical modalities might be interesting. So from $W \to \ast$ (all worlds accessible), we looked at the relative version, $W \twoheadrightarrow V$, to capture equivalence classes of accessible possible worlds.

Then we looked at a temporal type theory via $T_1 \rightrightarrows T_0$, time intervals projecting onto their ends, generating the four temporal logic operators.

Finally, we had the thought that any span $A \leftarrow C \to B$ generates two pairs of adjoint operators, operating between types depending on $A$ and types depending on $B$. It turned out that this is what the authors are using in

- Brendan Fong, David Jaz Myers, David I. Spivak,
*Behavioral Mereology: A Modal Logic for Passing Constraints*[arXiv:2101.10490].

Here, when you have a system and two parts of that system, properties of the state of the first may dictate or allow properties of the state of the second. E.g., my left hand being in contact with this table necessitates that my right hand is in this room, and it allows that my right hand touches the bed.

Is there any value in the quantum version of this? The most direct analogue of Fong et al. would seem to be operators acting on properties of the Hilbert spaces of subsystems. But in Quantum Monadology we’re looking for linear dependency over non-linear sets of measurement values.

Hmm, could there be something where a quantum system has two different sets of measurement values, corresponding to different operators, and then one passes between corresponding dependent Hilbert spaces?

]]>Yes. The “quantum monadology” is just a sub-selection of sections of the big file equipped with a new title page (and some mild adjustment of cross-references, where necessary).

We’ll split off further bits in a similar manner, but keep it all unified as a book, eventually.

]]>What happens then to ’QS: Quantum Programming via Linear Homotopy Types’? Is it to be a book in which Quantum Monadology forms a part?

]]>We finally have a polished and essentially finalized version of the monadic sub-aspect of the project, now called:

$\,$

**The Quantum Monadology** (pdf behind this link)

]]>

Abstract.The modern theory of functional programming languages commonly uses monads for encoding computational side-effects and side-contexts beyond bare-bone program logic. Even though quantum computing is intrinsically side-effectful (as in quantum measurement) and context-dependent (as on mixed ancillary states) little of this monadic paradigm has previously been brought to bear on quantum programming languages (the two exceptions being Altenkirch \& Green’s “Quantum IO monad” and Coecke et al.’s “classical structures” Frobenius monad).In this paper, we analyzse the system of (co)monads on categories of parameterized spectra – for the present purpose specialized to set-indexed complex vector spaces – which arise from Grothendieck’s “motivic yoga of operations” given by pushing foward and pulling back over maps. Interpreting an indexed vector space as a collection of alternative possible quantum state spaces parameterized by quantum measurement results, we find that these (co)monads provide a natural and expressive language for functional quantum programming.

We close by indicating a domain-specific quantum programming language (

`QS`

) embeddable into the recently constructed linear homotopy type theory (`LHoTT`

) which naturally expresses these monadic quantum effects in transparent do-notation. Once embedded into`LHoTT`

, this should make for formally verifiable universal quantum programming with classical control, dynamic lifting and topological effects (discussed in the companion article [TQP]).

It’s not easy to know what you mean to say if you conflate “pure mathematics” with “parameterized spectra”!? ;-)

But if you look at *quantum state monad* or that section 4.3, you see that quantum channels get identified with transformations (morphisms) between linear (co)state (co)monads. This concept of monad transformations has not been put to much use in homotopy theory before. So this indeed suggests that there may be room to enrich the theory of parameterized spectra by some new perspective.

But this is idle speculation at this point. First to actually fully nail down the monadic formulation of quantum channels, then we’ll see where to go from there. The next step will drop at *quantum state monad* in 5 minutes…

I was imagining an influx via LHoTT of quantum informational terms via synthetic parameterized homotopy theory to parameterized spectra, but maybe the latter has all the concepts it needs.

]]>But quantum channels have their very origin in pure mathematics! (Stinespring 1955, Arveson 1969), and quantum information/probability has been quite the subject of pure mathematics since the last decades, just as information/probability theory is. It’s a well-matured subject in pure math, with stable definitions and people busy proving theorems.

Incidentally, this thread here does not touch on quantum channels. That’s instead the topic of *quantum state monad*, which gives a first glimpse of a linear modal perspective on quantum information – maybe that’s what you have in mind. This is the (now regrettably slowly evolving) content of section 4.3 in the draft.

It would be fun if the language of quantum information theory (quantum channels, etc.) got transferred over into pure mathematics.

]]>That’s what I expect.

As a first example you might count the new model for parameterized $H\mathbb{K}$-module spectra from the EoS article, which was found by pushing this perspective.

]]>Is there any way in which thinking of linear HoTT as a universal quantum certification language could give rise to a novel idea in parameterized stable homotopy theory?

]]>[deleted, sorry for the noise]

]]>added improved account (here) of the modal/effectful typing of (controlled) quantum (measurement) gates

]]>Okay, have sent it.

]]>Thanks.

I could share this privately, if you are interested.

Yes, that sounds interesting.

]]>Let me suggest that one may think of this as “inspecting what is the case in world $b$”.

Something similar is used for repeat-until-success computing, where a computation is valid (operated as intended) only if some ancillary qbit is afterwards found to have collapsed to a fixed $b \in Bit$. The usual idea is that if not, then one goes back (by “uncomputing”) and repeats the computation, until one finds oneself in a world where the flag qbit did collapse to $b$.

But in a more rudimentary form of this computing paradigm, one could do a single run and if it fails just accept failure and throw an exception, of sorts, by setting the quantum state to 0 (not a unitary process, of course). That would be the monadic effect you describe: If you find yourself in world $b$ then keep the result, in all other worlds flag failure by setting the state to zero.

(Incidentally, I have a tentative note on a monad that expresses actual repeat-until-success computing: but it’s a little subtle since it invokes a fixed-point-operation to produce the infinite tree of possible worlds of all possible repeat-until-success scenarios. I could share this privately, if you are interested.)

But I see the point that with all the attention spent on base change along $B \longrightarrow \ast$, one should, if only for some kind of symmetry, discuss also the situation of base change along $\ast \longrightarrow B$. Something to think about more.

]]>Perhaps an obvious point, but in the nonlinear case, base change for $b: 1 \to B$,

$b^{\ast}: \mathbf{H}/B \to \mathbf{H}$is projecting out the $b$-fibre, so that composing with its right adjoint gives a monad on $\mathbf{H}/B$ which maintains the $b$-fibre and collapses the rest to $\ast$. So like a nonlinear version of quantum measurement.

]]>In another life …

I’d have convinced the philosophy establishment that this is very much what they should be interested in, and have them fund me to explain it to them. From the recent online conference I attended, ’The Heuristic View: Logic, Mathematics, and Science’, the message hasn’t even got through that category can be useful in producing new maths!

Oh yes, Remark 4.21. That’s great.

By the way, if you ever revise the article, I picked up three typos on p. 52

]]>$V \in Mod(V)$; $A_1 := \sum_{i_1} (i_2)^{\ast}A_1$, and more generally in Example 4.15, $A_1$ and $A_2$ mixed up; a bite more

I’d say this is what “Quantization via Linear Homotopy Types” was all about:

To recall, with Joost Nuiten I had cleaned up the cohomological formulation of geometric quantization (later sec 5.2 in his thesis, pp. 104) to the extent that it could be formulated as the categorical semantics of what ought to be a construction in linear homotopy type theory (LHoTT) — the latter being the “integral transform” in LHoTT (Def. 4.18, p. 53) that “Quantization via Linear Homotopy Types” revolves around (I guess it revolves so much that people lose sight of the pivot of the revolution… In another life I would rewrite it more concisely to the point).

]]>Does linear HoTT pick up anything of what you say in #21? There was that idea of a “symplectic semantics” for (a fragment of) linear logic.

]]>That quote (“It could even be argued…”, cf. GoogleBooks) starts our reminding me of the “geometrical formulation of quantum mechanics” (really: “symplectic formulation”), but it ends apparently referring to geometric quantization, which is more about “deforming” or “prequantizing” the symplectic structure to something that is no longer (just) a symplectic structure.

I would then go a little further and observe that symplectic structure, in turn, is just a shadow of (prequantum) line bundles and that the real point here is that quantization in broad generality is about forming spaces of sections of higher line bundles.

One cool thing I want to write up my scattered notes on is how Hilbert space structure arises from this abstract perspective: Remarkably, it’s when the “higher lines” are KR-lines that hermitian inner product structure appears on the corresponding quantum states. This is one of those things that sound completely outlandish once you look at it and see that it follows by elementary inspection.

]]>I’ve picked up enough from you of the ’let the maths do the talking’ idea to end a recent article with

Perhaps the answer to Friedman’s puzzle as to why quantum physics wasn’t integrated into philosophy properly is simply that neither the mathematics nor logic were ready.

Still, there’s the work to be done (which you are doing) “translating” the formalism into a precise natural language, as with the Gell-Man principle, “The possible is necessary and hence actualized”.

Then I’m also wondering if *this* rapprochement between the quantum and classical can be related to *that* pointed to by Catren and Anel in *New Spaces in Physics*:

It could even be argued that symplectic geometry opened the path to the comprehension of quantum mechanics as a continuous extension of classical mechanics and no longer as a sort of “new paradigm” discontinuously separated from the classical one

(something about category-theoretic ’points’ being Lagrangian submanifolds) which chimes with things we once discussed about the prequantum present in classical physics.

]]>