0003 Splitting logics into builder syntax and interpretation
1 Summary
Logics within CatColab specify an underlying double theory, a collection of front-end widgets that users can use to build models, which analyses are available to models in that logic, and maybe some other odds and ends besides. It seems possible that a better separation of these aspects would make the creation and modification of logics simpler for developers, and also provide a clearer foundation for how we might think about migrations between logics.
Here I will sketch out why viewing logics as functors from instances of a schema to models of a theory could be a good idea, and what an implementation might look like. Much of this comes from conversation with Jason Brown and Evan Patterson.
The motto that I might try to summarise this with is something like
The core should know about mathematical abstractions such as double theories, and the front-end must therefore have some understanding of this. But, as much as possible, the front-end should be a builder for instances of schemas with the extra knowledge of how these instances are to be interpreted in the core.
2 Motivation
Consider stock-flow diagrams. These are realised in CatColab as models of a tabulator double theory, and for good reason: the compositional structure of tabulators is useful. However, for many applications (i.e. for many choices of analyses), we could view stock-flow diagrams as Petri nets, where flows become transitions and links simply become another input arc; there exists an ODE semantics on Petri nets that, under this interpretation, precisely recovers mass-action semantics on stock-flow diagrams. Alternatively, we could consider stock-flow diagrams as causal loop diagrams (CLDs), where flows become spans and links become arrows to the apex of a span; there also exists an ODE semantics on (\mathbb{N}-graded) CLDs that, under this interpretation, precisely recovers mass-action semantics on stock-diagrams, but, furthermore, motif finding will show that flows do not compose.
In short, there are many double theories in which we might wish to interpret stock-flow diagrams, but the way in which users can build stock-flow diagrams (i.e. the fact that they can models as colimits of elementary stock-flow diagrams, namely a single stock, a single flow between two stocks, and a single link into a flow) remains unchanged.
This suggests that we could separate out the actual data structure that is being built in a notebook from the way in which it is being computed with by the analyses. That is, we could define the logic of stock-flow diagrams to consist of
- a single front-end builder syntax, namely the ability to create stocks, flows, and links; and
- a collection of interpretations of models thus created in various double theories.
3 Mathematical specification
The mathematics here is somewhat informal, since I have yet to actually be careful with proofs. This should not, however, affect the reading of this RFC, whose purpose is to figure out whether or not this seems like a sensible path to follow in the first place.
Definition 1 A logic \mathtt{L} consists of
- a schema \mathsf{B}, called the builder schema; and
- a collection of (1-)functors I_i\colon[\mathsf{B},\mathsf{Set}]\to[\mathbb{T}_i,\mathbb{S}\mathsf{et}] for some double theories \mathbb{T}_i, where each I_i is called an interpretation (of \mathtt{L}) in \mathbb{T}_i.
There are different adjectives that we can use to describe interpretations, corresponding to factorisations. For example, the co-continuous interpretations are those that arise from functors \mathsf{B}\to[\mathbb{T}_i,\mathbb{S}\mathsf{et}]. There is a more restrictive adjective that we might also be interested in, for which we will give a “definition” that makes sense whenever it makes sense, and doesn’t when it doesn’t.
Definition 2 Let \mathbb{T} be a double category with no non-trivial cells. Define the span replacement \mathsf{SpanRepl}(\mathbb{T}) of \mathbb{T} to be the 1-category given by replacing every loose arrow in \mathbb{T} by a span (thus freely adding a new object for each loose arrow). If \mathbb{T} has tabulators, then \mathrm{Tab}(f) is precisely the apex of the span corresponding to f.
For example, consider the theory \mathbb{T}_\text{cat} for categories, given by a single object V with the loose identity arrow E\colon V\mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}V. Then \mathsf{SpanRepl}(\mathbb{T}_\text{cat}) is the schema for graphs E\rightrightarrows V. As another example, consider the tabulator theory \mathbb{T}_\text{tab} for categories with links. Then \mathsf{SpanRepl}(\mathbb{T}_\text{tab}) is the schema for stock-flow diagrams with links (shown in Section 4).
Definition 3 An interpretation (i.e. functor) I\colon[\mathsf{B},\mathsf{Set}]\to[\mathbb{T},\mathbb{S}\mathsf{et}] is ccf (co-continuous free) if it arises from a profunctor P\colon\mathsf{B}^\mathrm{op}\mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\mathsf{SpanRepl}(\mathbb{T}). It is furthermore truly ccf if P is a functor, and identity ccf if P is the identity functor.
For example, if \mathsf{B} is the schema for graphs, then the profunctor \mathsf{B}^\mathrm{op}\to\mathsf{SpanRepl}(\mathbb{T}_\text{cat})=\mathsf{B} that sends vertices to vertices and edges to spans, gives a ccf interpretation. As another example, if \mathsf{C} is the schema for stock-flow diagrams with links, then the identity functor \mathsf{C}^\mathrm{op}\to\mathsf{SpanRepl}(\mathbb{T}_\text{tab})=\mathsf{C} gives a ccf interpretation (in fact, it gives something much stronger, since the profunctor is actually a functor, and the functor is actually the identity).
I don’t yet know how exactly to classify this hierarchy of adjectives, coming from the increasingly general sequence of types of migration:
| adjective | form |
|---|---|
| identity ccf | \mathsf{B}^\mathrm{op}\xrightarrow{\operatorname{id}}\mathsf{SpanRepl}(\mathbb{T}) |
| truly ccf | \mathsf{B}^\mathrm{op}\to\mathsf{SpanRepl}(\mathbb{T}) |
| ccf | \mathsf{B}^\mathrm{op}\mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\mathsf{SpanRepl}(\mathbb{T}) |
| co-continuous | \mathsf{B}^\mathrm{op}\to[\mathbb{T},\mathbb{S}\mathsf{et}] |
| \mathsf{B}^\mathrm{op}\mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}[\mathbb{T},\mathbb{S}\mathsf{et}] | |
| [\mathsf{B},\mathsf{Set}]\to[\mathbb{T},\mathbb{S}\mathsf{et}] |
but it seems like (a) this would be good to understand, as we do for e.g. duc-queries vs arbitrary queries, and (b) quite a few key examples seem to be at least ccf.
4 Examples
We will take the logic for stock-flow diagrams as our running example, spelling out the mathematical story and then giving pseudo-code for implementation.
4.1 Mathematical example
The logic \mathtt{L}=(\mathsf{B},\{I_\text{tab},I_\text{sgn},I_\text{sym}\}) of stock-flow diagrams is given by the following:
\mathsf{B} is the schema for stock-flow diagrams with links
I_\text{tab}\colon[\mathsf{B},\mathsf{Set}]\to[\mathbb{T}_\text{tab},\mathbb{S}\mathsf{et}], where \mathbb{T}_\text{tab} is the tabulator theory of categories with links, and I_\text{tab} is induced by the “obvious” functor \begin{aligned} \mathsf{B}^\mathrm{op} &\longrightarrow [\mathbb{T}_\text{tab},\mathbb{S}\mathsf{et}] \\\mathsf{Stock} &\longmapsto x \\\mathsf{Flow} &\longmapsto x\to y \\\mathsf{Link} &\longmapsto x\overset{\overset{z}{\downarrow}}{\to}y \end{aligned} (note that this is identity ccf).
I_\text{sgn}\colon[\mathsf{B},\mathsf{Set}]\to[\mathbb{T}_\text{sgn},\mathbb{S}\mathsf{et}], where \mathbb{T}_\text{sgn} is the theory of signed categories, and I_\text{sgn} is induced by the functor \begin{aligned} \mathsf{B}^\mathrm{op} &\longrightarrow [\mathbb{T}_\text{sgn},\mathbb{S}\mathsf{et}] \\\mathsf{Stock} &\longmapsto x \\\mathsf{Flow} &\longmapsto x\xleftarrow{-}f\xrightarrow{+}y \\\mathsf{Link} &\longmapsto x\xleftarrow{-}\overset{\overset{z}{\downarrow}}{f}\xrightarrow{+}y \end{aligned} (note that this is ccf but not truly ccf).
I_\text{sym}\colon[\mathsf{B},\mathsf{Set}]\to[\mathbb{T}_\text{sym},\mathbb{S}\mathsf{et}], where \mathbb{T}_\text{sym} is the (modal) theory of symmetric monoidal categories (written as Petri nets), and I_\text{sym} is induced by the functor \begin{aligned} \mathsf{B}^\mathrm{op} &\longrightarrow [\mathbb{T}_\text{sym},\mathbb{S}\mathsf{et}] \\\mathsf{Stock} &\longmapsto X \\\mathsf{Flow} &\longmapsto X\to\boxed{F}\to Y \\\mathsf{Link} &\longmapsto X\to\overset{\overset{Z}{\downarrow}}{\boxed{F}}\to Y \end{aligned} (note that this is at least co-continuous, but I have no idea how \mathsf{SpanRepl}(-) behaves with respect to modalities, so am not too sure beyond this).
4.2 Pseudo-implementation example
Let’s look at the current front-end definition of stock-flow diagrams. The main chunk of interest (with some lines omitted) is:
primitive-stock-flow.ts
theory: thCategoryLinks.theory(),
modelTypes: [
{
tag: "ObType",
obType: { tag: "Basic", content: "Object" },
name: "Stock",
description: "Thing with an amount",
shortcut: ["S"],
cssClasses: [styles.box],
svgClasses: [svgStyles.box],
},
{
tag: "MorType",
morType: {
tag: "Hom",
content: { tag: "Basic", content: "Object" },
},
name: "Flow",
description: "Flow from one stock to another",
shortcut: ["F"],
arrowStyle: "double",
},
{
tag: "MorType",
morType: { tag: "Basic", content: "Link" },
name: "Link",
description: "Influence of a stock on a flow",
preferUnnamed: true,
shortcut: ["L"],
},
],If we make a rough attempt at translating Section 4.1 into code, then we might end up with something like the following:
builder: [
{
tag: "ObType",
name: "Stock",
description: "Thing with an amount",
shortcut: ["S"],
cssClasses: [styles.box],
svgClasses: [svgStyles.box],
},
{
tag: "MorType",
name: "Flow",
description: "Flow from one stock to another",
shortcut: ["F"],
arrowStyle: "double",
},
{
tag: "MorType",
name: "Link",
description: "Influence of a stock on a flow",
preferUnnamed: true,
shortcut: ["L"],
},
]
interpretations: [
{
name: "Category with links",
theory: thCategoryLinks.theory(),
mapping: [
("Stock", { obType: { tag: "Basic", content: "Object" }}),
("Flow", { morType: { tag: "Hom", content: { tag: "Basic", content: "Object" }}}),
("Link", { morType: { tag: "Basic", content: "Link" }}),
]
},
{
name: "Flows as spans",
theory: thSignedCategory.theory(),
mapping: [
("Stock", { obType: { tag: "Basic", content: "Object" }}),
("Flow", ⚠️),
("Link", ⚠️),
]
},
{
name: "Petri net",
theory: thSymMonoidalCategory.theory(),
mapping: [
("Stock", { obType: { tag: "Basic", content: "Object" }}),
("Flow", { morType: { tag: "Hom", content: { tag: "Basic", content: "Object" }}}),
("Link", {
morType: { tag: "Hom", content: { tag: "Basic", content: "Object" }},
domain: {
apply: { tag: "Basic", content: "tensor" },
⚠️
},
codomain: { apply: { tag: "Basic", content: "Object" }},
}),
]
},
]Any interpretation that is not identity ccf poses a problem: how could (and how should) we express that an object in the schema is sent to an entire motif?
Note that there is still some strict rigidity enforced by this separation, since we declare upfront in builder that e.g. stocks are ObType and flows are `MorType``, which means that we cannot contradict this in any interpretation. I am not sure if this is actually a feature or a bug.
4.2.1 Analyses
If a logic admits interpretations into multiple theories, then we need to consider what should happen with analyses. As an obvious example, visualisation will be different for each interpretation. More serious, however, is an example like motif finding, where the results can be in clear disagreement: e.g. composite flows exist when we interpret a stock-flow diagram with I_\text{tab} or I_\text{sym}, but not with I_\text{sgn}. However, I also think that this is a feature, not a bug.
Analyses could come with drop-down menus for switching between interpretations, and it could be possible that having a global (i.e. per analysis notebook) option for picking one single interpretation proves user-friendly.
4.2.2 Migrations
We can specify a migration between logics in different ways, again in some order of increasing generality:
- Specify a functor of builder schemes
- Specify a migration of instances of builder schemes
- Specify a migration of models of interpretation theories.
5 Rationale and alternatives
We could take this idea and either considerably restrict its scope or lean into it even more. The former would look like still associating a single theory to each logic, but including information about non-trivial migrations within the logic definition itself. The latter would look like actually specifying the builder schema as a schema even more explicitly, building it up as a colimit of \{ \mathsf{Object} \} \qquad\text{and}\qquad \{ \mathsf{Source}\leftarrow\mathsf{Arrow}\to\mathsf{Target} \}. For example, we might define the builder schema for stock-flow diagrams as
interface Object {
name: string;
}
interface Arrow {
name: string;
source: Object[];
target: Object[];
}
let stock: Object = {
name: "Stock",
}
let flow: Arrow = {
name: "Flow",
source: [stock],
target: [stock],
}
let link: Arrow = {
name: "Link",
source: [stock],
target: [flow],
}Another option would be to actually allow for the interpretation functors to be defined in the core, and then merely called in the front-end.
6 Prior art
It seems possible that compositional notebooks can help with defining interpretation functors that send objects to motifs.