web cats · theory: applied category theory

Moving the thread on the general stream to Applied Category Theory stream.
This is how that thread started on 02 April.

Henry Story (Jul 27 2020 at 11:15):

Now that I have experience with Zulip chat, I think this is a good place to have these discussions, on Category Theory applied to the World Wide Web.

Currently I am working with @Ryan Wisnesky on mappings between his work on Categorical Databases and RDF using his CQL tool written in Java and also some libraries I am writing in Scala. A great way to learn.

Here is an interesting question which had a bit of traction recently:
Is OWL/RDF typed or Untyped? I can come up with quite a lot of other questions regarding protocols, coalgebras, game theory, etc...

Antonin Delpeuch (Jul 27 2020 at 18:14):

Antonin Delpeuch (Jul 27 2020 at 18:18):

I am also working on semantic web related tools (OpenRefine, Wikidata) and involved in a W3C community group (https://www.w3.org/community/reconciliation/), but most of that is unrelated to CT.

Henry Story (Jul 27 2020 at 20:36):

Yes the banana-rdf libraries are available on github. They use Scala's Path Dependent Types to encode a type abstraction of RDF types, so that one can then write RDF code independently of implementations (Jena, Rdf4J, JavaScript libs) without needing to wrap the Java objects in an extra layer. (see GraphTest.scala for an example) So you can change between Jena and Sesame in one line of code, and also compile to JS.
(but that last part needs more work).

Antonin Delpeuch (Jul 28 2020 at 19:51):

Henry Story (Jul 31 2020 at 07:42):

I am about to implement OWL2-RL in CQL. OWL2 RL is the rule language fragment of the W3C Description Logic framework OWL (Ontology Web Language). CQL is exactly right for that fragment.

Henry Story (Aug 02 2020 at 12:28):

A simple question for category Theorists.
We know that

s,t: A \to B

represents a small category that induces functors to

Set

each picking out a graph.
What do the following produce? Where does one find them used?

Nathanael Arkor (Aug 02 2020 at 13:50):

Henry Story (Aug 02 2020 at 14:02):

It would be quite interesting to see if that meshes with the experience of RDF. Ie. If some fundamental properties of RDF are related to uniform hypergraphs. (if that is indeed the correct way to render the above shapes)

Tim Berners-Lee and Dan Conolly told me that in their implementation of the cwm reasoner, they ended up with quints, which allowed them (if I remember correctly but it's a long time ago) to follow paths of reasoning. It would be nice if that just falls out of a small category

s,t,u,v,w: A \to B

or if they were speaking of something else.

Henry Story (Aug 10 2020 at 15:26):

I am trying to find the right words for the type of symmetry between a server publishing an Access Control Rule for a Resource, and a client that needs to know the rules for access in order to authenticate. The symmetry is not one of knowledge since parts of the access control rules may be hidden. It is a symmetry in the rules of the games perhaps. (There is a discussion here on this topic for reference). Perhaps there is a duality there.
It reminds me of the duality in roles described in a couple of papers (I reference there) in the literature on dialogical logic between the person making a claim and the person trying to refute it. But there is the added dimensions that parts of the rules may be hidden: eg an ACL may say that only members of a group can have access but the members of the group be hidden. (If they are hidden the client will know it cannot access it)

Henry Story (Aug 29 2020 at 11:19):

I put together a presentation giving the intuitions of how RDF relates to functors from the small category

s,r,o: A \to N

to Set and

s,r,o,g: A \to N

to Set. These do seem to be related to hyper graphs, but the way those are presented it is not yet obvious. Is there a paper that is closer to the presentation I am giving here?
SemWeb-as-Cats.key.pdf

Henry Story (Aug 29 2020 at 18:03):

Henry Story (Sep 01 2020 at 16:11):

There could be some work for mathematicians to prove that existing RDF graph normalization schemes are correct or finding more optimal ones. These are needed for a number of different applications of which signing RDF graphs (ie the 3 and 4 uniform hypergraphs mentioned above). See Ivan Herman post to the w3c semantic web mailing list. He's probably a good person to contact.

Henry Story (Sep 11 2020 at 16:31):

I was trying to formalize RDF Literals (and so XML Datatypes) and it occurred to me that those look very much like dependent types, in particular

\Sigma

types. Indeed a Literal in RDF presents itself as a pair of a String and a URI. So in NTriple, Turtle, NQuad or N3 notation a Literal is written as "..."^^<...> where the first hole is filled in with a Unicode character string and the second hole is filled in with a IRI (an International Resource Identifier - a generalization of URIs to Unicode themselves a generalization of the URLs we use every day). So one could represent it as a pair

\text{String} \times \text{IRI}

. But really the types of strings that are legal depend on the IRI. So the xsd:dateTime IRI gives a result only for strings that have a certain format, e.g. "2002-10-10T12:00:00+05:00" .
So if we take IRI's to be a type in the HoTT universe

\text{IRI} : \mathcal{U}

, then we also have a family of types

\text{Lit}: \text{IRI} \to \mathcal{U}

where we could think of the type selected by the first IRI to be a set of legal strings for that type. Those pairs could then be mapped to the correct type (eg, a DataTime type with its own identity criteria). Doing this we would be able to match more precisely the intent of RDF Literals, and we would also end up with pairs

(u,s): (u: \text{IRI}) \sum\ Lit(u)

The other way to present these is the much less satisfactory way of defining Literals as subsets of

\text{String} \times \text{IRI}

. It is correct but it does not really say what subsets are valid.

This is interesting if true, as it means that Dependent Types appear in foundational elements web data technologies. I wonder how I need to model this using cc @David Spivak's Functorial DBs.

Earlier this year I wrote up some other places dependent types turn up on the Web having read @David Corfield's modal HoTT book.

Henry Story (Sep 18 2020 at 14:47):

Watching Andrei Bauer's series of talks on Proof assistants I came across this one MMT: Meta Meta Model Tool by Florian Rabe. His project is to find a way of translating results between all the different proof assistants. His description how far they got and the difficulty of the task is quite sobering. Some of the tasks they hope to be able to achieve is to be able to build a search engine of proofs. But even that is daunting. They seem to have RDF output, from one of the slides, as the interchange format.
Andrei at one point asks how come Mathematicians seem to be able to communicate their results among each other, given the difficulty of doing this between proof assistants.

MMT = Meta Meta Model Tool Is the project that attempts to provide a bridge between all the different proof assistants, developing something like a Math Interchange Format. Written in #Scala (producing #RDF?). https://kwarc.info/people/frabe/ See talk https://vimeo.com/421123419 https://twitter.com/bblfish/status/1306951592374042624/photo/1

- The 🐟‍‍ BabelFish (@bblfish)

Valeria de Paiva (Sep 18 2020 at 14:52):

Well evolution shaped "language" for hundreds of thousands of years. Language is a very powerful tool, and polysemy is a feature, not a bug. (a feature we haven't quite mastered yet, but a feature)

Henry Story (Sep 18 2020 at 14:56):

In the talk Rabe admits (and @Andrej Bauer agrees) that type theory may not be as close to mathematical practice as he initially thought.
I wonder if Category Theory is here closer to mathematical practice, as its basic concept of that of an arrow is so flexible. (I am not a mathematician, so I can't tell)

Henry Story (Sep 18 2020 at 15:07):

MMT seems takes URL at their core see their URIs page. I think the claim made about their URL format being the right way of doing things is incorrect, but fixing that would be relatively easy to do. (Actually part of my thesis is to explain how URLs are meant to work).

Henry Story (Sep 18 2020 at 17:06):

Jacques Carette (Sep 18 2020 at 19:08):

Because of the large gap between the theory and practice. For example, a result of 'institution theory' is that the category of signatures has pushouts. This is true, but essentially unimplementable: there are no canonical pushouts, as computing them requires making choices of names. In theory, that's fine. In practice, that's doomed, as it means that when you get a new theory via a pushout, you don't actually have any concrete means to refer to what's in it.

There are ways around that, and most systems that claim to be based on institution theory do some mighty horrible hacks to get there.

And that's just the start. Many operations from institution theory are not computable. That means that you can define all sorts of things, but then you can't have any computer help to check your work. [This is why people doing programming languages and proof checkers insist on decidable type checking.] Examples of further issues: 1) deleting an item from a theory, 2) saying that your theory denotes the initial model. Neither of these can be exhibited syntactically (in general).

BTW, Rabe knows institution theory very well, has written papers about it, and is good friends with people whose main work is all in institution theory. The choice was quite deliberate. [I've also published with Florian, we've worked together for a number of years.]

Valeria de Paiva (Sep 18 2020 at 19:19):

well I also have a paper with Florian Rabe (An Institutional View of Categorical Logic and the Curry-Howard-Tait Isomorphism (with Joseph Goguen, Till Mossakowski, Florian Rabe, and Lutz Schröder). In Int J Software Informatics, 1 (1), pp. 129–152, 2007) on why abstract Categorical Proof Theory and not abstract Model theory (Institutions) is necessary for mathematics.

Henry Story (Sep 18 2020 at 20:10):

I was wondering why there had not been that many publication on institution theory after 2008 or so.

Jacques Carette (Sep 18 2020 at 20:17):

Henry Story (Sep 18 2020 at 20:36):

thanks! I was looking a 3 years ago. Perhaps I was focusing my search on what Institution Theory had to say on Modal Logic. (My maths may not have been good enough to pick on things at the time).

Henry Story (Sep 19 2020 at 06:50):

Florian Rabe's talk on MMT whose long term goal is to provide a framework to allow exchange of proofs between the many different Proof Assistants made me think of this quote by @David Corfield in his book "Modal HoTT"

That made me wonder if Modal HoTT is not aiming at something very similar on the theoretical side to what Florian is doing. HoTT I think it would be fair to say subsumes quite a large space of logics. But just watching Andrei Bauer's series on Cubical HoTT implementations shows that there are few different cubical HoTT Proof Assistants built on different models already. Could it be that Modal HoTT would be a way to create morphisms (ie translations) between these and other models? Would there be any logics of interest to Florian not covered by this?

This would still leave the question of the interchange format between the Proof Assistants of course (which I think of as in the space of web technologies).

David Corfield (Sep 19 2020 at 09:53):

If we can use the terms of Mike Shuman's n-theory idea (https://golem.ph.utexas.edu/category/2018/04/what_is_an_ntheory.html), versions of HoTT would be instances of 2-theories. There may well be 2-morphisms between them. Mention of modal HoTT introduces the possibility of translation via adjunctions of 1-theories written in a HoTT 2-theory. It's probably easier to choose a simpler modal 2-theory such as modal propositional logic. We could specify a 1-theory here which would have a model whereby there are two Boolean algebras related by adjunction generating modalities. For instance, one could think of the possibility modality which sends a proposition, X, to the proposition, P ->X, for a fixed P. This is to mediate between two inference spaces where one has the advantage of being able to use P.

David Corfield (Sep 19 2020 at 09:56):

Henry Story (Sep 19 2020 at 10:55):

:thinking: The idea of n-levels does have a family resemblance with the levels suggested by the name Meta Meta Theory (MMT).

Henry Story (Sep 19 2020 at 14:55):

Re Institutions I found a 2010 article by Florian Rabe The Future of Logic: Foundation Independence which shows how his project was related or even emerging out of Institution Theory.

John Baez (Sep 19 2020 at 15:04):

Jules Hedges (Sep 19 2020 at 15:11):

It's possible this is one of those questions where you would get an economics Nobel for answering it convincingly

Henry Story (Sep 19 2020 at 15:26):

It is a category theoretic way to think of all logics together. Copied from nlab:

Henry Story (Sep 19 2020 at 15:32):

It certainly is impressive to have such a reasonably short framework cover so much if not all of logics.

Jacques Carette (Sep 19 2020 at 15:36):

@Henry Story gave the formal definition. The intuition is that it is a way to work with an abstract satisfaction relation. Whether you want to deal with provability or truth (or some other thing) over some class of abstract structures, institutions aim to be a setting for you to do that in. For things to work, you need a basic vocabulary (signatures), ways to compose those signatures into sentences (the S functor), a way to pick out 'structures' over the vocabulary, and ways to pick out which sentences about structures you'd like to consider as theorems.

Henry Story (Sep 19 2020 at 15:36):

Nathanael Arkor (Sep 19 2020 at 15:37):

It's impressive if you can prove useful results with such a concise framework. Simply covering a wide range of logics (without being able to prove anything) is easy.

Nathanael Arkor (Sep 19 2020 at 15:38):

(I presume institutions can be used to prove useful results: I just wanted to point out there's a worthwhile distinction there.)

Henry Story (Sep 19 2020 at 15:46):

@Jacques Carette when where those problems you mentioned further up about Institution Theory recognised?

Jacques Carette (Sep 19 2020 at 15:53):

AFAIK, the adherents of institution theory have not, yet. Basically because the overlap between people able to do work at that level of generality tend to not be implementors. It's not that they can't write code, they just rarely do. And these problems only become clear when you implement.

The same thing is true regarding people who use category theory in software specifications and in other places. If you dig hard into what they actually do, they really want skeletal strict categories. And that does not really agree with the modern take on category theory.

Whenever you see any setup that involves 'named objects' and then later all pushouts/pullbacks exist, you know something has gone awry and the theory won't translate well to concrete computations.

Henry Story (Sep 19 2020 at 16:06):

Institution Theory comes with a notion of functors between institutions, which are meant to act as translators between different logics and specification languages.

Could it be useful if used as a map then perhaps? So then it would allow one to know how the different logics fit together in a common framework. A bit like knowing where the galaxies around us lie, even though we won't be going there soon. That would already be quite useful given the huge number of logics out there...

Henry Story (Sep 19 2020 at 17:35):

In Rabe's 2010 paper/pamphel "The future of Logic: Foundation Independence" he does write

Jacques Carette (Sep 19 2020 at 18:11):

As far as I know, this is not (currently) useful. The reason is that each logic translation, currently, needs to be built by hand. We don't have great tools (outside of the cases when we have conservativity results) to build logic translations. Institution theory takes them as given, and goes on from there.

An analogy: it's like assuming that you have an elliptic curve of a particular rank, and then going on from there. The problem is, our methods for exhibiting actual curves of certain ranks are not good. So such results are only useful in theory, even though they are sometimes claimed to be useful in practice.

John Baez (Sep 19 2020 at 19:54):

That doesn't tell me what an institution is, just points in the general direction.

John Baez (Sep 19 2020 at 19:55):

Later it says more, but it's sort of rambling and chatty, in a way that makes it hard to see exactly what the concept is.

Jacques Carette (Sep 19 2020 at 19:55):

??? Henry gave the formal definition a few messages ago, and I gave an intuitive definition after that.

John Baez (Sep 19 2020 at 19:55):

John Baez (Sep 19 2020 at 19:58):

John Baez (Sep 19 2020 at 20:01):

Given a morphism of signatures

\varphi:X\to X'

and a sentence

e\in S(X)

, the sentence

S(\varphi)(e)

i.e. the "

\varphi

-translation" of

e

into an

X'

-sentence, holds in a X'-structure

\mathfrak{A}'

iff

e

holds in

M(\varphi)(\mathfrak{A}')

John Baez (Sep 19 2020 at 20:03):

So I guess a signature could for example be a set of free variables, with a map of signatures being an arbitrary function between such sets. Then the functoriality of

S

says that sentences behave nicely under substitution of free variables.

John Baez (Sep 19 2020 at 20:04):

M

would then gives the category of models that involve the given free variables.

John Baez (Sep 19 2020 at 20:07):

It's interesting to compare all this to traditional model theory, which has its own concepts of signature, structure, and satisfaction.

John Baez (Sep 19 2020 at 20:07):

Jacques Carette (Sep 19 2020 at 20:08):

A signature is closer to a set of (typed) generators and relations typically. Terminology comes from algebraic specifications - see for example https://www.cs.vu.nl/~eliens/oop/@text-8-2.pdf (first 2 pages).

John Baez (Sep 19 2020 at 20:09):

I don't know anything about "algebraic specifications", but I know the concept of signature in model theory, and I feel that should be a special case of this business. I guess you could say in model theory a signature has "generators" but no "relations".

Jacques Carette (Sep 19 2020 at 20:11):

Yes, it is supposed to be a generalization of both situations. And algebraic specifications are really an outgrowth of universal algebra, but done by/for computer scientists.

John Baez (Sep 19 2020 at 20:20):

Valeria de Paiva (Sep 20 2020 at 00:30):

Beg to differ: they only do a bit of what I want a logic to do. As I was saying above, institutions allow you to do some kind of categorical model theory, not categorical proof theory. Satisfaction relations are only about theorems in your logic, we want to know about different proofs of theorems, we want to model derivations, not only whether something holds or not. At the end of the day, you do want to have both categorical model theory and categorical proof theory and we don't have that, as far as I can see, yet.

Jacques Carette (Sep 20 2020 at 12:15):

Henry Story (Sep 22 2020 at 12:31):

There was a very interesting thread on Twitter which started out discussing Institution Theory where @Valeria de Paiva expressed the same doubts about IT as above that it only deals with satisfaction relations but not with proofs so then I asked if she had looked at Modal HoTT that @David Corfield mentioned above indirectly.
https://twitter.com/valeriadepaiva/status/1308077885941407744

Yes, I have had a look. what I don't like about it is that the modalities are all of the S4-shape, while logicians prefer a less committed style of modality. https://twitter.com/bblfish/status/1308055431714144261

- Valeria dePaiva (@valeriadepaiva)

Henry Story (Sep 22 2020 at 12:33):

To this @Alex Kavvos pointed to research by @Mike Shulman pointing to the potential source of trouble in HoTT. Something that Spatial Type Theory could be solving. (I think that's part of Modal HoTT but I am not sure)
https://twitter.com/lambdabetaeta/status/1308098428212260867

@valeriadepaiva The commitment to S4 comes from a very particular place, which is axiomatic cohesion - used as technology to relate topology to homotopy. A fun and inspiring paper: https://arxiv.org/abs/1509.07584

- Alex Kavvos (@lambdabetaeta)

Henry Story (Sep 22 2020 at 12:37):

As I understand glancing at the paper (I have to finish something for work) the Spatial Type Theory brings topology back into HoTT which only has homotopy. I guess this could allow one to express David Lewis' Counterfactual Logic of nested spheres of worlds enoding a distance relation between them. With only Homotopy these would otherwise collapse, giving us thus only S4.
(If my guesses are correct, then this is super interesting, perhaps enough to allow me to overcome the himalayan learning curve of maths)
https://twitter.com/bblfish/status/1308316070881759232

@lambdabetaeta @valeriadepaiva Could one express Shulman's paper in terms David Lewis would understand? Namely: HoTT cannot express the differences of the nested spheres from "Counterfactuals", as it collapses them, giving us S4. But with Modal HoTT we can, see: https://arxiv.org/abs/1509.07584 https://twitter.com/bblfish/status/1308236842836385792

- The 🐟‍‍ BabelFish (@bblfish)

Valeria de Paiva (Sep 22 2020 at 13:50):

@Henry Story it's the other way round: I'm complaining that institutions only deal with satisfaction relations, not with proofs.

Valeria de Paiva (Sep 22 2020 at 14:01):

well, I'm not an expert in Lewis' counterfactual logic, but from what I dimly remember there's nothing too deep about its semantics: it's just another kind of Kripke semantics--hence proof-irrelevant-- where the set of worlds happens to be spheres. Lewis Philosophy is impressive, the maths not so much, if memory does not fail me. or maybe I had a particularly clear teacher.

Henry Story (Sep 22 2020 at 14:02):

Arg! You are right @Valeria de Paiva I fixed the text above.
(The editors can delete both this exchange for clarity if needed)

Henry Story (Sep 22 2020 at 14:09):

Yes, you are right about the lack of proof relevance in Lewis' Counterfactuals. That is why I was looking to see what the advances were in modal logic over the past 45 years to see what modern tools I could use to get the same effect. I asked a question on the HoTT café 5 years ago re Lewis as I could not quite see how HoTT got us there. This current thread seems to point to an answer. If I interpret it correctly Spatial Type Theory (Modal HoTT?) could give us a proof relevant Counterfactuals. Then I could develop the argument from Epistemology in the Cloud using a future Modal HoTT proof assistant :-) (I am assuming HoTT is proof relevant in the way you are thinking of it)

Mike Shulman (Sep 22 2020 at 15:26):

I'm not sure what you mean by that. Modal HoTT includes theories with all kinds of modalities. Spatial type theory with its

\sharp

and

\flat

modalities is just one particular instance.

Rich Hilliard (Sep 22 2020 at 15:45):

@Valeria de Paiva asked about proof theory in institutional setting.
I vaguely recall Goguen and Burstall later took a syntactic approach to Institutions with "parchments" and "charters". I don't know whether proof theory was in their minds.
Also Diaconescu's book (Institution independent model theory?) tackles proofs in one chapter.

Valeria de Paiva (Sep 22 2020 at 16:13):

Sorry I have not asked, I said they don't do proof theory. my paper on that is with Joe Goguen and was published with him, posthumously. it's very old (2007) so things could have changed, but I believe Rabe, Schroeder and Till M (my co-authors) would probably tell me, if things had changed radically.

Valeria de Paiva (Sep 22 2020 at 16:18):

Mike, in the tweet quoted I said I had had a quick look at it and my impression was that the modalities were S4-like ones. I probably need to read it properly.

Henry Story (Sep 22 2020 at 18:11):

It would be great to have an intro book to Modal HoTT that is more mathematical than David Corefield's Philosophical introduction Modal HoTT. Something like the HoTT Book would be ideal, but I guess that is a huge amount of work. For the moment it is a bit daunting to get a feel for these new modalities.

David Corfield (Oct 06 2020 at 08:33):

I should have added that the Licata-Shulman-Riley approach to modal type theory doesn't require the operators to be of S4-shape. Their account of a modal form of simple type theory is here: https://drops.dagstuhl.de/opus/volltexte/2017/7740/pdf/LIPIcs-FSCD-2017-25.pdf. They're working on a similar modal dependent type theory.

David Corfield (Oct 06 2020 at 08:44):

But this is cutting-edge stuff! We're a few years off from a HoTT book-like treatment of modal HoTT.

Sketches of a formal treatment of modal dependent type theory are in the HoTTEST talks by Dan (March 21, 2019) and @Mike Shulman (April 12, 2018): https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html. My chapter on what philosophy might do with modal HoTT is very much at the exploratory stage.

Henry Story (Oct 06 2020 at 08:54):

How far do you think we may be from an implementation in Proof Assistants? (A Cubical Modal HoTT Agda, RedTT, ... ?)

Mike Shulman (Oct 08 2020 at 16:48):

Agda-flat implements a single

\flat

-style modality. I don't know of anyone working right now on a generic modal proof assistant.

Henry Story (Nov 18 2020 at 10:08):

New Episode just released! From Knowledge Graphs to Knowledge Categories https://youtu.be/-N33MZa3B9o @joshsh interviews Ryan Wisnesky of @ConexusAI #categorytheory #knowledgegraphs #graphtheory #abstractalgebra #grouptheory #rdf #semantictech https://twitter.com/TheGraphShow/status/1328930283022934019/photo/1

- TheGraphShow (@TheGraphShow)

Henry Story (Nov 18 2020 at 10:09):

The first episode looks at RDF and property graphs. @Joshua Shinavier interviews Jans Aasman, founder of lisp powered RDF Franz.com graph DB. The hypergraph structure of RDF is mentioned there, and the pros and cons of RDF vs Property Graphs is discussed.
https://twitter.com/bblfish/status/1328996131502743553

@TheGraphShow @joshsh @jansaasman @Franzinc Discussing #RDF and #PropertyGraphs @TheGraphShow asks how a global graph can emerge. What would the financial incentives be? How would privacy fit in? I recently added this story to the Access Control Use Cases @project_solid to address those questions: https://solid.github.io/authorization-panel/wac-ucr/#conditional-payment https://twitter.com/bblfish/status/1328996131502743553/photo/1

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (Nov 26 2020 at 18:03):

Eric Forgy (Nov 26 2020 at 18:31):

Jules Hedges (Nov 26 2020 at 19:28):

Henry Story (Nov 26 2020 at 20:27):

Yes, @Jules Hedges, I don't know either why the list of speakers for the "ACT for Industry" workshop was not put up. So I uploaded the PDF with the bio of the speakers and the title of their short presentation : https://co-operating.systems/2020/11/SemWeb_Pro_ACT_For_Industry.pdf

Jules Hedges (Nov 26 2020 at 21:53):

Henry Story (Dec 03 2020 at 13:52):

I put up the slides for the SemWeb Pro 10 minute Web Cats Intro talk. Not sure when the video of all the talks will be published.

Henry Story (Dec 03 2020 at 13:59):

As I recently learned about Simplicial Sets reading Spivak's Higher Dimensional models of Networks this caught my attention as I have been looking for modalities in the space of graphs... (There did not seem to be that much work on Google Scholar that builds on this though).

Henry Story (Dec 05 2020 at 18:44):

Ryan Wisnesky (Dec 06 2020 at 23:23):

The phrase 'embedded dependency' comes from database theory; formulae in regular logic or 'lifting problem' are probably both more recognizable to category theorists

Henry Story (Dec 27 2020 at 07:50):

I put together some pointers on Higher Dimensional Networks and their potential relation to the web, starting from @David Spivak's paper of the same name, which covers graphs, hypergraphs and simplical sets. Spivak's paper makes the case that higher dimensional networks are what are needed to model certain types of group interactions. But which ones? What can one not express in first order logic? It looks like recent work modeling epistemic logic using simplicial complexes points to the missing dimensions being found in a move to modal logic.

Henry Story (Dec 27 2020 at 15:20):

Mhh. I guess Simplicial Sets are pretty important. @Emily Riehl starts her book Elements of ∞-Category Theory with a definition of a Simplex Category... :open_mouth:

Henry Story (Jan 23 2021 at 22:51):

I am very thankful to the EU for sponsoring our project "Solid-Control" to enhance access control on the Web and Privacy. https://nlnet.nl/project/SolidControl/

Henry Story (Jan 23 2021 at 22:57):

Solid-Control aims to developing the access control and authentication layer of Tim Berners-Lee's Social Linked Data (Solid) project. This involves bringing in research from mathematics such as Abadi's work on "saying that" logic of access control to the standardisation efforts (see this discussion on Capabilties and Access Control) as well as writing a "demo" server (3rd version) and client libraries, as per IETF motto "rough consensus and working code".

Henry Story (Jan 24 2021 at 09:45):

Martin Abadi's logic of Access Control is incredibly useful for working on decentralised security for the web. In his tutorial notes he shows how the modal logic of "saying that" can be given an interpretation in classical logic and in constructive logic. (Indeed it is cited as a major piece of work in @Valeria de Paiva's 15 year retrospective paper on intuitionistic modal logic. Abadi oddly enough did not seem to be aware of the semantic web, as it solves the problem of importing names that he mentions at the end of his paper when discussing the prolog like language Binder). Anyway, this means that the question on the web we need to face is which version of the modal of saying that fits with RDF. This may seem quite odd since RDF as argued in @Evan Patterson's Knowledge Representation in Bicategories of Relations is a first order logic. But that does not take into account the extension of RDF to quads, for which Pat Hayes proposed an interpretation in terms of Context Mereology (and where he was really proud to find a connection with speech acts), and which I think we can in CT think of as essentially 4 regular hypergraphs

s, p, o, g : A \to N

Henry Story (Jan 24 2021 at 15:27):

Indeed there is something that reminds me of type theory in the way one can use the quads of RDF. For example one could think of any RDF graph G as a Proposition (and so a type). Then the 4th element acts a bit like a witness to the proposition. So we could write using in type theoretic syntax:

<https://www.w3.org/People/Berners-Lee/card> : G

where https://www.w3.org/People/Berners-Lee/card is the name of the witness of the graph G.
The odd thing about the semantic web, is that one starts with the name of the witness to get the type.
This can be tried out by entering the following in a unix/linux/mac-os shell the command

curl https://www.w3.org/People/Berners-Lee/card

This returns the graph, which I am thinking of as the type.
One could copy the returned content and put it on another web server, and so create another witness of the graph. The copied witness won't be in the same position on the Web and won't have the same incoming links and so will not be the same witness.

Henry Story (Jan 24 2021 at 17:29):

Valeria de Paiva (Jan 24 2021 at 21:21):

hey @Henry Story yes, I do think that the logic of "saying that" is very interesting and not fully investigated, despite Abadi and others' work on it. I had a proposal in the middle 90's to do such investigation (you can read about it in https://www.cl.cam.ac.uk/~lp15/Grants/auth.html) which was approved by EPSRC, but by then I had a proper job in Birmingham and Larry then changed the project very much. of course I was not thinking of RDF then, but a few years later I was thinking of the semantic web, when again presented a project like that at the Kestrel Institute (https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.443.3739&rep=rep1&type=pdf). I still think this is an exciting project, but one that I haven't had much time for, recently. thanks for reminding me!

Henry Story (Jan 24 2021 at 21:33):

Thanks for the links @Valeria de Paiva . A lot of useful pointers in there :-)
Reading Pat Hayes' Named Graphs, Provenance and Trust' it seems really that everything is open in terms of reasoning with quads (Named Graphs) as long as the projection from quads to graphs preserves the semantics of RDF graphs. It allows one to work at the intensional level, but the logics to be built on it are left wide open. It may even allow one to do constructive logic at that point: after all the guard protecting a resource needs to build proofs just as in constructive logic.

Henry Story (Jan 24 2021 at 22:10):

In definiting access control reasoning on the web there is one serious constraint: the client that follows a Link: <doc.acl>; rel="accessControl" after a 401 Unauthorized response on a resource, needs to be able to reason from the document returned by following the accessControl link (and relevant closures of linked to documents), what proofs the Guard will accept (if any) to authenticate the client.

Henry Story (Jan 25 2021 at 09:31):

One intruiging possibility is that the quads of RDF means we move from 3-regular hypergraphs to 4-regular hypergraphs and that this is what enables the modal properties needed to express something like Abadi's says relation.
@David Spivak wrote about higher dimensional networks in 2009 paper where he argues that there are things that cannot be expressed in the lower dimensional networks that can be expressed in the higher ones. A recent paper shows for example that one can express epistemic modal logic with simplicial sets. (I put together a set of papers I found on the subject here).
This is where I was hoping Category Theory could help the Semantic Web community: by showing how the structural move from triples to quads (and perhaps beyond) opens up these dimensions, and perhaps determines certain logical properties.

Henry Story (Jan 25 2021 at 10:09):

If the work on access control is moving towards Linear Logic as with Nigam's work (and if it turns out to be useful for our use cases), then it would be interesting to know if linear logic and higher dimensional networks are related, ...

Henry Story (Jan 25 2021 at 10:47):

Valeria de Paiva (Jan 25 2021 at 23:08):

Henry Story did you notice that Eric Goubault (a friend of mine) is the same guy both in the simplicial model of intuitionistic S4 (the version you thought was complicated) and in "Knowledge and simplicial complexes" that you thought was nicer?

Henry Story (Jan 26 2021 at 10:03):

Ah yes, you are right. Eric Goubault was one of the authors of the 2003 paper On the geometry of intuitionistic S4 proofs and also of the 2020 paper Knowledge and simplicial complexes. I may have come across the second, following links on Google Scholar, but I am not sure I noticed Goubault having contributed to both. For context, the first paper abstract starts with

It goes into great detail of what programs are and as I do not yet know about "nerves", it was a bit worried I was perhaps going down the wrong track, even if the S4 relation to Abadi's logic of saying-that was there. The 2020 paper is beautifully illustrated with many examples from the multi-agent epistemology literature, so that helped me understand what simplicial complexes were.

Another 2020 article Networks beyond pairwise interactions: Structure and dynamics which is also very nicely illustrated looks at the use of simplicial sets and hypergraphs in complexity studies in biological, social and technical systems (and I think argues that hypergraphs are more general...)

Henry Story (Jan 26 2021 at 10:08):

So again if I am right that RDF quads form 4 uniform hypergraphs, then this structure could explain its modal logical component from a Category Theory point of view.
It is a bit odd in a way, because one could be tempted to confuse these triples and quads with Products in say functional programming. The thought here goes: what's so special about triples or quads or quints? Those are just products

A \times B \times C \times D

and in programming those are used all the time, just another useful data structure. But programmers using those are not moving into higher dimensional networks, when they use those. Indeed those don't seem to have anything to do with modal logic. A similar question can come from people with a logical background. Many logics such as Prolog allow one to have predicates over tuples, where one does not make a major (metaphysical) difference between Parent(M,C) and four place predicates such as registered(Student, Course, Credits, TimeSlot) . What is the right response to that?

John Baez (Jan 26 2021 at 14:56):

I don't understand any of this stuff, but you mentioned one thing that sounds a lot simpler than all the rest: the nerve of a category. This a way of turning a category into a simplicial set by turning each n-tuple of composable morphisms like this:

A_0 \stackrel{f_1}{\to} A_1 \stackrel{f_2}{\to} \; \cdots \; \stackrel{f_n}{\to} A_n

into an n-dimensional simplex, simply by drawing them and all their composites. See this for the tetrahedron you get from a 3-tuple of composable morphisms:

John Baez (Jan 26 2021 at 14:58):

This picture, alas, doesn't make it clear that no skill or cunning is required to draw the simplex: you just draw all the composite morphisms.

Henry Story (Jan 26 2021 at 16:35):

Ah indeed @John Baez , put that way the concept of a nerve of a category does not seem that mysterious, now that I have a good intuition of what simplicial sets are.

I don't think the semantic web pieces are much more complicated. The quad structure just allows on name sayings of things, and so to relate an agent to things they said. So AdminC1 says { Jim canread file1 } relates AdminC1 to the one triple graph { Jim canread file1 }. So here we are no longer linking nodes in a graph but a node to a whole graph. ( a bit like the top node in the four simplex connects to a whole triangle below it). Assume that on computer C1 the rule is that what AdminC1 says is true, and so on C1 we do have that Jim canread file1. But that rule is not true on another computer, where another admin rules. Then it may be that on C1 there are a number of users, and AdminC1 allows each user to set rules when restricted to a subset of the files on that computer space... That is the intuition behind Abadi's "says" logic. I think it is modal because it relates not objects in a graph (thought of as description of the world), but an agent to a graph.

Henry Story (Jan 26 2021 at 19:59):

Thanks for the pointer. That lead me to the very readable 2006 article A Linear Logic of Authorization and Knowledge, which provides 2 very nice examples of where linear logic can be useful: 1. a description of how to assign students to courses given that each student has certain credits and 2) a banking application.
It is a good to know that the 2015 article by Nigam finds some versions of that logic to be undecideable, even if they identify some fragment to be PSPACE complete.

From the semantic web point of view it would be interesting to know what one needs in addition to first order logic, or rather N3, to get to linear logic. This would help get an idea how long it may be before we can make use of these logics on the web. The use cases are interesting enough to sustain research projects leading to standardisaton efforts.

The place to start would be to look at N3. I received very good feedback for the 2019 PhD thesis Notation3 as the unifying logic for the semantic web, which has examples with the "says" relation as well as for cryptography. I need to look at it to see how it fits with Abadi's work. (I actually learnt about the semantic web sudying Tim Berners-Lee's and Dan Connolly's python cwm implementation of such a reasoner.)

dusko (Jan 26 2021 at 20:49):

in my experience, the problem with really applying CT in security, i.e. with real cryptographers and people defending companies, is that we don't start from their problems, but expect them to learn linear logic, or BAN logic. the result is not only that they ignore us, but also that we ignore their problems, no matter how much we try not to. each of the proposed logics turned out to miss something essential, and some of them almost everything (as a quick search of eg discussions about BAN logic shows).

if we honestly believe that CT is useful, then there is no reason to look for a way to apply CT to a Domain X (eg security). just spell out the problems of Domain X, and CT will emerge.

dusko (Jan 26 2021 at 20:54):

i have been teaching security courses for some 13 years now. the current page is
http://www.asecolab.org/courses/ics355/
but i post the lecture notes as we go, so currently there is just the first one, with the taxonomy of the concepts, and the second one --- about static access control. no reason to inject any CT, since already the UNIX and the android AC systems are some matrices, and if you take updates into account, it is a bicategory.

dusko (Jan 26 2021 at 20:55):

dusko (Jan 26 2021 at 20:59):

Henry Story (Jan 26 2021 at 21:01):

I am happy to act as a translator :-) I came from writing semantic web apps to CT by seeing how CT had applications in programming hyper-apps in Scala, and found many very beautiful ideas here.
On the SemWeb side, we are trying to build a decentralised web where every Web Resource can be access controlled, data can link from one resource to another, allowing us to turn every app into a browser (a hyper-app), creating a global decentralised social network with no center of control, all based on open standards, building on what exists and developing what will be needed.
So all in all, I have 4 years understanding of CT, and 25 years working on the web.

Valeria de Paiva (Jan 26 2021 at 21:14):

Henry Story (Jan 26 2021 at 22:05):

[...]But yes, my programme of extending Curruy-Howard to as many modal logics as possible is still being pursued. and this includes description logics (https://www.researchgate.net/profile/Valeria_De_Paiva2/publication/239480936_Constructive_Description_Logics_what_why_and_how/links/0c960528af4c1321b6000000/Constructive-Description-Logics-what-why-and-how.pdf), hybrid logics and many other variants of modal logics.

Thanks Valeria. I found your presentation to the MIT CT Seminar Relevant Dialectica Categories very helpful to understand the Curry Howard motivation behind your work.

As a Scala programmer I really like using strong types, and I have seen how far one can go with them using Agda recently too. As a Semantic Web developer I am not sure if I have types or not (OWL gives a class hierarchy logic) and how those would map to Curry Howard. So I asked a question on Web Cats issues Is OWL/RDF typed or untyped? Should it be?. Evan Patterson's model in terms of bicategories of relations would show how they could be strongly typed (a future RDF perhaps?). Pat Hayes offers and argument against and Eric Prud'hommeaux argues that Shapes do give us the important features of types (I need to look into that). One would need to carefully study the advantages of RDF as it is used, and see what the advantages of moving to a Curry Howard friendly typing system would be. (I think the place where stronger type reasoning would make most immediate sense would be with the RDF datatypes (ints, dates, etc...). I wonder how you see this, as you have worked with Description Logics and are a firm believer in Curry Howard.

Henry Story (Jan 26 2021 at 22:29):

The other question I have is how to move from @Evan Patterson's bicategories of relation as a model of RDF (so forgetting about the previous typing problems) to a modal logic. This is why I was investigating higher dimensional networks (esp. 4-regular hypergraphs) as that is the structure that RDF follows to open the space where modal properties are expressible. (see issue 3).

Henry Story (Jan 27 2021 at 09:40):

Re: RDF and types. It may be that RDF is typed. It is all built on Set theory after all, and Sets are types at homotopy level 2 according to HoTT. Description logics, on which OWL semantics is based makes the distinction between T-boxes where relations between types are described, and A-Boxes which is where objects of the form bob : Person are placed.

I guess the problem comes from it allowing us to have bob : Person and bob : Agent.

But perhaps that should be bob : Thing and Agent, Person : Set and these get related via the <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> (written with prefix notation in Turtle as rdf:type - the colon is a bit confusing there for type theorists). rdf:type is a relation (abbreviated a in Turtle as it used so often ) so that we really have 2 relations: bob a Person and bob a Agent . (which is a possible way to model membership in the bicategories of relations).

Valeria de Paiva (Jan 29 2021 at 01:44):

@Henry Story I'm not sure how exactly one wants to cash out the Curry-Howard correspondence for weak logics like EL or ACL. my attempts so far have been to construct modal logics of context, built on description logics, putting together the description logic paper above with the paper on a modal logic of contexts (based of John McCarthy's suggestion that context can be modeled via an operator like "isTrueIn(context Phi)". this is very underspecified, as these contexts based on modal intuitionistic logic K don't give you lots of inference, but they at least capture the feature that modal contexts stop information leaking in or out. You can read about it--if interested-- in my Textual Inference Logic papers. More recently Dick Crouch and Katerina Kalouli have used the description logic EL with named graphs to describe our logic of sentence inference. you may like their version better, it's in https://www.aclweb.org/anthology/S18-2013.pdf

Henry Story (Jan 29 2021 at 13:43):

That is a great article @Valeria de Paiva you linked to "Named Graphs for Semantic Representations" discussing the work you are involved in! It looks like we're coming to the same point from completely different places :-)

It is interesting to see the relation with Donald Davidson that pops up there. When I was learning RDF I intuitively interpreted it either in terms of Donal Davidson (Author of Truth and Interpretation) or in terms of David Lewis's possible worlds. As an historical asside to those who may come across this thread: both were students of the famous Willard Von Orman Quine , whose historical relation to Carnap was laid out by @Steve Awodey in this fascinating talk "Mac Lane and Carnap's Logical Syntax of Language".

Henry Story (Jan 29 2021 at 13:57):

The relation to (Kripke, Hintikka, Lewis) modal logic was hinted at in the 2004 RDF Semantics specification where the meaning of an RDF graph is explained in terms of possible worlds. But that was later dropped in 1.1, I guess because the metaphysical assumptions were confusing some people too much. (It did help me a lot though). That is part of the reason I have been looking to how one can legitimate these anew but structurally with a minimum of metaphysical assumptions. The CT way to talk of Possible Worlds is I believe via ultrafilters, though also interestingly enough via Coalgebras, as I learnt from @Corina Cirstea .

Henry Story (Jan 29 2021 at 14:09):

The article explains well how the move from triples (ie functors from labelled directed graphs understood as functors from to small category

s,p,o: A \to N

Set

) to quads (i.e. hypergraphs corresponding to Functors from the small category

s,t,o,g : A \to N

Set

) increases the expressivity by allowing one to speak of relations to what others say, think, believe, dream, etc... instead of just relations between objects.

Henry Story (Jan 29 2021 at 14:48):

It is actually really interesting to look at the swap repository now archived on github where Tim Berners-Lee tried out these concepts 20 years ago.
One import file is the log.n3 file which defines log:Truth as a type of graphs, and log:implies as a relation between formulas.

Henry Story (Jan 29 2021 at 15:05):

Some examples are this example of a definition of a Transitive Property in test/rules13.n3 where I think :means is shorthand for iff

@forAll <#a>, <#b>, <#p> .

{  <#p> a daml:TransitiveProperty . } :means {
  { @forAll <#x> , <#y> , <#z>.
    { <#x> <#p> <#y>. <#y> <#p> <#z>. } log:implies { <#x> <#p> <#z>. }
  } a log:Truth.
} .

Valeria de Paiva (Jan 29 2021 at 15:07):

hi @Henry Story the connection to Davidsonian semantics has been in my work in NLP since the beginning: the paper
A basic logic for textual inference, https://www.aaai.org/Papers/Workshops/2005/WS-05-05/WS05-05-008.pdf from 2005 makes it clear. This is inherited from some 20 years of previous work by Xerox PARC researchers. the modelling discussion here is how todeal with contexts in the semantics: I first tried modalities (following McCarthy's suggestion), the new suggestion is "naming graphs" in the new paper. But no, there are many more ways of dealing with modal logic than "ultrafilters"--which are not my cup of tea.

Henry Story (Jan 29 2021 at 15:12):

Ah! I guess that means that there are other ways to think of modalities other than ultrafilters... (well there is also the coalgebraic view of course)

You may like this rule then following Tarski's System T, disquotational conception of truth which Donald Davidon built so much on, in the file rules13.n3 :-)

@forAll :x, :y, :z.

{ { :x :y :z } a log:Truth .  } log:implies { :x :y :z } .

{ :sky :is :blue } a log:Truth .

Valeria de Paiva (Jan 29 2021 at 15:24):

Henry Story said:

quote
Ah! I guess that means that there are other ways to think of modalities other than ultrafilters....

Yes. my formalizations of modal logic uses CCCs+(co-)monads (Intuitionistic necessity revisited 2000) or fibrations (Fibrational modal type theory 2016), Alex Kavvos did a recent PhD thesis on the subject.

Henry Story (Jan 29 2021 at 15:25):

I think it should be possible to model some of Abadi's :says relation, :believes relations etc... using such tools. Indeed ont:imports works somewhat this way. Here's a fun one tom-mary.n3 demonstrating nested contexts :-)

<#Tom> :believes {
    <#Mary> :wants {
        <#Mary> :marriedTo [ a :Sailor ]
    }
}.

Valeria de Paiva (Jan 29 2021 at 15:29):

yes, we can deal with simple propositional attitudes like this and even more complicated ones like Karttunen's in Computing relative polarity for textual inference.

Henry Story (Jan 29 2021 at 15:33):

What is needed I think then is to work out what the N3 folks are doing over at the N3 W3C Community Group - the work is going on at the github n3 repo and see how your research and the work from CT can help inform decisions made there. Clearly it won't be as advanced in many areas, but it has really useful applications. It would really be a pity if the wrong decisions get made there because of lack of mathematical insight.
(I should follow that too).

Henry Story (Feb 06 2021 at 12:16):

I think the origin of the problem comes from trying to build Applications in typed languages such as Scala and having to work with Linked Data on the Web. There is a simple conceptual problem, just trying to work out what how these systems relate, which affects the programming of them, and also teaching people how to use these.

We can see one attempt to help bridge the gap in this project described in 2019 Semantic Query Integration With Reason where they made changes to the Scala 3 compiler so as to fetch ontologies used by say SPARQL queries, so that the results could be well typed.

But when I write Linked Data software, things seem a lot more dynamic than that. I may follow a relation whose range is foaf:Agent and whose url is, say https://acme.org/agents/xyz#i> and on fetching the remote Graph (dereferencing it) the node we fall on may state this URL to refer to a Person (a subclass of Agent). As we get more info what from far away looked like some Agent (Robot? Deer or even Lion) we find out to be a Person, .... Each of these are types. Could it be that Gradual Typing is the right place to look?
(That was following a suggestion on Twitter by @Jules Hedges .

@_julesh_ I love types. I think there are half ways between static and dynamic types. As you gain more information about an object you can deduce more about it's type, narrow it down. An animal moving in the distance, turns out to be a lion not a zebra.

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (Feb 06 2021 at 18:44):

As I want to build a Web Server for the Solid Control Project I have looked around at various frameworks from Rust, to Haskell, and the Akka framework running written in Scala.

Akka is based on the Actor Model developed initially proposed in 1973 and the history of its evolution is described with passion in a 2010 retrospective by Carl Hewitt in "Actor Model of Computation: Scalable Robust Information Systems". Here is a citation that should interest people here:

Reading this, and with some experience using Akka 5 years ago, it feels like the Actor model is very close to the model of the Web. And it also explains why Akka is used by LinkedIn, PayPal, Tesla, and many other giants to do billions of transactions a day.
The Solid Web is perhaps Actors with a preference of messages being encoded as RDF Quads, giving us a logical notion of context that does not seem to be made explicit in the simple message passing (even if it is compatible with it).

Henry Story (Feb 06 2021 at 18:50):

So as I was catching up on Akka, which added typed actors last year, I came across a course on it that mentioned the 2015 A gentle introduction to multiparty asynchronous session types, which I am now reading... Session types give a mathematical foundation to allow one to defined protocols using types in actor systems, and much more generally too I guess.

Henry Story (Feb 07 2021 at 15:15):

The "Gentle Introduction to Session Types" above is still very abstract, so I wanted to find if session types had been developed for a programming framework based on Actors, to better understand the relationship between the two. That led me to this work on EffPi, which is an interesting example of Academia meeting industry. EffPi uses Scala3's dependent function types which can verify a type-based protocol. To verify additional properties of the protocol such as liveness they added a compiler plugin that makes use of mCRL2 a formal specification language that comes with a toolset for "linearisation, simulation, state-space exploration..."

This slide from the Sept 2019 talk on EffPi (Pi for 𝛑-calculus) shows a story of the meeting of research on Akka used in Industry (coming from the Hewitt's work on Actors) and academic work on Session Types (used to prove properties of protocols ). https://twitter.com/bblfish/status/1358392715118010369/photo/1

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (Feb 07 2021 at 15:19):

It would be interesting to know where Session Types are positioned in the Category Theory landscape.

Henry Story (Mar 22 2021 at 17:49):

I finally had time to join the N3 Group CG at the W3C for their meeting, and due to time zone mix ups was able to have some very interesting conversations there. I found out that Jos de Roo's EYE Reasoner has support for Linear Logic now (cc @Valeria de Paiva ) and they recently published a paper on this: Predicting future state for adaptive clinical pathway management.
I won't have time to study it immediately as I have to meet my milestones for the EU project on access control....

Valeria de Paiva (Mar 22 2021 at 18:51):

Henry Story (Mar 23 2021 at 06:37):

The document they are working on is the N3 spec.
My question yesterday was a bit teasingly whether it should not really be called N4.
As N3 It seems to indicate more that it is working in the bicategory of relations. But the context apparatus of the language allows it to express LauraLane believes { Superman a FlyingBeing } which indicates that it would be better modelled as a 4 regular hypergraph.
As I understand there is always a way to reduce the dimensions, (ie you can flatten a simplicial set) but doing that tends to make things more complicated or even will loose information.

Henry Story (Mar 27 2021 at 16:40):

The W3C Verifiable Credentials Group is looking for reviews of the document attached to this email RDF Dataset Canonicalization - Formal Proof. Perhaps someone here will, looking at it, see how the same thing can be shown more elegantly or even find a faster algorithm. Or just give a review of it :-)

Henry Story (Apr 03 2021 at 14:57):

Superman, Laura Lane, and Clark Kent all turn up in this 2019 paper Towards Supporting Multiple Semantics of Named Graphs Using N3 Rules, as well as a number of more practical examples related to medical ontologies, that show 4 different ways contexts are interpreted on the SemWeb.

Henry Story (May 13 2021 at 09:18):

Here is a question that keeps popping in my head regarding Graphs, Setoids and RDF.
@Jacques Carette's Agda Categories library is built on setoids. RDF is known to be specified in terms of Sets. But I keep wondering if the semantic element of the Semantic Web does not really give us setoids after all, ie. could one not think of RDF as "really" specified in terms of setoids?

If I look at the functor category from the small category with three arrows

s,r,o: A \to N

to Set I get essentially the category of graphs (which is close to RDF). But those types of graphs, in the semantic web would correspond perhaps the abstract syntax. RDF adds another mapping from names to things, in terms of which truth can then be defined, and since it does not have a unique naming assumption, multiple names can map to the same object. Multiple names mapping to the same object just seems to be another way to say that we are dealing with setoids. Ie the names can form equivalence classes.

Mike Shulman (May 13 2021 at 13:10):

If I can ask a silly question, why three arrows

A\to N

? An arrow in a graph has only a source and a target. Is it that relations in RDF have their own "name" as well as two things that they relate?

Mike Shulman (May 13 2021 at 13:12):

Regarding setoids, a general setoid is equipped with not merely an equivalence relation, but a collection of witnesses for the truth of that equivalence relation. Can two names every name the same object "in more than one way"?

Jacques Carette (May 13 2021 at 13:32):

agda-categories is built on setoids mostly because of constructivity reasons. That this works well for basic category theory goes back to Huet-Saibi in 2000. Jason and I "discovered" that it keeps working very well into quite complex parts of category theory. Though eventually things do go a little sideways: the category Set is a topos, but Setoids is only a (really nice) pretopos. So presheaves and profunctors are not quite as magical and over-powered in this setting.

That most things are built on set is largely an accident of classical education not showing people there's even a choice here. A complete formalization of RDF done in an effective manner (i.e. things that ought to compute, do in fact compute) would tell. To really "tell", it would probably have to be done multiple times, in different settings, such as in Isabelle/HOL, cubical agda and 'plain' agda (for example).

So setoids seem to be nice when you have all sorts of equivalence relations floating around, especially when you have multiple equivalences on the same underlying carrier. But they carry a large proof burden too. So they are not zero cost.

[And all the things @Mike Shulman mentions too: the "proof relevance" of the equivalence relation is a rather interesting phenomenon.]

Nathanael Arkor (May 13 2021 at 13:41):

Jacques Carette (May 13 2021 at 13:45):

Not as far as I know, only a Pi-W-Pretopos. The subobject classifier's universal map is "too big" - there was a lot of discussion of this at this issue, along with links to a number of relevant papers.

Nathanael Arkor (May 13 2021 at 13:49):

Oh, the nLab suggests that the problem could be that even though they might form a Grothendieck topos, a Grothendieck topos is confusingly not necessarily an elementary topos in weak foundations!

Mike Shulman (May 13 2021 at 13:52):

Yes, probably it would be better to call it a "category of sheaves" or a "Grothendieck pretopos" in that case. Essentially any category is a "category of sheaves" over itself, namely sheaves on the one-point space.

Mike Shulman (May 13 2021 at 13:55):

A very serious disadvantage of using setoids rather than sets is that they give you the wrong answer when interpreting mathematics internally in a category. For instance, if you define the set of real numbers in constructive mathematics and then interpret it in the topos of sheaves on a space

X

, you get the sheaf of continuous real-valued functions on

X

. But if you do the same thing with the setoid of real numbers, you get nothing of the kind.

Mike Shulman (May 13 2021 at 13:57):

Setoids make sense (and, indeed, are unavoidable) when building mathematics from a weak foundation that doesn't have its own notion of "quotient", like Martin-Lof's original type theory. But when you start from a foundation that already has quotients, working with setoids loses all the information about those quotients by introducing new "free" quotients.

Mike Shulman (May 13 2021 at 14:00):

It's true that setoids are better-behaved than sets for doing category theory in a constructive set-based foundation. For instance, the 2-category of categories (in the usual sense) with hom-sets is not constructively exact (in the appropriate sense for a 2-category), whereas the 2-category of e-categories (categories with hom-setoids) is. But in my opinion this mostly goes away in a homotopy type theory foundation.

Mike Shulman (May 13 2021 at 14:00):

Mike Shulman (May 13 2021 at 14:01):

Sorry for the long spiel, but setoids and categories are something I've been thinking a lot about recently for some reason, so I had a lot to say. (-:

Jacques Carette (May 13 2021 at 14:10):

While I started on setoids and categories accidentally, I've also been thinking about them a lot. It does seem that HoTT does add something, though the design space still a lot of places left to be explored. All-setoids-all-the-time is sub-optimal, but all-univalence-all-the-time seems similarly problematic.

Why I'm still exploring is the following: if one rebuilds categories by successive enrichment (constructively), i.e. -1 categories are -2 enriched, and so on, it looks like 0-categories really want to be Setoids, with then 1-categories being "naturally" E-Categories. The point being that -1-categories don't collapse to just 2 things. With excluded middle, yes, that's immediate. Without? I conjecture that it's in fact equivalent to excluded middle. [No proof yet.]

Mike Shulman (May 13 2021 at 14:13):

Henry Story (May 13 2021 at 14:23):

@Mike Shulman yes, I understand the third arrow as what allows one to group arrows together. So I can say

TimBernersLee --knows--> VintCerf .

I tried to illustrate this and argue for it in the slides and (sketch of a) paper Functorial RDF.

VintCerf --knows--> DanBrickley
VintCerf --olderThan--> DanBrickley

etc... In a way the Grothendieck construction gives this too, but then RDF goes into the direction of hypergraphs with DataSets, and I am not sure how that maps to Grothendieck constructions.

Mike Shulman (May 13 2021 at 14:25):

Yes, that's true; you have to additionally saturate / Rezk-complete to get back to the "correct" (IMO) notions of set and category.

Jacques Carette (May 13 2021 at 14:26):

A lot of the work that I do has its origins in symbolic computation, where syntactic issues matter a lot. Quite a number of objects have a kind of 'syntactic polymorphism' to them that is most definitely not extensional (a given polynomial with coefficients in

\mathbb{N}

can be interpreted in many fields, and behaves quite differently over small

\mathbb{Z}_p

than over

\mathbb{C}

) . This can be encoded in type theories, but every layer of coding makes things awkward and less 'first class'.

What I'm looking for is a kind of 'onion' type system where the inner ring is as nice as possible (HoTT with univalence and more), and concentric rings where one loses properties gradually. I want to be able to make statements like the object X is non-denoting a valid mathematical statement (like

\infty / \infty

), without too many layers of quotations. There are many things that we can write down that look reasonable, but turn out to not be meaningful. The way it fails to be meaningful can itself be a non-trivial mathematical result.

Mike Shulman (May 13 2021 at 14:28):

I don't see anything non-univalent about that. A polynomial is, of course, an abstract object of the rig

\mathbb{N}[x]

, not the function that it induces on any given field, and that's true already in pencil-and-paper mathematics.

Mike Shulman (May 13 2021 at 14:31):

Oh no, wait, I jumped too fast. Setoids being equivalent to sets is equivalent to AC, and the status of this statement about derivators (which is what I've been thinking about recently) is not clear to me, but if you just mean the ordinary 1-categories of these things then yes, I believe it's equivalent to LEM. Sorry.

Jacques Carette (May 13 2021 at 14:32):

I now realize that I was assuming decidability of inhabitation constructively, which is more than excluded middle. But that's not full choice, is it?

Jacques Carette (May 13 2021 at 14:32):

Mike Shulman (May 13 2021 at 14:35):

What do you mean by "decidability of inhabitation"? Isn't decidability of anything an instance of LEM?

Henry Story (May 13 2021 at 14:38):

That is a difficult question :-) The RDF semantics just speaks of a function from names to things.
(But those are specs reached by consensus, so we should not think that they settle the matter of what mathematics underlies the structures they are using. Rather the way the semantic web is used should be a guide to answering that question.)
The simplest example would be a URL that refers to a document say https://nlab.org/Monad and that is then later made to redirect to https://nlab.org/monad. Do they refer in the same way? It seems not quite, the path in space-time that a request for one takes is different from the second.

The way this works is defined by RFC 2616 Hypertext Transfer Protocol -- HTTP/1.1 §10.3.2 301 Moved Permanently.
The client makes a request on a resource <...Monad> and the server responds with a 301 Moved Permanently answer which I think counts as a proof object that the first URL now refers to the same things as the second URL.

Things get a bit more complicated for URLs that refer to objects-in-the-world, via descriptions found on the web, as for example with a WebID. An individual could have two such WebIDs - one professional and one for work say, and the descriptions could be done in such a way that one can build a proof that the referents have to be the same.

So yes, I think we do have witnesses to the equivalence of two terms, and one should not equate two terms unless one has such witnesses. (That fact does not come out that well from the current RDF semantics though ...)

Jacques Carette (May 13 2021 at 14:38):

Part of my problem (with things like polynomials) is that a lot of texts in symbolic computation are very sloppy about intensional vs extensional issues. They treat things interchangeably, even though they shouldn't. And write everything down as if it was all the same. So it's very hard to disentangle what is what.

Mike Shulman (May 13 2021 at 14:38):

Jacques Carette (May 13 2021 at 14:39):

On decidability: I probably confused myself because I was doubting myself after your error. I use this definition.

Mike Shulman (May 13 2021 at 14:41):

Ok, that looks like the strong untruncated form of LEM that's incompatible with univalence (which is never what I mean by LEM). But I don't think you need that to show that the preorder reflection of Set is equivalent to 2. All you need is that given

f:X\to Y

such that

X

is at least as inhabited as

Y

there exists a function

Y\to X

, and for that all you need is that there exists an element of

X

Jacques Carette (May 13 2021 at 14:44):

Agreed! I have a hard time pinpointing what my discomfort is with assuming univalence all the time. In part, it might be due to an incorrect internalization of what a 'function' is. I just keep thinking about spaces with too few points, that would end up identifying two things that are still somehow different, just because we didn't have enough points to tell them apart.

Mike Shulman (May 13 2021 at 14:49):

Well, you can still talk about pointless locales in univalent mathematics. That's not a problem because their "continuous maps" are encoded by functions backwards on their underlying frames, not determined by what they do to points.

Jacques Carette (May 13 2021 at 14:50):

Would you be able to give me a helping hand with formalizing exactly what "the preorder reflection of Set is equivalent to 2" requires in the meta-theory? I'll resurrect my dead code; I think I just need a hint or two.

Mike Shulman (May 13 2021 at 14:52):

Sure. I'd be even more interested if you can factor it through "the preorder reflection of Set is equivalent to Prop", which I suspect is equivalent to something like the "propositional axiom of choice", followed by "Prop is equivalent to 2" which of course is equivalent to LEM.

Jacques Carette (May 13 2021 at 14:56):

Hmm, that might be quite challenging to do in Agda. Though I'm willing to give it a try.

The eventual thing I'm interested in is about -1-categories, as -2-enriched categories. If I follow your chain, it still says that (the category of -1-categories is equivalent to 2) is equivalent to LEM. [And yes, my pure guess was that indeed, one level up from that has a strong choice flavour, but I wasn't willing to go there until I had this 'easy' case done.]

Mike Shulman (May 13 2021 at 15:39):

Well, I would call those "pre-(-1)-categories". Actual (-1)-categories should satisfy a Rezk-completion condition that makes them equivalent to Prop without any classicality assumptions.

Jacques Carette (May 13 2021 at 15:57):

I am amenable to that terminology. Hmm, a quick search on Rezk completion condition gives me things that are above my comprehension level of these matters. Is there a way to phrase a "Rezk completion condition" specialized to this situation? Is it obvious that this in some sense forces LEM?

Mike Shulman (May 13 2021 at 16:21):

Mike Shulman (May 13 2021 at 16:22):

Rezk completion of an ordinary (pre-)category says that isomorphic objects are equal (in an appropriate univalent sense, where equalities can actually carry the information of particular isomorphisms). In a pre-(-1)-category, all objects are isomorphic, so Rezk completeness says that all objects are equal. Thus, it is just a proposition.

Henry Story (May 16 2021 at 09:35):

Here is a much better example on how two web identifiers (a.k.a URLs) can have the same reference but in a different way, as discussed above
A recent tweet by @Amar Hadzihasanovic pointed out that what used to be called "Computational Trinitarianism" on nlab is now called "computational trilogy".

The legendary nLab page on “computational trinitarianism” is now called “computational trilogy”. Not sure yet how I feel about that. https://ncatlab.org/nlab/show/computational+trilogy

- Amar Hadzihasanovic (@amar_hh)

Henry Story (May 16 2021 at 09:38):

From a terminal you see how this is encoded in the HTTP exchange when you make a call to the old page

curl -I https://ncatlab.org/nlab/show/computational+trinitarianism

The -I flag on curl tells it to only return the HTTP headers. Running that in the console will open a connection to nlab, which returns the following message:

HTTP/2 301
date: Sun, 16 May 2021 09:31:20 GMT
content-type: text/html; charset=utf-8
cache-control: no-cache
location: https://ncatlab.org/nlab/show/computational+trilogy
x-runtime: 35
set-cookie: instiki_session=60ca073898c53ed9d461f6f8f2602417; path=/; HttpOnly
strict-transport-security: max-age=15768000
cf-cache-status: DYNAMIC
cf-request-id: 0a161d1a8b00004ee0fd10b000000001
expect-ct: max-age=604800, report-uri="https://report-uri.cloudflare.com/cdn-cgi/beacon/expect-ct"
report-to: {"endpoints":[{"url":"https:\/\/a.nel.cloudflare.com\/report?s=5tjGVBp1Ew3TWm4Qo64LXSAyLnvuKzIaW2z1Sg9wd57GvEJnYUmKS37ulZ57j1cHD7GKFq8XajeJ6u0Yyo11gkQMjyklfllj%2FOQjUNBZeV5CybBfKTFM3A%3D%3D"}],"group":"cf-nel","max_age":604800}
nel: {"report_to":"cf-nel","max_age":604800}
server: cloudflare
cf-ray: 650397a41a724ee0-FRA
alt-svc: h3-27=":443"; ma=86400, h3-28=":443"; ma=86400, h3-29=":443"; ma=86400

The 301 is the code for Moved Permanently redirect, and the location header tells the browser where to look for the new content, namley at location: https://ncatlab.org/nlab/show/computational+trilogy.

Henry Story (May 16 2021 at 09:45):

The above 301 response can then be seen as a proof object that https://ncatlab.org/nlab/show/computational+trinitarianism and https://ncatlab.org/nlab/show/computational+trilogy considered semantically can be related as equivalent, falling thus in the same equivalence class. If one can do that with slice categories in HoTT, I'd be happy with that too of course :-)

Henry Story (May 16 2021 at 10:54):

ww (May 17 2021 at 08:44):

Sort of. This gets us into all kinds of trouble with RDF. Taking this at face value and ignoring the equivocation of "thing" and "document about thing" (let's not open up that can of worms just now), the assertion that

\ldots \mathtt{trinitarianism} \cong \ldots \mathtt{trilogy}

depends on the context. Some people say this is true, some people object. We can't write down statements about the controversial statement itself in RDF.

Henry Story (May 18 2021 at 14:00):

I was very careful in choosing the URLs https://ncatlab.org/nlab/show/computational+trinitarianism to choose one that referred to a document. :-)
Since as shown above ncatlab.org is redirecting that URL to </nlab/show/computational+trilogy> and since nlab is the one in charge of that namespace, those definitions are what would be called analytic. This leads me to think that if one were to model this in HoTT, one would use the ≡ symbol here.

Now to your point regarding context, I think that presupposes that RDF does not, or cannot have a notion of context, which I think is a widespread misunderstanding. We were discussing belief contexts in RDF further up with @Valeria de Paiva, and there is a nice literature of discussions on Clark Kent, Superman and Lois Lane discussing how Laura Lane loves Superman but not Clark Kent even though they are identical.
Well the article points to the fact there may have been a problem reaching consensus on how to distinguish these cases, but I think that is different from it not being expressible in RDF.

Henry Story (May 21 2021 at 10:40):

Here is some recent Category Theory I came across writing a read-write web server in Scala.
When I last wrote this 7 years ago, I used a Free Monad construct to use as a DSL (I was pointed to it and worked out how to use it without understanding any CT). The Scala Cats library has a page documenting how one can use Free Monads. They illustrate their code with one interpreter as a natural transformation, but one can easily create a DSL to GET, PUT, PATCH, content on the web, and have the resulting free monad script sent around from actor to actor, each one peeling off the top command on the stack, executing it (interpreting it locally) and then sending the rest of the stack (after application of the monad function) on to the next actor.

Henry Story (May 21 2021 at 10:46):

There is a very helpful talk On Free and CoFree from 2016 Pure Functional Database Programming with Fixpoint Types with slides, where Rob Norris shows how one can use Fix for recursive data structures and CoFree as a way to annotate such recursive data.

Henry Story (May 21 2021 at 13:54):

Having studied that talk carefully, I have come I think to an interesting view of what Datasets in RDF should be. Following Rob Norris I wrote the following definitions

case class CoFree[F[_], A](head: A, tail: F[CoFree[F, A]])
// Graph Functor -- modelled on ProfF
case class GraF[A](g: Rdf#Graph, other: Set[A]=Set())

type DataSet = GraF[CoFree[GraF,Uri]]

It turns out that RDF DataSets datastructure may not have been written to allow them to contain DataSets - as I may have discovered today on the semantic-web mailing list. But that seems like something that could be fixed and also that people will want to be fixed for reasons of signing rdf graphs.

Henry Story (May 21 2021 at 14:33):

case classes are essentially product types. Whatever is between the [...] are type arguments, meaning that the case classes above are actually a functors, CoFree is a bifunctor I guess as it takes two arguments, one of which is a functor.

Alex Gryzlov (May 21 2021 at 14:50):

I think you're talking about categorical semantics for (higher-kinded) inductive types, which are traditionally viewed as some flavor of polynomial functors.

Henry Story (May 21 2021 at 14:59):

Yes. I think it would be quite easy to rewrite this in terms of Polynomial Functors, ... though I won't get to that for a while, as the programming is taking up most of my time right now. CoFree is I think on the coalgebra side of things. I actually got to Category Theory from programming. It is articles such as this series on Comonads that made me really want to find out what was going on :-)

Henry Story (May 21 2021 at 20:32):

I found out that N3 graphs can contain graphs (formulae) recursively (see mail on n3 dev list).

Henry Story (May 22 2021 at 06:57):

If I remember correctly from reading Bart Jacobs I could translate the above Scala to Category Theory as follows. First I translate the GraF case class to the following polynomial Functor

\mathscr{G}

which as a first attempt I defined as

\mathscr{G}(X) = G \times \mathcal{P}(X)

where

G

is the set of RDF Graphs and

\mathcal{P}

is the Powerset functor.

Henry Story (May 22 2021 at 07:10):

The documentation for cats.free.Cofree which is a slightly more elaborate version of the above CoFree, states that:

Actually that matches my experience. I built a very simple instruction set with a only 1 instruction set in LDPCmd

sealed trait LDPCmd[A]
case class Get[T](url: Uri) extends LDPCmd[Option[T]]
type LDPScript[A] = Free[LDPCmd,A]

from which I could build a function fetchWithImports that given a URL will return an LDPScript to fetch a graph and all the imports of that graph and the imports of those graphs recursively. At present that returned a List of NamedGraphs, but a better result would be the Cofree structure I mentioned above, with DataSets inside DataSets - which then indeed matches perfectly the definition of cofree in the scala file quoted above.

Henry Story (May 22 2021 at 07:15):

Following the previous interpretation of the scala case class CoFree should be a Functor taking a functor F and a type A, or pehaps a "functor on the product category of endofunctors on Set"

\times

Set

\to

Set?

Henry Story (May 25 2021 at 16:26):

Henry Story (May 28 2021 at 04:13):

Yesterday I watched the introductory talk Symmetric Monoidal Categories, A Rosetta Stone by @John Baez. I studied SMCs a little bit last year here and there, but I think I needed this talk working at the intuitive level (mostly examples) to help something go click.
John's emphasis on their relation to Open Worlds rather than closed worlds made another click (A bit like opening a safe). His pointing me to @Brendan Fong 's The Algebra of Open Systems which I quickly read the Preface which explains the role of Open World thinking at that very approachable intuitive/philosophical level, made me put a few strands of thought together and the door (safe?) openened up.

Great introduction from examples to Symmetric Monoidal Categories by @johncarlosbaez : their use in electrical engineering, quantum theory, programming, logic, ecology and other *open* systems with some thoughts on the 3rd law of thermodynamics. https://www.youtube.com/watch?v=DAGJw7YBy8E&t=18s

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (May 28 2021 at 04:27):

Henry Story (May 28 2021 at 04:34):

A very important part of the semantic web is (one is always told) the Open World Assumption. (Evan's paper has a section on that). So how does that fit?
Well my thought is the following: the connectors on these RDF Graphs are identified by URLs.
These are what allows graphs to be composed.

Without URLs (not even in relation position) one could only ever put two RDF graphs together side by side.
This is what one would be forced to do if one took normal SQL databases or Graph databases and tried to put them together without assuming that they had anything in common. So the URIs in RDF play the role of telling us ahead of time how graphs can be composed. (It does not mean they should be btw, as one graph may contain false information or be from an unreliable source, just like one does not want to compose every Akka streaming component one finds on the web that fits together)

Caleb Foong (May 28 2021 at 04:45):

I think surely we can connect two RDF graph if they contain entities with the same URI, but isn't that two restrictive? For example, how about two entities having a "isa" relationship? In general, can we construct a some connections between entities of two RDF graphs, not necessarily for all, but some , and then piece them together

Henry Story (May 28 2021 at 04:48):

if you did not even have <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> to identify the "isA" relation then you would not a priori be entitled to equate a graph in one DB that had a relation named "isA" with another one in another graph database named "isA". The second graph database may be using relations named "isA" as a shorthand for "issueAtomic" for example.

Henry Story (May 28 2021 at 04:52):

RDF is built on this ability to name things with URLs allowing graphs to be stuck together. With that feature one can of course build a lot more: one can name relations with inferential properties such as <http://www.w3.org/2000/01/rdf-schema#subPropertyOf>, whose inferential property is that if {?r1 rdfs:subPropertyOf ?r2. ?a ?r1 ?b} then { ?a ?r2 ?b }.

Henry Story (May 28 2021 at 05:01):

Yes, you could have a third RDF Graph (G3) that contained only one relation linking a node in G1 to a node in G2.
Those would have to be named nodes if you don't use the inferential properties of OWL I mentioned earlier. Once you have regular or geometric logic, built on identifiable relations such as <http://www.w3.org/2002/07/owl#inverseFunctionalProperty> you can then identify blank nodes or even differently named nodes in two graphs.

A simple example is that <http://xmlns.com/foaf/0.1/mbox> relating an Agent and an email inbox is defined to be inverse functional. So if you have G1:

<https://www.w3.org/People/Berners-Lee/card#i>
          <http://xmlns.com/foaf/0.1/mbox> <mailto:timbl@w3.org> .

<https://webid.mit.edu/timbl#i>
        <http://xmlns.com/foaf/0.1/mbox> <mailto:timbl@w3.org> .

Then, because the objects of the relations are the same, it follows that the subjects can be identified - i.e. fall in the same partition of a given syntax/semantics setoid (?). Expressed in RDF one can conclude that

<https://www.w3.org/People/Berners-Lee/card#i>
       <http://www.w3.org/2002/07/owl#sameAs> <https://webid.mit.edu/timbl#i> .

Henry Story (May 28 2021 at 05:14):

But none of that would work if you could not compose RDF graphs along nodes (or relations) named with the same URLs.

Henry Story (May 28 2021 at 07:00):

Actually here is a view of the sticking together of 3 graphs from my Semweb Pro presentation last year.
My thought, which would need to be verified, is that this fits the Symmetric Monoidal Category view of sticking things together. It would also show how the Semantic Web is an Open World System (which it has to be, as it is designed to make global interlinking of information possible).
Slide from SemWeb Pro presentation

Henry Story (May 28 2021 at 07:48):

Btw, I just found that there is a whole course online on Knowledge Graphs ending next week. The last talk is with Prof Jim Hendler and Doug Lenat What are some research issues in Knowledge Graphs?. Jim Hendler is very famous in the Semantic Web community, and wrote the Book "Semantic Web for the Working Ontologist" whose third edition came out last year. There is a short biography of him there https://twitter.com/bblfish/status/1321753388195975168

@lescarr Are you trying to compete with @jahendler? You've got a way to go still! Check out his bio on edition 3 of his "Semantic Web for the Working Ontologist" (4 lines from the bottom) http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?products_id=1564 #Semweb https://twitter.com/bblfish/status/1321753388195975168/photo/1

- The 🐟‍‍ BabelFish (@bblfish)

Eric Neumann (Jun 01 2021 at 15:14):

I have concerns that the literal notion of a knowledge graph may have serious limitations. Both the nonstandard means of handling nary relations and the expressive bounds of 1-graphs limits the practical kinds of representations possible.

This may also reflect the bounded range of problems that Description Logic can address. It might be helpful to catalog various problems in domains that DL will have issues representing. Many exist in biology that require high order graphs, ie gene transcription factors and regulation.

Henry Story (Jun 01 2021 at 16:05):

I am a new to the "knowledge graph" terminology, so I need to watch a few of those lectures to see where that comes from and what it covers...

Caleb Foong (Jun 02 2021 at 08:41):

@Eric Neumann you might wear to look at https://grakn.ai it addresses some of the problems you mentioned

Henry Story (Jun 03 2021 at 15:44):

I was going to say that it looks to me like TypeDB from grakn is a closed world database. And indeed in the comparison page to the Semantic Web

That is why I recently pointed to John Baez's talk on symmetric monoidal categories, which led me to the PhD thesis by @Brendan Fong which starts with the importance of Open World Systems. I put the first two pages of his thesis on Twitter as those are easily readable even by non-mathematicians.

@johncarlosbaez @ejpatters Ah yes, the preface to Brendan Fong's thesis "The Algebra of Open and Interconnected Systems" https://arxiv.org/abs/1609.05382 should be of great interest to Philosophers as well as #linkeddata folks interested in what is behind the Open World Assumption. cc @DJRoss70 https://twitter.com/bblfish/status/1398230682237911041/photo/1

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (Jun 03 2021 at 15:50):

The idea is quite simple but very deep from those two pages: where closed world mathematics works well for physical systems, it does not work well at all for biological systems. And so of course not for human instititutions either, such as economics. The person who brought economics from to think in terms of this divide is I am told Nicholas Georgescu-Roegen a mathematician who argued in detail the biological aspect of economics and its negenthropic dimension. (He was notably, a research assistant of "creative destruction" Schumpeter.)

If Brendan and John Baez have found the mathematical structural difference between closed world and open world, between physical and biological systems, between entropic and negantropic systems, then this is a hugely important discovery.

Henry Story (Jun 03 2021 at 15:51):

So starting just from that point we should be skeptical that a closed world database is going to be that helpful to @Eric Neumann with modelling problems in biology.

Henry Story (Jun 03 2021 at 15:58):

Is the Semantic Web related to Symmetric Monoidal Categories? Well it happens that 6 months ago before I started the EU project on access control on Solid, I was annotating the Agda-Web-Semantic Library in order to understand what was going on there. It is the Agda proof of the thesis put forward in the article "Integrity Constraints for Linked Data" which has the following abstract.

Henry Story (Jun 03 2021 at 15:59):

Notice the last line "We prove that datasets with integrity constraints form a symmetric monoidal category, from which the soundness of acyclic dependency graphs follows."

Henry Story (Jun 03 2021 at 16:01):

So now I am even more keen to get back to finishing reading that paper and Brendan's thesis :-) (when I get some spare time...)

Henry Story (Jun 03 2021 at 16:12):

Henry Story (Jun 14 2021 at 08:40):

A basic question on the Linked Data Signatures came up that reveals an interesting aspect of RDF. The question was "why sign the graph and not just the bytes?" There is a simple A-level maths answer using combinatorial mathematics. For a graph with

n

subject relation object triples, the number of ways of serialising those into a list is

n!

, i.e. the factorial of

n

scala> def fact(n: BigInt): BigInt =
     |   n match
     |      case 1 => 1
     |      case x => x * fact(n-1)
scala> fact(3)
val res0: Long = 6
scala> fact(5)
val res2: Long = 120
scala> fact(120)
val res4: BigInt = 6689502913449127057588118054090372586752746333138029810295671352301633557244962989366874165271984981308157637893214090552534408589408121859898481114389650005964960521256960000000000000000000000000000

(The same applies for named graphs seen as subject relation object graphName quads).
So with a graph of 120 triples - a very small graph - the number of possible serialisations is huge. And that is without taking into account white-spacing lenience of the basic formats, that there are at least 6 different formats to serialise to that have even more flexibility (some being desgined to be read by humans), and that probably most format (e.g. XML) could be mappedf to RDF.

So an RDF graph, and DataSet (Sets of graphs) considered this way is a very powerful equivalence relation on serialisations. (and we have only been thinking syntactically here: semantics allows one to create equivalences between graphs via identifying the references of nodes).

Henry Story (Jun 14 2021 at 08:44):

The proposal is to create a canonical serialisation of an RDF Graph, hash it and sign that.
But I was just wondering if in the space of all possible ways of canonicalising such a graph, there was a known best way - or most interesting/composable? - way of doing that.

Henry Story (Jun 16 2021 at 17:21):

A discussion on "Principles of Identity in Web Architecture" started on the W3C Technical Architecture Group this week.
I wrote a reply there today referencing work on the Yoneda Lemma, coalgebras, and the recent talk by @John Baez on Symmetric Monoidal Categories. I hope I have not completely mungled all these concepts.
Perhaps some of you will get some calls from W3C folks... :-)

Jon Awbrey (Jun 16 2021 at 22:08):

Identity, Indiscernibility, Individuality, Information, and their Interminglings are perennial topics in Peirce circles, especially in view of his radically pragmatic spins on the questions, pace both Leibniz and nominalists of all stripes. I will dig up some links. JA

Henry Story (Jun 17 2021 at 04:44):

Pat Hayes who contributed to the discussion thread and is famous for his early criticism of AI is a big fan of Peirce I believe. Sadly the W3C has a lossy archive for html e-mails, and so it is difficult to work out what his statements are in his e-mails and what he is replying to. But they were the most fun to read.

Jon Awbrey (Jun 18 2021 at 15:04):

I spent a lot of time in the WC (Ha!) and several Web Ontology forums 15 or 20 years ago. As a rule one wastes a lot of breath spilling all one's best ideas as to what the future might hold and then some Dudes with a military contract come in and tell you This Is The Way It Goes (TITWIG) — and it's always regression to the legacy in place.

Henry Story (Jun 18 2021 at 16:24):

yes, W3C is a consortium that is designed to get often mortal enemies to cooperate and produce standards by convincing enough participants that it is in their interest to spend that time (often 3 years) to work on a standard that everyone will then be able to use.
It is quite amazing that it works.

Henry Story (Jun 18 2021 at 16:27):

It works because the participants follow the dictum that "a rising tide lifts all boats" and they each want to get a bigger part of the pie, but won't get any if it is not available to all to use.
I think one could and perhaps should explain this in terms of the prisoners dilemma and game theory. It's located at MIT, so I would guess that has been done.

Henry Story (Jun 18 2021 at 16:30):

It is actually very important to have large players or extreemly dynamic and ambitious ones. A standard with only a few small players participating is not useful, and really a waste of time.
Anyway, it is all about network effects.

Henry Story (Jun 18 2021 at 16:38):

But ideally - and I think the semantic web is going in that direction - standards would be close to mathematical objects, so that one could have proofs and serious discussions on issues.

Henry Story (Jun 18 2021 at 16:39):

Ah this is a nice video that I think illustrates perfectly what it must be to Work at the W3C:
https://youtu.be/vTwJzTsb2QQ
I have a hunch it may be similar working with mathematicians ;-)

Jon Awbrey (Jun 18 2021 at 17:15):

I still observe/participate in several spin-offs of the old SUO (Standard Upper Ontology) and Ontolog Forums, but they operate more in what one member described as a "water-cooler" kibitzing fashion than a state-of-the-art research SIG. Okay as far as it goes I guess ...

Henry Story (Jun 18 2021 at 17:20):

Ah, yes, I have not participated in the Upper Ontology work nor looked much in that direction. It seemed too "philosophical" ("academic"?) to me. I have been more interested in building applications that would read and write linked data in order to grow the system organically the way the web grew. That is following Ruth Garett Millikan's view that Language falls with the Category of the biological - very broadly understood as: that which reproduces.
Somehow I ended up in Category Theory, because it turned out to be useful :-)

Jon Awbrey (Jun 18 2021 at 18:08):

Very copacetic with what I took away from Chomsky and the evolutionary philosophy of Peirce. Often refer to natural languages as Naturally Evolved Organs — Wake Up, NEO! — and thereby hangs a tail ...

Eric Neumann (Jun 24 2021 at 17:23):

As I stated a few weeks ago, I’m hoping to start a discussion on thinking about the Web in a different light that attempts to include its collective role and activities as a living substrate for multiple authors (human and machine) to extend and modify it across multiple edges in an ever adapting form. This perspective I am proposing for the Web is best understood as a Comonad *, an object from algebraic category theory.

Eric Neumann (Jun 24 2021 at 17:27):

Since its inception, the World Wide Web was always described as a graph of URL internet located documents with http links embedded in each document (page). This has proven to be a very powerful and extensible model for publishing on the web and sharing documents by contextualized reference. Many features have been layered onto this: visually formatted pages, bookmarks, embedded javascript, breadcrumbs, cookies, already-viewed affordances, etc., but all these basically maintain the Web as a stateless entity when traversed and viewed. Even the semantic web emerged as a data extension of the Web with semantics introduced to describe entities and relations more precisely and in support of logical inference, yet the Web itself (http mechanics) doesn’t gain or utilize anything from these semantics, and so we have limited means for its extension. Keeping http simple like this is probably why the Web took off; it also limits its general potential and relies on third-parties for work-arounds, both open and closed.

However, this graph model of the Web is not quite accurate, since in fact the Web changes and the way new links are introduced define critical mechanics of the Web not yet addressed explicitly by a graph model. More importantly, without the ability for users to view a web page (document) or navigate across the links, the Web as only a graph has virtually no value: it needs observers and actors to perform actions onto it. If on the other hand the views, the various contexts of users, and current location of a browser are considered as part of the overall Web model, what emerges is an algebraic framework for the Web (including algebras and coalgebras).

Eric Neumann (Jun 24 2021 at 17:31):

More specifically, if we assume the Web can grow indefinitely (perhaps not an infinite web, but certainly one where we don’t know when it will stop), we will need a formulation that encompasses this, analogous to the concept of streams of data which are List-like but have no obvious size but do have a current index. This is where Comonads possibly come in: they handle structures of unknown size with possible (even multiple) contexts over different of its elements. Comonads (W) consist of 2 maps (aka natural transformations, since a comonad is more accurately defined as an endofunctor):

A coproduct 𝛅: W(X) → W(X) × W(X) a kind of data copy & branch, and a counit 𝛆: W(X) → X that extracts some specific (focused) content out.

Eric Neumann (Jun 24 2021 at 17:39):

A common example used to describe a Comonad is the universal covering, which is a map (functor actually) taking a pointed space (𝑋, 𝑥0) and producing the space of homotopy classes of paths starting at 𝑥0 (think paths on top of other paths). This example extends to the rooted tree model on directed graphs G, whose vertices are all the paths starting from a root 𝑥0, and are connected if they have a single edge between them in G. This notion of spaces of traversals really begins to suggest the link between the usage of the Web and Comonads.

Other familiar example of Comonads are the Reader Comonad (its dual is the Writer Monad), which takes a set X and adds (reads) extra data (A) onto it , and the Stream Comonad, which takes a monoid sequence like time T and adds sets of maps T → X for the various histories or trajectories of X (which are contravariant in T) . The coproduct 𝛅 duplicates the data or relative histories and passes it along, while the counit 𝛆 forgets the rest of the data or the different histories and returns the value at the local context. This further characterizes a comonadic model of how web browsers work with the Web. (see Runar Bjarnason's blog example http://blog.higher-order.com/blog/2016/04/02/a-comonad-of-graph-decompositions/)

The Comonad of a graph can be visualized as a graph of graphs with different context views at each higher-level graph vertex. Going to a page involves selecting an index onto the Web and forming an element of its coproduct, namely the traversal; the browser request of the new page (http-get) at a site and its rendering of the http-response is the extraction (counit 𝛆). That’s all very abstract, but this lets us establish multiple forms of these principles for using with or even extending the current Web.

Eric Neumann (Jun 24 2021 at 17:49):

So, what actually can be the (indexed) contexts on a Comonad of a Web graph? I believe there are several practical candidates which I would like to list for consideration, in hopes they will elicit a useful discussion in this thread…

Eric Neumann (Jun 24 2021 at 17:59):

Eric Neumann (Jun 24 2021 at 18:13):

Also consider, this is happening many times each second across the same Web by web users all over the planet! It's not different from what Tim BL was thinking, but here we include the activities of all users as part of the overall algebra, not just the static Web graph object.

Jon Awbrey (Jun 24 2021 at 18:14):

Dear Eric,
Don't know much about co-monads but this sounds a lot like manifolds to me and I've done some thinking about co-products and wreath products in webby contexts. There is a close connection between manifolds and C.S. Peirce's triadic sign relations.

Henry Story (Jun 24 2021 at 18:21):

Thanks @Eric Neumann . That's right on track for what I was thinking web-cats should be about :-)

Henry Story (Jun 24 2021 at 18:39):

I was looking at monads and comonads about 5 years ago exactly with this type of thinking in mind, but I also felt I needed to learn more about Cats than what I could glean through reading (some excellent) programming blogs such as those @Eric Neumann linked to above.

So my first discovery at university was coalgebras which led me to @Corina Cirstea. Those seemed to fit very nicely to HTTP and I wrote up in my first year report how a Web Resource can be thought of as coalgebraically as a thing which changes state. GET is the method allowing observation of the state of a resource

\text{GET}: S \to R

named by a URL and PUT is the way to change the state of a resource

\text{PUT}: S \to S^{R}

, i.e. give a state of a resource, put is a function that if you give it a new representation will return a new state S.
Coalgebras and comonads are closely related so that was a nice find. Except that we need to then deal with infintely many resources simultaneously. That may well be where the comonadic space comes in nicely.

Eric Neumann (Jun 24 2021 at 18:54):

Jon,
That certainly may be the case, since we are dealing with a graph topology and the triadic reaction you mention could ornament elements of the graph. Pushouts could be regarded as Coproducts could be the semantically constrained mergers of parts of the Web graph to form larger semantically valid graphs. My focus on Comonads is to include some (co)algebraic active elements (e.g., user behavior) in the way the Web is used, and to capture/represent much of what is done as logical formalisms. These hopefully could help developers utilize (Co)Algebra languages for developing more powerful applications and platforms in the future.

Jon Awbrey (Jun 24 2021 at 19:02):

Operating under the influence of Peirce as I do, my Master's Piece used a threesome here. TAP for changing the state based on input, PAT for putting a symbol in the output stream, and APT for testing the equality of two values.

Jon Awbrey (Jun 25 2021 at 17:32):

While I've got it on my mind, here's a few links to what documentation I've put on the web so far about my old Theme One Program.

Henry Story (Jun 26 2021 at 06:03):

I found the book "Diagrammatic Immanence" discussed on the Peirce channel very interesting, but the whole thing is still quite fuzzy. My feeling is that the tripartite structure of Peirce is what J.L Austin onwards thematised under the heading of speech acts. That would fit as Peirce was a pragmatists, and so how one uses words for a pragmatist is essential to understanding their meaning. (It is quite possible that the author did not make that link as he is influenced by Deleuze who was upset with those philosophers - ordinary language philosophers - because they perhaps too often made reference to common sense, which in France or Germany after the second world war may not have seemed as such a good foundation for things, as it might have in the UK or US).

Henry Story (Jun 26 2021 at 06:09):

Be that as it may, if what is at stake are speech acts then I think this is a major part of the web, and I argue for that at length in my second year PhD report. That is what we are discussing here in part when looking at coalgebras. Those are probably just the key ingredient with a lot more required. Session types tend to come up.

So interestingly in the latest research on integrating Akka Typed and Session Types we find dependent function types appear. See this thread: https://twitter.com/bblfish/status/1358412385007112193

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (Jun 26 2021 at 06:15):

So one way one can make @Eric Neumann 's point is that modelling the web as a graph misses out on speech acts - which I call document acts, since there really is no speech involved. It took analytic philosophy about 50 years to cotton on to the importance of speech acts, so it is not surprising that this is being repeated on the web, even by its practitioners.
When one does understand speech acts, then one tends to point out that truth is not the only reason for language, and that can appear to those who are defending truth as crime worthy of excommunication.

Henry Story (Jun 26 2021 at 06:19):

But those are 50-70 year old debates. They are understood now. And we have mathematics for them. I have a feeling that linear logic is one aspect of that: POSTing content to a server (say an order for a book on amazon) creates a new resource and will take money out of your account. Doing it twice will take money ouf of your account twice.

Henry Story (Jun 26 2021 at 06:34):

I was just wondering what Robert Brandom who defends a merging of pragmatic and analytic thinking had to say on Peirce and fell on this article Brandom, Peirce and the overlooked friction of Contrapiction and interestingly enough Diagrams come up there too....

Henry Story (Jun 26 2021 at 09:10):

That article is actually very helpful. It may not be quite fair to Brandom, but it helps a lot in explaining what how the Peirceans think of how diagrams should work.

Henry Story (Jun 26 2021 at 09:17):

If I have understood correctly, it should be quite easy to say what Peircean Diagrams are on the Semantic Web: they are just the RDF Graphs or the RDF DataSets. Those can be expressed as Bicategories of Relations and drawn with string diagrams.
(I have recently suggested that DataSets may be Cofree structures on those graphs, and it seems to work in the code examples I put together).

Jon Awbrey (Jun 26 2021 at 13:15):

There's a long and tangled history here. I would place thinkers like Frank Ramsey, Charles W. Morris, and J.L. Austin in the camp of early assimilationists who attempted to grapple with the issues of pragmatism — its logic, semiotics, and theory of inquiry — but who came to it from a constitutionally different perspective and never quite pierced to the core of it. Some called themselves pragmatists, at least in some phases of their careers, some did not, and some contributed to the popular spin and warp of pragmatic semiotics, but what they turned out all too often clouds the key issues.

Jon Awbrey (Jun 26 2021 at 13:32):

I have 20+ years experience participating in various discussion lists and working groups on so-called “Ontology” and “Semantic Web” topics and I can tell you they have yet to get the first principles of Peirce's semiotics and logical graphs.

Henry Story (Jun 26 2021 at 13:50):

The Web is a structure designed to be used by billions of people, and approachable to nearly anyone to build on with minimal understanding of how it actually works. Most people who use the web don't really understand how it works. I would say that even people who develop web sites don't really understand the architecture. They use it.

In some respects the whole of it is so complex that there is a discipline called Web Science to study it. They had a conference last week https://websci21.webscience.org

The Semweb as a tool that has to be designed to get that type of uptake too, so it has to be aproachable. It is a lot more ambitious in a way, requiring some minimal understanding of logic, the ability to name new words, etc...
There are few people who understand it, because few people are building the apps to get it to work as intended.

But for a pragmaticst that should be no problem: the most important thing is that it needs to work. (If we had to wait for people to understand, we'd never make any progress.)

Still to build it out, I want to work out what the real mathematics behind it is. And I have been gathering quite a lot of different pieces that can be useful.

Henry Story (Jun 26 2021 at 13:56):

So instead of discussing what people on some mailing lists think, it would be more interesting to have your take on whether the presentation of the Semantic Web in @Evan Patterson's Knowledge Representation in Bicategories of Relations captures a good aspect of the conception of Diagrams that Peirce was talking of. These are diagrams that give us first order logic. Those diagrams don't capture modal logic, so I am looking forward to CT getting there too. But first order logic is a good start I would say.

Henry Story (Jun 26 2021 at 14:07):

The problem, is I don't have time to be a Peirce expert. Since this is a Category Theory forum, what we want to do is help integrate his work into Category Theory.
So my recent question is: do the string diagrams of bicategories of relations count as diagrams in Peirce's work? If you have an article that answers that, then that would be fine. But my guess is that if you look at it, with your knowledge of Peirce, it should be quite easy for you to tell.

Henry Story (Jun 26 2021 at 14:47):

As I understand, Category Theory has been developed since the beginning as a framwork to translate theories between different mathematical spaces. So there should be no problem finding that some of Peirce's ideas can be translated into bicategories of relations, or to find the concept of Diagrams taken up in various parts of mathematics, philosophy or engineering. What is important to understand is just what gets lost in a translation and what gets captured by it.

Henry Story (Jun 26 2021 at 15:33):

So it should be really easy to help work out what those diagrams capture and what important pieces are missing. Then we can look to see if the missing pieces are and if

Then one can try to work out what use cases the missing pieces would make possible if available, the cost of developing the pieces, standardising them, the business or geopolitical value in having them, etc... As you see it would be quite possible for there to be missing pieces and for that not to be a problem because there is no value in hainv them right at the start. But perhaps there is....

Jon Awbrey (Jun 26 2021 at 15:34):

Henry Story (Jun 26 2021 at 15:53):

Jon Awbrey (Jun 26 2021 at 16:36):

What they are doing there is highly developed but it starts from a very different starting point and takes very different assumptions for granted.

If you are a programmer, you know how hard it is to explain the things you learn through hard knocks programming practice to folks who have never done that. And of course there are diverse programming styles whose devotees have sundry cognitive styles and difficulty understanding each other.

Programming changes a person. I started out in a proof-theoretic mode, trying to write an ATM for Peirce's α-level logical graphs and I tried all the tricks of the proof-theoretic trade in trying to do that. Failure teaches to try another tack and I gradually, painfully, reluctantly shifted into model-theoretic gear. Long story short and a dozen style changes later I eventually learned one or three things. I'll try to say what those are. I kind of know how that will go ... but maybe it will be healthy exercise.

Eric Neumann (Jun 26 2021 at 17:40):

Henry Story (Jun 26 2021 at 17:51):

I am actually writing a Web Server in Scala called Reactive-Solid, which uses Free Monads (from the cats library) to allow my access control layer to be scripted to fetch the needed data on the server and on the web.
Here is a Diagram of a Web Server with a number of resources and their associated Access Control Rules, and an imports relation which I have built to return me a cofree comonad of all the graphs it found following the :imports link. That seems close to what you are describing, but it's looking at it from the free monad side I think.

Henry Story (Jun 26 2021 at 18:00):

Eric Neumann (Jun 26 2021 at 18:08):

@Henry Story I think this is a specific example of exactly what I was describing. It seems it even demonstrates how a sequence of actions can be combined (monads) and the how the set of structured results (comonadic) are returned from this. I’ve got a hunch that (co)algebras here not only can make web actions sequences well-defined (and therefore consistency checked), but any indexable processing on the Web ala trees, graphs, etc.

Henry Story (Jun 26 2021 at 18:28):

I had also found this page related to a talk Free for DSLs, cofree for interpreters. But I did not completely understand it at the time. Same with the previous talk on UIs...

Henry Story (Jun 26 2021 at 18:38):

Henry Story (Jun 27 2021 at 12:10):

For those who want to know what co-fun is, I think it is what happens when you watch David Laing's Lambda Jam talk Cofun with Cofree Comonads. It is short but it lifts off like a rocket. You get to learn about comonads too on the way. You need a bit of Haskell under your belt though.
The aim of the talk is to show how one can use free and cofree monads together, the one as a DSL and the other as an intepreter.

Henry Story (Jul 03 2021 at 16:12):

I opened an issue on web-cats wiki called Quads and Contexts for the SemWeb to gather pointers on the topic of context in the semantic web. That follows a question on Twitter by Dan Brickley (author on the first RDF specs, famous for friend of a friend ontology, and behind the search engine's schema.org) in a longish twitter thread where I tried to point to how Category Theory could help that effort.

Jon Awbrey (Jul 03 2021 at 16:28):

The matter of context is one of the oldest questions in all the Nerd “Ontology” and Semantic Web working groups I've known over the last 20 years. There's a specific way it's handled in Peircean Semiotics but that has largely flown over the heads or under the radar of all the mainstream legacies. Will dig up some links …

Henry Story (Jul 04 2021 at 07:41):

There is a Zulip thread Optics and Servers related to CT and Web Servers focusing on Optics.

Eric Neumann (Jul 28 2021 at 21:02):

Eric Neumann (Jul 28 2021 at 21:06):

Eric Neumann (Jul 28 2021 at 21:12):

Eric Neumann (Jul 28 2021 at 21:16):

Eric Neumann (Jul 28 2021 at 21:17):

“The path to how I got to this site” is a context that has value for marketers, optimizers, and future smart sites which can use the path to offer more focused local items. In fact, the path is itself a graph of contexts (path history context, PHC) with the head being the current location.

Eric Neumann (Jul 28 2021 at 21:18):

Path Comonads can be saved and analyzed locally by users as part of a knowledge model. Instead of constantly bookmarking pages using weak semantics, the structure of multiple related pages is hyper-bookmarked as a semantic structure with context for a themed knowledge model. This knowledge can be individualized or aggregated with a community, and if indexed forms a Knowledge Context (KC).

Eric Neumann (Jul 28 2021 at 21:20):

Eric Neumann (Jul 28 2021 at 21:24):

Eric Neumann (Jul 28 2021 at 21:28):

Eric Neumann (Jul 28 2021 at 21:29):

I hope to intentionally show which aspects of the Web can be currently implemented, possibly by extending browsers or search tools, as well as ornamenting web sites with additional reachable (http-get) labelled attributes. How the Web mechanism itself could be extended is a real possibility but not yet considered in this initial discussion.

Henry Story (Jul 29 2021 at 05:02):

Just for reference, @Eric Neumann's first part on comonads and the web starts here.

Henry Story (Jul 29 2021 at 05:09):

Eric, I also started a recent thread on learning: (co)algebras and (co)monads. That could be a good place for more theoretical beginners discussions.

Henry Story (Jul 29 2021 at 05:18):

Henry Story (Jul 29 2021 at 05:26):

The Scala comonadic Graph library Quiver, you mentioned is being maintained here.

Henry Story (Aug 09 2021 at 06:15):

So the web is a distributed dynamical stateful system in the form of a graph which is also a database. That then looks like Poly should be the right tool to describe the World Wide Web?

I was thinking resources on the web can be modelled as stateful actors. A single resource can be modelled coalgebraically as a simple lens with getters and setters. That was my first thought 3 years ago when I discovered coalgebras. But then I could not quite work out how the fit the client and the server together and how to get a massively distributed system of billions of such actors.

Ah finally! @myers_jaz explains how Poly relates to and differs from Coalgebras! https://www.youtube.com/watch?v=QNuGyjHJtP8&list=PLhgq-BqyZ7i6IjU82EDzCqgERKjjIPlmh&index=6

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (Aug 13 2021 at 14:47):

There was a conference earlier this year on Poly, which seems to cover a huge amount of things: lenses, comonads, categories, wiring diagrams, ... It is so wild, David Spivak admited that he was Poly Amorous.

I have put together a thread of many talks on the subject, of which this talk @Tarmo Uustalu is very helpful as it is looking at it from the computer science point of view: https://twitter.com/bblfish/status/1426169218869911552

This talk on Polynomial functors is looking at it from the computer science PoV, which is very helpful, as it makes a few links to what is widely known, which otherwise is not so obvious. https://www.youtube.com/watch?v=-klwGDWN54s

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (Aug 13 2021 at 20:39):

Actually that talk by Tarmo Uustalu has a very fun twist in it. They were looking at polynomials nearly 10 years ago from an abstract perspective and came up with a bunch of laws, and could not work out what those meant.... (I don't think I should give away what it turned out to be, but I can understand the surprise!)

Henry Story (Aug 14 2021 at 06:44):

Henry Story (Aug 14 2021 at 07:03):

in one of the last slides of Bryce's talk, there seems to be a fun word game. He writes:
"There is a double category ℂof(ε) of internal categories, functors, and cofunctors..."
Given that

Perhaps a really simple way of explaining ℂof(ε) is that it is a categorification of "Java™ Beans"?

Henry Story (Aug 20 2021 at 12:55):

@Eric Neumann would you be ok with copying your idea of comonads over to the web-cats issue DB? That would help anchor them a bit better for further discussion.

Eric Neumann (Aug 20 2021 at 13:01):

Web-cats issue dB ? Not sure if you’re referring to a journal or another stream?

Henry Story (Aug 20 2021 at 13:02):

Eric Neumann (Aug 20 2021 at 13:02):

Henry Story (Aug 20 2021 at 13:04):

There are good here, it's just that with the stream of discussions they are going to be less easy to discuss. :-)

Eric Neumann (Aug 20 2021 at 13:04):

Henry Story (Aug 20 2021 at 13:04):

Henry Story (Aug 20 2021 at 13:05):

Eric Neumann (Aug 20 2021 at 13:07):

Just let me know the name of an issue to create. It seems Zulip constantly reacts to bright shiny discussion… we need to target web researchers.

Henry Story (Aug 20 2021 at 13:08):

"Comonads and the Web"?
I think there are enough programmers now who know about monads that comonads can be interesting topic.

Henry Story (Aug 20 2021 at 13:13):

We just need to grow the web-cats community :-) so that it can generate some buzz.
Actually the very nice thing about Cats is that it gives us a language where we can bring all the programmers together withouth having to decide on a programming language .

Eric Neumann (Aug 20 2021 at 13:15):

Henry Story (Aug 20 2021 at 13:17):

yes, with time we may think about how one can split the ideas up, as there are a lot of them. :-)

Henry Story (Aug 20 2021 at 13:39):

Henry Story (Aug 20 2021 at 13:42):

The idea with starting Web-cats was to get to the point where we could start a Web-cats W3C Community Group.

Eric Neumann (Aug 20 2021 at 13:49):

Henry Story (Aug 20 2021 at 13:52):

Henry Story (Aug 20 2021 at 14:01):

Eric Neumann (Aug 20 2021 at 16:55):

Henry Story (Aug 20 2021 at 19:10):

Henry Story (Aug 20 2021 at 19:13):

I gave a presentation there. I put up a description of those who spoke here. Tim Berners-Lee was there at least at the beginning. And I mentioned that it would be an interesting thing to put together.

Henry Story (Aug 20 2021 at 19:14):

Community Groups are not that hard to put together though. You just need enough people to get it going. I think it is more important to get the right people interested. Also in the end you would not really want to use the mailing list for much exchange, so it would end up here or another repo. Perhaps in normal times it means people could come to W3C Technical Plenaries or some other meetings like that, more easily. But I think it would not be bad to have a Cats presence at the W3C, just to gather all those that know about it so that there can be a bit richer an exchange.

Henry Story (Aug 23 2021 at 08:00):

Perhaps we should ask support from Topos Insitute for a Web-Cats W3C community Group, or ask them what requirements they think would be useful to have. (one has to make sure it is worth it...)

John Baez (Aug 24 2021 at 04:14):

Henry Story (Aug 24 2021 at 05:54):

Well I was thinking it would be good if the Topos Inst. were involved in the creation of the Group, setting out what the aims could be, and how such interactions could take place. But at least one should chat to see if this make sense.

I first suggested the idea on the semantic web mailing list nearly two years ago. There was the semweb pro meeting last year. But the applicability of Category Theory is not limited to the Semantic Web.

Eric Neumann (Aug 24 2021 at 13:32):

I would suggest outlining a few points of WHY we feel CT is relevant to the Web, past, present and future. This can also include semantic web specific goals, but I'm pretty sure it encompasses web applications, service transactions (especially for multiple agents), future search engines, info source validation, etc. These points may make it more effective for a first series of discussions between the groups.

Valeria de Paiva (Aug 24 2021 at 15:47):

well, I don't think there is work in the Topos Institute n the direction of the semantic web at the moment. I can only speak for myself but while I have done plenty of work of semweb stuff in the past, I am not doing anything on that at the moment.

John Baez (Aug 24 2021 at 16:18):

The Topos Institute is not a large amorphous entity; it's a fairly small group of people. Not counting administrators, the people who work at the Topos Institute are David Spivak, Brendan Fong, Valeria de Paiva and Evan Patterson. There are also a number of summer interns, and I work as their "scientific advisor". So, "getting the Topos Institute involved in this" means finding one or more of these people who are interested in this.

Henry Story (Aug 24 2021 at 16:52):

yes, I was not thinking of making this a huge thing - I would not have time myself.

From my e-mail to one list 2 years ago, we had a little over 5 people express interest in category theory and creating a community group. If you look at the list of members they reach quite widely, so there may be quite a lot more out there interested, participating in various groups.

It would just have to be a space where one can gather people across the w3c with interest in category theory (and type theory) and its application to those technologies. It could allow them to come together and meetup perhaps, learn about what the Topos institute as well as others are doing, ... The mailing list would not be so useful for discussing mathematics due to unclear support of unicode. The gitlab repo and channels such as this one would be where discussions take place, just as most discussions at w3c not happen on github (for better or worse).

But yes, we'd want to keep it low key. I don't see that this is going to be high volume anyway. I mean it is category theory! :-)

Henry Story (Aug 24 2021 at 16:58):

yes, I mentioned the semweb as that is what I have been researching. But it goes much wider. If my intuition that dynamical systems as expressed by Poly could be used to model the Web, then the work going on at the Topos instiute could be directly relevant for modeling the web at large. (see note on actors.

John Baez (Aug 24 2021 at 17:01):

Well, if even you don't have time for this, we should wait for someone who does.

It's all too easy to fantasize about projects that would be good for other people to do.

Henry Story (Aug 24 2021 at 17:02):

yes, I mean I would not have time for a "huge thing". But I'd have time to help put it together and participate where I could.
W3C community groups are lightweight.

This should be contrasted to The W3C Working Groups which need real investment, and support from the likes of IBM, Google, or very large numbers of members, and can cost companies a few man years to be involved in. That is where final standards get developed.
(I participated in one LDP as an individual, and it cost me a lot of time!)

Henry Story (Aug 24 2021 at 17:06):

yes, I mentioned the semweb as that is what I have been researching. But it goes much wider. If my intuition that dynamical systems as expressed by Poly could be used to model the Web, then the work going on at the Topos institute could be directly relevant for modeling the web at large. (see note on actors).

There is work by @Ryan Wisnesky and @Joshua Shinavier from Uber on Algebraic Property Graphs (ie graph databases) which is also something that is being looked at by members of the W3C... I don't claim to be able to keep up with even a fraction of what is going on....

As @Eric Neumann pointed out above, one could put together lists of ways Cats and the web come together.

But I agree the criteria should be that it just brings interested people together to apply category theory to the web, and should not be costly to maintain, and prove valuable by finding new applications.

Eric Neumann (Aug 24 2021 at 17:26):

Henry Story (Aug 25 2021 at 14:00):

Btw. @Eric Neumann, the Quiver Scala library for comonadic graphs (graphs in the context of a node) from Verizon, has been updated to Scala 3. I opened an issue on banana-rdf with links to it.

Eric Neumann (Aug 25 2021 at 15:08):

Henry Story (Aug 25 2021 at 15:12):

Henry Story (Aug 26 2021 at 06:59):

Henry Story (Aug 26 2021 at 15:48):

Eric Neumann (Aug 29 2021 at 13:46):

I’m wondering if lenses are the right abstraction for constraining web interactions (e.g. changing state on 1 or more sites), so that they can’t become corrupted. It could also constrain the output from a site to a browser or web client, prohibiting certain classes of responses.

Henry Story (Aug 29 2021 at 14:15):

I'll try to remain grounded and see how much of a web server can be modelled by poly lenses. If poly is very much like actors, then that would be directly relevant to my programming. Also it would help in Solid argue for access control modes.

Note that there we have a guard in front of every resource that needs to verify if the incoming request is allowed. So that would be the next thing to work out as to how that is represented.

One thing I think I remember reading somewhere is that in reasoning co-monads are related to the left of the turnstile and monads to the right. So that is what makes me think that our agents have the whole web as a co-monad (with only parts of it that are known and only some parts that are trusted).

Eric Neumann (Aug 29 2021 at 14:21):

I’m guessing “to the left of the turnstile” means can extract from an object (comonad)— it can’t insert something (no publicly accessible unit).

Henry Story (Aug 29 2021 at 14:24):

Something like that yes. The left of the turnstile is the environment. Our environment is the Web.

Henry Story (Aug 29 2021 at 14:55):

Henry Story (Aug 29 2021 at 14:57):

It is interesting that an indexed comonad appears here, where the logic of access control requires indexed monads.

Eric Neumann (Aug 29 2021 at 15:24):

Indexing is one of the key means to keep track of comultiplied contained objects within container objects, e.g. lists of lists, graphs of graphs, etc

Eric Neumann (Sep 10 2021 at 14:56):

@Henry Story seeing your discussion of web servers and lenses made me think about a few issues: one of my rationales for inserting CoMonads into web models is that it allows defining the user-browser component to how the web works; what should browsers/clients be allowed to do and what should they not be allowed? Both (all) sides of web stakeholders view pages and/or activity, and they use this info to make the next decision of action.

It now occurs to me that the bigger picture of users + website creators probably should be modeled as a game(s). It’s already been shown that games and lenses have a deep association. We can initially classify these into acceptable games and misuse (true adversarial) games, that is, some are like search sites and productive community sites, while others are about misleading, misinformation, and extracting your funds without return of services. This is interesting from a philosophical point of view, but I wonder if it can help defining proper regulators and safety mechanisms into the system.

Henry Story (Sep 10 2021 at 16:31):

David Lewis in his 1969 PhD thesis Convention - a Philosophical Study, showed how linguistic conventions can be explained as starting off as equilibrium states in games of coordination. He went on to analyse how all of language works that way, as a game of truthfulness and trust. That is the coordination view of games, and that works with the web too: create a URL - any URL - in a domain you possess, and put some content there, and from there on, as people link to it, it will become more anchored , gain a reputation, which will create a type for it if you want: a space of changes that allowably make others keep telling the truth as they link to it. Changes to that document are acceptable in so far as they don't make others liars where they previously were telling the truth. This is known as meta-stability, a word D.K.Lewis uses 3 times in that book.

Access Control as discussed on the security + ct thread here on the other hand is more of an adversarial game where the client wants to prove that it is allowed access to a resource in a mode as sepecificed in the access control document. There the client needs to reason in terms of what the guard takes as facts and find the credential that will help convince it to give access. To do that it can use linked web resources, but clearly not every such resource. The guard will there tend to be a somewhat paranoid reasoner.

Henry Story (Sep 23 2021 at 18:01):

Henry Story (Nov 04 2021 at 18:30):

"HTTP applications are just a Kleisli function from a streaming request to a polymorphic effect of a streaming response - what's the problem?" where @rossabaker explains a web server starting from modelling it as a Request => Response function. #http4s https://www.youtube.com/watch?v=urdtmx4h5LE

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (Apr 19 2022 at 10:37):

The Function Ontology: https://fno.io
"The Function Ontology is a way to semantically declare and describe functions, without depending on the implementation."
I thought this could be of interest to folks here

Henry Story (Apr 20 2022 at 11:55):

Henry Story (May 10 2022 at 06:44):

Henry Story (Aug 09 2022 at 09:29):

@GavinMGleason @namedgraph @TerminusDB @lukefeeney If you delve deeply into the OWL specification docs (admittedly not easy) you will find a 'direct' semantics and also one done via an OWL-RDF-RDFsemantics route, and a proof of their equivalence.

- Pat Hayes (@PatHaye67745536)

Henry Story (Aug 09 2022 at 13:42):

There is an interesting initial discussion on the n3 mailing list on pure functions and RDF https://lists.w3.org/Archives/Public/public-n3-dev/2022Jul/0016.html
I think this is a place where Category Theory has answers that could help a lot, especially @Evan Patterson 's Knowledge Representation in Bicategories of Relations which builds on @David Spivak 's work on functional Ologs, and extending it to relational ologs, ie functors from small bicateogories to Rel (or other monoidal categories).

Some use cases for the existing function ontology is to describe software artifacts and to allow one to describe extensions to mapping languages. But currently that mixes OO constructs, partial functions, etc... That turns out to be useful in places, but it does make one wonder if one could be more precise.

Henry Story (Aug 09 2022 at 14:02):

Henry Story (Aug 23 2022 at 13:03):

Great this channel is now public again, but with the official Zulip theme now!
(the place to ask is on the (non public, ie you need an account) public access topic thread here .

This is allowing me to link semantic web theorists like Doerthe Arndt to the CT community here. Doerte's PhD thesis Notation3 as the Unifying Logic for the Semantic Web looked at N3 logic, developed bottom up by Tim Berners-Lee et al. to see how to bring it on a formal footing by considering the two implementations of it:

See this e-mail on the n3-dev mailing list of w3c pure functions (in rdf) for an example of a discussion where CT could help make a practical difference.

Henry Story (Aug 23 2022 at 17:15):

Some Web slides on N3 logic (essentially first order logic for the web) https://josd.github.io/Talks/2022/08swig/#(1) covering reasoning with proofs, linear logic, etc...
A list of reasoning examples is given on slide 24

Henry Story (Aug 23 2022 at 18:00):

Those slides are from Jos De Roo who I was surprised has been reading @Bob Coecke 's "Picturing Quantum Processes" (see his August 19 Tweet
).

What a nice coincidence https://www.cambridge.org/core/books/abs/picturing-quantum-processes/processes-as-diagrams/8C9F4826C1A690849AEC6AE049F92F1F "Similarly in logic, proofs can be represented by morphisms in a category, with propositions as the objects. This trifecta of morphisms, programs, and proofs are all connected by what’s known as the Curry-Howard-Lambek isomorphism"

- Jos De Roo (@josderoo)

Henry Story (Aug 29 2022 at 11:01):

Has anyone written a good JS library to display RDF ontologies as String diagrams?

I am looking for a good JavaScript library to display RDF ontologies as UML, but it may be interesting to also show string diagrams as shown in the paper "Knowledge Representation in Bicategories of Relations"
https://twitter.com/bblfish/status/1564205045469560834

Anyone know of a good #JS library that can display elegantly an #OWL Ontologies as UML diagrams? That would be very useful to help OO developers read #RDF ontologies...

- The 🐠 BabelFish (@bblfish)

Henry Story (Aug 31 2022 at 20:25):

I am just watching the last talk on HoTT by @Chaitanya Leena Subramaniam "Semantics of HoTT" where he gives Functorial (Lawvere) semantics of HoTT: contexts are objects, context morphisms are ...
I wonder what this type of semantics would look like for RDF? (not so easy as RDF only has one type (perhaps the datatypes could count as distinct ones)...
https://www.youtube.com/watch?v=NpzqeZd4Yw0

Henry Story (Sep 04 2022 at 08:34):

Two intriguing relations between Description Logics (DL) and Functional Programming (FP):

Henry Story (Sep 07 2022 at 19:59):

It looks like we have the next stage after functional and relational Ologs in this research from Michael Lambert a student of @Evan Patterson's !
""My goal in this post is to convince you that double categories are good for knowledge representation, databases, and data manipulation."
https://twitter.com/ToposInstitute/status/1567210128541188097

New blog post: Michael Lambert writes about how data operations are functorial semantics. "My goal in this post is to convince you that double categories are good for knowledge representation, databases, and data manipulation." https://topos.site/blog/2022/09/data-operations-are-functorial-semantics/

- Topos Institute (@ToposInstitute)

I just feel like this is a little bit outside my reach. I would need two lectures to introduce some of the concepts used, which I think I already saw with polynomial functors course...
To generate interest, it would help if one started from a sketch of the practical advantages over relational ologs and how these advantages intuitively relate to the new structure. (Perhaps it is there already, and I just need to read it slowly)

Henry Story (Sep 08 2022 at 08:18):

Because the web can be modeled with actors (and web servers are being built on that model, e.g. akka.io and similar libs in Rust) and there is a close link between actors and the pi calculus, I'll leave a pointer to a very interesting discussion in Zulip CT on recent models of the pi calculus. Some highlights also in this twitter thread https://twitter.com/bblfish/status/1566897926340739080

Henry Story (Jan 17 2023 at 15:32):

Henry Story (Jan 24 2023 at 23:18):

Henry Story (Jan 26 2023 at 11:02):

So I found out that Pat Hayes' BLogic, now RDF surfaces has an initial spec introduction by the Community Group.
https://w3c-cg.github.io/rdfsurfaces/

Note the spec starts referring to Peirce.
Pat Hayes' was making the point that this gives one full first order logic. So I wonder now how that ties in with @Evan Patterson's Bicategory of Relations paper? Are these equivalent? My feeling is that RDF Surfaces must go a bit further, as it is more intensional. But perhaps that reveals itself when adding new types of surfaces...

Ryan Wisnesky (Jan 30 2023 at 02:39):

Henry Story (Jan 30 2023 at 11:02):

yep, that could be an interesting (little?) project. The 1Lab has libraries for bicategories I think https://1lab.dev/Cat.Bi.Base.html
So one would need to look at how that maps to RDF surfaces, for which one would need a formalisation I guess to map to. ( Perhaps just functors from

s,r,o,g: A \to N

, to Set, and natural transformations of those? But one would still need to map it to some formalism that would be agreed to represent surfaces correctly... )
I have no idea how long this could take to do... And I have to work part time....
But I think this could be relevant to the PhD and to my work.

Henry Story (Feb 24 2023 at 13:17):

Thinking about Is OWL/RDF typed or untyped? Should it be?, I started wondering if it could be that RDF is really in the dual space of constructive logic. I know it is build in Set, but I am interested in what the consequences would be if one thought of it as a co-constructive logic.

Ryan Wisnesky (Feb 24 2023 at 16:15):

Based on papers like https://philarchive.org/rec/TRACLF-2, it seems typing remains the same; to obtain a co-constructive logic, you dualize an intuitionistic logic, leaving its type system alone.

Alex Gryzlov (Mar 01 2023 at 11:27):

There are several flavours of "co-constructive" logics: subtractive, bi-intuitionistic, dual-intuitionistic, anti-intuitionistic. Typically what you get is some notion of "subtraction" instead of implication, then negation can be defined as "subtracting from the truth" instead of "implying falsity", etc.

Henry Story (Jun 30 2023 at 09:21):

Sicne 2016 I have been very interested in the no longer maintained library called Quiver because of this very good blog post
"A Comonad of Graph Decompositions"
https://blog.higher-order.com/blog/2016/04/02/a-comonad-of-graph-decompositions/
I had been wondering how that could be used for RDF.
I was just interested in writing a new Scala RDF library so I followed the term "Inductive Graph representation" from a paper in 2001 to discover that work had been done on inductive RDF graph representations too.
I wrote links to all the papers in this mathstodon Toot:
https://mathstodon.xyz/@bblfish/110628405269892430
Do people have experience with working with such Graphs?
one of the diagrams of the Comonad blog

Henry Story (Jun 30 2023 at 09:31):

At the same time I was also sent out some feelers to see if there was any new type of data structure for RDF I should watch out for. Jos de Roo who has been working on RDF surfaces, a way of adding negation to RDF by introducing Peirce's alpha and beta graphs
https://w3c-cg.github.io/rdfsurfaces/
suggested I use those. But what is their data structure?

Henry Story (Jun 30 2023 at 09:36):

That made me wonder if this this could be modelled with something like labelled directed simplicial sets.
Perhaps the apex of a pyramid groups together the graphs at the lower level as being true or false surfaces, and higher order pyramids allow a nesting of these surfaces?

Anyway I was wondering what a good FP representation of such a structure would be.

Stream: theory: applied category theory

Topic: web cats

Henry Story (Jul 27 2020 at 11:05):

Henry Story (Jul 27 2020 at 11:15):

Antonin Delpeuch (Jul 27 2020 at 18:14):

Antonin Delpeuch (Jul 27 2020 at 18:18):

Henry Story (Jul 27 2020 at 20:36):

Antonin Delpeuch (Jul 28 2020 at 19:51):

Henry Story (Jul 31 2020 at 07:42):

Henry Story (Aug 02 2020 at 12:28):

Nathanael Arkor (Aug 02 2020 at 13:50):

Henry Story (Aug 02 2020 at 14:02):

Henry Story (Aug 10 2020 at 15:26):

Henry Story (Aug 29 2020 at 11:19):

Henry Story (Aug 29 2020 at 18:03):

Henry Story (Sep 01 2020 at 16:11):

Henry Story (Sep 11 2020 at 16:31):

Henry Story (Sep 18 2020 at 14:47):

Valeria de Paiva (Sep 18 2020 at 14:52):

Henry Story (Sep 18 2020 at 14:56):

Henry Story (Sep 18 2020 at 15:07):

Henry Story (Sep 18 2020 at 17:06):

Jacques Carette (Sep 18 2020 at 19:08):

Valeria de Paiva (Sep 18 2020 at 19:19):

Henry Story (Sep 18 2020 at 20:10):

Jacques Carette (Sep 18 2020 at 20:17):

Henry Story (Sep 18 2020 at 20:36):

Henry Story (Sep 19 2020 at 06:50):

David Corfield (Sep 19 2020 at 09:53):

David Corfield (Sep 19 2020 at 09:56):

Henry Story (Sep 19 2020 at 10:55):

Henry Story (Sep 19 2020 at 14:55):

John Baez (Sep 19 2020 at 15:04):

Jules Hedges (Sep 19 2020 at 15:11):

Henry Story (Sep 19 2020 at 15:26):

Henry Story (Sep 19 2020 at 15:32):

Jacques Carette (Sep 19 2020 at 15:36):

Henry Story (Sep 19 2020 at 15:36):

Nathanael Arkor (Sep 19 2020 at 15:37):

Nathanael Arkor (Sep 19 2020 at 15:38):

Henry Story (Sep 19 2020 at 15:46):

Jacques Carette (Sep 19 2020 at 15:53):

Henry Story (Sep 19 2020 at 16:06):

Henry Story (Sep 19 2020 at 17:35):

Jacques Carette (Sep 19 2020 at 18:11):

John Baez (Sep 19 2020 at 19:54):

John Baez (Sep 19 2020 at 19:55):

Jacques Carette (Sep 19 2020 at 19:55):

John Baez (Sep 19 2020 at 19:55):

John Baez (Sep 19 2020 at 19:58):

John Baez (Sep 19 2020 at 20:01):

John Baez (Sep 19 2020 at 20:03):

John Baez (Sep 19 2020 at 20:04):

John Baez (Sep 19 2020 at 20:07):

John Baez (Sep 19 2020 at 20:07):

Jacques Carette (Sep 19 2020 at 20:08):

John Baez (Sep 19 2020 at 20:09):

Jacques Carette (Sep 19 2020 at 20:11):

John Baez (Sep 19 2020 at 20:20):

Valeria de Paiva (Sep 20 2020 at 00:30):

Jacques Carette (Sep 20 2020 at 12:15):

Henry Story (Sep 22 2020 at 12:31):

Henry Story (Sep 22 2020 at 12:33):

Henry Story (Sep 22 2020 at 12:37):

Valeria de Paiva (Sep 22 2020 at 13:50):

Valeria de Paiva (Sep 22 2020 at 14:01):

Henry Story (Sep 22 2020 at 14:02):

Henry Story (Sep 22 2020 at 14:09):

Mike Shulman (Sep 22 2020 at 15:26):

Rich Hilliard (Sep 22 2020 at 15:45):

Valeria de Paiva (Sep 22 2020 at 16:13):

Valeria de Paiva (Sep 22 2020 at 16:18):

Henry Story (Sep 22 2020 at 18:11):

David Corfield (Oct 06 2020 at 08:33):

David Corfield (Oct 06 2020 at 08:44):

Henry Story (Oct 06 2020 at 08:54):

Mike Shulman (Oct 08 2020 at 16:48):

Henry Story (Nov 18 2020 at 10:08):

Henry Story (Nov 18 2020 at 10:09):

Henry Story (Nov 26 2020 at 18:03):