Distributive laws are important for algebraic reasoning in arithmetic and logic. They are equally important for algebraic reasoning about concurrent programs. In existing theories such as Concurrent Kleene Algebra, only partial correctness is handled, and many of its distributive laws are weak, in the sense that they are only refinements in one direction, rather than equalities. The focus of this paper is on strengthening our theory to support the proof of strong distributive laws that are equalities, and in doing so come up with laws that are quite general. Our concurrent refinement algebra supports total correctness by allowing both finite and infinite behaviours. It supports the rely/guarantee approach of Jones by encoding rely and guarantee conditions as rely and guarantee commands. The strong distributive laws may then be used to distribute rely and guarantee commands over sequential compositions and into (and out of) iterations. For handling data refinement of concurrent programs, strong distributive laws are essential.

翻译：分配律对于算术和逻辑中的代数推理至关重要，同样也对并发程序的代数推理具有同等重要性。在现有理论（如并发克林代数）中，仅处理部分正确性，且许多分配律是弱形式的——仅表现为单向细化而非等式相等性。本文聚焦于强化现有理论以支持证明强分配律（即等式形式），并在此过程中推导出具有普遍性的定律。我们的并发细化代数通过同时允许有限与无限行为来支持完全正确性，通过将依赖与保证条件编码为依赖命令与保证命令，实现了Jones提出的依赖/保证方法。强分配律可进一步用于将依赖与保证命令分配到顺序组合中，以及迭代结构的嵌入与提取。对于处理并发程序的数据细化，强分配律具有基础性意义。