并发交互的几何学:通过多个令牌处理多个端口(长版)
The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens (Long Version)
摘要:
我们介绍了一个几何的相互作用模型马扎的多端口相互作用组合子,图论的形式主义,它能够忠实地捕捉并发计算所体现的进程代数一样的$π$ -演算。引入的模型是基于令牌机,其中不是一个而是多个令牌被允许在同一时间遍历底层网络。我们证明了引入的模型的合理性和充分性。前者被证明是一个模拟结果之间的令牌机得到沿任何减少序列。后者是通过对网络和令牌机的收敛性进行精细分析而获得的。
英文摘要:
We introduce a geometry of interaction model for Mazza's multiport interaction combinators, a graph-theoretic formalism which is able to faithfully capture concurrent computation as embodied by process algebras like the $π$-calculus. The introduced model is based on token machines in which not one but multiple tokens are allowed to traverse the underlying net at the same time. We prove soundness and adequacy of the introduced model. The former is proved as a simulation result between the token machines one obtains along any reduction sequence. The latter is obtained by a fine analysis of convergence, both in nets and in token machines.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。