Not signed in (Sign In)

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 beauty book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory 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 homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory 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 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 stack 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 30 of 30

  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

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 27th 2023

    There’s a typo inside a diagram, so one I can’t fix.

    In the diagram numbered (3), there’s ∘ Bℋ\circ_B \mathcal{H} which should be ∘ B𝒦\circ_B \mathcal{K}, above “read state”.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeFeb 27th 2023

    Thanks! Fixed now (here).

    This is timely: With Topological Quantum Gates in HoTT done, now I just have to get two referee reports out of the way, and then to finally pick up the story of quantum programming in linear HoTT here.

    diff, v45, current

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 27th 2023

    I’m looking forward to discussing this passage in QS

    Besides these technical properties, the logical language QS is curiously satisfying on quantum-philosophical grounds: For example, the internal language-construct in QS for quantum measurement via the modal logic of necessity is verbatim the same as for classical measurement, only now applied to (dependent) linear types where it happens to imply the collapse of the wavefunction in the categorical semantics. But in the internal logic this effect is just standard conditioning of expectations. In this sense the notorious “measurement problem” of quantum physics disappears when we speak proper QS. (This is analogous to what happens internal to proper quantum probability theory, see there.) Moreover, the deferred measurement principle verified in QS implies that even this collapse of the wavefunction in subsystems may be arbitrarily postponed, by observers who have access to the system at large (the “bath”).

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeFeb 28th 2023

    What else to say, though? :-)

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 28th 2023

    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.

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeFeb 28th 2023
    • (edited Feb 28th 2023)

    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.

    • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 2nd 2023

    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.

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeMar 2nd 2023
    • (edited Mar 2nd 2023)

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

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 2nd 2023

    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∈Mod(V) V \in Mod(V); A 1:=∑ i 1(i 2) *A 1A_1 := \sum_{i_1} (i_2)^{\ast}A_1, and more generally in Example 4.15, A 1A_1 and A 2A_2 mixed up; a bite more

    • CommentRowNumber25.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 12th 2023

    Perhaps an obvious point, but in the nonlinear case, base change for b:1→Bb: 1 \to B,

    b *:H/B→Hb^{\ast}: \mathbf{H}/B \to \mathbf{H}

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

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeJul 12th 2023
    • (edited Jul 12th 2023)

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

    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∈Bitb \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 bb.

    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 bb 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⟶*B \longrightarrow \ast, one should, if only for some kind of symmetry, discuss also the situation of base change along *⟶B\ast \longrightarrow B. Something to think about more.

    • CommentRowNumber27.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 12th 2023

    Thanks.

    I could share this privately, if you are interested.

    Yes, that sounds interesting.

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeJul 12th 2023

    Okay, have sent it.

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeAug 6th 2023

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

    diff, v47, current

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeAug 15th 2023
    • (edited Aug 16th 2023)

    [deleted, sorry for the noise]

1 to 30 of 30

  1.