The $\mathrm{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 $\mathrm{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 $\mathrm{Caus}[\mathcal{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.
翻译:$\mathrm{Caus}[-]$ 构造取一个“原材料”的基础范畴,并构建一个高阶因果过程范畴,其类型编码系统集合之间的因果(即信号)约束。 notable 的示例包括高阶随机映射范畴和高阶量子通道范畴。 $\mathrm{Caus}[-]$ 中的良类型性对应过程构成的因果一致性,即任何指定类型的局部过程选择都会产生一个遵循因果约束的整体过程。由此,封闭过程总是以概率1发生,排除例如时间循环导致的因果悖论。先前已证明 $\mathrm{Caus}[\mathcal{C}]$ 给出 MLL+MIX 和 BV 逻辑的模型,因此这些逻辑提供因果一致性的充分条件,但未能提供完全刻画。在这项后续工作中,我们引入图类型作为工具,以研究此模型中图上的因果结构。我们探索其性质、标准形式和等价定义;特别地,一个过程服从图的所有信号约束当且仅当其可表示为根据图的边连接的局部因果过程的因子分解的仿射组合。然后利用图类型的性质证明一种保守扩展pomset逻辑的新因果逻辑对因果一致性的完备性。关键额外成分是区分原子的概念,其对应于一阶状态,仅允许信息单向流动。利用因果逻辑保守扩展pomset逻辑的事实,我们最终给出pomset与BV之间的分离陈述的一个具有物理意义的解释。