## Commutativity logic for probabilistic trace equivalence: complete or not?

Joint work with Nathan Bowler.

There’s a well-known monad (on Set) for probabilistic choice – the probability distribution monad. And there’s a well-known monad for I/O – the free monad on a signature (set of operations). We’ve developed a new monad for the combination of probabilistic choice and I/O using trace semantics. But we don’t know whether this third monad is the *tensor* of the first two; tensoring is a standard way of combining monads.

We know the answer to be yes if instead of *infinite probabilistic choice* (i.e. choosing between infinitely many options), we treat only* finite *probabilistic choice, or *nondeterministic *choice whether finite or infinite. It would round out our story beautifully if we could obtain a positive answer for infinite probabilistic choice too. That’s why we care about this question. It boils down to the completeness of an infinitary logic, as described in the extended abstract:

Commutativity logic for probabilistic trace equivalence: complete or not?

As always in science, a negative answer would be equally welcome.