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.
@InProceedings{lopez_et_al:LIPIcs.CSL.2018.29, author = {Lopez, Aliaume and Simpson, Alex}, 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 = {Ghica, Dan R. and Jung, Achim}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.29}, 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} }
Feedback for Dagstuhl Publishing