带参数化操作的高阶进程研究

Higher-order process models are the extension of sequential higher-order functions in the setting of concurrent computation, and achieve distributed computation through process-passing. The theoretical framework of higher-order processes is essentially different from that of first-order processes. The operation of parameterization is frequent in programming languages, and includes process parameterization and name parameterization. Parameterization is an effective way to increase the capability of higher-order processes in concurrent computation. However, there still exist some critical open problems concerning parameterization, which keeps the higher-order process theory and method from further developing. .. This project focuses on the following aspects. .(1) Simpler characterization of bisimulation on higher-order processes with parameterization; .(2) The expressiveness of higher-order processes in the setting of parameterization;.(3) Decidability of strong bisimulation on higher-order processes with parameterization, axiomatization, and the design and analysis of related algorithms... This project is aimed at largely expanding the theoretical framework of higher-order process models, through exploiting and replying to several important open problems concerning parameterization over higher-order processes. The outcome of this project is expected to provide referential insight for research on higher-order process models and, more broadly, concurrent computational models as well.

高阶进程模型是顺序计算式高阶函数在并发计算场合的扩展，通过进程传递来实现分布式计算，在理论体系上与一阶进程模型有本质不同。参数化是程序语言中的常见操作，分为进程参数化和名参数化两类，是提升高阶进程并发计算能力的有效方法。对于高阶进程模型中的参数化操作，仍有一些重要问题目前尚无解答，因而阻碍了高阶进程理论及方法的进一步发展。.. 本项研究主要探讨下列问题：.（1）参数化场合高阶进程的互模拟简化刻画；.（2）参数化条件下高阶进程的表达能力；.（3）带参数化操作高阶进程的强互模拟的可判定性、公理系统及相关算法的设计与分析。.. 本项目将深化拓展高阶进程的模型体系，探索与回答关于参数化操作的若干重要问题，为高阶进程模型及更广泛的并发计算模型的研究提供借鉴。

本项目经过四年的研究，探索了参数化高阶进程模型的若干关键问题，得到了一系列重要结论。具体包括以下：..（1）关于参数化高阶进程的互模拟简化刻画。证明了含有名抽象且以进程抽象为辅的进程传递模型中，可以得到上下文互模拟的简化刻画，在该刻画中成功定义了正规互模拟（nomal. bisimulation），同时给出了相比以往更直接的证明刻画正确性的方法。.（2）关于参数化高阶进程的表达能力。给出了一个更加简洁、直观的参数化高阶进程对一阶进程的编码，证明了编码的全抽象性质。此外，证明了带进程参数化的高阶进程的交互完备性，说明进程参数化与名参数化在表达能力的意义上地位对等，在计算、交互意义上两者都有其价值。同时，在证明技术上，我们建立了参数化高阶进程中上下文互模拟的up-to context技术，该技术此前在高阶模型中尚无相关结论。.（3）关于参数化高阶进程的可判定性、公理系统及相关算法。证明对于配备两种参数化的高阶进程，强互模拟依然是可判定的，并且目前领域内已知的强互模拟都是重叠的，因而也都是可判定的。对没有restriction操作的参数化高阶进程的强互模拟完成公理化，公理系统与已有系统的不同之处在于扩展了与参数化操作对应的结构处理规则，我们证明了公理系统的完备性。进一步，我们给出了强互模拟的检测算法，该算法利用公理系统中的核心规则，将强互模拟检测转化为语法树的相等检测。算法的时间复杂度为O(nlog(n))，空间复杂度为O(n)，其中n为检测进程的尺寸。..本项目的结果深度拓展了高阶进程的模型体系，给出了参数化操作的若干重要问题的解答，并提供了一些有用的处理技术，这些为高阶进程模型及更广泛的并发模型的相关后续研究提供了有价值的参考。