Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: applied category theory

Topic: Labeled Transition Systems

Jade Master (Sep 12 2020 at 02:07):

Hi,

I thought that I would also ask this question here.

A transition system on A is just a relation T \subseteq A x A. It seems like *morally* a labeled transition should be a span A <- T -> A. This goes with the general philosophy that spans are proof-relevant relations. Is there any relation to the traditional definition?

- fuck the police and ice. (@JadeMasterMath)

Jade Master (Sep 12 2020 at 02:11):

The traditional definition of a labeled transition system is a set of states $S$, a set of labels $Q$, and a function
$f : S \times Q \to 2^S$
or a relation
$f \subseteq S \times Q \times S$
representing the possible evolutions of a state when an event occurs.

Jade Master (Sep 12 2020 at 02:13):

An ordinary transition system on a set of states $S$ is a function
$f: S \to 2^S$
or a relation
$f \subseteq S \times S$.

Cole Comfort (Sep 12 2020 at 02:18):

In $\sf Set$, a span $A \leftarrow T \rightarrow A$ can be seen as the categorified version of a $|A| \times |A|$ matrix over $\mathbb{N}$ where (I think) the sum of all entries is equal to $|T|$. So I don't think that you want to compose these things by pullback, because that is really just matrix composition (or multirelational composition).

Jade Master (Sep 12 2020 at 02:20):

Cole Comfort said:

In $\sf Set$, a span $A \leftarrow T \rightarrow A$ can be seen as the categorified version of a $|A| \times |A|$ matrix over $\mathbb{N}$ where (I think) the sum of all entries is equal to $|T|$. So I don't think that you want to compose these things by pullback, because that is really just matrix composition (or multirelational composition).

Well depends on if you're interested in multirelational composition. It is related to the transitive closure.

John Baez (Sep 12 2020 at 02:22):

A span $A \leftarrow T \to A$ give you a pair of elements of $A$ for each element of $T$.

If $T$ means "transitions" and $A$ means "states", then this sort of transition carries just one state to one other state.

John Baez (Sep 12 2020 at 02:23):

But in an ordinary labelled transition system, each transition carries each state to some set of states.

Jade Master (Sep 12 2020 at 02:26):

Oh yeah. I see what you mean.

John Baez (Sep 12 2020 at 02:33):

I think of a transition system as a box with a bunch of internal states and a button you can push. For each state, there's a set of states it can go to when you push the button.

John Baez (Sep 12 2020 at 02:34):

A labelled transition system is the same sort of thing but with a bunch of buttons.

Jade Master (Sep 12 2020 at 02:35):

I think if you have a span $A \xleftarrow{l} T \xrightarrow{r} A$, then you can get a labeled transition system
$f: A \times R \to 2^A$
where $R$ is the set of fibres of $l$, that is $R = \{ l^{-1} (a) | a \in A \}$.

Jade Master (Sep 12 2020 at 02:38):

Or maybe better would be a function
$f : A \times 2^T \to2^ A$
which sends a pair $(a, V)$ to the set $r(V \cap l^{-1} (a))$

Henry Story (Sep 12 2020 at 07:11):

Isn't the span the representation of a graph? Then you can look at it as a transition system if you think of moving from node to node by following arrows. If you have $s,t,o: A \to N$ then you have a graph with labelled arrows, which you can follow the labels on. Viewing it as a transition system is viewing it co-algebraically.
I think @David Spivak in "7 Sketches" relates both to Matrices and multiplication. (I had not done matrix multiplication for 30 years until reading his book)

Henry Story (Sep 12 2020 at 07:14):

RDF Graphs are essentially of the form $s,t,o: A \to N$. But there is an extension where those can be embedded in the larger space of $s,t,o,g: A \to N$ hypergraphs. This allows one to take into account where the information in a graph was found. It thus gives one the beginning of a logic of saying-that.

Henry Story (Sep 12 2020 at 07:32):

Now I think there is something going on in RDF and OWL to do with moving between an algebraic view of $s,r,o: A \to N$ graphs and how they can be composed, and the coalgebraic view of moving through the nodes. This comes out in @Valeria de Paiva 's Constructive Description Logics: what, why and how. She shows very concisely in 1 page, how there are two ways to move from description logics to subsets of First order logic: one a direct translation to FOL, and 2 a translation via Kripke propositional Modal Logic. (Description logics are implemented in RDF graphs, btw.) Going via Kripke Modal Logic is clear looking at the graph coalgebraically. And that fits because following @Corina Cirstea Modal Logics are Coalgebraic. So when one looks at a graph as a transition system one is also thinking of it in modal logic terms.
There is a version of OWL (Ontology Web Language) that is limited to rule based logics called OWL-RL. But there are other profiles of OWL that are more expressive. And my guess is that they can do that while maintaining some complexity results because they are thinking of traversing a graph coalgebraically, ie. as a state machine, or rather a labelled transition system.

Screen-Shot-2020-09-12-at-09.19.24.png

Valeria de Paiva (Sep 12 2020 at 16:34):

Henry Story said:

This comes out in Valeria de Paiva 's Constructive Description Logics: what, why and how. [...] Going via Kripke Modal Logic is clear looking at the graph coalgebraically. And that fits because following Corina Cirstea Modal Logics are Coalgebraic. So when one looks at a graph as a transition system one is also thinking of it in modal logic terms. [...] And my guess is that they can do that while maintaining some complexity results because they are thinking of traversing a graph coalgebraically, ie. as a state machine, or rather a labelled transition system.

Screen-Shot-2020-09-12-at-09.19.24.png

Many thanks @Henry Story for bringing this old draft to light, I need to go back to that! thanks also for reminding me of Cirstea et al paper on coalgebraic modal logic. I would've never drawn the kinds of conclusions you and the coalgebraic community draw, because influenced by Curry-Howard, I wanted proofs in constructive description logic to be some kind of restricted lambda-calculus terms. I tend to think of Kripke or frame semantics as simply another semantics, so wouldn't naturally think of it $$Prop\to \powerset (W)$$ as a blueprint for all kinds of semantics.
actually, if anything (because Kripke semantics is posetal) I would prefer to think of categorical semantics as the blueprint for all semantics. But I don't know how to do it, really. and the connection with graphs and transition systems is very interesting!