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.
|Name||Electronic Notes in Theoretical Computer Science|
|Conference||34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018)|
|Period||6/06/18 → 9/06/18|
- final coalgebra
- nondeterministic strategies
- algebraic effects