Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthormetaweta
   • CommentTimeDec 7th 2010
   • (edited Dec 8th 2010)
   • PermaLink
   Author: metaweta
   Format: MarkdownItexIt looks to me like you can define a labeled transition system object in any pointed category: - objects - $E, V, L$ for edges, vertices, and labels - morphisms - $s:E \to V$ for the source vertex of the edge - $t:E \to V$ for the target vertex of the edge - $l:E \to L$ for the label of the edge - $i:1 \to V$ for the initial state, where 1 is the point object 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$?

   It looks to me like you can define a labeled transition system object in any pointed category:

   • objects
     • $E, V, L$ for edges, vertices, and labels
   • morphisms
     • $s:E \to V$ for the source vertex of the edge
     • $t:E \to V$ for the target vertex of the edge
     • $l:E \to L$ for the label of the edge
     • $i:1 \to V$ for the initial state, where 1 is the point object

   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$?

2. • CommentRowNumber2.
   • CommentAuthorHarry Gindi
   • CommentTimeDec 7th 2010
   • (edited Dec 7th 2010)
   • PermaLink
   Author: Harry Gindi
   Format: MarkdownItexYou should change the category of this post to "mathematics, physics, philosophy".

   You should change the category of this post to “mathematics, physics, philosophy”.

3. • CommentRowNumber3.
   • CommentAuthorDavidRoberts
   • CommentTimeDec 7th 2010
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexYou 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$.

   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$.

4. • CommentRowNumber4.
   • CommentAuthorTim_Porter
   • CommentTimeDec 7th 2010
   • (edited Dec 7th 2010)
   • PermaLink
   Author: Tim_Porter
   Format: MarkdownItexAlthough 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!)

   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!)

5. • CommentRowNumber5.
   • CommentAuthormetaweta
   • CommentTimeDec 8th 2010
   • (edited Dec 8th 2010)
   • PermaLink
   Author: metaweta
   Format: MarkdownItexI'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’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.

6. • CommentRowNumber6.
   • CommentAuthorTim_Porter
   • CommentTimeDec 8th 2010
   • (edited Dec 8th 2010)
   • PermaLink
   Author: Tim_Porter
   Format: MarkdownItexI 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](http://www.daimi.au.dk/~luca/papers.html).

   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.