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: systems

Georgios Bakirtzis (Mar 23 2020 at 21:50):

I intend this place to be about systems. From theory (Ashby, Mesarovic) to systems thinking (Leveson on safety for example) to practice (modeling, simulation, tools) to control (Pappas, Tabuada, Ames). General discussion is welcome but lets try to keep most of the content in relation to category theory. I know some people are working in _some_ of these areas (@David Spivak @Blake Pollard for example).

Joe Moeller (Mar 23 2020 at 23:52):

What's the difference between "systems" and "networks". Trying to figure out if I work on systems or not :thinking:

Georgios Bakirtzis (Mar 23 2020 at 23:54):

What do your networks do?

Joe Moeller (Mar 24 2020 at 00:01):

I think of my work as specifically thinking about networks categorically+combinatorially, in an almost pure math sorta way. So they don't technically do anything, but they aren't prohibited from doing anything. :shrug:

Georgios Bakirtzis (Mar 24 2020 at 00:02):

Welcome to the area of systems theory :), your formalism can be used to construct an architecture of a system (say graphs, automata, petri nets). Have you tried to apply your findings to a particular system? In general, system theorists are very interested in more formal ways of organizing information.

Joe Moeller (Mar 24 2020 at 00:02):

I've done some work with Petri nets.

Georgios Bakirtzis (Mar 24 2020 at 00:04):

The general consensus (which is not shared by CT people) is that petri nets don't scale. But the work is still important. I would be very interested in hearing your thoughts about how to model systems with a lot of elements with petri nets, how can we reduce the general complexity or manage it with your work etc.

Georgios Bakirtzis (Mar 24 2020 at 00:05):

I mean this from a "practical" standpoint of modeling, a system with thousands of states is difficult to model and validate with a petri net.

John Baez (Mar 24 2020 at 00:11):

It'd be good to talk to Jelle Herold about that scaling issue, since has a company that's trying to use Petri nets to handle complex systems.

John Baez (Mar 24 2020 at 00:12):

I use Petri nets to study chemistry, and I just prove theorems about it, so scaling isn't a problem.

John Baez (Mar 24 2020 at 00:12):

Theorems scale. :upside_down:

John Baez (Mar 24 2020 at 00:14):

But I'd be really curious what Jelle and others say about using Petri nets for managing industrial processes. (This does not mean drawing enormous diagrams on paper.)

Georgios Bakirtzis (Mar 24 2020 at 00:18):

Yeah I have talked to Jelle and Fabrizio, I can't wait for him to prove me wrong. My understanding is that the scope of Statebox is very specific software systems. What happens when you add physical behavior? I would like to know so I am working with Christina on a general wiring diagram approach (not a petri net), if Statebox can automatically translate that, ensure a number of safety contracts with reasonable efficiency I would be ecstatic.

Georgios Bakirtzis (Mar 24 2020 at 00:18):

Maybe some of Joe's work can help? Could you send me a paper on your work? I am not familiar unfortunately.

Georgios Bakirtzis (Mar 24 2020 at 00:21):

John we talked briefly at ACT 2019 but as a reminder I actually come from the systems theory people not CT. I think CT will become useful in the systems domain so any approach that helps us get there is of interest to me.

John Baez (Mar 24 2020 at 00:21):

Yes, I remember talking as we walked around that field in Oxford!

It's mainly Jade who has been working on Petri nets in our gang; Joe and Jade are writing a paper on colored Petri nets that is not out yet.

John Baez (Mar 24 2020 at 00:24):

Well, actually Joe has a paper on Petri nets too! Too many students writing too many papers to remember them all. :upside_down:

Philip Zucker (Mar 24 2020 at 00:24):

Out of curiosity, does anyone have any references on mixed integer programming being applied to Petri nets? I mentioned an idea to a colleague and he seemed highly skeptical it would scale.

Philip Zucker (Mar 24 2020 at 00:25):

I guess, as has been said, that scaling has been an issue in general in petri nets

Georgios Bakirtzis (Mar 24 2020 at 00:26):

John Baez said:

Well, actually Joe has a paper on Petri nets too! Too many students writing too many papers to remember them all. :upside_down:

Great give me some time to read it but if you and Joe are open to it, I will probably have some questions.

John Baez (Mar 24 2020 at 00:27):

Sure, we may want a thread on Petri nets. "Systems" is incredibly general.

John Baez (Mar 24 2020 at 00:27):

From a certain point of view, everything is a system....

Georgios Bakirtzis (Mar 24 2020 at 00:28):

