You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
`0003` Splitting logics into builder syntax and interpretation
3
+
`0003` Splitting logics into builder declaration and interpretation
4
4
author: Tim Hosgood
5
5
date: 2026-03-27
6
6
bibliography: _references.bib
@@ -19,9 +19,20 @@ It seems possible that a better separation of these aspects would make the creat
19
19
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.
20
20
Much of this comes from conversation with Jason Brown and Evan Patterson.
21
21
22
-
The motto that I might try to summarise this with is something like
22
+
The motto that I might try to summarise this with is something like the following:
23
23
24
-
> 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.
24
+
::: {.callout-note}
25
+
### Summary
26
+
27
+
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.
28
+
:::
29
+
30
+
This RFC touches on *two* suggestions:
31
+
32
+
1. Rethinking the front-end editor as an editor for **builder declarations** (@sec-builder-declarations)
33
+
2. Allowing a single front-end logic to have multiple **interpretations** (@sec-interpretations).
34
+
35
+
It is reasonable that each of these suggestions merit their own RFC with more detail; this current document exists more to give context to those future conversations.
25
36
26
37
27
38
@@ -37,7 +48,7 @@ In short, there are many double theories in which we might wish to *interpret* s
37
48
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.
38
49
That is, we could define the logic of stock-flow diagrams to consist of
39
50
40
-
1. a *single* front-end **builder syntax**, namely the ability to create stocks, flows, and links; and
51
+
1. a *single* front-end **builder declaration**, namely the ability to create stocks, flows, and links; and
41
52
2. a *collection* of **interpretations** of models thus created in various double theories.
42
53
43
54
@@ -48,12 +59,58 @@ That is, we could define the logic of stock-flow diagrams to consist of
48
59
*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.*
49
60
50
61
::: {#def-catcolab-logic}
51
-
A **logic** $\mathtt{L}$ consists of
62
+
A **(CatColab) logic** $\mathtt{L}$ consists of
52
63
53
-
1. a schema $\cat{B}$, called the **builder schema**; and
64
+
1. a small (possibly necessarily finite) category $\cat{B}$, called the **builder declaration**; and
54
65
2. a collection of (1-)functors $I_i\colon[\cat{B},\Set]\to[\dbl{T}_i,\SSet]$ for some double theories $\dbl{T}_i$, where each $I_i$ is called an **interpretation** (of $\mathtt{L}$) in $\dbl{T}_i$.
It is reasonable to interpret the builder declaration $\cat{B}$ as a schema, used for building instances $\cat{B}\to\Set$.
72
+
However, this is not quite the attitude that I intend.
73
+
Rather, we should consider $\cat{B}$ as specifying a system of *dependent types*.
74
+
75
+
I am not a type theorist, at all, so I will give an example rather than use more words (and the words I do use will be softened by scare quotes).
76
+
Consider the category
77
+
$$
78
+
\cat{B}
79
+
= (E \rightrightarrows V)
80
+
$$
81
+
which we recognise as the schema for graphs, since to give a functor $G\colon\cat{B}\to\Set$ is precisely to give sets $G(E)$ and $G(V)$ along with source and target functions $s,t\colon G(E)\to G(V)$.
82
+
One can think of constructing the object
83
+
$$
84
+
G(E) \rightrightarrows G(V)
85
+
$$
86
+
by gluing together basic blocks: we can posit the existence of some $e\in G(E)$ (a "walking edge") and this "automatically" implies the existence of two vertices, namely $s(e)$ and $t(e)$.
87
+
We can then posit the existence of, say, $x,y\in G(V)$, and make the identifications $s(e)=x$ and $t(e)=y$.
88
+
89
+
Let's compare this to what happens in practice in e.g. CatColab, where a user is building a graph as a model of the theory of graphs.
90
+
The initial state of a new notebook has $G(E)=G(V)=\varnothing$.
91
+
The user can posit the existence of an edge $e\in G(E)$ by creating a morphism and naming it $e$.
92
+
But this leaves the notebook in an incomplete ("non-compiling") state: the arrow $e$ needs to have a source and target set; CatColab does not freely create two objects for the source and target.
93
+
94
+
This difference in behaviour (or attitude) can be seen as an artefact of working with the 1-categorical schema $E\rightrightarrows V$ rather than the corresponding (under some correspondence that we briefly describe in @sec-interpretations) double-categorical "schema" $V\xproto{E}V$.
95
+
96
+
But we can also change the way that we read our 1-categorical schema.
97
+
Using the fact that our $\cat{B}$ is a direct category, we can start from the locally initial elements (i.e. ones with no incoming morphisms) and assign a degree to each object in $\cat{B}$ such that $\deg(x)<\deg(y)\implies\Hom_\cat{B}(x,y)=\varnothing$ (and we can do this, to be imprecise, in a "best possible way", making each object have the minimal possible degree).
98
+
In our running example of $\cat{B}=(E\rightrightarrows V)$ we can take $\deg(E)=0$ and $\deg(V)=1$.
99
+
Then we can build up the data of *type dependencies* by running over objects of increasing degree: objects of degree $0$ correspond to types with no dependencies; objects of degree $1$ to types with dependencies on those of degree $0$; and so on.
100
+
To return to our example of graphs, we see that we get two types: the non-dependent type $V\colon \mathcal{U}$, and the dependent type $E:V\times V\to\mathcal{U}$.
101
+
This means that to declare a term of type $E$ we need to give two terms of type $V$ at the moment of declaration.
102
+
103
+
Rather than rambling on about type theory (since, again, I do not know about type theory), I will simply repeat the main point:
104
+
105
+
::: {.callout-note}
106
+
### Summary
107
+
108
+
Builder declarations can be understood as describing a system of dependent types, and notebooks are precisely constructions of terms of these types.
109
+
:::
110
+
111
+
112
+
### Interpretations {#sec-interpretations}
113
+
57
114
There are different adjectives that we can use to describe interpretations, corresponding to factorisations.
58
115
For example, the **co-continuous** interpretations are those that arise from functors $\cat{B}\to[\dbl{T}_i,\SSet]$.
59
116
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.
@@ -90,6 +147,12 @@ I don't yet know how exactly to classify this hierarchy of adjectives, coming fr
90
147
91
148
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.
92
149
150
+
::: {.callout-note}
151
+
### Summary
152
+
153
+
Rather than a front-end logic prioritising a *single* double theory in catlog, it could correspond to *multiple* double theories (and perhaps even other things besides).
154
+
:::
155
+
93
156
94
157
95
158
## Examples {#sec-examples}
@@ -161,117 +224,6 @@ The logic $\mathtt{L}=(\cat{B},\{I_\text{tab},I_\text{sgn},I_\text{sym}\})$ of s
161
224
(note that this is at least *co-continuous*, but I have no idea how $\spanr{-}$ behaves with respect to modalities, so am not too sure beyond this).
162
225
163
226
164
-
### Pseudo-implementation example
165
-
166
-
Let's look at the current front-end definition of stock-flow diagrams.
167
-
The main chunk of interest (with some lines omitted) is:
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?
270
-
:::
271
-
272
-
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.
273
-
274
-
275
227
#### Analyses
276
228
277
229
If a logic admits interpretations into multiple theories, then we need to consider what should happen with analyses.
@@ -303,13 +255,13 @@ We can specify a migration between logics in different ways, again in some order
303
255
304
256
We could take this idea and either considerably restrict its scope or lean into it even more.
305
257
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.
306
-
The latter would look like actually specifying the builder schema as a schema even more explicitly, building it up as a colimit of
258
+
The latter would look like actually specifying the builder declaration as a schema even more explicitly, building it up as a colimit of
0 commit comments