We have several papers proposing denotational semantics for various PP formalisms. It would be good to be able to compare them. Here’s a challenge to the authors of these papers:

For your semantics, please give a few examples of each of the following:

- interesting equivalences between open terms that are equated in your semantics. These should include both equivalences that are expressible in other formalisms, and those that are particular to the language that you are modeling.
- interesting equivalences between open terms that are
*not*equated in your semantics. Please explain why you believe these pairs of terms should be equivalent, and why they are not equated by your semantics. - terms that are equated in your semantics, but perhaps should not be considered equivalent (if any).

You can do this in the comments or as new posts, or at worst, in your posters.

Having these examples in hand will enable us to have much more fruitful discussions about the various proposed semantics.

Looking forward to a fun discussion,

–Mitch

Our poster is specifically about the semantics of probabilistic choice (which I’ll write “<w>” in ASCII, for various w in [0,1]), and specifically its interaction with nondeterministic choice (“[]”).

We declare various properties of <w> and [] in isolation (associativity, commutative, idempotence, etc). We also declare that probabilistic choice distributes over nondeterministic choice:

m <w> (n [] p) = (m <w> n) [] (m <w> p)

We do *not* declare that nondeterminstic choice distributes over probabilistic:

m [] (n <w> p) /= (m [] n) <w> (m [] p) — in general

because if you have both distributivities, the theory collapses; for example,

m <w> n

= {- idempotence of [] -}

(m <w> n) [] (m <w> n)

= {- assuming [] distributes over <w> -}

((m [] m) <w> (m [] n)) <w> ((n [] m) <w> (n [] n))

= {- idempotence and commutativity of [] -}

(m <w> (m [] n)) <w> ((m [] n) <w> n)

= {- associativity etc of <w>; let w’ = 1-w, v=w^2+w’^2 -}

(m <w^2/v> n) <v> (m [] n)

and so any straight probabilistic choice gets polluted with some fraction of nondeterminism too (see “Unifying Theories of Programming with Monads”, UTP 2012, p23).

We declare that both operators are *algebraic*, which means that composition (monadic bind) distributes backwards over them:

(m <w> n) >>= k = (m >>= k) <w> (n >>= k)

(m [] n) >>= k = (m >>= k) [] (n >>= k)

We do *not* declare that composition distributes forwards over either choice. In particular, if you combine this property

m >>= (\ x -> k x <w> k’ x) /= (m >>= k) <w> (m >>= k’) — in general

and idempotence of [], you can conclude the undesirable distributivity of [] over <w> (see our abstract for the calculation). However, this property

m >>= (\ x -> k x <w> k’ x) = (m >>= k) <w> (m >>= k’) — for deterministic m

does seem to hold in the special case deterministic m; in particular, it holds for probability distributions alone, when not interacting with nondeterminism. In “Just Do It” (ICFP 2011), we wrongly asserted this property in general: as an *axiom* of the equational theory of probabilistic choice, so inherited when probabilistic choice is combined with nondeterministic. It should have been a *theorem*, provable in certain models of the theory of probabilistic choice, but not provable in others (such as those that add nondeterminism). So the bottom line of our poster is that these equational properties are tricky to get right!

Here’s a related question for each proposal of a denotational semantics: What is a distribution that you can barely express in your language, and what is a distribution that you can almost express in your language?