Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 definitions 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 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 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

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeAug 26th 2022
   • PermaLink
   Author: Urs
   Format: MarkdownItexI am after a triviality, just wondering if it has an established name: $\,$ Under the [[computational trilogy]] we may essentially think of any morphism as representing a computation. But in the practice of computation, we care about "programmable computations", where a collection of potential computation steps is equipped with names, such that we may *call* them by their names, sequentially. Clearly, this translates to the notion of fibration (type family): The paths in the base are the names of computation steps, and to call them means to invoke the type transport along them. $\,$ In the context of classical computation this perspective might not appear to be overly compelling, but it seems to me that making this explicit (trivial as it may be) is necessary to get to the bottom of formalizing what quantum computation is about: in which case the fibration is a dependent linear type, the base being the "classical control" of/on a collection of "quantum gates". For example, what people really mean by "having topological quantum gates" is a linear type family over the delooping of a braid group. That's my motivating example, but I'd like to take a step back and see this as a special case of a more general paradigm. $\,$ In any case, has this perspective been made explicit anywhere? Maybe it's too trivial to carry it's own name.

   I am after a triviality, just wondering if it has an established name:

   $\,$

   Under the computational trilogy we may essentially think of any morphism as representing a computation.

   But in the practice of computation, we care about “programmable computations”, where a collection of potential computation steps is equipped with names, such that we may call them by their names, sequentially.

   Clearly, this translates to the notion of fibration (type family): The paths in the base are the names of computation steps, and to call them means to invoke the type transport along them.

   $\,$

   In the context of classical computation this perspective might not appear to be overly compelling, but it seems to me that making this explicit (trivial as it may be) is necessary to get to the bottom of formalizing what quantum computation is about: in which case the fibration is a dependent linear type, the base being the “classical control” of/on a collection of “quantum gates”.

   For example, what people really mean by “having topological quantum gates” is a linear type family over the delooping of a braid group. That’s my motivating example, but I’d like to take a step back and see this as a special case of a more general paradigm.

   $\,$

   In any case, has this perspective been made explicit anywhere? Maybe it’s too trivial to carry it’s own name.

2. • CommentRowNumber2.
   • CommentAuthormaxsnew
   • CommentTimeAug 26th 2022
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexCould you expand a little on what exactly you mean by > where a collection of potential computation steps is equipped with names, such that we may call them by their names, sequentially.

   Could you expand a little on what exactly you mean by

   where a collection of potential computation steps is equipped with names, such that we may call them by their names, sequentially.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeAug 26th 2022
   • PermaLink
   Author: Urs
   Format: MarkdownItexMaybe best to show a simple example of what I have in mind. The following is the type family which represents a computer whose memory consists of a single bit, and whose only instruction is a NOT gate: $$ \array{ P &\xrightarrow{\phantom{---}}& Set^{\ast/} \\ \Bigg\downarrow &{}^{{}_{(pb)}}& \Bigg\downarrow \\ \;\;\;\; \mathclap{ \mathbf{B} F \Big( \big\{ NOT \big\} \Big) } \;\;\;\; &\;\;\;\;\xrightarrow{\phantom{--}}& Set \\ \ast &\mapsto& \{0,1\} \mathrlap{ \;\;\; \color{blue} \text{state space} } \\ \mathllap{ {}^{ \mathllap{ \color{green} \text{gate name} \;\;\; } NOT } } \Big\downarrow && \Big\downarrow \mathrlap{{}^{ \left[ \array{ 0 &\mapsto& 1 \\ 1 &\mapsto& 0 } \right] \mathrlap{ \;\;\; \color{green} \text{gate execution} } }} \\ \ast &\mapsto& \{0,1\} \mathrlap{ \;\;\; \color{blue} \text{state space} } } $$ Here $F(-)$ denotes the free monoid/group and $\mathbf{B}(-)$ denotes forming delooping.

   Maybe best to show a simple example of what I have in mind.

   The following is the type family which represents a computer whose memory consists of a single bit, and whose only instruction is a NOT gate:

   $$\array{ P &\xrightarrow{\phantom{---}}& Set^{\ast/} \\ \Bigg\downarrow &{}^{{}_{(pb)}}& \Bigg\downarrow \\ \;\;\;\; \mathclap{ \mathbf{B} F \Big( \big\{ NOT \big\} \Big) } \;\;\;\; &\;\;\;\;\xrightarrow{\phantom{--}}& Set \\ \ast &\mapsto& \{0,1\} \mathrlap{ \;\;\; \color{blue} \text{state space} } \\ \mathllap{ {}^{ \mathllap{ \color{green} \text{gate name} \;\;\; } NOT } } \Big\downarrow && \Big\downarrow \mathrlap{{}^{ \left[ \array{ 0 &\mapsto& 1 \\ 1 &\mapsto& 0 } \right] \mathrlap{ \;\;\; \color{green} \text{gate execution} } }} \\ \ast &\mapsto& \{0,1\} \mathrlap{ \;\;\; \color{blue} \text{state space} } }$$

   Here $F(-)$ denotes the free monoid/group and $\mathbf{B}(-)$ denotes forming delooping.

