博弈语义与π演算的通用理论在计算机科学中的应用

40理论计算机科学电子笔记71（2003）网址：http://www.elsevier.nl/locate/entcs/volume71.html30页过程和游戏本田康平1，2伦敦大学玛丽皇后学院计算机科学系，伦敦，E1 4NS，英国。摘要如果我们希望有一个共同的数学基础，在此基础上，统一理解和整合计算中的各种科学和工程技术，那么计算的一般理论是很重要的对这样一个普遍理论的探索可能采取不同的途径。作为通向一般理论的可能途径之一的一个案例，本文一方面建立了Hyland和Ong基于博弈的序列函数模型与 另一方面是π演算这种联系在我们最近的研究中起到了重要作用，我们使用π演算作为基本的数学工具来表示不同类别的行为，尽管对应的确切形式还没有以公开的形式提出。通过弥补这种对应关系，我们试图明确理论计算机科学两个不同线程之间的思想和结构的收敛。这种融合表明了一种方法，组织我们对计算的理解和方法，我们认为，提出了一个有前途的途径，以一般的理论。关键词： 博弈语义，类型化π演算1介绍现代世界的计算以多样性和快速变化为特征计算科学也不例外，我们有不同的活动和理论，处理不同的主题，并使用不同的方法。因此，寻求一种通用的计算理论是有价值的，它可以提供一个共同的数学基础，在这个基础上，我们可以统一和整合这些不同的科学理论和工程学科。尽管计算与物理现象具有不同的性质（关于这一区别，我们在此不再进一步扩展;除了注意到复杂性之外），1 部分由EPSRC赠款支持GR/N/376332电子邮件：kohei@dcs.qmul.ac.uk2003年3月，出版社dbyElsevierScienceB。 V. 操作访问和C CB Y-NC-N D链接。本田41计算系统 从科学的角度来看，一般理论将帮助我们组织计算方面的科学知识，从工程学的角度来看。如果没有这样一个统一的理论，很难想象我们如何能够集成用于构建和控制计算系统的各种方法。当我们需要控制由不同编程语言编写的分布式组件组成的应用程序的行为时，这种集成变得至关重要，这些组件作为一个整体服务于用户因此，从科学和工程的角度来看，寻找计算的一般理论是很重要的。而对一般理论的追求可能采取不同的路径和方法。例如，我们可以引入一个通用的代数框架，它可以捕获计算的不同概念，如Meseguer [33]引入的并发项重写和Montanari等人[12]的计算模型，最近的结果来自这两个链在本论文集中讨论;另一个以类似目标开发的模型是Milner的双图理论[39]。正如本论文集以及Jensen和Milner [26]最近的一项工作中所展示的那样，这样一个代数框架可以为现有系统和理论提供一个综合的、经常具有启发性的理解基础，以及一个广阔的平台。用于实验和开发新概念、方法和工程理念。对一般理论的不同的研究方法将从一个理论对于一个核心的（如果受到限制的话）计算类的不同的但等价的表述开始，这样人们就可以找到这样一个理论的基本形式。这些不同的演示文稿中的每一个都服务于特定的科学/工程需求：作为一个整体，它们为分支和应用奠定了坚实的基础。在我们对这个理论有了满意的解释之后，特别是包括了不同表示的等价性，我们可以把它推广到更广泛的计算领域。Hoare[16]为这种方法提供了一个强有力的案例，专注于基本命令式编程的理论，为此他研究了不同的（观察，代数和操作）方法来呈现相同的理论，并表明它们在某种意义上是等价的，每一个都可以以循环的方式从另一个导出。不同的表达不仅服务于不同的工程目的，而且还澄清了计算的数学理论可以采取的不同形式：它们的相互可导性允许应用的灵活性，并增加了对它们数学地位的信心最后，还有一种方法是挑选出一个具体的数学结构，它可以代表一大类计算现象，并试图在这个结构的基础上发展一个一般理论。 当 所选择的结构具有广泛的代表计算的能力，当这种代表帮助我们有效地推理和控制计算现象时（与直接处理它们相比），本田42方法会特别成功。由Scott和Strachy[45]提出的域和指称语义学理论是这种方法的先驱这些不同的方法相互补偿：如果没有周围的一般代数理论，对具体结构的理解将是有限的;但一般代数理论在与强大的具体结构相结合时也可能变得最有效。核心理论的不同表述也可以扩展到一般的代数论域，从而获得丰富性和适用性;前者可能提出另一种有用的一般代数论域表述，这将有助于更深入地理解。事实上，任何一般理论，无论多么强大，都只能给出一种抽象计算现象的方法：其他抽象总是可能的，不同数学抽象之间的相互作用将丰富我们的科学理解。因此，不同的方向可以作为我们应该努力，同时允许相互丰富的互动。本文试图在这个广泛的对话领域中放置一小部分技术结果，一方面建立Hyland和Ong[24]，3引入的语义单向性与以Milner，Parrow和Walker的π演算[40]为中心的类型化过程理论[5]另一边。这两个理论之间的等价性，最初在[5]中观察到，以及它与线性逻辑[14]的联系，我们最近尝试使用类型化π演算作为表示和分析不同类型计算的基本工具[5，6，47，23]，即使对应的精确形状还没有以公开的形式呈现。通过以精确的形式呈现这种对应关系，我们希望展示两个不同的研究线索如何达到一个共同的结构来表示计算。这两个线程有着完全不同的起源：π演算是基于前面对进程代数的研究[4，15，35]的一种演算，它试图捕捉结构动态变化的并发计算在一个简单的句法;而语义宇宙的Hyland和Ong，基于前面的语义研究顺序性（cf. [44，34，27，7，8，42]），用于给出高阶函数中序列性的精确语义说明。此外，π演算的版本是这个巧合的中心，是Boudol，Tokoro和我在90年代初引入的最小系统x（→y）。P|x→v−→P{→v/→y}。异步通信是不受约束的、与同步通信一致的会话[35]形式这个异步版本的π演算中的进程正是那些构成序列语义宇宙中的交互的3 与之密切相关的语义宇宙是由阿布拉姆斯基独立提出的， 是的[1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19本田43与类型的概念相结合，它施加了一个行为约束，通过该约束，进程的行为就像顺序高阶函数一样。这种巧合的重要性体现在两个方面。首先，它表明了计算现象的广度，这些现象可以通过在两条链中发现的操作结构来精确地表示，即名字传递过程。[4]可以肯定地说，序贯纯函数是π演算最不希望精确捕捉到的：因此，通过与Hyland-Ong博弈的联系，它在π换句话说，Hyland-Ong博弈中序列高阶函数的精确可表示性通过进入π演算而被定位在更广泛的背景下。其次，将Hyland-Ong对策与π-演算联系起来的技术结果伴随着一种具体的方法，通过这种方法，我们可以获得名称传递过程的计算表示的精度。在π-演算中，有一系列的研究（从米尔纳开始[37]，cf.[43，29，17，18]）关于类型的概念，称为排序，它本质上限制了进程中名称的使用，从而限制了它们的行为。事实证明，一个干净而简单的类型结构来自Hyland-Ong博弈的π演算表示，实际上可以定位为π演算过程的现有类型概念的分支。关于这种类型的结构，有几点值得注意。首先，与现有的过程类型相比，它有几个新的特征，其中包括对偶性（以接近线性逻辑的形式）。第二，这种类型结构只在Hyland-Ong博弈中隐含地存在，至少是全部存在：在那里，关于交互的动态行为规范，包括无罪，与静态类型结构一起使用。通过转移到π-演算，一个简单的静态类型规则变得明确，实际上它与原始规范是等价的。第三，也是最有趣的是，由此产生的类型化的过程世界表达了一个比原始Hyland-Ong游戏更广泛的顺序纯函数类，例如，捕获按值调用行为（参见[5];在第6节中，我们将展示如何从类型化进程的宇宙中“读取”Hyland-Ong游戏的宇宙，作为后者的真子集）。通过随后对博弈语义和类型化π演算的研究，我们发现从Hyland-Ong博弈中产生的序列类型构成了一个成员一个统一的家庭类型的过程，其中包括各种形式的计算。因此，π演算和Hyland-Ong博弈之间的联系不仅表明了它们具有的某种运算结构的重要性，它还指出了使用这种结构进行精确表示的具体方法，为研究计算提供了一种新的工具和框架。4 关于这一点，米尔纳 一微积分的目标是信息系统的分析”，将其与目标是“物理系统分析”的微积分进行本田44是的。π演算及其基于对偶的类型共同构成了精确建模不同计算类别的行为和代数的统一基础，预测了一般理论的一种可能形式最后，我们进一步讨论了目前的工作与其他研究的关系。正如我们已经提到的，π-演算是过程代数的最新形式之一不同形式的进程代数（包括ACP[4]、CSP[15]和CCS/SCCS[35]）基于不同的同步和进程合成概念。在π演算中使用名字传递--它的区别性特征--更好地定位为一种以正交于不同进程演算之间的区别的方式丰富交互结构的方式。从这个意义上说，一个非常简单的名字传递表面的形式，值得注意的是，许多进程代数的共同层，其中包括并行组合和隐藏，在现有理论中提供了本质的可重用性：而从标准进程代数的观点来看，在通信中使用类型和隐藏可能构成新的元素。Hyland-Ong博弈和π演算之间的联系是由Hyland和Ong自己观 察 到 的[25]。结 果 之 间 的 差异[25]和[5]一样，这项工作是[25]基于直接来自其游戏语义的行为表征的具体过程，而在这里和[5]中，顺序过程纯粹是由句法类型规则生成的，行为表征来自于此。类型的语法和语义理论已经在顺序编程语言的上下文中研究了几十年，其中集中在λ演算上。交互类型和功能类型之间的主要区别在于可表示行为的类别例如，即使是无类型的λ-演算也是作为强类型的进程出现的，我们将在第2.1节中看到。3.6.高阶函数的类型是一个丰富的领域，具有深刻的理论和强大的应用。Hyland-Ong博弈和类型化π演算之间联系的一个重要方面是它对进程类型继承函数类型丰富性的方式的建议。正如我们已经提到的，本工作中的类型概念可以定位在过去研究的π演算的各种类型中，参见。[43，29，17，18]。在这种情况下，所提出的类型学科作为线性类型的一种特殊形式出现，其中类型的对偶性起着基本的作用。探索所提出的类型概念在π演算的一般类型宇宙中的精确定位（如[19]中所讨论的）将是一个有趣的研究课题Abramsky 、 McCusker、 Laird 和其他人，以及本作者，已经探索了Hyland-Ong游戏的不同变体，并建立了不同语言结构在游戏中的可嵌入性，参见。[2，3，11，28，22，30，32]。这些研究有助于识别不同的计算机领域，本田45⊕基于交互类型的工作站，深入分析代数属性用逻辑和范畴的语言来描述每个宇宙。正如本研究所揭示的那样，类型化交互的特征在博弈和π演算之间精确地对应，并且在表达上从根本上不同。通过在π演算的背景下定位博弈的不同概念，博弈中的不同算子及其代数被重新捕获在一个共同的，更简洁的，名字传递过程及其代数的基础上;而博弈给出的逻辑和范畴清晰度可以是明确类型化交互结构的有效手段一个密切相关的领域是在[31]中研究的线性逻辑的极化版本，这是另一个，这次是证明论的，通过博弈和类型化π演算研究的类型化相互作用类的表达（在这方面的精确联系将在其他地方报道）。这三个研究领域的相互作用，丰富了我们对这些研究从不同角度、使用不同技术工具所研究的共同结构的理解，从而使我们对它有了更全面、更深入的理解。最后，我们将本工作中的顺序类型规则与其原始版本[5]进行比较，后者被用作我们随后研究的基础。这两类学科的唯一区别在于对“选择”的表述方式不同。[5]使用分支/选择性pes（写作[&i∈I→τi]↓和[i→τi]↑）表示的选择，其中，与线性逻辑中的λ-演算和加法器中的总和相对应;而在本说明中，我们仅使用一元相互作用来表示选择，这实际上对应于Hyland-Ong博弈（也对应于[9，10]，其对无类型动态的强调[5]中使用的选择表示的优点在于它提供了一种易于处理的语法来表示各种选择概念，包括一般的值传递和对象。另一方面，本研究中研究的表示提供了一个关于选择的更分析的观点：事实上，它的运算结构直接对应于自米尔纳早期工作以来已知的一元π演算 作为一种不同的优点，该协议的语法类型规则将建议一种可能的方式来对类似的操作结构进行类型化。由于这些利益，提出一种可供选择的类型结构的替代形式，这是计算的一个基本概念，除了与Hyland-Ong宇宙的对应之外，它本身可能有一个优点。论文的结构 在剩余部分中，第2节在介绍了π演算的语法之后，非正式地说明了π演算中选择协议的基本思想。第三节介绍了带和的类型化π演算的语法。第4节给出了一个简短的介绍海兰和Ong的宇宙顺序高阶递归。第五节从类型化过程中构造了一个范畴论域，并证明了它与Hyland-Ong论域的等价性本田46≡⟨⟩||||||−→|||致谢。从[5]开始，我与Berger和Yoshida进行的一系列合作工作丰富了我对类型化π演算作为计算基础理论核心工具的看法。我衷心感谢乌戈·蒙塔纳里，他邀请我参加2002年在比萨举行的关于重写逻辑的研讨会，在这次热烈的讨论中，我最终写了这篇文章。我特别感谢与Jose Meseguer就技术和非技术主题进行的讨论。我感谢法比奥·加杜奇在研讨会上进行了愉快的讨论，也感谢他作为会议记录编辑的耐心和轻松的态度这项工作得到了EPSRC赠款GR/N/37633的部分支持。2π-演算中的求和：一个预览2.1选择协议在进行技术讨论之前，我们非正式地概述了操作结构和表示选择的类型的中心思想。以下是使用绑定、异步输出的π演算的语法。设x，y，. 和a，b，. 在名称的无限集合（也称为通道或端口）上的范围。P：：=x（→y）。P|！x（→y）。P|x（→y）P|P|Q|（νx）P|0的情况。x（→y）。P是输入，其接收名称s的向量（以在P中以形式参数s→y来初始化d）viax。 ！x（→y）。这是复制的版本。 x（→y）。P（resp.！x（→y）。P）通常被称为线性输入（或 响应于输入）。 输出x（→y）P输出新名称→y的向量。 P|Q是一个复杂的组合。对于{Pi} i ∈ I的n元平行合成，我们有时写为{Pi}i∈I（其中如果I={Pi} i，则{Pi} i∈IPi=0）。（νx）P说x是P的局部。 0是不作为，表示缺乏行为。 我们假设是优 先 级最弱的，因此x（y）.P Q（分别）x（y）P Q，resp.（vx）P Q）表示（x（y）.P）Q（resp.（x（y）P）Q，resp.（（νx）P）Q）。输出prefix应该被视为异步输出，因为x（→y）P对应于标准syn tax中的（v→y）（x→yP）。结构一致性是标准的，除了它包括刚才提到的输出一致性规则，并在附录中列出。关于模过程因此，约简规则如下所示。x（→y）。P|x（→y）Q−→（ν→y）（P|Q）！x（→y）。P|x（→y）Q−→！x（→y）。P|（v→y）（P|Q）这种关系在，（νx）和x（→y）下是封闭的，但在（线性和复制的）输入前缀下不是。使用这种语法，我们概述了如何通过一系列本田47一元名传递[36，21]。x（z1z2）（z1.P1|z2.P2）|x（z1z2）z1左边的进程有两个选择，它向continuationc发送两个名字，z1和z2;然后它用这些名字等待。如果z1被调用，那么P1变为活动状态：z2和P2也是如此.另一方面，左侧的流程选择信息，在初始调用后接收两个新名称，然后通过输出到 结果，我们得到以下缩减：x（z1z2）（z1.P1|z2.P2）|x（z1z2）z1−→（νz1z2）（z1.P1|z2.P2|z1）−→P1|（ν z2）z2.P2上面我们假设z1和z2都不出现在P1和P2中.注意（νz2）z2。P2的行为为0，因为它既不能自己约化，也不能与外界相互作用。因此，选择P1而不是P2。请注意，对于这个表示选择的协议，选择端只调用z1或z2，而不是两者都调用，这一点很重要：这是执行选择的端所期望的行为选择的一方。另一方面，选择方期望这些名称中的每一个恰好出现一次，以便完成选择以确定性方式（也可以通过分支，但在本文中，我们只考虑这种简单的形式，因为它将给出其他相关协议的基础）。 这种“期望”是一种基本的名称传递过程的良好组织（或类型化）行为的一部分，我们将在下面讨论。2.2打字选择让我们把重点放在上述过程的以下子项上。（z1.P1|z2.P2）对于这个过程，上面提到的关于名称使用的假设是只调用z1和z2中的一个，这就是选择的地方这意味着，对于这个术语，以下减少是自然的：（z1.P1|z2.P2）|z1−→P1从非类型化进程的角度来看，这当然是不正确的，因为z2仍然可用于调用：但是，在类型化进程中。因为我们期望环境遵守选择协议，z2将永远不会被调用，因此z2.P2将被安全地垃圾收集，从而证明减少是合理的。由于这种调整依赖于进程的类型，我们可以添加一个注释，例如：（z1.P1z2.P2），作为一个无类型的进程，它仍然是相同本田48||↓⊕‡►作为（z1.P1）的事物|z2.P2）。现在我们可以把上面的缩减写为：（z1.P1&z2.P2）|z1−→P1。语法类似于标准的（保护的）和，通常写为z1.P1+z2.P2，尽管目前的和表示法涉及类型信息，如其基本要素。因此，底层的无类型进程实际上是无求和的π演算，由标准的并行组合运算符组合。所涉及的动力学可以通过一个基本的无类型的方程定律来证明，只要基本的过程是良好类型的。这个注释，用替换了一些，对于选择的易处理的语法规则也是必不可少的，在这里我们希望将两个可能的选择，在z1和z2，作为一个集合。例如，我们可以键入，假设P1和P2具有相同的类型Γ：►（z1.P1z2.P2&）dz1：（）↓&z2：（）↓，Γ.该类型表示它假设环境将选择z1或z2，而不是两者都选择（这里表示线性输入：因此（）↓表示不携带任何值的一次性输入）。我们有一个双重的选择类型：►z1d z1：（）↑ z2：（）↑.读取↑作为输出，这一次的输入表明它假设环境正在等待两个选项，一个在z1，另一个在z2，并且进程有可能选择z1或z2。在这种情况下，该过程选择z1。当然，还有另一种选择左分支。► z1d z1：（）↑z2：（）↑，正如符号所暗示的，输入选择和输出选择有一个自然的对偶概念：在上面的例子中，输入和输出之间的类型是严格对偶的，在z1和z2处，既有单独的（（）↓和（）↑），也有共同的（和）。在合成中，这些对偶类型相互湮灭，因此我们得到：►（z1.P1&z2.P2）|z1d z1：π，z2：π，Γwhere意味着在通道处不可能进行进一步的合成，这是有意义的，因为在任何一个名称处都不再有选择的可能性这种二重性对于有一个连贯的组合概念是基本的：事实上，虽然我们可以将输出z1输入为z1dz1：（）↑，但这个过程不能与上面的输入组合，因为它不伴随着输入中的其他选择。这种二重性是拥有类型化过程的一致性宇宙的基础。本田49联系我们↓↑↓ ↑3一类带和的类型π3.1过程在这一节中，我们正式介绍了类型π演算与总和，这是本研究的中心。作为进程的语法，我们使用与第2节中相同的语法，除了线性输入“x（→ y）。P&“i 现在可以 代替d b y“i ∈ I xi （ →yi）.P i“（其中I是有限集且xi/ = xi，i = j）. 过程&“i x i（→ y i）.P i“称为f的sumxi（→yi）.Pi，其中hich，正如我们已经讨论过的，最好理解为并行复合式的简写形式，其中ni∈Ixi（→yi）.Pi在假设下-稍后具体化为ty pes- 环境服从求和协议我们还可以在绑定名称上添加类型注释，为了更简单的表示，我们省略了这些注释。线性输入的减少相应地被扩展：&i∈Ixi（→yi）.Pi|xi（→yi）Q−→（ν→yi）（Pi|Q）它扔掉了未被选中的树枝。重要的是要记住，上面给出的总和的减少只在类型化设置中有意义：然而，当进程确实是类型化的时，我们可以从类型化的动态恢复非类型化的动态，正如我们将在后面正式演示的那样3.2信道类型通道类型表示流程在其通道上的交互结构。它使用四种动作模式，！然后呢？.正如符号所表明的，和是相互对偶的，而！然后呢？是相互的双重性。信道类型然后由以下语法给出。τ：：= τI|τO|τI：：=（→τO）↓|（→τO）！τO：：=（→τI）↑|（→τI）？这里→τ表示y的向量。 我们称之为τI输入类型和τO输出类型。在每种输入/输出类型中，类型p e的括号内的向量的元素在类型pe中是可识别的。 当m（→τ）p是p型时，我们有时会讨论p的性质.如果τ是p型的，我们有时记为τp.给定一个输入/输出类型τ，τ的对偶，记作τ，是通过对τ中的作用模式进行对偶归纳而得到的。设md（τ）为除 md（τ）d=efτ外的最外模。正如可以猜测的那样，输入类型表示输入行为，类似于输出类型。对类型指示在一个通道处输入和输出都存在。我们只使用符合以下约束的通道类型：• 在n（→τO）↓中，每一个都携带着这种类型的信息？-type，对于r（→τI）↑的对偶y。• I n（→τO）！你说什么？-typeorra↑-type，对于r（→τO）↓. 在[5]中，基本上使用了相同的约束，尽管本田50[5]只能携带唯一的线性类型。相反，这里的复制类型本田51⊕ⓈⓈ/∈∈联系我们=/∈⊕⊕可以携带多个线性类型。正如我们后面将要看到的，这表明了选择行为。我们定义了一个部分交换运算τ <$τJ：（1）τ<$τ =<$（md（τ）=↓）（2）τ <$τ = τ（md（τ）=！（3）τ_∞ τ = τ（md（τ）=？）. 如果这些规则都不适用，则ττJ没有定义，在这种情况下，我们写τ=τJ。3.3动作类型我们首先定义一个主要的行动类型如下。(1) &i∈Ixi：τi是当nxi/=xjifi=/j且md（τi）=↓时的一个随机作用。 对偶地，对于i∈Ix i：τ i。 {x i}称为这个素数作用类型的定义域。(2) x：τ是素作用型，当md（τ）！、、怎么样？. x称为domain这种主要的行动类型。形式（1）的素数作用类型有时称为和型。然后，一个动作类型是一个素数动作类型的有限集合，使得它们的任何两个域彼此不相交。5Γ，π，.范围超过动作类型。我们经常把一个动作类型看作是从名字到动作类型的基本有限映射，把Γ在x处的像写成Γ（x），把dom（Γ）写成Γ的定义域或在其中使用的名字。注意，Γ由底层映射以及线性类型名称的和分组确定。对于从Γ的定义域中取o → x的结果，我们也写为Γ/→x.接下来，我们定义了动作类型上的部分代数子定义3.1当下列条件全部满足时，(i) 对于每个x∈dom（Γ）∈dom（λ），Γ（x）=λ（x）.(ii) 若&ix i：τ i∈ Γ且x i∈ dom（n），则有nix i：τ i∈ n;对偶地若nixi：τ i∈ Γ且x i∈ dom（n），则有&ix i：τ i∈ n。(iii) 的对称情况（ii）。如果r = 0，我们将r = 0设置如下：（r = 0）（x）=τ i，或者（1）xdom（r）和τ= r（x），（2）xdom（r）和τ= r（x），或者（3）xdom（r）dom（dom）τ= Γ（x）<$（x）.此外，一个和类型在Γi中，它要么在Γ/fn（）中，要么在Γ/fn（Γ）中。根据代数，当我们合成Γ和Γ时，结果类型只能包含来自Γ或Γ的素动作类型，或者在公共通道上合成素动作类型的结果注意，一个和素动作类型被作为一个整体来处理，通常涉及多个名称。这个约束对于类型规程的一致性是必不可少的。5 在许多示例中（包括表示Hyland-Ong游戏中的游戏的类型），动作类型不包含两个 - 主要动作类型，或两个-主要动作类型。 在这种情况下，没有必要按和对它们进行分组。然而，在一般类型化过程中，例如在标记转换中，按主要动作类型进行分组是必要的本田52‡↓ ↑/∈联系我们⊕3.4捆绑规则其中φ是一个IO模，是集合{I，O}中的一个元素。当φ和φ之一（或两者）为I时，我们写φ = φ。如果两者都是，则Ifsoφ是I，如果else是O我们将逐一介绍打字规则。在每个规则中，我们假设在前件中引入的通道/动作类型是格式良好的。基本的合成规则很简单，来自[5]。（零）−►I0d（Par）►φiPidΓi （i=1，2）Γ=φφ=φ► 公司简介|Qd τ τ（RES）►φP dΓ，x：τmd（τ）∈{！，}►φ（νx）PdΓ（弱）►φP dΓ-xmd（τ）∈ {？，}►φP dΓ，x：τ在（Par）中，我们对类型和IO-模使用部分代数，使得结果过程总是顺序的。在（RES），我们不隐藏一个通道，表明需要其双重-这要么，或？-mode.在（Weak）中，Γ-x表示xdom（Γ）。这种弱化直观地表明，不使用OK？- 通道;并且-通道可以不存在，因为线性输入和输出彼此零化。接下来，我们介绍线性前缀规则，这是我们介绍选择概念的唯一地方。(In↓）►OPid↑？Γ-→x，→yi：→τi（1≤i≤n）►Iixi（→yi）.PidΓ，ixi：（→τi）↓（出↑）►IPdΓ，→y：→τiΓ=ixi：（→τi）↑► Oxi（→yi）PdΓixi：（→τi）↑In（In↓）中，Γ-→x如前所述，表示dom（Γ）→x=. 对这些规则的一些看法：• In（In↓），r-→x确保x1，. ，xn. 这里，如在第2部分中所示，“i X i：（→ τi）↓“指示选择的& 还请注意，Γ只包含输出类型，因此输入前缀不会抑制另一个输入，输出模式转换为输入模式。这遵循[5]，并且与游戏语义中所谓的输入-输出交替密切相关[1，1]。• （Out↑）引入一个选择类型的集合，直到（In↓）。“i x i：（→ τ i）↑“表示一个进程可能做的选择。（Out↑）具有与（In ↓）成对的输入-本田53输出交替，将输入模式转换为输出模式。最后，使用=和表示输出的异步字符。本田54►► ⊕ ►⊕⟨ ⟩ ⟨ ⟩►⟨ ⟩ ⟨ ⟩1 2 1 2 1 1 22≡≡≡1‡211 21最后，我们总结了具有复制输入和输出的类型化规则(In！）►OPD？Γ-x，→y：→τ►我！x（→y）。PdΓ， x：（→τ）！（出去？）►IPdr，→y：→τr=x：（→τ）？► Ox（→y）PdΓx：（→τ）？这两个规则都不涉及选择：这是因为这些名称可以根据需要多次使用。在（在！），则在T中的抑制通道不能包含线性输出，因为通过在复制下，这些通道可以用于输出任意多次。（出去？）与（Out↑）相同，只是没有求和类型。下面是类型化进程的简单示例实施例3. 1（i）Lettxd=ef！x（bb）。b和fxd=ef！x（bb）。B. 然后R是tx或fx之一，我们有IRd x：（（）↑（）↑）！. tx和fx分别代表（按名称调用）真理和谬误他们的双重身份是该条件式给出n为：ifxthenPelsePd=efx（bb）. （b. P&b. P）。它的类型是：如果x那么P1，否则P2dx：（（）↓（）↓）？假设，►O P i dA（i = 1，2），我们可以检查t xif x then P 1 else P 2 − → 2|tx|P1，对称地，fx|if x then P1else P2−→2 f<$x<$|P2.(ii)我们还可以构造这些代理的按值调用版本。在这种情况下，真和假出现Ob1db1：（）↑b2：（）↑和Ob2db1：（）↑b2：（）↑，而条件出现Ob1 d b1：（）↑ b 2：（）↑。Ib1.P2&b2.P2db1：（）↓&b2：（）↓. 在这些编码中消除了按名称调用编码中的n间接3.5基本语法属性我们首先列出序列过程中动力学的基本性质。下面welet→→d=ef−→。支持3. 2（i）（对象约化）如果P→→Q，则►φQd Γ。(ii)（序贯性）若P−→P1J，2，则P1J<$P2J，证据 见附录二✷接下来，我们正式建立了无类型演算和他们动力学中的微积分。 我们首先定义Eras e（纪元P d↓↑！？A，w→）as（νw→）PJ，其中PJ是在Pin中转动each的结果，以使lcompo-宗教裁判所。由于模式的名称从来没有与其他名称组合，隐藏它们不会影响代数和动力学。进一步将J写为添加公理（νx）x（→y）的结果。P0mm至（这个方程是可由untyped strong bisimilarity证明的，所以它对进程的行为没有影响）。我们现在可以声明如下。通过检验约简的两个本田55生成规则，证明是容易的。本田56►►≡000为φdef3.3设φP d A且P0=（φP d A）。然后又道：def(i) P−→PJ意味着P−→ <$JPJ，其中PJ<$（<$PJd A）。(ii)P0−→P0J蕴含P0J<$j <$$>（<$φPJd A）使得P−→PJ。最后，我们列出一个我们将在下一节中重复使用的属性。让我们说一个过程P是素数与主题x，或简单地素数，如果P是输入与主题x或Px（y1.y n）n∈IP i使得每个P i与主语y i互素.然后，我们考虑输出前缀类型的一个变体，它是通过在（Out ↑，？）的。这种受限的类型系统被称为基本类型。请注意，在素数类型系统中，我们可以假设输出前缀下的活动名称受该前缀的约束我们可以很容易地检查：命题3.4如果在原始的类型化规则中可导出P0 dA，那么对于某些P0dA，我们在素类型化系统中有P0 dA。命题3.4说，我们可以假设，不失一般性，所有的预固定过程都是素数，只要我们讨论的性质在素数下不变。3.6无限延伸在本小节中，我们将π演算扩展到它的无穷对应物，包括类型和过程。虽然这不是必要的，至少在其最一般的形式中，为了捕获许多标准的计算行为，需要无限扩展以与Hyland和Ong [24]的原始范畴精确等价。它也有一些兴趣在建模无类型的顺序演算，我们将在后面看到。结构相当简单。一个过程现在是一棵可能无限的树，它的高度至多为可数的6，使得它的每一个满子树7都具有以下形状：&i∈Ixi（→yi）. P|！x（→y）。P|x（→y）P|i∈IPi|（v→x）P|0的情况。其中I和每个名称向量可能是无限的（为了简单起见，假设这样的向量由序数的初始段索引，从0开始）。为了使α-转换在无限名称出现的情况下成为可能，我们将整个名称集合设置为一个真类。结果过程有时被称为无穷大过程，它包括原始无穷大过程作为一个真子集。在无穷过程中，我们使用明显的扩展来定义原始方程（特别地，我们假设嵌套的nested[6]对可数高度的限制并不是实质性的，但使许多讨论变得简单。图7树T0的全子树T是T0的子树，使得在每个顶点，T包含T0在相应顶点的本田57≡uu i i∈ω m i i ∈ωu i i∈ω x m i i ∈ω联系我们我u我≈i∈ω我i∈ω我我我我我我我我p可能在有限向量中，如（→x）（→y）P（→y）（→x）P）。还原规则和以前一样精确地通道类型也进行了类似的扩展，允许每个向量是有限的或无限的，并且每个类型是有限的或可数的有限高度，其中和以前一样的良构条件。一个和类型可以有一个无限域;一般来说，一个动作类型也是如此。 使用无限的过程和类型，类型化规则如前所述被精确地给出，将每个规则读取为对进程的每个完整子树例3.2（无类型λ-演算的表示）无限延拓从无类型高阶函数的表示的角度来看有一些有趣之处以下是无类型λ演算的编码，自1996年以来为作者所知。[[x]]d=efCCux[[λx. M]]d=ef！u（x·{y}）。P（[[M]] d=ef！u（{y} ）。P）[[MN]]d=ef！u（{y}）。（vx）（P|[[N]]）（[M]]d=ef！u（x·{y}）。P）其中，我们设置CCd=efµ Xab。！a（{y}）。b（{z}）<$X<$zy<$，其中ch定义一个无限树作为一个最小固定点（X ab等。表示在前面的方法中通过名称的实例化）。在定义above中，{yi}i∈ωi是由自然数集合索引的名称的向量(note这导致具有相同索引集的向量）。让我们展示如何模拟（λx.x）M−→M下面我们省略索引集ω，令def[[M]]x=！x（{z}）。P.[[（λx. x）M]]d=ef ！u（{y}）。（νx）（x（{z}）<$C C <$zy<$|[[M]]）I I I I I X−→！u（{yi}）。（v{zi}）（iC Cziyi|P）def快！u（{zi}）。P=[M]]u。在第一行，注意λx。xd=ef！u（x·{y}）。x（{z}）<$C C <$zy <$. 在最后一行，标准（无类型）弱双相似性，其建立很容易通过使用闭包[36]。通过这种方式，我们可以证明β和η-等式：事实上，编码过程模捕获无类型λ演算最大相容性理论作为独立的构想，编码与[13，28]中的无类型λ演算的博弈模型密切相关。相比之下，过程编码在表示上简洁，直接捕获了原始演算的动态;而[13，28]中的模型对环境语义结构具有更丰富的代数见解。本田58›→ →∈↓↑↑4Hyland-Ong Games4.1阿里纳斯Hyland和Ong博弈被引入作为表示顺序高阶递归的内涵结构（如引言中所述，Abramsky，Jagadeesan和Malacaria[1]和Nickau[41]在同一时间引入了密切相关且基本等同的语义宇宙）。在本节中，我们简要介绍了他们的宇宙。Hyland和Ong的构建基于两个概念，舞台和策略。我们首先定义竞技场。在森林下面是一个无环有向图（X，）（如果存在从x到y的有向边，则写为x，y X），其中每个节点最多有一个传入边，并且存在最少的元素w.r.t.偏序›→。这些最小的元素被称为它的根。我们只考虑高度至多可数的森林（高度不可数的森林不构成任何技术问题，但无意义）。我们计算森林中每个节点的高度，从每个根的1开始。定义4.1竞技场，由A，B，. 是一个（可能是无限的，但至多是可数深度的）森林（X，›→）（其中x，y，. 与两个标记函数op：X→ {O，P}和qa：X→ {Q，A}一起，使得：(i) 如果x是奇数高度（或（x）=O（x =0）（x）=P）。此外，如果x是根，则qa（x）=Q。(ii) 如果qa（x）=A，那么对于没有y，我们有x→y。竞技场中的节点通常被称为移动。op-标记是多余的：然而显式地拥有它便于建立它与π-演算的联系O代表对手，P代表玩家。另一方面，Q和A代表问题和答案。我们将对偶算子设置为O=P和P=O（qa-标签上没有对偶）。我们将这些模式组合为OQ、OA、PQ和PA。在[24]中使用了这些动作的以下简写符号：[代表OQ-移动，（代表P Q-移动，）代表OA-移动，和]代表PA-移动。例4.1一个简单的arena例子是布尔arenaB，它有一个根标记为OQ，两个后续节点都标记为PA（可以写为true和false），仅此而已。稍后我们将看到B对应动作类型x：（（）↑（）↑）！. 事实上，如果我们延长它的通道type（（）↑（）↑）！作为一个语法树，根有！- 模式，我们认为这是一个OQ-，或[-，移动;和每个（）↑可以简单地被认为是标签的节点，我们认为是一个PA-，或]-，移动，作为一个整体B。 我们可以这样猜测，！、、怎么样？、 和 分别对应于[，（，）和](in具体地，并且可能令人困惑的是，对手对应于输入，而玩家对应于输出）。本田59⇒·›→·4.2战略接下来我们构建策略。我们的介绍受益于[32]。写A来表示A的二元化，它交换OP-标签，但不交换QA-标签。给定一个区域A和B，通过将A和B不相交地组合，并从B的每个根向A的每个（原始）根添加一条有向边，可以得到一个区域AB。注意这又是一个竞技场，叫做从A到B的函数竞技场。在一个（有限）序列下面是从ω的有限初始段（自然数的集合）到一个元素集合的映射。相关初始段的元素称为其索引。如果σ是一个序列，i是它的下标，则σ[i]表示σ的第i个元素.定义4.2从A到B的动作序列是A中移动的有限序列σB连同其指数上的正态关系，写为 ia j（其中i，j是σ的指数），使得：(i) （初始移动）如果σ=xσJ，则x是A<$B的根。(ii) 如果ia