Semantics for Local Computational Effects

Starting with Moggi's work on monads as refined to Lawvere theories, we give a general construct that extends denotational previous termsemanticsnext term for a global previous termcomputationalnext term effect canonically to yield denotational previous termsemanticsnext term for a corresponding previous termlocalnext termprevious termcomputationalnext term effect. Our leading example yields a construction of the usual denotational previous termsemanticsnext term for previous termlocalnext term state from that for global state. Given any Lawvere theory L, possibly countable and possibly enriched, we first give a universal construction that extends L, hence the global operations and equations of a given effect, to incorporate worlds of arbitrary finite size. Then, making delicate use of the final comodel of the ordinary Lawvere theory L, we give a construct that uniformly allows us to model block, the universality of the final comodel yielding a universal property of the construct. We illustrate both the universal extension of L and the canonical construction of block by seeing how they work in the case of state.