Not signed in (Sign In)

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homology homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory kan lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeOct 3rd 2022

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

    diff, v6, current

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

    We have been talking about it, meanwhile it’s recorded as this Prop. at quantum reader monad.

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

    diff, v36, current

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

    diff, v38, current

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)