4. • CommentRowNumber4.
   • CommentAuthormaxsnew
   • CommentTimeAug 26th 2022
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexKind of sounds like a [[transition system]] to me, but I'm not sure if that would generalize beyond this example

   Kind of sounds like a transition system to me, but I’m not sure if that would generalize beyond this example

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeAug 26th 2022
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, I see. True, every fibration of sets over the delooping of a free monoid defines a "transition system". Maybe I should chase references on transition systems. It would be strange if category theorists hadn't thought of adjusting the definition of transition systems to the functors that they clearly want to be. Meanwhile, as you may have seen, I have found a semi-technical/semi-philosophical text that, for what it's worth, comes fairly close to saying that computation is path lifting/transport: [here](https://ncatlab.org/nlab/show/computation#vanLeeuwenWiedermann17).

   Thanks, I see. True, every fibration of sets over the delooping of a free monoid defines a “transition system”.

   Maybe I should chase references on transition systems. It would be strange if category theorists hadn’t thought of adjusting the definition of transition systems to the functors that they clearly want to be.

   Meanwhile, as you may have seen, I have found a semi-technical/semi-philosophical text that, for what it’s worth, comes fairly close to saying that computation is path lifting/transport: here.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeAug 26th 2022
   • PermaLink
   Author: Urs
   Format: MarkdownItexSomething like a translation from transition systems to path lifting/transport happens around [pp. 10-12](https://www.brics.dk/RS/94/7/BRICS-RS-94-7.pdf#page=12) of [Joyal, Nielsen & Wisnkel 1994](https://ncatlab.org/nlab/show/transition+system#JoyalNielsenWisnkel94) -- though it seems somewhat baroque.

   Something like a translation from transition systems to path lifting/transport happens around pp. 10-12 of Joyal, Nielsen & Wisnkel 1994 – though it seems somewhat baroque.

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeAug 27th 2022
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexWhat comes to mind is [[type refinement]]. Our page has a limited view I think. From a [course](http://noamz.org/mgs2019/) by Noam Zeilberger: > taking as a guiding principle the naive idea of viewing type refinement systems categorically as "forgetful" functors from a category of typing derivations to a category of terms. A bifibrational picture as we discussed [here](https://nforum.ncatlab.org/discussion/7042/extrinsicintrinsic-currychurch-distinctions/?Focus=69626#Comment_69626).

   What comes to mind is type refinement. Our page has a limited view I think.

   From a course by Noam Zeilberger:

   taking as a guiding principle the naive idea of viewing type refinement systems categorically as “forgetful” functors from a category of typing derivations to a category of terms.

   A bifibrational picture as we discussed here.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeAug 27th 2022
   • (edited Aug 27th 2022)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks for the pointer -- but I have to admit that I am not sure what to make of it. What i have in mind is not using any new concepts, just the plain foundations of dependent type theory. All I am saying is: Look, if we say that morphisms/terms-in-context are computations, then we should say that path-lifted morphisms/transported terms are programmed computations (executed programs). I think this is clear/obvious -- or it will be once you think about it for a minute. What I am really wondering is if anyone has drawn attention to this perspective. In fact, [van Leeuwen & Wiedermann 2017](https://ncatlab.org/nlab/show/computation#vanLeeuwenWiedermann17) essentially say this, only that they don't have type-theoretic language available to them (it seems) and the point-set topology which the do invoke falls slightly short of what one would get under type-theoretic semantics in topological spaces -- but it's close enough that one recognizes the idea. I have created a tikz graphics that illustrates the point at a glance -- temporarily here: * [pdf](https://www.dropbox.com/s/h3xwdfslvpqzj73/what-is-computation.pdf?dl=0) (3 pages, overlay) $\,$

   Thanks for the pointer – but I have to admit that I am not sure what to make of it.

   What i have in mind is not using any new concepts, just the plain foundations of dependent type theory. All I am saying is: Look, if we say that morphisms/terms-in-context are computations, then we should say that path-lifted morphisms/transported terms are programmed computations (executed programs).

   I think this is clear/obvious – or it will be once you think about it for a minute. What I am really wondering is if anyone has drawn attention to this perspective. In fact, van Leeuwen & Wiedermann 2017 essentially say this, only that they don’t have type-theoretic language available to them (it seems) and the point-set topology which the do invoke falls slightly short of what one would get under type-theoretic semantics in topological spaces – but it’s close enough that one recognizes the idea.

   I have created a tikz graphics that illustrates the point at a glance – temporarily here:

   • pdf (3 pages, overlay)

   $\,$

9. • CommentRowNumber9.
   • CommentAuthorDavid_Corfield
   • CommentTimeAug 27th 2022
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexSounds like the kind of question that would get a good answer on Twitter, if addressed e.g. to Jon Sterling and Andrej Bauer.

   Sounds like the kind of question that would get a good answer on Twitter, if addressed e.g. to Jon Sterling and Andrej Bauer.

10. • CommentRowNumber10.
    • CommentAuthorvarkor
    • CommentTimeAug 27th 2022
    • PermaLink
    Author: varkor
    Format: MarkdownItexI'm not quite sure if this is what you're looking for, but it's worth taking a look at [[rewriting]], which sounds at least related to your question.

    I’m not quite sure if this is what you’re looking for, but it’s worth taking a look at rewriting, which sounds at least related to your question.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeAug 29th 2022
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhat about if we change the fibration to a (pseudo)functor? Then this looks to me like the standard situation of categorical semantics, where we have a [[syntactic category]] $Syn$ whose morphisms are "names" for computation-functions, and a semantics functor $Sem : Syn \to Set$ that interprets each such name by an actual function that "performs" the described computation.

    What about if we change the fibration to a (pseudo)functor? Then this looks to me like the standard situation of categorical semantics, where we have a syntactic category $Syn$ whose morphisms are “names” for computation-functions, and a semantics functor $Sem : Syn \to Set$ that interprets each such name by an actual function that “performs” the described computation.

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeAug 29th 2022
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes, that's the picture! I'd like to consider this *internal* to a type theory since I am after (much as van Leeuwen & Wiedermann [were](https://ncatlab.org/nlab/show/computation#ReferencesConceptualizationViaPathLifting)) including "continuous programs", such as the paths in configuration spaces that serve as gates for quantum topological quantum computation; but if there are texts that speak of external semantics functors as encoding computation, I'd be interested. For instance, a common question is whether a set of instructions/gates is "universal" for a prescribed notion of computation, and in this picture this means equivalently that the semantics functor is full. That's the kind of triviality that category/type theorists could be expected to have dwelled on. At least that's what it means classically. For quantum computation and using the internal picture, the usual notion of universality (as in [FLW00](https://ncatlab.org/nlab/show/quantum+computation#FreedmanLarsenWang00)) means that the semantics functor has *dense image* on morphisms. This can neatly expressed internal to a suitable modal type theory and is no longer quite as trivial.

    Yes, that’s the picture!

    I’d like to consider this internal to a type theory since I am after (much as van Leeuwen & Wiedermann were) including “continuous programs”, such as the paths in configuration spaces that serve as gates for quantum topological quantum computation; but if there are texts that speak of external semantics functors as encoding computation, I’d be interested.

    For instance, a common question is whether a set of instructions/gates is “universal” for a prescribed notion of computation, and in this picture this means equivalently that the semantics functor is full. That’s the kind of triviality that category/type theorists could be expected to have dwelled on.

    At least that’s what it means classically. For quantum computation and using the internal picture, the usual notion of universality (as in FLW00) means that the semantics functor has dense image on morphisms. This can neatly expressed internal to a suitable modal type theory and is no longer quite as trivial.