Everything is indeed a system :)

John Baez (Mar 24 2020 at 00:29):

Okay, we can have a discussion stream called "everything". :upside_down:

Georgios Bakirtzis (Mar 24 2020 at 00:30):

Haha, we can diverge as needed, but I think I constrained the domain on my first post as much as possible.

janet singer (Mar 24 2020 at 00:33):

Getting back to @Joe Moeller ‘s question, is a network a type of system representation? Does every system have a network representation, and if not why not?

janet singer (Mar 24 2020 at 00:52):

Or per @Giorgos Bakirtzis the formal representation in a network can be taken as corresponding to the architecture of a system?

Georgios Bakirtzis (Mar 24 2020 at 00:52):

At some level it always should, no?

janet singer (Mar 24 2020 at 01:02):

That’s a good way of framing it which shifts focus to taking ‘at some level’ seriously.

janet singer (Mar 24 2020 at 01:19):

As in ‘everything is a system’ becomes ‘everything can be represented as a system on some level’

Christian Williams (Mar 24 2020 at 02:04):

John Baez said:

But I'd be really curious what Jelle and others say about using Petri nets for managing industrial processes. (This does not mean drawing enormous diagrams on paper.)

actually Jelle has done tons of business optimization using Petri nets, before starting Statebox.

Georgios Bakirtzis (Mar 24 2020 at 15:17):

@Fabrizio Genovese is here so he can shed some light on this.

Fabrizio Genovese (Mar 24 2020 at 15:38):

It is true, Petri nets do not scale.

Fabrizio Genovese (Mar 24 2020 at 15:40):

I think this is fairly uncontroversial for anyone that tried to apply Petri nets to do real stuff. This is why you want to do Petri nets categorically. The power of Petri nets - in my view - is that they "present" (lots of details here but let's pretend they don't exist) free symmetric strict monoidal categories. Now:
"Free" means "you can map these categories wherever you want"
"Symmetric Strict Monoidal" means "These categories are the most general example of process theories, which is the bare minimum you need to do real world stuff, imho."

Fabrizio Genovese (Mar 24 2020 at 15:41):

So, the idea is that you use Petri nets as an abstracted model of whatever it is that you care about, and via functorial semantics you use that model to orchestrate what has to happen "for real". This is what Statebox does.

Fabrizio Genovese (Mar 24 2020 at 15:44):

So, for instance, you have a transition in your Petri net called "Login". This goes from place "Guest" to place "Logged in User". then from this place you can have other transitions like "shop", "update cart", "pay", "logout" etc. Now the important thing is that this "Login" transition is not a real login. It just represents the action of logging in. I don't want to represent the whole internal log in process in a Petri net cos that would be a useless nightmare. Using the functorial mapping I can map the generator corresponding to "login" in my free symmetric strict monoidal category to some haskell function (hence something living in the category of Haskell types and functions between them) that is an actual, real implementation of a login.

Fabrizio Genovese (Mar 24 2020 at 15:46):

So, as long as my functions are correctly implemented, I know that the nice proprieties I can prove on my Petri nets will translate to my code. For us, this is the only sensible way of using Petri nets in software. Call it "formally verified orchestration" if you want. Notice also that, depending on what your semantics does, this could be very powerful. E.g. Petri nets define languages that always terminate, but nothing forbids you to map transitions in your net to infinite loops in your semantics (if it allows it). So you can even do Turing-complete computation in this way. Clearly in this case it is not true anymore that nice properties of nets are transported to your semantics.

Kent Palmer (Sep 02 2020 at 17:10):

