Document Open Access Logo

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

Authors Aliaume Lopez, Alex Simpson

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2018.29.pdf
  • Filesize: 473 kB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
  • Theory of computation → Denotational semantics
  • Theory of computation → Axiomatic semantics
Keywords
  • contextual equivalence
  • algebraic effects
  • operational semantics
  • domain theory
  • nondeterminism
  • probabilistic choice
  • Markov decision process

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Aliaume Lopez and Alex Simpson. Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.29

Author Details

Aliaume Lopez
  • École Normale Supérieure Paris-Saclay, Université Paris-Saclay, France
Alex Simpson
  • Faculty of Mathematics and Physics, University of Ljubljana, Slovenia

References

  1. U. Dal Lago, F. Gavazzo, and P. Blain Levy. Effectful Applicative Bisimilarity: Monads, Relators, and Howe’s Method. In Proceedings of 32nd Annual Symposium on Logic in Computer Science, 2017. Google Scholar
  2. Jean Goubault-Larrecq. Full abstraction for non-deterministic and probabilistic extensions of PCF I: the angelic cases. Journal of Logic and Algebraic Methods in Programming, 84:155-184, 2015. Google Scholar
  3. Jean Goubault-Larrecq. Isomorphism theorems between models of mixed choice. Mathematical Structures in Computer Science, 27(6):1032-1067, 2017. Google Scholar
  4. Reinhold Heckmann. Probabilistic domains. In Proceedings of CAAP '94, number 787 in Lecture Notes in Computer Science. Springer, 1994. Google Scholar
  5. Martin Hyland, Gordon Plotkin, and John Power. Combining effects: Sum and tensor. Theoretical Computer Science, 357(1):70-99, 2006. Google Scholar
  6. Patricia Johann, Alex Simpson, and Janis Voigtländer. A generic operational metatheory for algebraic effects. In 2010 25th Annual IEEE Symposium on Logic in Computer Science, pages 209-218, July 2010. Google Scholar
  7. Klaus Keimel and Gordon D. Plotkin. Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science, 13(1), 2017. Google Scholar
  8. Dexter Kozen. A probabilistic PDL. Journal of Computer and System Sciences, 30(2):162-178, 1985. Google Scholar
  9. Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005. Google Scholar
  10. Matteo Mio. Upper-expectation bisimilarity and łukasiewicz μ-calculus. In Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, pages 335-350, 2014. Google Scholar
  11. Michael Mislove. Models supporting nondeterminism and probabilistic choice. In José Rolim, editor, Parallel and Distributed Processing: 15 IPDPS 2000 Workshops Cancun, Mexico, May 1-5, 2000 Proceedings, pages 993-1000. Springer Berlin Heidelberg, Berlin, Heidelberg, 2000. Google Scholar
  12. Michael Mislove, Joël Ouaknine, and James Worrell. Axioms for probability and nondeterminism. Electronic Notes in Theoretical Computer Science, 96:7-28, 2004. Google Scholar
  13. Gordon Plotkin and John Power. Adequacy for algebraic effects. In International Conference on Foundations of Software Science and Computation Structures, pages 1-24. Springer, 2001. Google Scholar
  14. Gordon Plotkin and John Power. Notions of computation determine monads. In International Conference on Foundations of Software Science and Computation Structures, pages 342-356. Springer, 2002. Google Scholar
  15. Gordon Plotkin and Matija Pretnar. A logic of algebraic effects. In Proceedings of the 23rd Annual Symposium on Logic in Computer Science, 2008. Google Scholar
  16. Andrea Schalk. Algebras for generalized power constructions. PhD thesis, TH Darmstadt, 1993. Google Scholar
  17. Alex Simpson and Niels Voorneveld. Behavioural equivalence via modalities for algebraic effects. In Proceedings of 27th European Symposium on Programming (ESOP). Springer, 2018. Google Scholar
  18. Michael B. Smyth. Power domains and predicate transformers: A topological view. In Proceedings of International Colloquium on Automata, Languages, and Programming ICALP 1983, volume 154 of Lecture Notes in Computer Sciece, pages 662-675. Springer, 1983. Google Scholar
  19. Sam Staton. Instances of computational effects. In Proceedings of the 28th Annual Symposium on Logic in Computer Science, 2013. Google Scholar
  20. Regina Tix, Klaus Keimel, and Gordon Plotkin. Semantic domains for combining probability and non-determinism. Electronic Notes in Theoretical Computer Science, 222:3-99, 2009. Google Scholar
  21. Daniele Varacca and Glynn Winskel. Distributing probabililty over nondeterminism. Mathematical Structures in Computer Science, 16(1), 2006. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact