Tensors of Comodels and Models for Operational Semantics

In seeking a unified study of computational effects, in particular in order to give a general operational semantics agreeing with the standard one for state, one must take account of the coalgebraic structure of 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 ract category theoretic literature, explain its significance for computational effects, and calculate it in leading classes of examples, primarily involving state. Key words: Countable Lawvere theory, model, comodel, global state, arrays, free cocompletion, tensor.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Gordon D. Plotkin, John Power
• Keywords: Computational Effects, Countable Lawvere Theory, ENTCS 2008, General Operational Semantics