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

nLab > Latest Changes: quantum circuits via dependent linear types

Bottom of Page

1 to 15 of 15

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

1 to 15 of 15

  1.  
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)
 
Back to Discussions Top of Page