# Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

## Standard

**Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies.** / Bowler, Nathan; Levy, Paul Blain; Plotkin, Gordon.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

## Harvard

*Proceedings of the 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV).*Electronic Notes in Theoretical Computer Science, vol. 341, pp. 23-44, 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018), Halifax, Canada, 6/06/18. https://doi.org/10.1016/j.entcs.2018.11.003

## APA

*Proceedings of the 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV)*(pp. 23-44). (Electronic Notes in Theoretical Computer Science; Vol. 341). https://doi.org/10.1016/j.entcs.2018.11.003

## Vancouver

## Author

## Bibtex

}

## RIS

TY - GEN

T1 - Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies

AU - Bowler, Nathan

AU - Levy, Paul Blain

AU - Plotkin, Gordon

PY - 2018/12/11

Y1 - 2018/12/11

N2 - 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.

AB - 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.

KW - final coalgebra

KW - nondeterministic strategies

KW - trace

KW - algebraic effects

KW - semilattices

U2 - 10.1016/j.entcs.2018.11.003

DO - 10.1016/j.entcs.2018.11.003

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 23

EP - 44

BT - Proceedings of the 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV)

A2 - Staton, Sam

T2 - 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018)

Y2 - 6 June 2018 through 9 June 2018

ER -