多态π演算的互模拟等价关系及其公理化

On the Bisimulation Equivalences in Polymorphic π-Calculus and Axiomatisations

类型系统在分布式系统理论中有着非常重要的作用。在为π演算引入多态类型系统后,需要对新的环境下进程的等价关系进行研究。在多态类型系统下,环境只能得知进程中通道的抽象类型,而无法得知通道的具体类型,此时环境的区分能力被削弱,所得到的互模拟关系更为粗糙。本文在以往文献研究的基础上给出了多态π演算互模拟的一个公理系统,并证明了公理系统的一致性和完备性。

Type systems are playing an increasingly important role in the theory of distributed systems. Polymorphism constrains the power of observers by preventing them from directly manipulating data values whose types are abstract, leading to notions of equivalence much coarser than the standard untyped ones. In this paper, we study the impact of polymorphism on the algebraic theory of the 〖WTBX〗π〖WTBZ〗calculus. Precisely, we give an axiomatisation of the polymorphic 〖WTBX〗π〖WTBZ〗calculus, which is both sound and complete on the closed finite terms.