Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Am starting a write-up (here) of how (programming languages for) quantum circuits “with classical control and/by measurement” have a rather natural and elegant formulation within the linear homotopy type theory of Riley 2022.
Aspects of this have a resemblance to some constructions considered in/with “Quipper”, but maybe it helps clarify some issues there, such as that of “dynamic lifting”.
The entry is currently written without TOC and without Idea-section etc, but rather as a single top-level section that could be !include
-ed into relevant entries (such as at quantum circuit and at dependent linear type theory). But for the moment I haven’t included it anywhere yet, and maybe I’ll eventually change my mind about it.
I have been preparing slides for a brief presentation of these ideas, tomorrow at QTML22.
An early and incomplete version of the slides is now here.
All comments are welcome. Hope to finalize these slides tomorrow morning.
Full-blow -> full-blown
Thanks. Will fix this in a moment…
On 77/112 you have product as left adjoint to context extension as left adjoint to coproduct. Surely the other way.
Thanks, I think I had spotted these and fixed. Hopefully. Latest version here. Going live now. Will fully polish up the overlay on the last slides later.
Oh, now I see which typo you meant. Luckily the organizers mixed up the time zone. Am fixing it now…
Given the subsumption of traditional quantum information formalisms within dLHoTT, I wonder if there’s something to be done regarding categorical compositional distributional semantics. Seemed odd to me not to embrace that part of natural language which is evidently dependently typed.
I don’t expect that I’ll be digging into the claimed relation to natural language formalization anytime soon.
On the dependent typing: The Oxford community has come ever so close to incorporating this, but maybe falling short (as far as I oversee the literature): Namely the category of (co)algebras over their “classical structures” Frobenius monad is that of dependent linear types, and the corresponding monadic functor is the dependent product-functor. That’s the way to recover dependent linear types if one didn’t start with them. Lem 5.61 in Heunen&Vicary’s book is beginning to see this, minus any monadic language.
Sounds interesting. Always good to see how something important may be recovered naturally.
Sounds interesting.
We have been talking about it, meanwhile it’s recorded as this Prop. at quantum reader monad.
Oh, I see. Yes.
I have added a fair bit of detail to the section “Quantum Programming Language” (here):
First a fairly comprehensive declaration of the (pseudo-)code sugaring of modal dependent linear TT that makes it a quantum programming language,
then followed by more examples (more basic examples and then the quantum bit flip code in addition the the teleportation protocol).
1 to 15 of 15