Alex Simpson: Contextual equivalence for algebraic effects under call-by-value, illustrated using combined probability and nondeterminism
I will present a systematic study of contextual equivalence in the presence of algebraic effects, adapting the "generic operational metatheory" of Johann, Simpson and Voigtländer (LiCS 2010) from its original call-by-name setting to call-by-value. As in the previous work, contextual equivalence is defined by specifying a basic operational preorder on ground-type effect trees. The main focus on the talk will be on three different approaches to defining such preorders:
(i) using direct operational considerations,
(ii) via a domain-theoretic monad, and
(iii) via (in)equational axiomatisations.
These will be illustrated via a nontrivial case study: the combination of probabilistic choice with (either angelic or demonic) nondeterminism. In each case (angelic or demonic), the three methods of specifying the basic preorder (operationally in terms of Markov decision processes, denotationally using a suitable powerdomain, and axiomatically) lead to a single canonical relation of contextual equivalence.
