Tensors of Comodels and Models for Operational Semantics

AbstractIn seeking a unified study of computational effects, one must take account of the coalgebraic structure of state in order to give a general operational semantics agreeing with the standard one for state. Axiomatically, one needs a countable Lawvere theory L, a comodel C, typically the final one, and a model M, typically free; one then seeks a tensor C⊗M of the comodel with the model that allows operations to flow between the two. We describe such a tensor implicit in the abstract category theoretic literature, explain its significance for computational effects, and calculate it in leading classes of examples, primarily involving state