Initial Algebras and Final Coalgebras Consisting of Nondeterministic Finite Trace Strategies

Nathan Bowler, Paul Blain Levy, Gordon Plotkin

Research output: Contribution to journalArticlepeer-review

Abstract

We study programs that perform I/O and finite or countable 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.
Original languageEnglish
Pages (from-to)23-44
Number of pages22
JournalElectronic Notes in Theoretical Computer Science
Volume341
DOIs
Publication statusPublished - 11 Dec 2018

Fingerprint Dive into the research topics of 'Initial Algebras and Final Coalgebras Consisting of Nondeterministic Finite Trace Strategies'. Together they form a unique fingerprint.

Cite this