TY - CHAP

T1 - Discrete Lawvere theories

AU - Power, John

PY - 2005

Y1 - 2005

N2 - We introduce the notion of discrete countable Lawvere V-theory and study constructions that may be made on it. The notion of discrete countable Lawvere V-theory extends that of ordinary countable Lawvere theory by allowing the homsets of an ordinary countable Lawvere theory to become homobjects of a well-behaved axiomatically defined category such as that of ω-cpo’s. Every discrete countable Lawvere V-theory induces a V-enriched monad, equivalently a strong monad, on V. We show that discrete countable Lawvere V-theories allow us to model all the leading examples of computational effects other than continuations, and that they are closed under constructions of sum, tensor and distributive tensor, which are the fundamental ways in which one combines such effects. We also show that discrete countable Lawvere V-theories are closed under taking an image, allowing one to treat observation as a mathematical primitive in modelling effects.

AB - We introduce the notion of discrete countable Lawvere V-theory and study constructions that may be made on it. The notion of discrete countable Lawvere V-theory extends that of ordinary countable Lawvere theory by allowing the homsets of an ordinary countable Lawvere theory to become homobjects of a well-behaved axiomatically defined category such as that of ω-cpo’s. Every discrete countable Lawvere V-theory induces a V-enriched monad, equivalently a strong monad, on V. We show that discrete countable Lawvere V-theories allow us to model all the leading examples of computational effects other than continuations, and that they are closed under constructions of sum, tensor and distributive tensor, which are the fundamental ways in which one combines such effects. We also show that discrete countable Lawvere V-theories are closed under taking an image, allowing one to treat observation as a mathematical primitive in modelling effects.

UR - http://dx.doi.org/10.1007/11548133_22

U2 - 10.1007/11548133_22

DO - 10.1007/11548133_22

M3 - Chapter

VL - 3629

T3 - Lecture Notes in Comput. Sci.

SP - 348

EP - 363

BT - Algebra and Coalgebra in Computer Science First International Conference, CALCO 2005, Swansea, UK, September 3-6, 2005. Proceedings

PB - Springer

CY - Berlin

ER -