I would like to call your attention to Schemas Theory (http://schematheory.net). Systems are just one Schema out of a whole set of schemas. Many of these appear in Wittgenstein's Philosophical Grammar and other sources. Concept of the Schema is from Umberto Eco Kant and the Platypus called there the "Mathematical and Geometrical" Schemas.

I have boiled down the references to different schemas that I have found in the literature to ten:

Pluriverse
Kosmos
World
Domain
Meta-system
--- Special Systems
System
Form
Pattern
Monad
Facet

The Schemas provide the context for the anomaly of Special Systems Theory.
See https://www.academia.edu/3795281/Special_Systems_Theory

Various papers on General Schemas Theory:
https://www.academia.edu/34831626/General_Schemas_Theory
https://www.academia.edu/37990709/On_the_Definition_of_a_Schemata
https://www.academia.edu/37881348/Schemas_Theory_Overview_Part_01_Origins_of_the_S_prime_hypothesis
https://www.academia.edu/37923141/Schemas_Theory_Overview_Part_02_Overview_of_the_Argument_from_the_Tutorial_on_Dagger_Theory
https://www.academia.edu/38049990/Schemas_Theory_Overview_Part_03_Advances_in_Schemas_Theory
For more papers on Schemas Theory see https://independent.academia.edu/KentPalmer

I try to use Category Theory as a vehicle for exploring Schemas in order to understand Design.

See Ph.D. Dissertation on Emergent Design
https://www.academia.edu/34831961/EMERGENT_DESIGN

Henry Story (Sep 02 2020 at 17:26):

I have been wondering about the relation between Universal coalgebra: a theory of systems and systems theory. Are these the same concepts?

Kent Palmer (Sep 02 2020 at 17:30):

For Systems Engineering Working Group of INCOSE.org see https://sites.google.com/site/syssciwg/

We have been trying to introduce more awareness of Category Theory over recent years into Systems Engineering but also Systems Science with our partnership with the ISSS.org

https://www.academia.edu/30762807/Systems_Philosophy_Questions_about_Mathematical_Category_Theory
https://www.academia.edu/37192095/Practical_Application_of_Schema_and_Category_Theories

But we have found it difficult to find people who know Category Theory to engage with us and teach us about it. So we are dependent on Engineers who have tried to learn it themselves to introduce it to us.

See as an example https://www.nasa.gov/consortium/CategoryTheory

Kent Palmer (Sep 02 2020 at 21:08):

There is a Systems Engineer (Rutten) that makes the case that the System is really a co-algebra. But his ideas being esoteric have not been generally recognized as important as they are in their implications for both Systems Science and Systems Engineering. See Rutten, J J. M. M. Universal Coalgebra: A Theory of Systems. Amsterdam: Computer Science/Department of Software Technology, 1996. I personally really like his work, but do not think it is the whole story. Note: I see you were pointing at the same paper. It is really good, but I am probably the only Systems Engineer to have read it. Most Systems Scientists would have no idea what he is talking about. A basic reference here would be Denecke, Klaus, and Shelly L. Wismath. Universal Algebra and Coalgebra. Singapore: World Scientific, 2009. @Henry Story

Georgios Bakirtzis (Sep 02 2020 at 21:31):

@Kent Palmer You're not the only one ;)

Fabrizio Genovese (Sep 02 2020 at 22:05):

Kent Palmer said:

For Systems Engineering Working Group of INCOSE.org see https://sites.google.com/site/syssciwg/

We have been trying to introduce more awareness of Category Theory over recent years into Systems Engineering but also Systems Science with our partnership with the ISSS.org

https://www.academia.edu/30762807/Systems_Philosophy_Questions_about_Mathematical_Category_Theory
https://www.academia.edu/37192095/Practical_Application_of_Schema_and_Category_Theories

But we have found it difficult to find people who know Category Theory to engage with us and teach us about it. So we are dependent on Engineers who have tried to learn it themselves to introduce it to us.

See as an example https://www.nasa.gov/consortium/CategoryTheory

As a category theorist I'd be happy to help :smile:

Fabrizio Genovese (Sep 02 2020 at 22:06):

I am part of that current of ACT that thinks that the more we CT people get exposed to applications, the better it is. So for me it's more about learning what engineers want than trying to convince them to use category theory for whatever reason!

Kent Palmer (Sep 03 2020 at 06:38):

@Giorgos Bakirtzis So glad to hear it. I was worried there for a minute. I was feeling awfully lonely.

Georgios Bakirtzis (Sep 03 2020 at 06:41):

@Kent Palmer We have some interesting work coming out and there are some people that use categories a little informally in Systems Engineering venues (e.g., https://ieeexplore.ieee.org/abstract/document/8369508?casa_token=zk1nwGU3C0kAAAAA:Z1pGvoCBgKR2Ehle_Flz7nll-qjVYmHKqdqmf04tgwOb3LSw8iK56WsEwlMko0dJ-w6uCgrRdA), but we are targeting cyber-physical systems venues not systems engineering venues (for various reasons that I can talk about if needed)

Kent Palmer (Sep 03 2020 at 06:49):

@Fabrizio Genovese But systems engineers don't know what they want. Look at SysML based on UML. It is a mess. Getting more complex all the time with no inner coherence. Yet their modeling could be based instead on Category Theory and then have some basis in mathematics, but they do not opt for that, they rejected it when it was suggested so I am told. Systems Engineers don't even know what "Systems" are even though it is in their name (by an accident of history rather than for a reason). That is why we forged a union with ISSS.org to that INCOSE.org could learn something about systems from people how have a clue. Sometimes a better way, a paradigm change, is going to come out of the blue and no one is asking for it, because they do not know what they need to solve their problems. Traditional Systems Engineering has undergone no paradigm changes as a discipline unlike Software Engineering, it basically just follows Software Engineering, and eventually it will follow Software Engineering into using Category Theory too. There will be "Functional" Systems Engineering eventually (Again!) but with a new meaning. But until Systems Engineering undergoes a paradigm change we will not know if it is real discipline or not. It may just be an artifact of government contractual practices. But I have hopes that there will be a real discipline of Systems Engineering that is founded in Systems Science eventually.

See https://www.academia.edu/36446262/Category_Theory_Centric_Systems_Science_and_Software_Systems_Engineering

Kent Palmer (Sep 03 2020 at 06:53):

@Giorgos Bakirtzis Looks interesting. Would like to read that paper. See https://www.academia.edu/36600384/The_Essential_Nature_of_Product_Traceability_and_its_relation_to_Agile_Approaches Might be relevant.

Georgios Bakirtzis (Sep 03 2020 at 06:55):

I sympathize with your overarching goal but having engaged with the community you are talking about I think you are generalizing a bit and are somewhat strong and unfair for no reason. SysML 2.0 with all its problems and all the problems it didn't solve actually formulated the problems we talk about here. And lest we forget, category theory is nice but (1) you have to SHOW how it is useful in a systems engineering context - my thinking here is that you will need a considerable (in size) case study which in turn would require us to build prototype tools first and (2) category theory is not the ONLY approach that addresses the problems in systems engineering, I like it but that doesn't mean that extending things like contract-based design or other methods like Ptolemy for real-time systems wouldn't work similarly. So all in all, I am glad I am seeing category theory proposed for this domain but there is a lot of the ground work to actually see if it works and show others that it works - which I personally am willing to do - but as of now category theory in system design is mostly philosophy and not a concrete paradigm shift that you define.

Henry Story (Sep 03 2020 at 09:25):

@Kent Palmer wrote in Category Theory Centric Systems Science and Software Systems Engineering

the dual of Geometry is Topology while the dual of Algebra is CoAlgebra.

I know and have studied the algebra/coalgebra duality. But I had not come across the idea of topology and geometry being duals. (I also know very little about that space, and am trying to get to know those better).

Fabrizio Genovese (Sep 03 2020 at 09:28):

Kent Palmer said:

Fabrizio Genovese But systems engineers don't know what they want. Look at SysML based on UML. It is a mess. Getting more complex all the time with no inner coherence. Yet their modeling could be based instead on Category Theory and then have some basis in mathematics, but they do not opt for that, they rejected it when it was suggested so I am told. Systems Engineers don't even know what "Systems" are even though it is in their name (by an accident of history rather than for a reason). That is why we forged a union with ISSS.org to that INCOSE.org could learn something about systems from people how have a clue. Sometimes a better way, a paradigm change, is going to come out of the blue and no one is asking for it, because they do not know what they need to solve their problems. Traditional Systems Engineering has undergone no paradigm changes as a discipline unlike Software Engineering, it basically just follows Software Engineering, and eventually it will follow Software Engineering into using Category Theory too. There will be "Functional" Systems Engineering eventually (Again!) but with a new meaning. But until Systems Engineering undergoes a paradigm change we will not know if it is real discipline or not. It may just be an artifact of government contractual practices. But I have hopes that there will be a real discipline of Systems Engineering that is founded in Systems Science eventually.

See https://www.academia.edu/36446262/Category_Theory_Centric_Systems_Science_and_Software_Systems_Engineering

I think the constrast you stress between System and Software engineering is virtual, and indeed, the problem is maybe exactly the idea of "following software engineering". Let me explain: With the success of startups and the like, industry has been demanding, in the last years, software paradigms that would be as agile as possible. The idea of "Develop now, think later, patch never" simply works best when you are developing stuff like apps and website. Here stability is a plus, what matters really is business advantage on competitors, for which speed in prototypation and development is paramount.

Fabrizio Genovese (Sep 03 2020 at 09:30):

This is also precisely why I think that stuff like cryptocurrency is revolutionary. It forces a paradigm shift. Smart contracts work exactly like apps, but they manage people's money, so they have to be as resilient as mission critical infrastructure. Now stability is not anymore a plus, it's needed. We are seeing this first hand, for example, with sushiswap.org. They launched like a week ago, already have like 500 million dollars locked in, and since day 2 have been asking around for some company to audit their code.

Fabrizio Genovese (Sep 03 2020 at 09:31):

As you can see, formal verification and formal methods are going to be naturally embraced by this community. This gives, in my opinion, a terrific opportunity to category theory and in general to any "correct-by-design" implementation metodology.

Fabrizio Genovese (Sep 03 2020 at 09:32):

You can, for sure, expect a rise in adoption of functional programming. But in general, what I think we're going to see in the next 10yrs or so is programming languages increasingly based on category theory, that become simpler to use by the day, and steadily incorporate theorem proving features that allow to optimize and verify bits of code.

Fabrizio Genovese (Sep 03 2020 at 09:34):

In the end, if as you say system engineering follows software engineering, it's just a matter of time until you'll see this trickling down to systems engineering. So keep pushing at what is now the fringe of software engineering, and expect to be riding a huge, revolutionary wave a few years from now. :smile:

Henry Story (Sep 03 2020 at 09:50):

I agree with @Fabrizio Genovese . There are different spaces. 1. One is based on quick iteration ( the startup) as the space to be explored is hardly known. One observes, transforms, evolves. (coalbebraically?) using the information one has gathered. 2. Then there is building the architecture of a system. Ideally those also evolve but they can't evolve at the same speed, since they build the framework on which others build. Blockchains are a good example. Web Architecture can also be thought of that way. It is interesting to look at the evolution of such a large scale system as the web. It started as a simple hypertext format without even images, to include everything we have today including cryptography, moving from synchronous HTTP exchanges to asynchronous HTTP/2.0, ... developing a logical layer (RDF), ...

Henry Story (Sep 03 2020 at 10:03):

The interesting thing is how the Web started from a couple of very basic (mathematical? logical?) ideas:
A declarative system of interlinked documents, built on a global decentralised naming system: URLs.
Unique unambiguous names are the center of logic since Frege. (what is new is the decentralised naming scheme). HyperText actually has a long history I don't know as well as I should.

Kent Palmer (Sep 03 2020 at 15:44):

Interesting responses thanks.

John Baez (Sep 03 2020 at 23:08):

Yet their modeling could be based instead on Category Theory and then have some basis in mathematics, but they do not opt for that, they rejected it when it was suggested so I am told.

If they rejected it, it's probably because 1) they have no idea what it means and 2) nobody showed them a bunch of concrete examples of how it works.

John Baez (Sep 03 2020 at 23:09):

It's sort of like kids rejecting unfamiliar foods before they've even tasted them... but with the extra problem that the food doesn't even exist yet, it's just something people are talking about.

Kent Palmer (Sep 04 2020 at 05:31):

However, our more recent experience is that Systems Engineers are becoming interested in Category Theory now for some reason. It has broken through as a subject of significant interest to a lot more of the thought leaders in this community. But we have no way to fill the demand for information about it because there are so few people who feel that they can speak with authority on it. When they try to teach themselves about it they hit a wall because it goes against all their intuitions and they really do not understand it at all, as soon as they start trying to read Category Theory books. Simple introductions to Category Theory are not enough. We need courses on Category Theory for practitioners taught by people who really know it and can answer tough questions about it with respect to practical problems they might attempt to apply it to.

Henry Story (Sep 04 2020 at 08:35):

Category Theory I think brings back the enthusiasm for the Web (everything is interconnected) but with the mathematics and proofs added to it, which helps ground things a bit.

Jules Hedges (Sep 04 2020 at 09:59):

Kent Palmer said:

Simple introductions to Category Theory are not enough. We need courses on Category Theory for practitioners taught by people who really know it and can answer tough questions about it with respect to practical problems they might attempt to apply it to.

There is demand for books similar to Categories For The Practicing Physicist, Categories For The Working Philosopher, and Category Theory For Programmers, I guess. Those are the only 3 that exist that I know of. One of these decades if I have nothing else to do I might write Categories For The Working Economist. It's just that writing good introductions is really hard and there's not many of us

Chad Nester (Sep 04 2020 at 10:45):

Are practitioners willing to pay for these courses?

John Baez (Sep 04 2020 at 17:41):

It would be interesting to see who is paying for the category theory courses taught by Statebox:

https://twitter.com/statebox/status/1300867481171619840

Who's afraid of #categorytheory? We've got 3 spots left. Sign up on https://training.statebox.org/ :ghost: https://twitter.com/statebox/status/1300867481171619840/photo/1

- Statebox (@statebox)

When Brendan Fong and David Spivak get the Topos Institute going, they plan to teach courses on category theory too.

Georgios Bakirtzis (Sep 04 2020 at 17:52):

Jules Hedges said:

Kent Palmer said:

Simple introductions to Category Theory are not enough. We need courses on Category Theory for practitioners taught by people who really know it and can answer tough questions about it with respect to practical problems they might attempt to apply it to.

There is demand for books similar to Categories For The Practicing Physicist, Categories For The Working Philosopher, and Category Theory For Programmers, I guess. Those are the only 3 that exist that I know of. One of these decades if I have nothing else to do I might write Categories For The Working Economist. It's just that writing good introductions is really hard and there's not many of us

There is this https://www.nasa.gov/sites/default/files/atoms/files/mssrc_uah_nasa_30-09-2018.pdf but as with everyone I have a different view of what needs to be covered, I will be writing a similar chapter with the material I think should be there (and supports the results of my dissertation but more comprehensive) for my dissertation. How that turns up idk, it will certainly not be a book

Georgios Bakirtzis (Sep 04 2020 at 17:53):

But I hope my whole current work/dissertation will be achieving this to some degree

Georgios Bakirtzis (Sep 04 2020 at 17:56):

I at least intend to write my dissertation as a self contained introduction and current results but I am not sure that's a good idea

Fabrizio Genovese (Sep 04 2020 at 19:51):

John Baez said:

It would be interesting to see who is paying for the category theory courses taught by Statebox:

https://twitter.com/statebox/status/1300867481171619840

When Brendan Fong and David Spivak get the Topos Institute going, they plan to teach courses on category theory too.

So, as of now our biggest demographic is software developers, especially people that are already interested in functional programming

Fabrizio Genovese (Sep 04 2020 at 19:52):

Interestingly, not all of our participants are taking the course on behalf of the company they work for. Some of them paid for it privately, out of personal interest and curiosity I guess

Fabrizio Genovese (Sep 04 2020 at 19:54):

Also, we were both humbled and shoked to see that some of our participants hail from US West Coast or other places which are up to +-9 hours wrt to central Europe time. These people would literally wake up at 3am to take the course, and this should give a measure of how interested in learning category theory they are

Fabrizio Genovese (Sep 04 2020 at 19:55):

Up to now all of our courses have been sold out. And I always redirect the participants here and recommend them to interact with the community. So if some former participant of the course happens to read these messages please feel free to chime in and talk about your experience if you want to!

Kent Palmer (Sep 05 2020 at 04:13):

@Chad Nester Not sure if there is the level of interest yet that would lead to their paying for courses. It is more like Tell Me More how this could help me? But we can only hope that this level of interest increases till they are willing to pay for courses.

Valeria de Paiva (Sep 05 2020 at 16:17):

Fabrizio Genovese said:

So, as long as my functions are correctly implemented, I know that the nice proprieties I can prove on my Petri nets will translate to my code. For us, this is the only sensible way of using Petri nets in software. Call it "formally verified orchestration" if you want. Notice also that, depending on what your semantics does, this could be very powerful. E.g. Petri nets define languages that always terminate, but nothing forbids you to map transitions in your net to infinite loops in your semantics (if it allows it). So you can even do Turing-complete computation in this way. Clearly in this case it is not true anymore that nice properties of nets are transported to your semantics.

I like the expression "formally verified orchestration": it speaks to the fact that one of the hardest things in software nowadays is getting the pipes going, wrappers for what needs to be wrapped, etc.

I wonder if anyone has looked at the gimmicky "no-code software development" (https://spectrum.ieee.org/tech-talk/computing/software/programming-without-code-no-code-software-development) with category theory lenses, yet. do you know?

Fabrizio Genovese (Sep 05 2020 at 17:38):

This is precisely what we want to achieve in the long run: Draw a Petri net, obtain a free monoidal category, map transitions into a semantics, check the execution state of your code by looking at string diagrams

Fabrizio Genovese (Sep 05 2020 at 17:39):

There are many examples of this already in production: LunaLang, Node-red, really many, some more successful than others. But none of them is "formal", or "typed". For me this is precisely what can be achieved with category theory, formally precise graphical programming

Fabrizio Genovese (Sep 05 2020 at 17:48):

wrt this, it's like ages that I think I should write up something about "categorical design". The idea is: Categories are great, but they do not live in a void. How can we practically employ them to build products? One of the most important properties, that I don't think is really stressed enough, is that any sort of categorical design should be free in some respect. This is for a couple of reasons:

• When we are lucky, we have a complete categorical description of something we care about, and we can leverage this to implement the description directly. This is very rare and often requires 10+ years of work. I'm thinking, for example, to ZX calculus which you can implement as-is and still be able to say everything you wanna say about quantum systems. Once you get it it's great, but rarely you do. Also we'll never be competitive in a world based on fast prototypation with this mindset. As such, we should realize that often the categorical descriptions we'll get will be incomplete, and in need to be supplemented with some semantic information (e.g. Petri nets as above).
• Categorical stuff can be completed with some sort of "external" semantic information only if it is free in some respect. If a category is free in some sense, then I can implement functors even without really defining them, and be sure that everything works correctly.
  For example: If I map the vertexes of a graph to some data and the edges to some transformations of data, I know that any graph path will lift to a sensible transformation. I can do this without using the word "category" or "functor" even once, but I know it will work because I know graphs generate free categories. I'm applying categorical design even without implementing categories formally.
  If I have a category that defines ways of orchestrating things which is not free with respect to the semantics I have in mind, this is not true anymore. And it's an implementational headache at this point.

Fabrizio Genovese (Sep 05 2020 at 17:49):

For these reasons we are keeping it relatively simple at statebox: Petri nets and their corresponding free symmetric monoidal categories are enough for us at the moment, also because free SMCs are free with respect to any reasonable semantics we can think about. :grinning:

Antonin Delpeuch (Sep 06 2020 at 07:11):

What do you mean by "free with respect to semantics"?

Fabrizio Genovese (Sep 06 2020 at 11:47):

For instance, if I intend my semantics to be a process theory, I should deal with Free strict symmetric monoidal categories. If my semantics also supports some notion of feedback, then I maybe be able to specialize to free traced or free compact closed categories

Fabrizio Genovese (Sep 06 2020 at 11:48):

But now consider the opposite: Your "orchestration category" is a compact closed category. So it naturally provides a way to flip inputs to outputs and vice-versa. Now suppose my target semantics is any functional programming language. I'll have a VERY hard time giving interpretations to my morphisms that doesn't make everything explode

Fabrizio Genovese (Sep 06 2020 at 11:50):

More precisely, I will have to PROVE that my interpretation is sound (that is, functorial). Practice-wise this means that working in a formally verified setting may be necessary to get some guarantees about my implementation. On the contrary, if I just use a free SMC, I know that a mapping from generating objects/morphisms to the semantics is enough to preserve everything

Fabrizio Genovese (Sep 06 2020 at 11:51):

This is because the category I am using for the orchestration is the free version of the categories I am using in the semantics, so I can leverage freeness. A free compact closed category is not a free SMC on the other hand, so I cannot rely on this fact anymore (unless I restrict my semantics to categories that are all compact closed, clearly)

Fabrizio Genovese (Sep 06 2020 at 11:52):

The reason why SMCs are central in categorical design, imho, is that nearly all meaningful notions of semantics implement an idea of "composing things"and an idea of "taking pairs of things".

Fabrizio Genovese (Sep 06 2020 at 11:53):

Now we have a lot of more expressive categories to model the idea of wiring systems together, in the last years we really considered wirings of processes in any possible way we could imagine. Still, I don't know how useful all this will be in practice if the price to pay is that freeness is lost.

Morgan Rogers (he/him) (Sep 06 2020 at 12:56):

As a side note, the same concept appears in categorical logic. We always start with a signature of some kind, the basic data of a theory. From this data, we inductively generate the syntax based on the operations which exist in our fragment of logic. With no extra axioms, this is the empty theory over that signature; in any category equipped with sufficient structure to interpret the logical operations, a model of this empty theory is completely determined by a valid choice of interpretation of the data in the signature. As such, there is a syntactic category for this theory, which is just the free such category generated from the data in the signature, just as Fabrizio was describing in the case of SMCs, so that a structure-preserving functor from this category directly corresponds to a choice of the necessary data in the codomain category. Adding axioms to the theory then corresponds to taking a quotient of that free category; a functor interpreting the signature is a model of the theory if and only if it factor through the quotient functor.
(this description would be a lot nicer with diagrams, but oh well)

Antonin Delpeuch (Sep 07 2020 at 05:27):

Sorry my question was probably unclear - I understand the interest in having free structures and functors from them into the semantics, I am just wondering whether "free with respect to the semantics" can mean anything stronger than that. Could it be turned into a definition?

Fabrizio Genovese (Sep 07 2020 at 09:41):

I think it can be understood as a design principle. "If you want to develop an application X, start by pinning down all the possible semantics you will need to do X, and use the free category on these semantics as your starting design point"

Antonin Delpeuch (Sep 07 2020 at 09:45):

Ok, so as I understand it, mathematically speaking, your syntactic category is just freely generated by a signature in the usual sense :)

Fabrizio Genovese (Sep 07 2020 at 10:29):

You may also have some equations that commonly hold in your semantics. It doesn't need to be "absolutely free" in the universal algebraic sense

Antonin Delpeuch (Sep 07 2020 at 11:04):

sure!

Georgios Bakirtzis (Oct 20 2020 at 13:43):

Here is a project webpage for the stuff I do with Christina Vasilakopoulou and Fabrizio Genovese https://bakirtzis.net/talon/ Feedback welcome, since this is a pretty early effort in the grand scheme of things :)

Jules Hedges (Oct 20 2020 at 14:00):

Wow, exciting

Georgios Bakirtzis (Oct 20 2020 at 14:35):

@Jules Hedges Thanks I would like to see open games in Catlab because they coinside with a lot of research in control!

John Baez (Oct 20 2020 at 15:09):

It's cool that Christina is working with you on this stuff.

Jules Hedges (Oct 20 2020 at 15:10):

Giorgos Bakirtzis said:

Jules Hedges Thanks I would like to see open games in Catlab because they coinside with a lot of research in control!

We should talk about this. I'm definitely considering that the open game engine ought to be rewritten in Julia, there are some good reasons to do so. I don't think there's any chance I'll be doing it myself though

Georgios Bakirtzis (Oct 20 2020 at 15:19):

@John Baez Yeah it's great :) It's also cool that Fabrizio is indulging me for the security stuff (which should be available in a couple of months)
@Jules Hedges Sure, we can talk about it, right now I am a bit swamped and trying to get a simple prototype out for the rest of the stuff but I intended to contract you once the initial steps where done.

Daniel Geisler (Oct 23 2020 at 12:27):

Usually mathematics searches for the simplest way to construct mathematical objects, but I want to research general systems which can model any other system. While certain CAs are Turing-complete, they are discrete and therefore problematic for modeling physics.
Consider dynamical systems. They are measure preserving continuous iterated functions $f^t(x)$ (E. Atlee Jackson, (1995). Perspectives of nonlinear dynamics 1, Cambridge, pg 51). I focus on continuous iterated functions $f^t(x)$ which are more general than dynamical systems.

The composition $f(g(x))$ can construct any iterated function at a fixed point, not at infinity, by setting $f(0)=0$ and $g(x)=f^{t-1}(x)$ with $t \in \mathbb{N}$. The first derivative of $f(x)$ at its fixed point $Df(0)$ is often represented by $\lambda$ and referred to as the multiplier or the Lyapunov characteristic number; its logarithm is known as the Lyapunov exponent.

The First Derivative

The first derivative results in the well known Linearization Theorem.

$$Df(g(x))=f'(g(x))g'(x)$$

$$=f'(f^{t-1}(x))Df^{t-1}(x)$$

$$=\prod^{t-1}_{k_1=0}f'(f^{t-k_1-1}(x))$$

$$Df^t(0)=\lambda^t$$

The Second Derivative

The higher derivatives can be evaluated in an analogous fashion from the second derivative.

$$D^2f(g(x))=f''(g(x))g'(x)^2+f'(g(x))g''(x)$$

$$=f''(f^{t-1}(x))(Df^{t-1}(x))^2+f'(f^{t-1}(x))D^2f^{t-1}(x)$$

Setting $g(x) = f^{t-1}(x)$ results in

$$D^2f^t(0)= f''(0) \lambda^{2t-2}+\lambda D^2f^{t-1}(0)$$

When $\lambda \neq 0$, a recurrence equation is formed that is solved as a summation.

$$D^2f^t(0)=f''(0)\lambda^{2t-2}+\lambda D^2f^{t-1}(0)$$

$$=\lambda^0f''(0) \lambda^{2t-2}$$

$$+\lambda^1f''(0) \lambda^{2t-4}$$

$$+ \cdots$$

$$+\lambda^{t-2}f''(0) \lambda^2$$

$$+\lambda^{t-1}f''(0) \lambda^4$$

$$=f''(0)\sum_{k_1=0}^{t-1}\lambda^{2t-k_1-2}$$

Daniel Geisler (Oct 23 2020 at 12:37):

I believe the main defect with my work is that it isn't based on CT except for the combinatoric portion.