It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.3K
- Chat 494
- ACT Study Group 6
- Green Mathematics 1
- Azimuth Math Review 6
- MIT 2020: Programming with Categories 53
- MIT 2020: Lectures 21
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 64
- Azimuth Code Project 110
- Drafts 1
- Math Syntax Demos 15
- Wiki - Latest Changes 1
- Strategy 110
- Azimuth Project 1.1K

## Comments

Do your worms die when they turn eggshells into compost?

`Do your worms die when they turn eggshells into compost?`

Worms like crushed eggshells. They use them for grit because they have no teeth. But you are correct, they do not die, instead they multiply and are ready for the next batch of compostable ingredients. So they should be yet another reusable output->input.

P.S. that one should be circular, back into the compost bin. Need to find out if cytoscape can handle that...

`Worms like crushed eggshells. They use them for grit because they have no teeth. But you are correct, they do not die, instead they multiply and are ready for the next batch of compostable ingredients. So they should be yet another reusable output->input. P.S. that one should be circular, back into the compost bin. Need to find out if cytoscape can handle that...`

Keith E. Peterson better?

By the way, there is real resource flow code and data behind this, cytoscape is auto-generating the graph, I'm not drawing it.

`[Keith E. Peterson](https://user-images.githubusercontent.com/117439/40493279-ffe1762c-5f37-11e8-9cfa-1ce59190c724.png) better? By the way, there is real resource flow code and data behind this, cytoscape is auto-generating the graph, I'm not drawing it. ![refresh worms](https://user-images.githubusercontent.com/117439/40493279-ffe1762c-5f37-11e8-9cfa-1ce59190c724.png)`

Okay, we can talk about this!

`Okay, we can talk about this!`

@(Bob Haugen) Well yeah, much better, now your worms aren't dying so you don't have to keep adding worms.

@(John Baez) I see that automatically drawn Petri nets got your attention.

`@(Bob Haugen) Well yeah, much better, now your worms aren't dying so you don't have to keep adding worms. @(John Baez) I see that automatically drawn Petri nets got your attention.`

Heh, no, Bob Haugen said he wanted to talk to me about some ideas... and I'm just reminding him that I do want to talk about them.

If there were nothing much going on beyond these pictures, there'd be nothing much to talk about: they're directed graphs, 'nuff said. But Bob says "there is real resource flow code and data behind this". Even more interesting is his remark in comment #91 that there are three "layers" at work. If we get a few "layers" of Petri nets interacting in some manner, that could be something interesting and new.

`Heh, no, Bob Haugen said he wanted to talk to me about some ideas... and I'm just reminding him that I do want to talk about them. If there were nothing much going on beyond these pictures, there'd be nothing much to talk about: they're directed graphs, 'nuff said. But Bob says "there is real resource flow code and data behind this". Even more interesting is his remark in [comment #91](https://forum.azimuthproject.org/discussion/comment/18063/#Comment_18063) that there are three "layers" at work. If we get a few "layers" of Petri nets interacting in some manner, that could be something interesting and new.`

