From comodels to coalgebras: state and arrays

John Power, Olha Shkaravska

Research output: Contribution to journalArticle

25 Citations (Scopus)

Abstract

We investigate the notion of a comodel of a (countable) Lawvere theory, an evident dual to the notion of previous termmodelnext term. By taking the forgetful functor from the category of previous termcomodelsnext term to Set, every (countable) Lawvere theory generates a comonad on Set. But while Lawvere theories are equivalent to finitary monads on Set, and that result extends to higher cardinality, no such result holds for comonads, and that is not only for size reasons: it is primarily because, while Set is cartesian closed, Setop is not. So every monad with rank on Set generates a comonad on Set, but not conversely. Our leading example is given by the countable Lawvere theory for global state: its category of previous termcomodels is the category of arrays, yielding a precise relationship between global state and arrays. Restricting from arbitrary comonads to those comonads generated by Lawvere theories allows us to study new and interesting constructions, in particular that of tensor product.
Original languageEnglish
Pages (from-to)297-314
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Volume106
DOIs
Publication statusPublished - 11 Dec 2004

Fingerprint

Coalgebra
Tensors
Countable
Monads
Term
Cartesian
Functor
Tensor Product
Cardinality
Closed
Arbitrary

Cite this

From comodels to coalgebras: state and arrays. / Power, John; Shkaravska, Olha.

In: Electronic Notes in Theoretical Computer Science, Vol. 106, 11.12.2004, p. 297-314.

Research output: Contribution to journalArticle

Power, John ; Shkaravska, Olha. / From comodels to coalgebras: state and arrays. In: Electronic Notes in Theoretical Computer Science. 2004 ; Vol. 106. pp. 297-314.
@article{8d6a3543fe324cbb9cefc3d893656d7d,
title = "From comodels to coalgebras: state and arrays",
abstract = "We investigate the notion of a comodel of a (countable) Lawvere theory, an evident dual to the notion of previous termmodelnext term. By taking the forgetful functor from the category of previous termcomodelsnext term to Set, every (countable) Lawvere theory generates a comonad on Set. But while Lawvere theories are equivalent to finitary monads on Set, and that result extends to higher cardinality, no such result holds for comonads, and that is not only for size reasons: it is primarily because, while Set is cartesian closed, Setop is not. So every monad with rank on Set generates a comonad on Set, but not conversely. Our leading example is given by the countable Lawvere theory for global state: its category of previous termcomodels is the category of arrays, yielding a precise relationship between global state and arrays. Restricting from arbitrary comonads to those comonads generated by Lawvere theories allows us to study new and interesting constructions, in particular that of tensor product.",
author = "John Power and Olha Shkaravska",
year = "2004",
month = "12",
day = "11",
doi = "10.1016/j.entcs.2004.02.041",
language = "English",
volume = "106",
pages = "297--314",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - From comodels to coalgebras: state and arrays

AU - Power, John

AU - Shkaravska, Olha

PY - 2004/12/11

Y1 - 2004/12/11

N2 - We investigate the notion of a comodel of a (countable) Lawvere theory, an evident dual to the notion of previous termmodelnext term. By taking the forgetful functor from the category of previous termcomodelsnext term to Set, every (countable) Lawvere theory generates a comonad on Set. But while Lawvere theories are equivalent to finitary monads on Set, and that result extends to higher cardinality, no such result holds for comonads, and that is not only for size reasons: it is primarily because, while Set is cartesian closed, Setop is not. So every monad with rank on Set generates a comonad on Set, but not conversely. Our leading example is given by the countable Lawvere theory for global state: its category of previous termcomodels is the category of arrays, yielding a precise relationship between global state and arrays. Restricting from arbitrary comonads to those comonads generated by Lawvere theories allows us to study new and interesting constructions, in particular that of tensor product.

AB - We investigate the notion of a comodel of a (countable) Lawvere theory, an evident dual to the notion of previous termmodelnext term. By taking the forgetful functor from the category of previous termcomodelsnext term to Set, every (countable) Lawvere theory generates a comonad on Set. But while Lawvere theories are equivalent to finitary monads on Set, and that result extends to higher cardinality, no such result holds for comonads, and that is not only for size reasons: it is primarily because, while Set is cartesian closed, Setop is not. So every monad with rank on Set generates a comonad on Set, but not conversely. Our leading example is given by the countable Lawvere theory for global state: its category of previous termcomodels is the category of arrays, yielding a precise relationship between global state and arrays. Restricting from arbitrary comonads to those comonads generated by Lawvere theories allows us to study new and interesting constructions, in particular that of tensor product.

UR - http://dx.doi.org/10.1016/j.entcs.2004.02.041

U2 - 10.1016/j.entcs.2004.02.041

DO - 10.1016/j.entcs.2004.02.041

M3 - Article

VL - 106

SP - 297

EP - 314

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -