可在www.sciencedirect.com在线获取理论计算机科学电子笔记338（2018）97-114www.elsevier.com/locate/entcs从CCS到LudicsStefano Del Vecchio1、 2和Mogbil11LIPN，CNRS- Université Paris 13，Villetaneuse，法国2 Dipartimento di Matematica e Fisica，Università Roma Tre，Roma，Italia。摘要本文从拓展Curry-Howard对应关系到线性逻辑演算的工作出发，给出了Milner通信系统演算（CCS）的另一个Curry-Howard对应关系把鲁迪克作为目标系统。 事实上，互动，Ludics的动态，允许充分代表两者微积分的不确定性和不连续性我们给出了一个解释CCS过程到仔细定义的行为的Ludics使用一个新的结构，称为定向行为，允许受控的交互路径使用修剪设计。我们的特点是执行过程的行为上的相互作用，通过隐含地表示事件结构的因果顺序和冲突关系。作为一个直接的结果，我们也能够解释死锁的进程，并确定无死锁的。关键词：通信系统演算（CCS），线性逻辑，Ludics相互作用，非决定论。1介绍进程代数是并行理论的一种方法，用于基于通信（通常是消息传递）和并行组合等原始操作的推理来建模交互系统;在最知名和最常用的系统中，有米尔纳在我们的工作中，我们专注于前者，以在Ludics[12]的证明理论环境中给出解释，它遵循交互式计算的范式将语法和语义重新结合在一起为这种演算找到一个合适的Curry-Howard对应物可以为并发计算提供一个逻辑基础，并对其动力学有一些了解并发的语义模型可以用来给进程代数提供语义例如CCS的事件结构[23][22]。像Petri网[18]，事件结构是一个真正的并发模型，但基于显式的因果顺序和并发关系来揭示并发性。使用这些概念的闭包，语义属性可以很容易地描述诸如（无）冲突、选择独立性和一致性等行为这样的闭包也存在于我们的解释中，但直接通过双正交性内在化在Ludics的行为中从另一个角度来看，我们的Ludics解释https://doi.org/10.1016/j.entcs.2018.10.0071571-0661/© 2018由Elsevier B. V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。98S. 德尔韦基奥河谷Mogbil/理论计算机科学电子笔记338（2018）97□⟧CCS表达了非确定性选择下所有可能的选择。不知何故，这使它更接近并发的交织模型，如跟踪和标记的转换系统[24]，其主要能力是表征观测等价性。动机及相关工作。这项工作的动机来自研究，旨在扩展Curry-Howard对应的功能设置之外，模型并发。许多方法实现了这样的对应关系（如[7]），尽管是通过将确定性强加给进程，即仅限于其中只能发生确定性行为的并发系统。然而，一般来说，过程的归约是不确定的和不连续的：这本质上限制了它与证明的割消或规范化的可能对应，其性质是连续的和确定的，从而有效地将过程限制为函数行为。我们从基于线性逻辑的作品开始[11]（它启发了许多系统，是一种特别与交互联系在一起的逻辑），强调了上述方法的困难;特别是[4]，[3]，[5]和[8]。 在[8]中，作者表明，尽管所提出的转换不是模块化的，但区分网是对应的合适目标系统，在这个意义上，我们不能组合两个区分网来表示两个过程的（并行）组合。但是，即使是证明网，具有与过程演算相似的动力学，具有局部和异步的割消过程，也无法在没有对应关系的情况下表达并发系统的行为，基于执行的调度[6]：从作为过程的证明网到作为执行的证明网，强调证明的意义在于它的范式，通过割消达到，而过程的意义不是它的多种不可约形式之一，而是如何达到每种形式：哪些通道通信，以及过程在每一步的形式是什么。 我们工作的目的是试图进行同样的通信，但在Ludics[12]的设置中，通过使用一个以互动为核心的逻辑系统Ludics在C.Faggian & Co.：从这种联系出发，作者旨在获得一种在Ludics内部表示复制（如 [2]）和非决定论的方法正如我们现在所理解的，我们的工作是采取与[9]相反的方向，通过使用行为有效地表示Ludics中事件结构的因果顺序和联系关系。这是使用一种新的结构来实现的，在[10]中发现，称为定向行为，它允许从仔细修剪的设计中控制交互路径。最后，我们在CCS中的执行和Ludics中的交互之间形成了一个强有力的对应关系，而不会失去其非决定性也不会失去其非连续性（即多重范式）。纲要在Ludics（设计、被设计和相互作用）和MCCS（CCS的一个简单片段）的背景概念和符号之后，我们在第三节中根据配备有分配函数的Ludics行为来定义过程P的解释P。第4节总结了主要结果S. 德尔韦基奥河谷Mogbil/理论计算机科学电子笔记338（2018）9799□⟧A（（AA）B） CΔ12`好吧1，100。3，Δ。2，。3，Δ（（1⊢2⊢D●+∶MCCS和Finishes及其扩展到无复制CCS。首先，我们专注于关于过程执行和Ludics交互之间的对应关系：P描述了P上的所有执行。然后，我们提出的并行组合作为合并的解释，和相应的流程执行的解释的操作版本。我们还给出了无死锁进程的一个特征，以一个充分条件的形式来检查对无死锁进程的解释。在最后一节中，我们解释了如何将我们的技术应用于完整的CCS，这是使用Terui的计算Ludics [ 20 ]复制2背景Ludics是一个抽象的乘法-加法线性逻辑证明在集中的纪律下（用于优化证明搜索空间由Andreoli [1]），因此切割自由和严格的交替之间的积极和消极的规则。设计Ludics的对象，将公式替换为地址，，. （自然数的序列）;子公式成为子地址。1，100。二、1，. 到给出一个直觉，证明被重写如下：例2.1公式（（A1<$A2）B）`C的一个集中证明是：ΔA1，C，Δ1ΔA2，Δ2A1A2&B`C，Δ在这里连接词&和同时被引入。更进一步，只考虑正公式，它变成AC，Δ1AΔ2A1<$A2，C，Δ<$B，C，Δ最后，在Ludics中，公式被遗忘，我们有- 是的1 .一、1个小时。3，Δ 1π。1 .一、2 ⊢Δ 2ξ⊢Δ其中Δ is是地址集合。形式上，设计可以这样定义定义2.2设计是一棵由抽象序列构成的树，这些序列由称为动作的规则构建和标记，每个分支都以一个积极的动作结束。规则如下：Daimon（DaiΔ）Δ其中Δ是有限个地址集。 Daimon是一个积极的行动。100S. 德尔韦基奥河谷Mogbil/理论计算机科学电子笔记338（2018）97● 积极行动：积极（+）∈⊂+N<$N<$P（N）<$.I=fin∈ ∈N- 是的ii∈I。我， - 是的我我， ，i∈1n1n∈N（+6，0.2，{1}）ξ⊢⊢ξ ξ ⊢联系我们нDCD <$C C ∈DB ={D1，...，Dn}ıı=消极行动：ξΔ介绍了....iΔ i.、1999年，Δ，Δ其中，i I和In。我是规则的分支，而你是它的焦点。Δ is是不相交的并且包含在Δ中。●.. . 好吧I，ΔI.. . （−，N，N ）这是规则的分支，以及它的焦点。、- 是的1、......、n，其中1，...，nI和I ;Δ Is包括在Δ中。分支表示由规则生成的分支的数量;即包含子地址的前提，带有，或带有我和我。 任何具有子地址.i作为焦点的规则都由规则来调整积极和消极的行动是严格交替和戴只能是设计的最后一步。交互作用相当于Ludics中的切割消除，并定义了它的动力学;设计交互的方式由其语法明确，缩小了与语义的差距。我们使用[17]中的表示和定义，基本上与开创性文章[12]相同。下面的例子给出了两个正交设计和它们之间的相互作用：10好吧二、1 .一、1，100。1 .一、1 .一、1н（−，. 二、1，{{1}}）9- 是的1 .一、1 .一、1（+，. 1 .一、1，{1}）4英寸。二、1 .一、1（+，. 二、1，{1}）8- 是的二、1美元。1 .一、1 .一、1好吧1 .一、1 .一、1，100。2（−，. 1 .一、1，{{1}}）5好吧1 .一、1（−，. 1，{{1}}）3个字符。二、1（−，. 2，{{1}}）7- 是的1 .一、1个小时。2（+，+）1，{1}）2- 是的1⊢⊢- 是的2（+，，{1， 2}）0好吧1，100。2（−，，{{1，2}}）1这里的数字表示第n个交互步骤。 互动始于在基础上进行切割（即结论和），并检查规则的前提：如果分支1， 2在相应的否定规则中找到匹配，则交互继续，如果到达Daimon，则成功结束：它完成了公理的角色，停止了证明搜索。在两个设计和之间成功交互的情况下，我们说它们是正交的，记为或（和反之亦然）。我们将把过程解释为行为;形式上我们有定义2.3行为是一组相同基础的设计通过双正交闭合，即，使得BB.MCCS，米尔纳CCS的一部分。首先，我们将我们的设置限制为CCS的乘法片段，如[4]所示，简称为MCCS，以使其尽可能简单。在第4.5节中，同样的工具将用于表示非确定性选择和名称隐藏（又名限制）。复制在第5节中讨论，并在K.Terui，called c-ludics [20].MCCS术语由以下语法描述：P，Q∶=1μal.Pam.P（PQ）ξS. 德尔韦基奥河谷Mogbil/理论计算机科学电子笔记338（2018）97101一DSX（+）∣R（P）D∣≡
下载后可阅读完整内容，剩余1页未读，立即下载
