Initial Algebras and Final Coalgebras Consisting of Nondeterministic Finite Trace Strategies

Nathan  Bowler; Paul Blain Levy; Gordon Plotkin

doi:10.1016/j.entcs.2018.11.003

Initial Algebras and Final Coalgebras Consisting of Nondeterministic Finite Trace Strategies

Nathan Bowler, Paul Blain Levy, Gordon Plotkin

Research output: Contribution to journal › Article › peer-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 language	English
Pages (from-to)	23-44
Number of pages	22
Journal	Electronic Notes in Theoretical Computer Science
Volume	341
DOIs	https://doi.org/10.1016/j.entcs.2018.11.003
Publication status	Published - 11 Dec 2018

Access to Document

10.1016/j.entcs.2018.11.003Licence: Creative Commons: Attribution (CC-BY)

Initial algebras and final coalgebras consisting of nondeterministic finite trace strategiesFinal published version, 316 KBLicence: Creative Commons: Attribution (CC-BY)

https://www.sciencedirect.com/science/article/pii/S1571066118300835?via%3DihubLicence: Creative Commons: Attribution (CC-BY)

Cite this

@article{e1b5360ecacc465fada9f9acc946bf0c,

title = "Initial Algebras and Final Coalgebras Consisting of Nondeterministic Finite Trace Strategies",

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.",

author = "Nathan Bowler and Levy, {Paul Blain} and Gordon Plotkin",

note = "Paper is originally part of 'Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV)'",

year = "2018",

month = dec,

day = "11",

doi = "10.1016/j.entcs.2018.11.003",

language = "English",

volume = "341",

pages = "23--44",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

}

TY - JOUR

T1 - Initial Algebras and Final Coalgebras Consisting of Nondeterministic Finite Trace Strategies

AU - Bowler, Nathan

AU - Levy, Paul Blain

AU - Plotkin, Gordon

N1 - Paper is originally part of 'Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV)'

PY - 2018/12/11

Y1 - 2018/12/11

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

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

U2 - 10.1016/j.entcs.2018.11.003

DO - 10.1016/j.entcs.2018.11.003

M3 - Article

VL - 341

SP - 23

EP - 44

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -

Initial Algebras and Final Coalgebras Consisting of Nondeterministic Finite Trace Strategies

Abstract

Access to Document

Fingerprint

Cite this