Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
Authors
Colleges, School and Institutes
External organisations
- Universitat Hamburg, Germany
- University of Edinburgh
Abstract
We study programs that perform I/O and finite nondeterministic choice, up to finite trace equivalence. For well-founded programs, we characterize which strategies (sets of traces) are definable, and axiomatize trace equivalence by means of commutativity between I/O and nondeterminism. This gives the set of strategies as an initial algebra for a polynomial endofunctor on semilattices. The strategies corresponding to non-well-founded programs constitute a final coalgebra for this functor. We also show corresponding results for countable nondeterminism.
Details
Original language | English |
---|---|
Title of host publication | Proceedings of the 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV) |
Editors | Sam Staton |
Publication status | Published - 11 Dec 2018 |
Event | 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018) - Halifax, Canada Duration: 6 Jun 2018 → 9 Jun 2018 |
Publication series
Name | Electronic Notes in Theoretical Computer Science |
---|---|
Volume | 341 |
ISSN (Electronic) | 1571-0661 |
Conference
Conference | 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018) |
---|---|
Country | Canada |
City | Halifax |
Period | 6/06/18 → 9/06/18 |
Keywords
- final coalgebra, nondeterministic strategies, trace, algebraic effects, semilattices