文章基本信息

标题：Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular
本地全文：下载
作者：Aliaume Lopez ; Alex Simpson
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：119
页码：1-17
DOI：10.4230/LIPIcs.CSL.2018.29
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：contextual equivalence; algebraic effects; operational semantics; domain theory; nondeterminism; probabilistic choice; Markov decision process