Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: applied category theory

Topic: reactive stuff

sarahzrf (Apr 30 2020 at 04:37):

so i was thinking about functional reactive programming & wondering what connections it might have to open dynamical systems, & i remembered having looked at arrow-based FRP, & looked over some old conal posts, & i'm thinking maybe we have something like...

fix a monoidal category $\mathbf M$, and let $\mathcal C$ be an $\mathbf M$-actegory. then define a profunctor $P : \mathcal C \mathrel{⇸} \mathcal C$:

$P(A, B) = \int^{M \in \mathbf M} \mathcal C(M \cdot A, M \cdot B)$

if $\mathbf M$ is symmetric monoidal (braided might be enough), i think we can make $P$ a promonad. write $(M \in \mathbf M, f : M \cdot A \to M \cdot B)$ for a representative of an element of $P(A, B)$; then i think we have $(1, \operatorname{id}_A)$ for identities, and to compose $(M, f : M \cdot A \to M \cdot B)$ with $(N, g : N \cdot B \to N \cdot C)$, do $(N \otimes M, M \cdot g \circ N \cdot f)$ except that's obviously not well-typed, you have to also insert the appropriate symmetries and structural morphisms and whatnot necessary to shuffle things around, but it should work

sarahzrf (Apr 30 2020 at 04:40):

if you specialize this to, say, $\mathbf M = \mathcal C = \mathbf{Set}$ as a cartesian monoidal category acting on itself by ⊗, you get

$P(A, B) = \int^{S \in \mathbf{Set}} \mathbf{Set}(S \times A, S \times B)$

sarahzrf (Apr 30 2020 at 04:40):

...well, that's probably broken due to size issues, but, waves hands furiously

sarahzrf (Apr 30 2020 at 04:40):

something something polymorphism is set theoretic

sarahzrf (Apr 30 2020 at 04:41):

anyway that looks like a locally stateful version of a State monad kleisli arrow to me!

sarahzrf (Apr 30 2020 at 04:43):

but i wonder if you could also pick some $\mathbf M, \mathcal C$ such that this produces a continuous-time kind of reactivity

sarahzrf (Apr 30 2020 at 04:44):

anyway these formulas look really suspiciously familiar to about 5 different things i've seen while reading about tambara stuff, so...

sarahzrf (Apr 30 2020 at 04:44):

@Exequiel Rivas does any of this look familiar to you? :)

sarahzrf (Apr 30 2020 at 04:45):

i did notice that the formula looks almost like the one in the right adjoint to U : Tamb → Prof, except that it's a coend instead of an end

Exequiel Rivas (Apr 30 2020 at 15:14):

@sarahzrf Yes, that looks like the right adjoint. I remember looking at that kind of thing for sort of a dual of the "strong profunctors" story for understanding loop (maybe we talked about this @POPL?). Let $P : \mathcal C \mathrel{⇸} \mathcal C$ be a profunctor with $\mathcal{C}$ being a $\mathbf{M}$-actegory. Then construct a new profunctor $P^{\exists}(A, B) = \int^{M \in \mathbf M} \mathcal P(M \cdot A, M \cdot B)$. I don't remember details (I'll look for notes but they might be permanently lost), but I think we obtain that thing you wrote as ${\mathsf{Hom}_\mathcal{C}}^\exists$?

Exequiel Rivas (Apr 30 2020 at 15:15):

Did you have any concrete model of arrow-based FRP in mind?

sarahzrf (May 01 2020 at 04:15):

not really, sorry

sarahzrf (May 01 2020 at 04:15):

i'm not super knowledgeable about frp, really

sarahzrf (May 01 2020 at 04:16):

i think i have played around a little bit with yampa (or maybe it was netwire...?) before but only briefly

sarahzrf (May 01 2020 at 04:16):

when you say "concrete model", do you mean like an implementation, or like a denotational semantics?

sarahzrf (May 01 2020 at 04:49):

