Semantics for Local Computational Effects

John Power

Research output: Contribution to journalArticlepeer-review

11 Citations (Scopus)

Abstract

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.
Original languageEnglish
Pages (from-to)355-371
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
Volume158
DOIs
Publication statusPublished - 5 May 2006

Fingerprint Dive into the research topics of 'Semantics for Local Computational Effects'. Together they form a unique fingerprint.

Cite this