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: Chapter in Book/Report/Conference proceeding › Conference contribution

1 Citation (Scopus)

193 Downloads (Pure)

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.

Original language	English
Title of host publication	Proceedings of the 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV)
Editors	Sam Staton
Pages	23-44
DOIs	https://doi.org/10.1016/j.entcs.2018.11.003
Publication status	Published - 11 Dec 2018
Event	34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018) - Halifax, Canada Duration: 6 Jun 2018 → 9 Jun 2018

Publication series

Name	Electronic Notes in Theoretical Computer Science
Volume	341
ISSN (Electronic)	1571-0661

Conference

Conference	34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018)
Country/Territory	Canada
City	Halifax
Period	6/06/18 → 9/06/18

Keywords

final coalgebra
nondeterministic strategies
trace
algebraic effects
semilattices

Access to Document

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

Bowler_Levy_&_Plotkin_Initial_algebras_and_final_Electronic_Notes_in_Theoretical_Computer_Science_2018
Checked for eligibility: 29/05/2019 Bowler, Nathan, Paul Blain Levy, and Gordon Plotkin. "Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies." Electronic Notes in Theoretical Computer Science 341 (2018): 23-44. https://doi.org/10.1016/j.entcs.2018.11.003
Final published version, 316 KBLicence: Creative Commons: Attribution (CC BY)

https://www.mathstat.dal.ca/mfps2018/preproc/

Cite this

Bowler, N., Levy, P. B., & Plotkin, G. (2018). Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies. In S. Staton (Ed.), 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

@inproceedings{62d54dc5895a402487ec58271953c9ca,

title = "Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies",

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

keywords = "final coalgebra, nondeterministic strategies, trace, algebraic effects, semilattices",

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

year = "2018",

month = dec,

day = "11",

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

language = "English",

series = "Electronic Notes in Theoretical Computer Science",

pages = "23--44",

editor = "Sam Staton",

booktitle = "Proceedings of the 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV)",

note = "34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018) ; Conference date: 06-06-2018 Through 09-06-2018",

}

Bowler, N, Levy, PB & Plotkin, G 2018, Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies. in S Staton (ed.), 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

Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies. / Bowler, Nathan; Levy, Paul Blain; Plotkin, Gordon.
Proceedings of the 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV). ed. / Sam Staton. 2018. p. 23-44 (Electronic Notes in Theoretical Computer Science; Vol. 341).

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

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 -

Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this