ok i actually read the first thing you wrote & that looks like Hom^∃ for sure

sarahzrf (May 01 2020 at 04:50):

i dont remember hearing about this at popl, but i mean, it's totally possible that you tried to tell me about it and i didnt absorb it :sweat_smile:

sarahzrf (May 01 2020 at 04:51):

is loop not a traced monoidal thing?

sarahzrf (May 01 2020 at 04:59):

orthogonally: i wonder if you could encode a continuous time thing like... $y \in P(1, \mathbb{R})$ by setting $M = \mathbb R$ and defining $y(t, \ast) = (t + dt, t)$ where $dt$ is some fixed infinitesimal—formalize this w/ tangent bundles if u like

sarahzrf (May 01 2020 at 05:00):

i.e.: write down a morphism which computes the infinitesimal step at a given point, & then u get the dynamics by integrating the thing

sarahzrf (May 01 2020 at 05:01):

i guess for "integrating the thing" to be something you can define you need to pick $\mathbf M$ to be something where the objects are spaces along which you can integrate, or something? idk

Jade Master (May 01 2020 at 18:23):

@Zanzi You might be interested in this:) (if this is the Zanzi I am thinking of, if not then sorry)

sarahzrf (May 03 2020 at 02:19):

ok i just worked something out—im pretty sure that this is the string diagram for the free tambara module on P
image.png

sarahzrf (May 03 2020 at 02:20):

...and im pretty sure that this is the string diagram for @Exequiel Rivas's P^∃
image.png

sarahzrf (May 03 2020 at 02:25):

in the first one the 2 circular nodes are $(M, A, B) \mapsto \operatorname{Hom}(M \cdot A, B)$ and $(M, A, B) \mapsto \operatorname{Hom}(A, M \cdot B)$; in the second one they are swapped

sarahzrf (May 03 2020 at 02:29):

is there a nice way of indicating an end in a Prof string diagram? @Mario Román, do you know maybe?

Mario Román (May 03 2020 at 07:17):

sarahzrf said:

ok i just worked something out—im pretty sure that this is the string diagram for the free tambara module on P
image.png

That's right. Putting these two dots is the action on objects of the Pastro-Street monad. I wrote about this here. You can also describe a Tambara module in a nice way and show that they are precisely the algebras for the Pastro-Street monad. Intuitively, if you put an optic around that free Tambara, there is a way of reducing it to just P (associativity and composing along the ⊗). This was meant to be an appendix to the article on open diagrams, but I decided to split it and I want to use it in the future to rewrite Pastro-Street with diagrams.

Mario Román (May 03 2020 at 07:20):

Regarding loops. I think these look similar to the Circ construction of Katis, Sabadini and Walters ("Feedback, trace and-fixed point semantics"); they describe that coend over the core subgroupoid without naming it. You can repeat the trick for every monoidal action, I think that is Exequiel Rivas' dual to strong profunctor. I am using the example of the Circ construction (slightly modified for simplicity) on §5.2 of open diagrams via coends. I also wrote a note with particular case of "initialized feedback" using pointed objects (link). All of these are notes in progress, but I think these are the same ideas.

Mario Román (May 03 2020 at 07:22):

sarahzrf said:

is there a nice way of indicating an end in a Prof string diagram? Mario Román, do you know maybe?

Regarding ends. In general, leaving wires open gives a nat.transf., so that seems the naive way of getting them. I see two ways of writing the end of a profunctor (that are equivalent because Yoneda). One is to do a derivation of P from the wire; which means a nat. transf.

∫ᵤᵥ hom(u,v) → P(u,v) ≅ ∫ᵤ P(u,u)

But that is also an element of Nat(hom,P). So you can explicitly use an evaluation profunctor ev : [Cᵒᵖ×D,Set] × Cᵒᵖ × D → Set to factor the profunctor P into evaluation of some object of [Cᵒᵖ×D,Set] and then draw the natural transformations from hom(-,-). There are other ways to do that (going to Set op, for instance), but these were the most convincing (see also how I did Tambara modules). There is also this note by Simon Willerton http://www.simonwillerton.staff.shef.ac.uk/ftp/TwoTracesBeamerTalk.pdf that describes them (I think, see the slide: Examples of Traces in Monoidal Bicategories).

