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.

I think you can show completeness if you can prove cancellation (e.g.., 1/2(A+B) \equiv 1/2(A+C) ==> B \equiv C).

How does cancellation imply completeness? I’d love to hear!

Here’s the basic idea. (Note: I’ll not bother to normalize expressions to amplitude 1.)

Let T_i be an enumeration of terms over (c,*) (i.e., binary trees). We want to reduce an expression M=M_0 to a normal form (+i:p_i T_i), where the sequence p_i is lexicographically minimal. We can compute the coefficient p_0 by rewriting M_0 to a sum over trees, computing the amplitude of each trace of T_0 in M_0, taking the minimum p_0 of these amplitudes, and rewriting M_0 to p_0 T_0 + M_1. We then compute p_1 from M_1, etc. So we have

M_i = p_i T_i + M_{i+1}

We want to do all of these rewritings in parallel, using summation, but we can’t, as (sum i: M_i) might diverge. However, using cancellation, we can get rid of any trees common to M_i and M_{i+1}, leaving

F_i = p_i T_i + W_i

(Think of F and W standing for “fuel” and “waste”; waste is essentially produced by a*b + c*d = a*d + b*c (“switching”), where a*d is the product we want for T_i, and b*c turns into waste.) If the total fuel or waste is bounded, then

(+i: F_i) = (+i: p_i T_i) + (+i: W_i)

Since, in the original process, M and all of the waste produced are consumed as fuel, (+i: F_i) = M + (+i: W_i), so cancelling all the waste, M = (+i: p_i T_i) and we’re done. So this reduces the problem to organizing things so as to bound the fuel/waste.

Let me summarize. We already knew the following facts:

(1) Every finitely probabilistic command is equal to a normal form:

(+i: p_i f_i (M_i,j)_j) where all the f_i’s are distinct and each M_i,j’s is a normal form.

(2) Every command is equal to

(+i: p_i f_i (M_i,j)_j) where all the f_i’s are distinct.

(3) Every command is equal to

1/2 M_0 + 1/4 M_1 + …

where each M_i is finitely probabilistic.

From this correspondence, I’ve learnt the following:

(4) If M is a command and N is a finitely probabilistic command

and p in [0,1] and p tr(N) 0. Induct on N in normal form, using (2).

Now suppose M and N are two commands with tr(M) = tr(N).

Put N = 1/2 N_0 + 1/4 N_1 + … by (3).

Obtain M = 1/2 N_0 + 1/2 A_0 by (4).

So tr(A_0) = tr(1/2 N_1 + 1/4 N_2 + …).

Obtain A_0 = 1/2 N_1 + 1/2 A_1 by (4).

So tr(A_1) = trace(1/2 N_2 + 1/4 N_3 + …).

Obtain A_1 = 1/2 N_2 + 1/2 A_2 by (4).

Etc.

So 1/2 M + 1/2 (1/2 A_0 + 1/2 A_1 + …) = 1/2 N + 1/2 (1/2 A_0 + 1/2 A_1 + …)

Cancellation would give M = N.

Thanks, Ernie! This has been very helpful.