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.

4 Responses to Commutativity logic for probabilistic trace equivalence: complete or not?

  1. Ernie Cohen says:

    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).

  2. Paul Blain Levy says:

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

  3. Ernie Cohen says:

    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.

  4. Paul Blain Levy says:

    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.

Leave a Reply