Mario Román (May 03 2020 at 07:24):

sarahzrf said:

orthogonally: i wonder if you could encode a continuous time thing like... $y \in P(1, \mathbb{R})$ by setting $M = \mathbb R$ and defining $y(t, \ast) = (t + dt, t)$ where $dt$ is some fixed infinitesimal—formalize this w/ tangent bundles if u like

Right? I even started reading the book on synthetic differential geometry to try to make this work. I wrote this for the discrete-time case; but I could not think much more about the continuous. I would bet there is many people here that would know what to do to get continuous feedback from the Circ construction.

Mario Román (May 03 2020 at 07:32):

Screenshot_20200503-103321_Squid~2.jpg

Mario Román (May 03 2020 at 07:35):

The (adapted) Circ construction: circconstruction.jpg. The original one is with Core(C), the generalized one I think is also what you were discussing.

Mario Román (May 03 2020 at 07:37):

This is the proposal for Tambara modules. tambara.jpg

Mario Román (May 03 2020 at 07:39):

And the Pastro-Street monad. pastrostreetmonad.jpg

Mario Román (May 03 2020 at 07:43):

I would be really happy to know if there is a nice way of relating this to reactive programming. (I am not totally sure, but I think Guillaume Boisseau has written about Tambara with trace instead of feedback)

Exequiel Rivas (May 03 2020 at 09:17):

Mario Román said:

Regarding loops. I think these look similar to the Circ construction of Katis, Sabadini and Walters ("Feedback, trace and-fixed point semantics"); they describe that coend over the core subgroupoid without naming it. You can repeat the trick for every monoidal action, I think that is Exequiel Rivas' dual to strong profunctor. I am using the example of the Circ construction (slightly modified for simplicity) on §5.2 of open diagrams via coends. I also wrote a note with particular case of "initialized feedback" using pointed objects (link). All of these are notes in progress, but I think these are the same ideas.

Yes, I saw this kind of structure when working trying to model loop from the arrow type-class. You can define what is a traced profunctor, which is the dual to a strong profunctor, and form a category, let's say $\mathrm{TProf}_\mathcal{C}$. Then you have an forgetful functor forgetting the trace structure $U : \mathrm{TProf}_\mathcal{C} \to \mathrm{Prof}_\mathcal{C}$. This functor has a left adjoint, call it Tambaraco or something, which, when it's composed to $U$ to form a monad, you get that ${-}^\exists$ I was mentioning above.

Exequiel Rivas (May 03 2020 at 09:18):

Then, you could say that the trace for a category $\mathcal{C}$ is an algebra for this monad on $\mathsf{Hom}_\mathcal{C}$. IIRC, you get almost all axioms but one, which is the one that tells you that taking the fixpoint of swap gives you identity.

Exequiel Rivas (May 03 2020 at 09:20):

(I guess that this would be "dual" to say that first (v : p x x) = swap : p (x, x) -> p (x, x))

Exequiel Rivas (May 03 2020 at 09:21):

There were more nice stuff, like the monad you get, and the comonad that you get for strong profunctors distribute.

Mario Román (May 03 2020 at 10:18):

Exequiel Rivas said:

Mario Román said:

Regarding loops. I think these look similar to the Circ construction of Katis, Sabadini and Walters ("Feedback, trace and-fixed point semantics"); they describe that coend over the core subgroupoid without naming it. You can repeat the trick for every monoidal action, I think that is Exequiel Rivas' dual to strong profunctor. I am using the example of the Circ construction (slightly modified for simplicity) on §5.2 of open diagrams via coends. I also wrote a note with particular case of "initialized feedback" using pointed objects (link). All of these are notes in progress, but I think these are the same ideas.

