Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Adequacy for Algebraic Effects with State
verfasst von : Gordon Plotkin
Erschienen in: Algebra and Coalgebra in Computer Science
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In previous work we gave an operational semantics and adequacy theorem for algebraic effects in programming languages. This covered finitary algebraic operations, thereby accommodating ordinary and probabilistic nondeterminism, output, and exceptions (but without handling), together with their combinations. With some extra effort, infinitary operations can also be covered, thereby also accommodating input and state. However one does not thereby obtain the natural operational semantics for state, which employs configurations of programs and states. We propose instead to consider the natural coalgebra of states given by the
update
and
lookup
operations; this coalgebra is the final comodel of the Lawvere theory for state. We therefore give an account integrating coalgebras given by comodels of Lawvere theories into the algebraic theory of effects. The coalgebras are used for the dynamics of the state component of the configurations.