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.

This entry was posted in Uncategorized. Bookmark the permalink.