Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 6 of 6
It looks to me like you can define a labeled transition system object in any pointed category:
Is that right?
Also, I assume that labeled transition systems are also interpreted in Set; when a path through the system has the same source and target $S$, is the function assigned to that path allowed to be an arbitrary function from $S$ to itself, or must it be the identity on $S$?
You should change the category of this post to “mathematics, physics, philosophy”.
You can consider this as an internal pointed graph over the chaotic graph on $L$ in the case that binary products exist, but you only really need a category with a terminal object, not a pointed category.
’interpreted in Set’ doesn’t mean much to me (although I think very structually) - it certainly isn’t the same as a labelled transition system object in Set. My guess is that you are looking at a collection of sets and functions between them as transitions. Then in that case you are allowed - without knowing anything about applications - to have non-identity endomorphisms of $S$.
Although the point is not discussed as such there, I would recommend glancing at the paper by Goubault and Mimram, which is linked to from the transition system page. There is also the coalgebra interpretation of them that is worth looking at. If I may play devils advocate a moment, I would ask what the point of generalising as such. There are very important and fascinating applications of LTS in mathematical biology, operational research, and other areas, but they need slightly different contexts, e.g., probabilistic, Markov chain, tropical algebra, timed, etc. These look to me to be more ’enriched’ rather than ’internal’ versions. Perhaps the right level of generality to pitch this theory at is not yet clear and is worth working on.
The final query on #1 is that loops can be sent to anything so I agree completely with David. Again look at Goubault and Mimram, and think of the other interpretations as they will govern what restraints there are in the general case. (Also I think LTS is limited in what it can model … like everything, … so think of the situation first and see if an LTS encodes some of it, then start adding bells and whistles to the LST!)
I’m just trying to understand bisimulation as it applies to lambda, pi, and blue calculus. I think in the context of lambda calculus, states are terms and labels are somehow connected to the alpha, beta, and eta rewrite rules—but it’s not immediately clear to me how that works, since those rules could potentially apply at multiple places within the term.
I have not a good enough knowledge of the pi and blue calculus to be able to answer in detail. There is, however, work by Yves Guiraud on using polygraphs to study rewriting in the lambda calculus. There are also Petri net models for some parts of linear logic, and they may be relevant, again see Yves (Two polygraphic presentations of Petri nets, Theoretical Computer Science 360 (2006), no. 1-3, 124–146.)
Returning to your original question, perhaps you want to control things more by varying the structure of $L$. The labelling alphabet then can be a free thing and have rewrite rules governing the higher dimensional structure. Instead of a LTS you will get a higher dimensional TS, something along the lines of G.L. CATTANI and V. SASSONE. Higher Dimensional Transition Systems. In Proceedings of the 11th Symposium on Logic in Computer Science, LICS ‘96, pages. 55-62, IEEE Press, 1996. , which seems to be available from Gian Luca.
1 to 6 of 6