Cut and run: musings on relational join, logical cut and communication rules

Unfortunately, this post is likely to be less coherent than the others because i'm just using this to jot down some notes about some -- very possibly wrong -- intuitions regarding relational joins, cut rules (in logics) and comm rules in process calculi. Abramsky has already observed situations where the semantics of processes as 'relations extended in time' provide interpretations of comm rules as 'joins extended in time'. He has also suggested a programme in which proofs are interpreted as processes and the cut rule is interpreted as a kind of comm rule.

i'm revisiting these ideas because i would like to flesh out the story of logic as distributive law. In a nutshell the core idea in the indexed composition proposal comes out of the fact that we can model a term language as an algebra (read monad), T, and a collection as a monad, S. Then formulae are interpreted as building terms over collections. The completeness of the logic is witnessed via a distributive law, l : ST -> TS. That is, every collection of terms can be written as a term of collections. This is a nice framework for the semantics of formulae, but what about proofs?

The thought i've been following is that indexed compositions are the key form of witness to internalize proof. Valid formulae have a normal form as an indexed composition. In some sense that's another way to look at the content of the algebraic databases post. Consider a basic form

f = { (a,b) | a <- A, b <- B, c₁(a,b),...,c_n(a,b) }

and another form

arg = { a | a <- A, c₁'(a),...,c_m'(a) }

We can construct

{ b' | (a',b') <- f, a' <- arg, c₁''(a',b'),...,c_k''(a',b') }

More suggestively, we have something of the form

f = { (a,b) | a <- A, b <- B, c₁(a,b),...,c_n(a,b) },
arg = { a | a <- A, c₁'(a),...,c_m'(a) },
c₁''(a',b'),...,c_k''(a',b') in Admissible
------------------------------------------------------
{ b' | (a',b') <- f, a' <- arg, c₁''(a',b'),...,c_k''(a',b') }

This looks and feels like a cut rule. It also looks and feels like a join. Moreover, there's a procedural way to get this construction from the logic-as-distributive-law. There are some subtleties, however. For example, there are lots of ways to cut two structures together that still conform to this general scheme. Are there conditions that ensure cut elimination?