# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeOct 1st 2022
• (edited Oct 1st 2022)

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.

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeOct 3rd 2022

added also the Kleisli map which is the “Bell state measurement”.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeNov 11th 2022
• (edited Nov 11th 2022)

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.

• CommentRowNumber4.
• CommentAuthorDavidRoberts
• CommentTimeNov 11th 2022

Full-blow -> full-blown

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeNov 12th 2022

Thanks. Will fix this in a moment…

• CommentRowNumber6.
• CommentAuthorDavid_Corfield
• CommentTimeNov 12th 2022

On 77/112 you have product as left adjoint to context extension as left adjoint to coproduct. Surely the other way.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeNov 12th 2022

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.

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeNov 12th 2022

Oh, now I see which typo you meant. Luckily the organizers mixed up the time zone. Am fixing it now…

• CommentRowNumber9.
• CommentAuthorDavid_Corfield
• CommentTimeNov 14th 2022

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.

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeNov 14th 2022

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.

• CommentRowNumber11.
• CommentAuthorDavid_Corfield
• CommentTimeNov 14th 2022

Sounds interesting. Always good to see how something important may be recovered naturally.

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeNov 14th 2022

Sounds interesting.

• CommentRowNumber13.
• CommentAuthorDavid_Corfield
• CommentTimeNov 14th 2022

Oh, I see. Yes.

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeNov 19th 2022

starting a section (here) which develops the actual programming (pseudo-)code for quantum circuits which is obtained by using the various monadic effects constructed in dLTT as discussed in the previous sections.

• CommentRowNumber15.
• CommentAuthorUrs
• CommentTimeNov 23rd 2022

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).