Pointwise Extensions of GSOS-Defined Operations

Final coalgebras capture system behaviours such as streams, infinite trees and processes. Algebraic operations on a final coalgebra can be defined by distributive laws (of a syntax functor $\FSig$ over a behaviour functor $F$). Such distributive laws correspond to abstract specification formats. One such format is a generalisation of the GSOS rules known from structural operational semantics of processes. We show that given an abstract GSOS specification $\rho$ that defines operations $\sigma$ on a final $F$-coalgebra, we can systematically construct a GSOS specification $\ov\rho$ that defines the pointwise extension $\ov\sigma$ of $\sigma$ on a final $F^A$-coalgebra. The construction relies on adding a family of auxiliary ``buffer'' operations to the syntax. These buffer operations depend only on $A$, and so the construction is uniform for all $\sigma$ and $F$.