A complete logic for causal consistency

The Caus[-] construction takes a base category of ``raw materials'' and builds a category of higher order causal processes, that is a category whose types encode causal (a.k.a. signalling) constraints between collections of systems. Notable examples are categories of higher-order stochastic maps and higher-order quantum channels. Well-typedness in Caus[-] corresponds to a composition of processes being causally consistent, in the sense that any choice of local processes of the prescribed types yields an overall process respecting causality constraints. It follows that closed processes always occur with probability 1, ruling out e.g. causal paradoxes arising from time loops. It has previously been shown that Caus[C] gives a model of MLL+MIX and BV logic, hence these logics give sufficient conditions for causal consistency, but they fail to provide a complete characterisation. In this follow-on work, we introduce graph types as a tool to examine causal structures over graphs in this model. We explore their properties, standard forms, and equivalent definitions; in particular, a process obeys all signalling constraints of the graph iff it is expressible as an affine combination of factorisations into local causal processes connected according to the edges of the graph. The properties of graph types are then used to prove completeness for causal consistency of a new causal logic that conservatively extends pomset logic. The crucial extra ingredient is a notion of distinguished atoms that correspond to first-order states, which only admit a flow of information in one direction. Using the fact that causal logic conservatively extends pomset logic, we finish by giving a physically-meaningful interpretation to a separating statement between pomset and BV.