进程演算的可解理论研究

Process calculus has been an active field of research in theoretical computer science. However, the solvability theory of process calculus has not been duly studied, which has become the bottleneck to the further development of process calculus theory. This project aims to provide a foundational framework for the study of solvability theory in the area of process calculus. We choose the Value Passing Calculus (VPC) and its extension to be the basic models of the study on the concurrent solvability theory. The concurrent programming language 'Erlang' will be interpreted as a case study to show the application of the new theory. We will focus on both the properties about the new theory and issues in comparison with the traditional theory. The significance of this project lies in that; we try to build a basic solvability theory which should be coherent with the well-studied model independent interaction theory. This can lead to the solution of some theoretical problems in the previous work. This project will contribute to both the theoretical and application aspects of process calculus.

进程演算是理论计算机科学研究中一个很活跃的分支，但关于进程演算的可解理论一直未得到应有的发展，这成为进程理论进一步发展的瓶颈。本申请项目旨在为研究基于进程演算的可解性理论提供一个基础性框架。具体将研究基于VPC及其扩展模型的并发可解理论，并解释并发程序语言"Erlang"，来说明对新理论的应用。我们在考察新理论本身性质的同时，强调与已有理论的对比研究。本项目的重要性在于试图从底层模型出发，以有效解决以往研究中出现的困难为目标，构建一整套与上层交互式理论相融洽的并发可解理论体系。本项目将对进程演算的理论和应用研究都做出贡献。

在进程演算及其相关研究中，基于模型独立概念的并发可解理论是领域内最重要、也最基础的研究课题之一。通过本项目，我们深入研究和发展了并发可解理论及相关课题。我们的主要研究成果包括如下三个方面：1）提出并研究了VPC_sigma演算，研究了其与经典VPC演算的关系，并用它解释了Core Erlang，论证了新解释的合理性。这是用进程演算解释Erlang语言已知的最强的结论。也是进程可解理论研究的重要推广和应用。 2）在模型独立理论研究方面，我们研究了若干重要一阶移动模型可解问题的类的比较关系，以及基本的完备性关系。得到了一些重要的相对化结论，为研究模型可解理论的层次关系做出了贡献。3）作为可解理论的具体模型，我们还研究了带参数化算子的高阶进程理论。除发展了语义刻画、代数理论等基本工作外，还得到了若干重要的完备性理论和相对表达能力结果。以上研究工作都服务于本项目的研究主题。本项目的研究成果及研究过程中所使用的一些方法和技术对并行理论领域发展有积极作用。.项目执行期间，依托项目发表了十余篇论文。年均支持举办了一次国际学术活动，并参与了多次国内外学术交流活动。依托本项目培养了若干硕士和博士生。