Yes, I saw this kind of structure when working trying to model loop from the arrow type-class. You can define what is a traced profunctor, which is the dual to a strong profunctor, and form a category, let's say $\mathrm{TProf}_\mathcal{C}$. Then you have an forgetful functor forgetting the trace structure $U : \mathrm{TProf}_\mathcal{C} \to \mathrm{Prof}_\mathcal{C}$. This functor has a left adjoint, call it Tambaraco or something, which, when it's composed to $U$ to form a monad, you get that ${-}^\exists$ I was mentioning above.

I see, I think trace without yanking is their definition of feedback, so these seem precisely a generalization. Thank you! :)

Jules Hedges (May 03 2020 at 10:27):

Mario Román said:

sarahzrf said:

orthogonally: i wonder if you could encode a continuous time thing like... $y \in P(1, \mathbb{R})$ by setting $M = \mathbb R$ and defining $y(t, \ast) = (t + dt, t)$ where $dt$ is some fixed infinitesimal—formalize this w/ tangent bundles if u like

Right? I even started reading the book on synthetic differential geometry to try to make this work. I wrote this for the discrete-time case; but I could not think much more about the continuous. I would bet there is many people here that would know what to do to get continuous feedback from the Circ construction.

If you can work this out I'll be very, very happy because I'll be able to get continuous-time games out of it. There's a much more general question hiding here: categorical systems theory seems to be inherently discrete space, and categorical process theory seems to be inherently discrete time (*), and I don't really know where to begin in extending to continuous space and time, with "infinitessimal morphisms"

Jules Hedges (May 03 2020 at 10:27):

*(here I mean roughly whether $\circ$ and $\otimes$ are both spacelike, or whether $\otimes$ is spacelike and $\circ$ is timelike - in optics I think of $\circ$ as timelike)

sarahzrf (May 03 2020 at 14:52):

Mario Román said:

sarahzrf said:

orthogonally: i wonder if you could encode a continuous time thing like... $y \in P(1, \mathbb{R})$ by setting $M = \mathbb R$ and defining $y(t, \ast) = (t + dt, t)$ where $dt$ is some fixed infinitesimal—formalize this w/ tangent bundles if u like

Right? I even started reading the book on synthetic differential geometry to try to make this work. I wrote this for the discrete-time case; but I could not think much more about the continuous. I would bet there is many people here that would know what to do to get continuous feedback from the Circ construction.

omg dude stop having my ideas 1 month early :sob:

sarahzrf (May 03 2020 at 14:52):

ok im gonna need to read that paper later, i have slides to work on aa

Mario Román (May 03 2020 at 18:21):

sarahzrf said:

ok im gonna need to read that paper later, i have slides to work on aa

I admit not to be particularly proud of that note yet; as Jules says, the continuous case is the one that should be nice to get.

sarahzrf (May 05 2020 at 17:30):

...this is faintly reminding me of the one time i managed to get a little bit out of trying to read about how perturbation theory works :eyes:
image.png

sarahzrf (May 05 2020 at 17:35):

i've never learned anywhere near enough physics to actually understand qft but i did manage to glean a concept or two once from an nlab page about like... decomposing the thing you wanna exponentiate into a sum of different contributing parts, and then alternating between integrating along the flows for those parts, and then taking a limit or integral or something as you make the alternation finer

sarahzrf (May 05 2020 at 17:35):

or... maybe i'm conflating it with some formula i saw for the lie group exponential...

sarahzrf (May 05 2020 at 17:35):

