2026-07-25T06:30:00Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9696 2024-03-06T10:44:51Z ddc:004 open_access

Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular Lopez, Aliaume Simpson, Alex contextual equivalence algebraic effects operational semantics domain theory nondeterminism probabilistic choice Markov decision process 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Aliaume Lopez and Alex Simpson 2018 Is Part Of LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2018.29 urn:nbn:de:0030-drops-96965 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.29 eng https://creativecommons.org/licenses/by/3.0/legalcode