Psi-演算重新审视：连通性与组合性
摘要：Psi-计算是一种参数化的进程计算框架，与流行的pi-计算扩展，如显式融合计算、应用pi-计算和spi-计算类似。对于框架中的所有计算，机械化证明了标准的代数和同余性质适用于所有计算。Psi-计算的局限性在于通信通道必须是对称和可传递的。在本文中，我们为Psi-计算提供了一种新的操作语义，允许我们解除这些限制并简化一些证明。关键技术创新是用原因给过渡加标注——描述它们起源的范围和通道的信息。我们提供了机械化证明，表明我们的扩展是保守的，并且保持了强和弱相似性的标准代数和同余性质。我们展示了与一个约简语义和钟腔伯努利性的对应关系。我们展示了如何捕获之前超出Psi-计算范围的带预排序的pi-计算，并展示了如何在非常强的质量标准下对混合选择进行编码。
作者：Johannes {AA}man Pohjola
论文ID：1909.06692
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22