@John Baez, do you see any resemblance here? (the screenshot is from p5 of https://arxiv.org/pdf/2003.06214.pdf)

sarahzrf (May 05 2020 at 17:44):

...it also reminds me of the hawaiian earring group, which i think i mentioned in a similar context a day or two ago—but this time im a lot more convinced of its relevance https://wildtopology.wordpress.com/2013/11/23/the-hawaiian-earring/

sarahzrf (May 05 2020 at 17:46):

the hawaiian earring is weird because of the fact that you can sort of do infinitary concatenation in its fundamental group, right

sarahzrf (May 05 2020 at 17:47):

or at the very least, it has loops that go around the circles in it infinitely many times, so you can't build them by finite concatenations of what you'd naïvely expect the generators to be by comparison to an infinite wedge sum

sarahzrf (May 05 2020 at 17:50):

well, if you look at the construction of the group given in that post, topological arguments for correctness of the construction aside, it's basically the same kind of thing as above—take a sequence of free groups F_n to be, intuitively, fundamental groups of the subspace of outermost n circles; connect them with projections F_{n+1} → F_n that throw away any occurrences of the n+1th generator; take the limit

Arthur Parzygnat (May 05 2020 at 17:58):

I can't really comment on the comb business, but I think you're thinking about how physicists derive the path integral from the time evolution equation in quantum mechanics. Check out page 6 of https://arxiv.org/pdf/quant-ph/0004090.pdf for example (this was the first reference I could find, but there are more standard ones as well like Feynman and Hibbs or Nakahara's book).

sarahzrf (May 05 2020 at 17:59):

yeah, "the thing you want to exponentiate" = the hamiltonian iirc

Arthur Parzygnat (May 05 2020 at 17:59):

It's not unrelated to exponentials and Lie group stuff. A similar derivation can be done for parallel transport.

sarahzrf (May 05 2020 at 18:00):

well, isnt the key point about the hamiltonian that time evolution is its exponential?

sarahzrf (May 05 2020 at 18:00):

i dont really know what im talking about, maybe im making a type error :)

John Baez (May 05 2020 at 18:04):

sarahzrf said:

i've never learned anywhere near enough physics to actually understand qft but i did manage to glean a concept or two once from an nlab page about like... decomposing the thing you wanna exponentiate into a sum of different contributing parts, and then alternating between integrating along the flows for those parts, and then taking a limit or integral or something as you make the alternation finer.

or... maybe i'm conflating it with some formula i saw for the lie group exponential...

It sounds like you're talking about the Lie-Trotter formula

$e^{A+B} = \lim_{N \rightarrow \infty} (e^{A/N}e^{B/N})^N$

which is definitely one of the tricks used in quantum field theory, taking the linear operator $A$ to be some simple "free Hamiltonian" and the linear operator $B$ to be "all the extra junk in the Hamiltonian".

John Baez (May 05 2020 at 18:05):

So it's like particles evolve freely for some time steps, then "interact", then evolve freely for a while more, etc.

Arthur Parzygnat (May 05 2020 at 18:05):

Yeah, time evolution is just the exponential if the Hamiltonian is independent of time. If the Hamiltonian depends on time, one uses a time-ordered integral, which is a formula generalizing the usual exponential. It solves a differential equation in a single variable of the form $\frac{dx}{dt}=Ax$ where $A$ is a matrix-valued function of time (and $x$ is a path of vectors in a space of appropriate dimension).

John Baez (May 05 2020 at 18:12):

But the main thing we use to get Feynman diagram expansions is the Dyson series. This is another way to compute $\exp((A+B)t)$, different from the Lie-Trotter formula. The Wikipedia explanation is absolutely wretched because it doesn't really define what $U(t,t_0)$ and $V(t)$ are, the two basic building blocks of this idea. Even worse, it says that it does define $U(t,t_0)$... in terms of two other undefined things. This is what happens if you let physicists take control.

John Baez (May 05 2020 at 18:13):

Alas, I have two hours to do whatever I want now and I don't want to spend it on saving the world from this crappy explanation of a beautiful idea.

Arthur Parzygnat (May 05 2020 at 18:13):

