基于通道的高阶进程演算的表达能力的研究

交互是进程演算理论的核心内容；表达能力是交互的一种具体体现。高阶进程能够在通道上传递进程对象，在交互中的行为与传统的一阶进程有很大不同。本项目将研究高阶进程演算表达能力方面的几个重要问题，主要包括三点：1.研究一般情况下，高阶pi演算（不带重名命名及抽象操作）与一阶pi演算在表达能力上的相对关系；2. 寻找从full lambda演算到高阶pi演算的编码，并考察该编码与已有的从full lambda演算到一阶pi演算的编码间的关系；3.探索如何在高阶pi演算中编码条件操作子match 和/或 mismatch等程序语言要素。本项目将在统一的交互式理论框架下展开；研究结果将进一步揭示高阶进程演算的本质特性，对表达能力相关的研究具有重要参考价值。

针对项目的研究内容，对项目的完成情况做以下概述。..首先，关于高阶pi演算与一阶pi演算在表达能力上的相对关系，我们的到了以下几点主要结论。第一，给出了带relabelling操作子的高阶pi演算到一阶pi演算的编码。该编码充分利用了一阶进程的传名能力，强调了传名机制的原子性。第二，作为一个推论，证明了基本高阶pi演算（只具有前缀、并发复合、限制操作）到一阶pi演算的翻译的存在性，该存在性亦可以直接构造证明。第三，一阶 pi 演算无法翻译到基本高阶 pi 演算，该（否定）结论传递了更多信息，不但形式地证明了传进程并不比传名有更强的表达能力，也揭示了如果需要提升高阶进程的表达能力，则必须要扩展基本高阶pi演算。当然，这并非说明高阶pi演算没有实际用途，在一些（建模）场合使用进程传递依然可能比名传递简洁有效。..其次，我们得到了full lambda演算到高阶pi演算的编码策略，该策略与已有的从full lambda演算到一阶pi演算的编码并不兼容，因为它需要本质地使用一些额外的操作（如动态抽象定义、条件元语）。由此可见高阶进程在编码（full） lambda演算或进行解决具体问题算法的编程时，相对一阶演算并不具有优势，但另一方面，从实际角度讲，它们的编程思想（传名之于传进程）有一定互补性。..再次，相应地在上述研究中，我们考察了条件操作子在高阶进程中的解释，其结果显示，在高阶场合下对条件语句的支持较弱，对于多分支的语句无法予以较好地解释，尤其是if…then…else…中对else部分无法进行有效解释。这再次体现了高阶进程在表达能力上与一阶进程的本质不同。..最后，我们还做了一些扩展的探索，例如初步考察了抽象操作的完备性，对lambda演算编码中的局部结构、抽象操作的进一步表达能力等。这些为本项目研究的延续工作提供了基础。