(This is a bit of a brain-dump, and I'm not sure how much this actually contributes to the discussion, but I'd love to hear anyone's thoughts! I find this subject utterly enthralling.)

Over here, I raised the question of enriched categories over a simple four-element lattice, which we now know is the Dunn/Belnap 4 valued logic, which we've been denoting by

Belnap4.You can think of this as the lattice of knowledge about some arbitrary proposition. The least element represents "no knowledge"; the greatest element represents "contradictory knowledge", and the other two represent that you know the proposition is true or that the proposition is false. Very similar lattices arise in the work of Lindsey Kuper and Ryan Newton on lattice variables (LVars), which represent increasing knowledge about the value contained in a variable. Vijay Saraswat's concurrent constraint programming (CCP) seems to give a broad framework for studying programs that operate over such domains of increasing knowledge.

I'm absolutely

fascinatedby this topic, and I quite badly want to find something to contribute to the field. (The LVars paper was arguably one of the main reasons I became a Ph.D. student!) The CCP approach is quite a pure kind of logic programming, whereas the LVars approach includes some functional aspects as well. I think there's some serious category theory underlying all of this (especially CCP), but I'm just not familiar enough with category theory to see it.`(This is a bit of a brain-dump, and I'm not sure how much this actually contributes to the discussion, but I'd love to hear anyone's thoughts! I find this subject utterly enthralling.) [Over here](https://forum.azimuthproject.org/discussion/comment/18463/#Comment_18463), I raised the question of enriched categories over a simple four-element lattice, which we [now know](https://forum.azimuthproject.org/discussion/comment/18477/#Comment_18477) is the [Dunn/Belnap 4 valued logic](https://plato.stanford.edu/entries/logic-manyvalued/#Dun4ValSys), which we've been denoting by **Belnap4**. <center>![](https://plato.stanford.edu/entries/logic-manyvalued/4V-info.gif)</center> You can think of this as the lattice of knowledge about some arbitrary proposition. The least element represents "no knowledge"; the greatest element represents "contradictory knowledge", and the other two represent that you know the proposition is true or that the proposition is false. Very similar lattices arise in the work of Lindsey Kuper and Ryan Newton on [lattice variables](https://dl.acm.org/citation.cfm?id=2502326) (LVars), which represent increasing knowledge about the value contained in a variable. Vijay Saraswat's [concurrent constraint programming](https://dl.acm.org/citation.cfm?id=96733) (CCP) seems to give a broad framework for studying programs that operate over such domains of increasing knowledge. I'm absolutely _fascinated_ by this topic, and I quite badly want to find something to contribute to the field. (The LVars paper was arguably one of the main reasons I became a Ph.D. student!) The CCP approach is quite a pure kind of logic programming, whereas the LVars approach includes some functional aspects as well. I think there's some serious category theory underlying all of this (especially CCP), but I'm just not familiar enough with category theory to see it.`

Re the comment about "three layers" - we got code for all three layers, and generating the schedule layer from the recipe layer. Also got a few slide decks describing it, short long

Been used by several groups. Big and messy. I'm simplifying it to generate these cytoscape graphs and will try to categorize everything at least on the "observations of what happened" layer by June 4 with some readable code running on the Web.

`Re [the comment about "three layers"](https://forum.azimuthproject.org/discussion/comment/18511/#Comment_18511) - we got code for all three layers, and generating the schedule layer from the recipe layer. Also got a few slide decks describing it, [short](https://speakerdeck.com/mikorizal/salsa-recipe-plan-reality) [long](https://speakerdeck.com/mikorizal/5-nrp-recipe-concepts-and-tutorial) Been used by several groups. Big and messy. I'm simplifying it to generate these cytoscape graphs and will try to categorize everything at least on the "observations of what happened" layer by June 4 with some readable code running on the Web.`

Hey Jonathan Castello,

Melvin Fitting has a 1989 paper on semantics for logic programming via Belnap's four value logic. Fitting observes that Belnap's four value logic is just a special case of a

bilattice.I am not familiar with CCP, but it appears to be akin to CCS? If so, you might want to check out Milner's

Action Structures and the π-Calulus(1995). There are various categorical semantics for CCS. John Baez has n-Category Lab blog post from 2009 with a bibliography. Also, John's former student Mike Stay wrote a PhD thesis on category theory and π-Calulus in 2015 so that's worth a look. John also has a blog post from 2016 discussing applying the π-calculus to biology.`Hey [Jonathan Castello](https://forum.azimuthproject.org/discussion/comment/18523/#Comment_18523), Melvin Fitting has a [1989 paper](http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/BilSemLP.pdf) on semantics for logic programming via Belnap's four value logic. Fitting observes that Belnap's four value logic is just a special case of a *bilattice*. I am not familiar with CCP, but it appears to be akin to [CCS](https://en.wikipedia.org/wiki/Calculus_of_communicating_systems)? If so, you might want to check out Milner's [*Action Structures and the π-Calulus* (1995)](https://link.springer.com/chapter/10.1007/978-3-642-79361-5_8). There are various categorical semantics for CCS. John Baez has n-Category Lab [blog post from 2009](https://golem.ph.utexas.edu/category/2009/08/the_pi_calculus.html) with a bibliography. Also, John's former student Mike Stay wrote a [PhD thesis on category theory and π-Calulus in 2015](http://math.ucr.edu/home/baez/thesis_stay.pdf) so that's worth a look. John also has a [blog post from 2016](https://johncarlosbaez.wordpress.com/2016/01/02/biology-and-the-pi-calculus/) discussing applying the π-calculus to biology.`

Hmm, bilattices as defined by Melvin Fitting are interesting! A bilattice is just a set with a pair of partial orderings, each making it into a lattice, with the meet and join operations of either one being monotone with respect to the other one.

I feel there should be a more elegant way to state this idea using more category theory, but I'm not getting it. I believe a "lattice object in the category of lattices" works out to be just a lattice again - the compatibility conditions are so strong that the two lattice structures are forced to coincide.

`Hmm, bilattices as defined by Melvin Fitting are interesting! A bilattice is just a set with a pair of partial orderings, each making it into a lattice, with the meet and join operations of either one being monotone with respect to the other one. I feel there should be a more elegant way to state this idea using more category theory, but I'm not getting it. I believe a "lattice object in the category of lattices" works out to be just a lattice again - the compatibility conditions are so strong that the two lattice structures are forced to coincide.`

I haven't had the time to really dig into the references you've provided, Matthew, but I'm super interested! I just started reading Fitting's bilattice paper, and I like what I see so far.

One minor thing that bothers me at the moment (I'm currently up to section 2) is that a truth-ordering is assumed to be present. If we consider the lattice with \(\bot \le x \le \top\) for all \(x\) in some fixed set \(S\), there is no obvious need for a truth-ordering, even though the knowledge-ordering makes just as much sense as for

Belnap4. But I suspect the codiscrete preorder would work just as well here.In fact, it occurs to me that the truth-ordering is mostly necessary for defining the logical operations on booleans; so if you don't intend to perform operations using your data, but merely intend to

add knowledgeto existing data, then the codiscrete preorder is all you need. Whatever operations you define on your data must act on some lattice structure compatible with the knowledge ordering in order to guarantee the existence of least fixed points -- and perhaps that's all there is to it.Must read more!

`I haven't had the time to really dig into the references you've provided, Matthew, but I'm super interested! I just started reading Fitting's bilattice paper, and I like what I see so far. One minor thing that bothers me at the moment (I'm currently up to section 2) is that a truth-ordering is assumed to be present. If we consider the lattice with \\(\bot \le x \le \top\\) for all \\(x\\) in some fixed set \\(S\\), there is no obvious need for a truth-ordering, even though the knowledge-ordering makes just as much sense as for **Belnap4**. But I suspect the codiscrete preorder would work just as well here. In fact, it occurs to me that the truth-ordering is mostly necessary for defining the logical operations on booleans; so if you don't intend to perform operations using your data, but merely intend to _add knowledge_ to existing data, then the codiscrete preorder is all you need. Whatever operations you define on your data must act on some lattice structure compatible with the knowledge ordering in order to guarantee the existence of least fixed points -- and perhaps that's all there is to it. Must read more!`

Followup to https://forum.azimuthproject.org/discussion/comment/18530/#Comment_18530

Got the code for the "what happened" layer cleaned up, fixed a bug, and deployed here: http://valueflows.pythonanywhere.com/vocab/egg2worm-flow/

Code is here: https://github.com/valueflows/django-vocabulator

Not yet categorized, working on that today. Where should I take this stuff next?

`Followup to https://forum.azimuthproject.org/discussion/comment/18530/#Comment_18530 Got the code for the "what happened" layer cleaned up, fixed a bug, and deployed here: http://valueflows.pythonanywhere.com/vocab/egg2worm-flow/ Code is here: https://github.com/valueflows/django-vocabulator Not yet categorized, working on that today. Where should I take this stuff next?`

I recommend that people good at coding and category theory talk to Ryan Wisnewsky. He recently joined Azimuth, and his self-introduction says this.

My name is Ryan Wisnesky, and I worked as David Spivak's postdoc to create both a company and open source project that implements the 'schemas as categories' idea in working software, called AQL. Seeing as how the seven sketches course is now reaching the database portion, I wanted to say hi and also solicit community involvement in the CI and CatData projects - see below.

Categorical Informatics (CI) (http://catinf.com), a data modeling/integration/migration company pioneering a new approach to data based on category theory, is looking to recruit an initial technical staff as it moves from grant-based to angel-based funding. CI was spun out of the MIT math department in 2015 by David Spivak (http://math.mit.edu/~dspivak/) and Ryan Wisnesky (http://wisnesky.net) and maintains an open-source data integration tool, AQL, available at http://catinf.com/download.php .

In CI's approach to data, a database schema is a finitely presented category C and a database instance on C is a set-valued functor C -> Set. The instances on C form a category (indeed, a topos), C-Inst, a functor F from C to another finitely presented category D (so F : C -> D) induces three adjoint data migration functors: Delta_F : D-Inst -> C-Inst, Pi_F : C-Inst -> D-Inst, and Sigma_F : C-Inst -> D-Inst. These data migration functors provide an alternative basis of operations for querying data (compared to SQL) and migration/integrating data (compared to

`the chase`

algorithm). At a high level, the objects of C correspond to entities (e.g., Employee, Department, etc), the generating morphisms of C correspond to foreign keys / functions (e.g., worksIn : Employee -> Department, manager : Department -> Employee), and the generating equations of C correspond to data integrity constraints (e.g., manager ; worksIn = id)The connections to functional programming and database theory are significant and are discussed in a series of papers available at http://categoricaldata.net/fql.html . For example, the query language obtained from delta/sigma/pi can be written using 'SQL-ish' notation, and reasoning about schemas and functors requires use of automated theorem proving methods (e.g., Knuth-Bendix completion).

CI is interested in talking with people who have backgrounds in - category theory - type theory / functional programming - automated theorem proving - database internals / SQL at scale

Please send inquiries to ryan@catinf.com

`I recommend that people good at coding and category theory talk to [Ryan Wisnewsky](https://forum.azimuthproject.org/discussion/2217/introduction-ryan-wisnesky/p1). He recently joined Azimuth, and his self-introduction says this. --- --- My name is Ryan Wisnesky, and I worked as David Spivak's postdoc to create both a company and open source project that implements the 'schemas as categories' idea in working software, called AQL. Seeing as how the seven sketches course is now reaching the database portion, I wanted to say hi and also solicit community involvement in the CI and CatData projects - see below. --- Categorical Informatics (CI) (http://catinf.com), a data modeling/integration/migration company pioneering a new approach to data based on category theory, is looking to recruit an initial technical staff as it moves from grant-based to angel-based funding. CI was spun out of the MIT math department in 2015 by David Spivak (http://math.mit.edu/~dspivak/) and Ryan Wisnesky (http://wisnesky.net) and maintains an open-source data integration tool, AQL, available at http://catinf.com/download.php . In CI's approach to data, a database schema is a finitely presented category C and a database instance on C is a set-valued functor C -> Set. The instances on C form a category (indeed, a topos), C-Inst, a functor F from C to another finitely presented category D (so F : C -> D) induces three adjoint data migration functors: Delta_F : D-Inst -> C-Inst, Pi_F : C-Inst -> D-Inst, and Sigma_F : C-Inst -> D-Inst. These data migration functors provide an alternative basis of operations for querying data (compared to SQL) and migration/integrating data (compared to `the chase` algorithm). At a high level, the objects of C correspond to entities (e.g., Employee, Department, etc), the generating morphisms of C correspond to foreign keys / functions (e.g., worksIn : Employee -> Department, manager : Department -> Employee), and the generating equations of C correspond to data integrity constraints (e.g., manager ; worksIn = id) The connections to functional programming and database theory are significant and are discussed in a series of papers available at http://categoricaldata.net/fql.html . For example, the query language obtained from delta/sigma/pi can be written using 'SQL-ish' notation, and reasoning about schemas and functors requires use of automated theorem proving methods (e.g., Knuth-Bendix completion). CI is interested in talking with people who have backgrounds in - category theory - type theory / functional programming - automated theorem proving - database internals / SQL at scale Please send inquiries to ryan@catinf.com`

@Bob You might like to initiate the Applied Category Theory repo which somebody has created on the Azimuth code project's github. If anybody with relevant code want commit rights then if they post a github name here or as an issue one of us can add you to the "organisation" as a committer.

azimuth-project

NB 'azimuth-project' is an organisation not a repo or user so the github search box won't find it afaict. Grrr...

`@Bob You might like to initiate the Applied Category Theory repo which somebody has created on the Azimuth code project's github. If anybody with relevant code want commit rights then if they post a github name here or as an issue one of us can add you to the "organisation" as a committer. [azimuth-project](https://github.com/azimuth-project/applied-category-theory-course) NB 'azimuth-project' is an organisation not a repo or user so the github search box won't find it afaict. Grrr...`

Jim

Thanks for the offer, but I fear it is too early. My ultimate goal with this first step was to be able to categorize the 3 layers of resource flows - recipe (design), plan/schedule, observations of what happened - which are all related and mappable to each other. I got code for all 3 layers but it is huge and messy. I just cleaned up the observation layer and am working on categorizing that. I can post more somewhere if anybody is interested.

Once I get the first layer categorized, and get some feedback and probably some correction of my errors, I could add appropriate comments to the code, and drop it in that repo if it fits.

`[Jim](https://forum.azimuthproject.org/discussion/comment/19132/#Comment_19132) > You might like to initiate the Applied Category Theory repo Thanks for the offer, but I fear it is too early. My ultimate goal with this first step was to be able to categorize the 3 layers of resource flows - recipe (design), plan/schedule, observations of what happened - which are all related and mappable to each other. I got code for all 3 layers but it is huge and messy. I just cleaned up the observation layer and am working on categorizing that. I can post more somewhere if anybody is interested. Once I get the first layer categorized, and get some feedback and probably some correction of my errors, I could add appropriate comments to the code, and drop it in that repo if it fits.`

@Jim I'd like to commit some code. Name is Cobord to add to the organization.

`@Jim I'd like to commit some code. Name is Cobord to add to the organization.`

Hi @Amar, I'll try and do it Thurs am BST.

`Hi @Amar, I'll try and do it Thurs am BST.`

@Amar I've apparently sent you an invite to be an owner - so you can commit code to extend any of the existing projects - and a member of "core" whatever that is.

`@Amar I've apparently sent you an invite to be an owner - so you can commit code to extend any of the existing projects - and a member of "core" whatever that is.`

I added Grant Roy to GitHub a few days ago - he's the one who first contacted me about using GitHub for matters related to this course - but I didn't make him an "owner", out of some (perhaps misplaced) sense of caution. I guess an "owner" can do stuff like delete all our previous projects, perhaps by accident. But maybe they're automatically backed up and hard to truly delete?

`I added Grant Roy to GitHub a few days ago - he's the one who first contacted me about using GitHub for matters related to this course - but I didn't make him an "owner", out of some (perhaps misplaced) sense of caution. I guess an "owner" can do stuff like delete all our previous projects, perhaps by accident. But maybe they're automatically backed up and hard to truly delete?`

I have them all archived :).

`I have them all archived :).`

Should I change to contributor instead of owner? Or anything I may commit can be in a separate branch, before they get merged to the master branch.

`Should I change to contributor instead of owner? Or anything I may commit can be in a separate branch, before they get merged to the master branch.`

From https://www.scuttlebutt.nz/ where we had a category theory study group for awhile (until this class started):

and in another comment from a different person:

`From https://www.scuttlebutt.nz/ where we had a category theory study group for awhile (until this class started): > The encoding function should be a function from these values to byte buffers, and it needs to have the following properties: > * actually be a (total) function (each value has exactly one encoding) > * be injective (different values produce different encodings) > * have an inverse function (aka decoding) > * the inverse function is injective (different encodings decode to different values) > > The current system does not have all of these, so doing the same stuff, just more efficient, won't make things any better. Maybe faster, but still fundamentally broken. and in another comment from a different person: > Bijections with json get tricky, because, well, json. I'd argue that we don't actually want bijections between encoding and json, but between encoding and javascript values.`

Okay thinking abstractly about what you are doing.

That is we have a serialization of js values into json, which we then parse into correct encodings, which we use the identity serialization into bits on.

Going the other way we "parse" (check) the bits into encodings, then serialize into json, then parse into js values.

And we want the part from js to valid encodings to be a bijection, even though it's parts aren't.

I'm over thinking this aren't i?

`Okay thinking abstractly about what you are doing. That is we have a serialization of js values into json, which we then parse into correct encodings, which we use the identity serialization into bits on. Going the other way we "parse" (check) the bits into encodings, then serialize into json, then parse into js values. And we want the part from js to valid encodings to be a bijection, even though it's parts aren't. I'm over thinking this aren't i?`

@Amar I think it's v. improb. that somebody who joins the Azimuth and has code to post will trash the azimuth-project repo. I'd be very happy if somebody pushed their own commits to improve my toy code. I've got your back covered so don't demote yourself :).