The Lie--Trotter product formula is used when splitting the Hamiltonian into two parts. But before that, one breaks up the interval of time into $n$ steps. They're both used, but generally for different purposes. The time step breaking up is where compositionality comes in $U(T=t_1+\cdots+t_n)=U(t_1)\cdots U(t_n)$, where the $U$ is just notation for the unitary evolution for the system [Blah, one has to be careful about the meaning of $U(t)$ here when the Hamiltonian depends on time... it might be better to write $U([T,0])=U([T,t_n])\cdots U([t_1,0])$.] Meanwhile the Lie--Trotter product formula is used to simplify the resulting expressions. For example, with a Hamitlonian like $H=\alpha p^2\pm\beta V(x)$, where $\alpha$ and $\beta$ are some constants, $p$ is momentum (derivative), and $x$ is position (multiplication operator), and $V$ is a function of $x$ (called a potential), and for a small enough time step, $U([t,0])\approx\exp(Ht)\approx\exp(\alpha p^2t)\exp(\beta V(x) t)$ for small enough $t$.

John Baez (May 05 2020 at 18:14):

Anyway, when you use the Dyson series and draw it diagrammatically you do get diagrams a bit like the one @sarahzrf was showing us, and I'm sure there is a connection.

Arthur Parzygnat (May 05 2020 at 18:14):

Right, I was surprised by the formula as well!

sarahzrf (May 05 2020 at 18:15):

re: hawaiian earring thing—for the hawaiian earring, we're taking a limit over G ← G + G ← G + G + G ← ... with projections down defined by [id, !]; for these combs, we're taking a limit over P₁ ∘ 1 ← P₁ ∘ P₂ ∘ 1 ← P₁ ∘ P₂ ∘ P₃ ∘ 1 ← ... (where im writing composition in diagrammatic order and 1 is the terminal profunctor) with projections down defined by the horizontal composition id ⁎ !

sarahzrf (May 05 2020 at 18:15):

and i should be working on getting my slides to their final form, so i dont have time to listen to a full explanation either :sob:

sarahzrf (May 05 2020 at 18:15):

:thumbs_up:

John Baez (May 05 2020 at 18:19):

WORK!!! :ogre:

sarahzrf (May 05 2020 at 18:19):

/me switches from procrastinating on zulip to procrastinating on twitter

sarahzrf (May 07 2020 at 16:25):

aha right! those are both terminal coalgebra constructions :light_bulb:

sarahzrf (May 07 2020 at 16:26):

oh wait no maybe not for the 2nd one :thinking:

sarahzrf (May 07 2020 at 16:26):

(also, this is conditional on $G + -$ and $P \circ -$ preserving the limits in question, which i don't know whether they do)

sarahzrf (May 07 2020 at 16:58):

oooh the 2nd one should be a terminal coalgebra construction (given the preservation of limits) if the infinite comb in question is the unfolding of a finite diagram w/ feedback, because then you have just the same couple of profunctors repeated over and over :D

sarahzrf (May 07 2020 at 17:38):

ok yeah im definitely seeing that coalgebras and particularly terminal ones are relevant to this kind of thing & the stuff over in "infinitesimal morphisms"

sarahzrf (May 07 2020 at 19:13):

i had a mental image just earlier that i kinda wanna hold on to as a motivation for this kind of thing, of like...

sarahzrf (May 07 2020 at 19:16):

a "section of the covering map ε : R → S¹"—not literally, of course, but some kind of "function" s : S¹ → R whose input must be varied continuously, so that if you take s(p) while varying p, it continues to live in the fiber over p, and eventually you may find that evaluating s(p) again after completing a full circle gives you a different result

sarahzrf (May 07 2020 at 19:17):

well, i could imagine that if there's a way to make this formal that resembles the stuff earlier in this thread, maybe it'd have to be smooth rather than just continuous, but w/e

sarahzrf (May 07 2020 at 22:04):

also OOPS i misquoted that article on what the hawaiian earring group is >.< it's actually a subgroup of the colimit i mentioned (but i wonder if it's the actual colimit in some other category, like maybe a category of normed groups...)