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