`@Amar I think it's v. improb. that somebody who joins the Azimuth and has code to post will trash the azimuth-project repo. I'd be very happy if somebody pushed their own commits to improve my toy code. I've got your back covered so don't demote yourself :).`

Christopher that seemed accurate to me.

Those quotes were from two people who participated in a category theory study group earlier this year and now have started using the concepts to analyze some of their problems. I thought the working hackers would appreciate more hackers hacking categorically. Or at least trying to do so...

`[Christopher](https://forum.azimuthproject.org/discussion/comment/19262/#Comment_19262) that seemed accurate to me. Those quotes were from two people who participated in a category theory study group earlier this year and now have started using the concepts to analyze some of their problems. I thought the working hackers would appreciate more hackers hacking categorically. Or at least trying to do so...`

Looks like the working hackers are too busy working...

In Chapter 4 we're talking about profunctors now. When I mentioned this on Twitter, Dan Piponi showed me this:

I It turns out that Dan Piponi first introduced profunctors in Haskell and they've subsequently caught on. I didn't know that, and it wasn't visible from the webpage above, but on Twitter Dan Piponi wrote:

and Bartosz Milewski responded:

`Looks like the working hackers are too busy working... In Chapter 4 we're talking about profunctors now. When I mentioned this on Twitter, Dan Piponi showed me this: * Dan Piponi, [Profunctors in Haskell](http://blog.sigfpe.com/2011/07/profunctors-in-haskell.html?m=1). I It turns out that Dan Piponi first introduced profunctors in Haskell and they've subsequently caught on. I didn't know that, and it wasn't visible from the webpage above, but on Twitter Dan Piponi wrote: > think I was the first to implement a Profunctor type class in Haskell. But I didn't anticipate how useful it'd turn out to be. and Bartosz Milewski responded: > Profunctors are the basis of the whole optics library in Haskell (lenses, prisms, grates, etc.). Guillaume Boisseau and @jer_gib wrote a great paper about it: [https://www.cs.ox.ac.uk/jeremy.gibbons/publications/proyo.pdf](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/proyo.pdf)`

That is a fascinating paper.

`That is a fascinating paper.`

Here's a question to the group: Since we can correspond programs in computer science with certain mathematical proofs in category theory, can we produce quines (a non-empty/inhabited computer program which takes no input and produces a copy of its own source code as its only output) in category theory?

`Here's a question to the group: Since we can correspond programs in computer science with certain mathematical proofs in category theory, can we produce quines (a non-empty/inhabited computer program which takes no input and produces a copy of its own source code as its only output) in category theory?`

Well I think for a quine to make sense we need a programming language, and the ability to talk about the source in the quine.

So I think a quine and a Godle(sp?) sentence are closely related.

`Well I think for a quine to make sense we need a programming language, and the ability to talk about the source in the quine. So I think a quine and a Godle(sp?) sentence are closely related.`

I think it should be in theory possible.

A quine is a program that has two parts,

the actual program that takes a representation of a program, copies it, and then executes either the original or the copy.

a representation of the above program.

`I think it should be in theory possible. A quine is a program that has two parts, - the actual program that takes a representation of a program, copies it, and then executes either the original or the copy. - a representation of the above program.`