GSOS rules and laws

A rule that specifies a labelled transition system over a (first-order) term/process language is a GSOS rule whenever it is of the form

\frac{
  \{ x_{i_j} \xrightarrow{a_j} y_j \}_{j}
  \quad
  \{ x_{i_k} \not\xrightarrow{b_k} \}_{k}
}{
  f(x_1, \dots, x_n) \xrightarrow{c} t
}

where

a_j, b_k, c are labels in the alphabet
x_{i_k} \not\xrightarrow{b_k} means that the process denoted by variable x_{i_k} cannot emit the label b_k
f is an operation of arity n
1 \leq i_j, i_k \leq n
the x_i and y_j are distinct variables, and no variables other than them appear in the term t

Categorical reformulation

Turi and Plotkin 1997 discovered that a set of GSOS rules can be reformulated as a GSOS law, i.e. a natural transformation

  \sigma : \Sigma(Id \times B) \Rightarrow B \Sigma^\ast

where

\Sigma is the polynomial functor corresponding to the syntax of terms
\Sigma^\ast is the free monad on \Sigma
B is the functor specifying the 'possible behaviours' of the transition system

A tutorial introduction to this correspondence is given by Klin 2011.

References

GSOS rules were first introduced in

Bloom, Bard, Sorin Istrail, and Albert R. Meyer. 1995. ‘Bisimulation Can’t Be Traced’. Journal of the ACM 42 (1): 232–68. https://doi.org/10.1145/200836.200876.

@article{bloom_bisimulation_1995,
	title = {Bisimulation can't be traced},
	volume = {42},
	doi = {10.1145/200836.200876},
	number = {1},
	journal = {Journal of the ACM},
	author = {Bloom, Bard and Istrail, Sorin and Meyer, Albert R.},
	year = {1995},
	pages = {232--268}
}

A tutorial introduction to various rule formats and their equivalent formulations as categorical laws is given in

Klin, Bartek. 2011. ‘Bialgebras for Structural Operational Semantics: An Introduction’. Theoretical Computer Science 412 (38): 5043–69. https://doi.org/10.1016/j.tcs.2011.03.023. pdf

@article{klin_bialgebras_2011,
	title = {Bialgebras for structural operational semantics: {An} introduction},
	volume = {412},
	doi = {10.1016/j.tcs.2011.03.023},
	number = {38},
	journal = {Theoretical Computer Science},
	author = {Klin, Bartek},
	year = {2011},
	pages = {5043--5069}
}

The categorical reformulation of GSOS rules originates in

Turi, D., and G. Plotkin. 1997. ‘Towards a Mathematical Operational Semantics’. In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 280–91. Warsaw, Poland: IEEE Comput. Soc. https://doi.org/10.1109/LICS.1997.614955. pdf

@inproceedings{turi_towards_1997,
	address = {Warsaw, Poland},
	title = {Towards a mathematical operational semantics},
	doi = {10.1109/LICS.1997.614955},
	booktitle = {Proceedings of {Twelfth} {Annual} {IEEE} {Symposium} on {Logic} in {Computer} {Science}},
	publisher = {IEEE Comput. Soc},
	author = {Turi, D. and Plotkin, G.},
	year = {1997},
	pages = {280--291}
}