License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2018.29
URN: urn:nbn:de:0030-drops-96965
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9696/
Go to the corresponding LIPIcs Volume Portal

Lopez, Aliaume ; Simpson, Alex

Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular

pdf-format:
LIPIcs-CSL-2018-29.pdf (0.5 MB)

Abstract

The "generic operational metatheory" of Johann, Simpson and Voigtländer (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on ground-type effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.

BibTeX - Entry

@InProceedings{lopez_et_al:LIPIcs:2018:9696,
  author =	{Aliaume Lopez and Alex Simpson},
  title =	{{Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic  (CSL 2018)},
  pages =	{29:1--29:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Dan Ghica and Achim Jung},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9696},
  URN =		{urn:nbn:de:0030-drops-96965},
  doi =		{10.4230/LIPIcs.CSL.2018.29},
  annote =	{Keywords: contextual equivalence, algebraic effects, operational semantics, domain theory, nondeterminism, probabilistic choice, Markov decision process}
}

Keywords: contextual equivalence, algebraic effects, operational semantics, domain theory, nondeterminism, probabilistic choice, Markov decision process
Collection: 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
Issue Date: 2018
Date of publication: 29.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI