Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationProceedings of the 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV)
EditorsSam Staton
Publication statusPublished - 11 Dec 2018
Event34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018) - Halifax, Canada
Duration: 6 Jun 20189 Jun 2018

Publication series

NameElectronic Notes in Theoretical Computer Science
Volume341
ISSN (Electronic)1571-0661

Conference

Conference34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018)
CountryCanada
CityHalifax
Period6/06/189/06/18

Keywords

  • final coalgebra, nondeterministic strategies, trace, algebraic effects, semilattices