基于π演算的编程与表达能力研究

论文摘要

π演算是由Milner、Parrow和Walker基于CCS演算提出的能够描述并发计算的模型。它是目前最重要的进程演算,因此其它模型与它之间的表达能力比较有着重要意义:对于一些顺序计算模型,如果能找到它们在π演算中的编码,那么我们可以从并发的角度来研究顺序计算;对于一些看似比π演算能描述更多现象的计算模型,比如能够描述移动设备上的移动计算的Ambient演算,如果能够找到它们在π演算中的编码,那么就进一步证明了π演算的表达能力。这样的问题一些已有了答案,而一些仍然悬而未决,其中比较著名的就是λ演算在π演算中是否存在编码的问题。本文运用基于π的编程提出一个解决上述问题的统一方法:即将其它模型的语法语义用程序解释,然后再用π演算进行编程,从而得到由其它模型到π演算的编码。这样的方法简单直接,我们用这种方法找到了λ演算在π演算中的编码,并研究了MA演算在π中的编码。我们相信此方法可以用来解决更多模型与π演算之间的表达能力比较问题。本文的主要贡献可概括为以下三个方面:1.基于π演算的编程与表达能力.π演算一直被人们当成进程代数的范例来研究,而从程序语言角度对π演算进行的研究不多。事实上,π演算有着天生的编程能力,可以方便地对各种数据结构进行编程。本文使用π演算对链表、树等常见数据结构及其操作进行了刻画和研究。模型之间表达能力比较的重要方法之一就是设计从一个模型到另一个模型的编码,可是往往由于模型之间的差别太大,这样的编码很难找到。大多数模型的对象都可以用程序来解释,归约的发生就像程序运行之后数据发生变化,本文以Spi演算、λ演算和MobileAmbient演算为例,用程序直观地解释了它们的语法语义。从而提出一种基于π的编程方法来辅助设计其它模型在π演算中的编码,使得原本很难联系的模型之间的编码变得简单直接。2.λ演算与π演算.上述方法的一个成功应用就是回答了一个长久以来未解决的问题:λ演算到π演算上有没有一个好的编码?Milner早在1990年就给出了Lazyλ演算到π演算的编码,Lazyλ是一个受限制的λ版本,Milner提出疑问,他认为完全λ演算的归约规则要从π的角度去解释是相当难的,甚至可能不存在这样的解释。本文提出将λ演算中的项表示为二叉树,β归约理解为对树结构的调整,我们可以发现λ演算的归约规则比Lazyλ演算的归约规则在树结构上更加对称,更加优美。在将二叉树和对树结构的操作用π编程之后,我们就得到了从λ演算到π演算的编码。为了证明编码保持(preserves)并反映(re?ects)归约,文章给出了定义在λ项和π进程上的子互模拟关系(subbisimilarity),并证明了该关系的存在性。另外,文章还证明了相对于Abramsky的ApplicativeBisimilarity该编码满足完全抽象(fullabstraction)的性质。这些性质都表明了编码的优良性。3. Ambient演算与π演算. Ambient演算是用来描述移动设备上的移动计算的模型,它的特殊操作子in、out、open体现了移动设备。Ambient演算提出以来人们一直在质疑它们的表达能力是否绝对地比π演算强。本文首先证明了SafeAmbient、Fair Ambient演算到π演算没有好的编码,然后着重考察了MobileAmbient演算(以下简称MA)到π演算的编码,我们用不同的别名来体现灰箱的层次,比如同样的名n,在不同的层次为它起不同的别名。因此,每个灰箱都拥有一个链表来存储名与它的别名对,而归约则体现为灰箱结构信息的修改。从而给出了MA演算到π演算的编码,该编码满足操作上的可靠性。但相对于MA的观测同余关系该编码没有完全抽象的性质。在试图构造一个完全抽象的编码的同时,我们发现一个特殊的进程(m)m[in n],并利用这个进程,证明了MA到π演算不存在满足完全抽象性质的好的编码。综上,本文提出了利用π演算自然的编程能力,来辅助设计从其它模型到π演算的编码的统一方法。作为方法的成功应用,我们给出了λ演算到π演算的编码,以及MA演算到π演算的编码。前者的优良性质进一步证实了π演算的表达能力,同时也使得从并发的角度研究λ演算成为可能;后者虽然没有类似的性质,但它辅助证明了否定的结果,说明移动设备不能很好地用移动计算来描述。这两者都有着重要的意义。

论文目录

• 摘要
• ABSTRACT
• 第一章 引言
• 1.1 研究背景
• 1.1.1 π演算的表达能力
• 1.1.2 λ演算与π演算
• 1.1.3 Ambient 演算与π演算
• 1.2 主要贡献
• 1.3 章节安排
• 第二章 预备知识
• 2.1 π演算
• M'>2.1.1 π^M
• def'>2.1.2 π^def
• 2.1.3 互模拟关系
• 2.1.4 Up-to 技术
• 2.2 λ演算
• 2.2.1 λ项与β归约
• 2.2.2 等价关系
• 2.3 Ambient 演算
• 2.3.1 MA 演算
• 2.3.2 FA 演算
• 2.4 本章小结
• 第三章 基于π的编程与表达能力
• 3.1 编码与表达能力研究
• 3.1.1 Spi 演算
• 3.1.2 λ演算
• 3.1.3 MA 演算
• 3.2 数据结构与π
• 3.2.1 链表
• 3.2.2 树结构
• 3.3 编码的性质
• 3.4 本章小结
• 第四章 完全λ演算到π演算的编码
• 4.1 背景与难点
• 4.1.1 Lazy λ到π演算的编码
• 4.1.2 完全λ演算编码到π的难点
• 4.2 在πdef 中的编码
• 4.2.1 λ演算与二叉树
• 4.2.2 二叉树与编码
• 4.2.3 β归约的模拟
• 4.3 编码的性质
• 4.3.1 归约动作
• 4.3.2 输入动作
• 4.3.3 对应性质
• 4.4 编码的正确性
• 4.4.1 Subbisimilarity
• 4.4.2 完全抽象
• 4.5 另一种编码
• 4.5.1 确定的编码
• 4.5.2 编码的正确性
• 4.6 本章小结
• 4.7 证明
• 第五章 Ambient演算到π演算的编码
• 5.1 结构化编码
• 5.2 SA FA 与 π
• 5.2.1 SA
• 5.2.2 FA
• 5.3 MA 与π
• 5.3.1 编码思路
• 5.3.2 编码
• 5.3.3 编码的性质
• 5.3.4 否定的结论
• 5.4 本章小结
• 第六章 总结与展望
• 参考文献
• 致谢
• 攻读博士学位期间发表的学术论文
• 攻读博士学位期间参加的项目
• 索引