Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 12 of 12
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.
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.
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.
Kind of sounds like a transition system to me, but I’m not sure if that would generalize beyond this example
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.
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.
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.
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:
$\,$
Sounds like the kind of question that would get a good answer on Twitter, if addressed e.g. to Jon Sterling and Andrej Bauer.
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.
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.
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.
1 to 12 of 12