λ-π演算: amb操作符在λ-演算中的编码和性质分析

理论计算机科学电子札记96（2004）73-89www.elsevier.com/locate/entcs论麦卡锡琥珀的再现在π演算阿诺·卡拉约尔IRISA - Rennes and LIP - ENS法国丹尼尔·赫什科LIP - ENS里昂，法国达维德·桑吉奥吉意大利博洛尼亚大学摘要我们研究了λ[]的编码，即用McCarthy的amb算子丰富的λ -演算的名称，到π -演算。从语义上讲，amb是一个具有挑战性的操作符，因为它表达了公平性约束。我们证明了，在λ -演算中对发散的某种解释（弱发散）下，忠实编码是不可能的。 然而，对分歧（强发散），编码是可能的，并且对于这种情况，我们得出结果 和共归纳的证明方法来推理λ[]，类似于纯λ-演算的编码。然后，我们使用这些方法来获得最重要的法律有关amb。我们把双相似性看作是π演算上的行为等价，这对公平性和双相似性之间的关系有一定的启示作为一个自旋-O的结果，我们表明，没有小步操作，λ[]的语义，它保留了术语的分支结构并产生正确的谓词收敛和（弱）发散。保留字：公平性，McCarhty1介绍二义性选择算子amb最早在[11]中引入，用来描述一种可能返回多个结果之一的（部分）函数的组合形式。[11]通过给出其主要属性来描述AMB。两1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.02274A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-最重要的属性都与公平有关。一个属性说amb是底部避免的，这意味着函数与未定义函数的组合应该返回前一个函数的结果。另一个重要的属性是，当被组合的函数计算的结果都被定义时，amb的行为就像一个非确定性的选择：它们中的任何一个都可能以不可预测的方式返回。具有amb属性的运算符的有用性已经被发现用于系统的规范，特别是操作系统，本质上是因为需要一种形式的公平非确定性来合并传入消息（参见[6，20]，还有[8]，研究了amb和其他非确定性运算符关于这个问题）。然而，我们对amb感兴趣的主要原因是，从语义上讲，40年后，amb仍然是一个非常具有挑战性的操作符[9，13，10，17，5]。由amb引入的困难在λ[]中很清楚，这是一个用二元运算符λ丰富的按名称调用的λ演算，它是Mc- Carthy的amb的获得λ演算语义和分析技术的两种标准方法是指称方法和运算方法。前者基于领域理论，后者利用应用性双相似性来推理语境对等。定义分析的问题是amb不是连续的（讨论见[13]）。Moran、Lassen和Pitcher在一系列著作中遵循了这种操作方法[9、13、10、17]。然而，证明应用双相似性的全等性（或类似的共归纳定义的关系，与上下文等价一致或至少给出了上下文等价的良好近似）的问题对于λ[]仍然是开放的。Howe[ 7 ]是证明λ-演算中应用双相似同余的常用方法因此，为了证明amb的一组特征定律，已经开发了一些“部分”证明技术，特别是在[ 13，10 ]中（这些技术是部分的，因为单独考虑，它们中没有一个由于上下文等价的定义对上下文的大量量化，在本文中，我们探索了另一种方法来给出λ[]的语义，通过编码到（异步）π演算中。开展这项研究有第一个原因是寻求证明方法来推理像λ[]这样包含表达公平性约束的运算符的语言。将λ演算（以及它的并行和非确定性扩展）编码到π演算中的问题已经得到了广泛的研究例如，在按名称调用的λ-演算的情况下，π-演算语义在λ-A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-75术语与经典的L'evy-Longo树语义学[19]相一致，这表明π演算语义与按名称调用λ演算的标准表示分析之间的一致性。此外，互模拟是π演算中的规范等价，并且具有良好的理论，以及强大的证明技术，可以减轻构建互模拟证明的任务。因此，人们可以希望在π演算中的工作可以帮助为λ[]定义有用的基于互模拟的技术。这项研究的第二个动机是表现力。π演算已经被证明是一个非常强大的形式主义。我们想知道π演算是否以及在什么条件下可以编码像amb这样复杂的算子。我们不知道其他尝试编码到表达公平性约束的π另一个动机是π演算中的公平性问题。虽然π演算的标准SOS规则没有提到公平性，但互模拟或类似语义等价的使用引入了这种性质。定义像amb这样的公平运算符的语义是更好地理解这个问题的一种方法为了说明这一点，考虑π演算项τ ω|a，其中τ ω表示可以执行无限多个内部动作的过程，a是在没有价值交换的情况下的输出，并且“|“是并行复合的运算符。在互模拟等价下，与测试等价相反，这个过程被认为与过程a相同。解释这种平等的一种方式是说，双相似性忽略了分歧。然而，另一种看待等式的方式是说双相似性包含一些公平性：在并行合成的公平实现下，左分量τω不可能总是占上风，因此最终将执行右侧的动作a。我们要解决的正是这第二种--通常被忽视的--对双相似性的解释，试图理解它在一个非平凡的具体例子上的意义。当研究像amb这样的非确定性算子时，上下文等价性是通过观察两个项在任何上下文中表现出收敛和发散的能力来定义的。可以区分两种分歧（见例）。[14]）：不可能收敛的计算是强发散，而弱发散对应于无限次计算，沿着它收敛到一个值的可能性永远不会丢失。两种形式的发散都出现在λ[]中：首先注意，通常总是发散的为了给出一个弱发散的例子，我们使用内部选择算子，可以在λ[]中编码如下：defM<$N=（KM<$K N）I，K和I是选择和恒等式的常用组合子根据定义76A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-对于λ[]，M<$N可以非确定性地演化为M或N。现在考虑这个术语Td=ef（其中固定定义为A A，固定λx。（x）def= λxy。y（xx y））。 由于内部选择的性质，T表现出弱发散，沿着它收敛到I被反复丢弃。在文献中对反磁轴承的运算研究中，没有区分强发散和弱发散。在本文中，相比之下，我们分开的情况下，强和弱的分歧计数的情况下，只有强分歧计数。有趣的是，强发散和弱发散之间的区别并没有影响amb的特征定律：我们在这里指的是一组捕捉amb基本属性的定律（例如，这些定律在[ 13 ]中进行了研究）-如上所述，amb的原始规范[ 11 ]是通过描述其行为属性在非常高的水平上给出的amb的语义在π演算中也是非常具有挑战性的我曾弱）解释λ[]中的发散，不可能忠实地编码到π演算中。通过这一结果适用于π演算，以及π演算的任何具有无穷算子的扩展。然而，我们也证明了，在对发散的强解释下，λ[]编码到π演算中是可能的，并且我们推导出了与纯λ演算编码相似的结果和共归纳证明方法（参见[19]）。然后，我们使用这些方法来获得麦卡锡的琥珀色的特征规律利用π-演算的证明技巧，其中一些定律的证明是非常简单的，特别是AMB的两个关键定律，底部回避定律lawM=MM，andthelawVVJ=MVVJ（其中V和VJ是λ-抽象）。我们还研究了局部按值调用的λ[]的扩展再次示出到π演算中的编码，然后使用该编码来导出源演算的代数定律。我们在上面已经提到，λ[]中的操作等价性的表征作为应用双相似性的一种形式仍然是一个悬而未决的问题。我们的研究结果表明，可能确实很难获得这样的双相似性。结果表明，λ[]不存在保持项的分支结构并产生收敛和发散的正确谓词的小步操作语义。具有这些属性的操作语义对于定义具有非确定性的语言（如λ[]）中的双相似性非常重要，因为互模拟是基于分支结构的A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-77在两个非确定性项之间的互模拟博弈中，挑战应该使用小步长语义。纲要在回顾了关于λ[]和π-演算的必要定义和结果之后（第2节），第3节介绍了我们对麦卡锡的amb的语义框架，以及它的一些结果，这些结果激发了下面几节的研究。在第4节到第6节中，我们介绍了我们对λ[]的π演算编码，并介绍了它的一些应用和发展。我们在第7节中总结并讨论了进一步的研究方向。详细的证据可以在[3]中找到。2背景本节包含背景材料。（然而，它也包含一些新的结果：λ[]的新语义和一些新的耦合模拟的最高证明技术2.1具有模糊选择我们假设我们有一个无限多的变量集，范围为x，y，. .λ[]的项随M，N，. ，由以下语法给出：Md=efX| λx.M|M1M2|M1M2.约束变量和自由变量的定义与通常一样。闭项是不包含自由变量的项。替换（写作M[N/x]）和α-转换的定义与通常一样。我们将进行α-转换。闭合值，范围为V，VJ，. 是抽象的。 一个上下文，范围为C，CJ，. 是一个包含空穴出现的项，记为[·]。给定上下文C，C[M]表示用C中的项M替换空穴获得的项。给定M，如果C[M]是封闭的，则C是封闭的，这个术语被扩展到C“封闭”几个项的情况下面是一些λ[]项，它们在下面会很有用：def defI = λx。 x=（λx. x x）（λx. x x）defdefdefK = λx y。 x固定= AA，其中A=λx y。 y（xx y）.我们引入一些关系的符号：定义2.1（关系）如果R是集合S，R−1表示R的逆，而R+和R表示传递性（分别为）。78A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-B ETA（λx. M）N→M [N/x]拉济M→MJM N→MJN特兰斯M→MJMJ→MJJM→MJJPARM→MJN→NJMN→MJNJ瓦尔湖M→V或M=VM<$N→V图1.一、λ[]闭项的运算语义传递闭包和自反闭包。两个关系R和SS的复合记为RSS，而T Rω表示S的元素的无限序列的存在，T = T0，T1，.。使得对于所有i，T iR Ti+1。在[10]之后，我们给出了闭λ[]-项的操作语义。定义2.2（→）关系→由以下规则在封闭术语上定义：图2.1，其中对称版本的LL被省略了。在定义→时，我们捕获了底层归约关系的传递的、非递归的在规则PAR中，允许amb的两个分量都演化。规则VALL，VALR在一个分支收敛时在amb的组成部分之间进行选择λ[]项I只能约化为I（使用VALL）;它不能发散，因为PAR不适用（记住→是非自相关的）。如果我们设置defW=固定λx。x<$I，则项W<$W可以通过P ar还原为自身，因此发散;它也可以通过VALL或VALR收敛到I。注2.3图2.1的语义→是新的。它与[13]（见[3]）中引入的语义~一致，但直接在λ[]-项上定义，而~的定义需要使用修饰项。定义2.4（m和m）一项M是收敛的，记为Mm，如果存在一个值V s.t。M→V或M = V。 M是发散的，记作M，如果M →ω。我们可以注意到，通过定义→，一个MI形式的项，对于任何M不能发散：这个观察在下面的几个证明中是有用的。定义2.5（观测等效性，使用发散）M和N个等效观测值，其中M=M N、i、f或t ext上的任何关闭c丙：（C [M]）C [N]和（C [M]C [N]）。A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-79P定义22.2异步π演算我们假设我们有一个无限的名称集合，也称为通道，我们用小写字母：a，b，......，x，y，.为了阿辛人在第4节的π-演算（简称Aπ）编码中，我们将使用π -演算名称来翻译λ[]变量，并且我们假设变量到名称之间存在注入，以便我们可以保留字母x来引用变量x的编码。 （可能是有效的）n个元组的范围与x，y，. . .Aπ项，我们将简称为过程，使用P，Q，.其定义如下：=零|P1|P2|啊！P|νx P|x（y）.P|你好。我们的演算有非活动进程（0），并行合成，复制，限制，输入前缀和异步输出。过程中的绑定名的定义是输入和限制操作符是绑定的。Aπ中的上下文是沿着λ[]上下文定义的。Aπ的后期操作语义照常引入。它定义法官，形式P的元素µ−→PJ，其中reµi是rann输入a（x）形式的a一种形式为νxay的输出，其中hxh是一种x occur y，或rτ的结构和名称，其中h表示内部def计算 我们引入以下符号：−→τ），µdef−→τdef=（µˆdefµˆ−→=或=ifµ=τ，−→=−→Othererwise，且==→−。结构一致性也像往常一样被定义，以捕捉过程的一些基本结构性质。它需要在以下结果的陈述中，这将有助于下面的证明：Proposition2.6（−→τ给定一个过程P，有，直到结构同余，有限个过程PJ，使得P我们将在进程上使用以下行为关系−→τPJ。定义2.7（行为等价物和前序，1999年，4）• 过程上的二元关系R是弱模拟，如果P RQ和JP−→P意味着存在Q使得Q=Q和PRQ。• 弱互模拟是对称的弱模拟。弱互相似性，写作“弱”，是最大的弱互模拟。• 耦合互模拟是一对模拟（SS1，SS-1），使得：- 如果P SS1Q，则存在QJs. t。Q∈QJ和PSS2QJ;- 如果P SS2Q，则存在PJs. t。PPJ和PJSS1Q。两个进程P和Q是耦合的双相似的，记为P4Q，如果存在80A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-2V1（ V2 V3）V1V2 V3（V1（V2V3））V4V1V2V3 V4图二. →的V 1 <$（V 2 <$V 3）和V 1 <$（V 2 <$V 3）<$V 4的导子树耦合互模拟（SS1，SS−1），使得P SS1Q和P SS2Q。耦合互模拟已经被用于π演算，例如在[15]中。n=2.8（π=π）给定一个名字p，Pp代表vxep<$yP−→对于一些x=0，y= 0。P和Q是等距离观测的，其中P=πQ，i（对于所有C和p，C [P] p惠C [Q]p）和（P0惠Q0）。λ=π的定义遵循λ[]中λ=M的模式（定义2.5，参见下文定义3.7在Aπ中，可观测量是输出粒子，可见的（强）发散，由被迫发散的项引起，将这些项等同于0。命题2.9（同余性质），其中，Aπ。我们有一个共同点4. 更进一步说，π=π和4π=π，并且我们将使用和4到e的表中给出了π=π 的性质。他的儿子很快就会疯掉的使用向上技术，基本上是向上上下文和向上扩展。这种技术是众所周知的，用于[19]。我们已经证明了它们可以适应于4（由于空间不足，我们省略了细节，参见[3]）。3再论λ[]的等价性我们现在提出我们的语义框架麦卡锡我们研究了λ[]的运算帐户，并引入了基于强发散的等价性。我们还表明，如果弱发散的概念，考虑到发散，那么一个忠实的编码到π演算是不可能的。3.1AMB的操作说明让我们看看如何描述amb→。 如果我们考虑图3.1中给出的项（其中V i s是值），我们可 以 看到，根据→，ambA. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-81合成使树木退化，并松散其分支结构。因此，在本发明中，→在λ[]计算中错过了一些选择。这种精度的缺乏可以被视为定义λ[]的基于互模拟的等价的缺点，因为这样的等价通常利用了对计算过程中做出的决策的准确分析。事实上，互模拟等价被认为比迹等价更具鉴别力，直观上是因为它们是基于树而不是基于单个执行（迹）。事实上，在所有的条款，formMV，→定义了一个大的步骤语义：这样的项只能（立即）收敛到一个值。→因此似乎太不精确，来推导出一个合适的互模拟概念。然后，人们可能会问，这是否可以通过提供λ[]的公平操作语义的分支保留表示来改进，在以下意义上：定义3.1（分支保持语义）我们说λ[]上的关系是分支保持语义，如果对于任何约简序列M0.MnV和任意λ[]-项P0，存在序列（Pi）i∈[0，n]使得M0<$P0+.+M nP n.这个定义表达了这样一个事实，即当一个项与另一个项并行放置时，该项的约简树被保留。对于一种可以表达并行组合和非确定性选择的语言来说，标准的小步语义通常具有这种属性，这是它们的组合性质的结果。事实证明，在这种情况下，将这个条件强加给λ[]的一个足够准确的语义，会阻止它排除禁止的分歧（根据amb定理3.2（λ[]没有保持分支的小步长语义）不存在λ[]的分支保留语义来验证规则BETA和LAZY，并归纳出与→相同的收敛和发散概念。证明（草图）设为λ []的分支保持语义。我们定义：Md=efFix（λ x. VJ<$（x<$V））MJd=efM<$V，其中V和VJ是值。 我们拥有：M+MJ+V和MJ+M+VJ.这就导致了矛盾，因为我们可以由此推断MI+MjI+MI，它授权了一个应该被排除的分歧。因此，这种不可能性结果表明，即使λ[]的某种形式的应用性双相似性是可能的（即，可定义的，可证明的一致性），它可能具有有限的实际用途。82A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-3.2强与弱分歧现在我们研究π演算如何影响λ[]的描述。通过对“合理的”翻译进行抽象推理定理3.3（无发散忠实编码）设是π-演算项上含有结构同余的等价关系。在Aπ中不存在λ[]的编码，使得对于任何闭项M：(i) [[[M]][[N]]M=MN（可靠性w. r. t. n=M）;(ii) [[[M]]−→τω优惠M→ω（发散忠诚度）;(iii) M→V<$[[M]]−→τ+[[V]]（保值）。证明（草图）我们根据以下条件进行推理：Zd=ef 固定λz。 （I）（λx. z（λy. （x））项ZI可以收敛到λx1... xn. xn，对于任何n≥ 1，且不能发散。使用子句（i）和（iii），这意味着着着[[[Z]]]的执行树（mod-ulo树）有无限多个节点。使用命题2.6，我们证明这意味着这棵树有无限分支。根据子句（ii），这与Z不能发散的事实相矛盾。注3.4先前的结果在任何有限元（即保持命题2.6）Aπ的扩张。 据我们所知，文献中所考虑的π演算的所有扩展都是无穷的，除了那些包括无穷和算子的扩展。如第1节所示，使用Aπ中的互模拟，我们可以区分强发散和弱发散，定义如下：定义3.5（强发散 和弱发散）设M是λ[]项。- M是强发散的，记为M²，如果M可以演化成一个不能收敛的项;- M是弱发散的，如果M表现出无穷计算，沿着它永远不会失去收敛的可能性。发散项（定义2.4）要么是强发散项，要么是弱发散项，或者两者都是，就像T发散项（T在第1节中定义）一样。注3.6强发散和弱发散之间的区别已经在[14]中出现。作者给出了一个拓扑参数，以表明该集合A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-83ppp[[λx.M]]pdef=vl（p<$l |l（x，q）。[[M]]q）[[[x]]pdef=vpJ（x<$pJ|pJDp）[[MN]]pdef=vq.[[M]]q| q(l). .vx.l|啊！x（r）。[[N]]r[[MN]]d=efvpJ（[[M]]J|[[N]]J|pJDp）wheeqDpd=efq（x）。pānx图三. π演算中λ[]的编码在所有计算的集合中，弱发散计算的实际上可以为λ[]引入合理的操作语义，使得收敛计算集和强发散计算集具有非空测度，而弱发散计算集具有空测度。发散项（定义2.4）要么是强发散项，要么是弱发散项，或者两者都是，就像T发散项（T在第1节中定义）一样。我们现在调整定义2.5，以关注强分歧。公式3.7（λ=λ）对于一个yM，N，Mλ=λN，如果对于一个任意的闭上下文C：（C [M]）惠C [N]） 和（C [M] 2惠C [N] 2）。关系式λ=λ和λ=M（定义2.5）定义如下：λ=M是可感知的对于导数s，它将由λ=λ，h=λ/λλ=M所表示的项分离。通常，λ=λ/λ=Mb eca us eλ=Midenti f iesweakanddstrongdiverences. We例如：我λ=λ/=固定λx。（x）/=λ=夏威夷岛定理3.2不成立，如果只有强发散计数，见[3]。4编码和可靠性我们的编码，写作[][][]，在图4中定义，并遵循应用和抽象运算符的λ一个λ[]-项M被映射到一个过程[[[M]]p，p是一个通道，其中值”（《易经》卷一）：“。抽象化条款为了考虑到这一点，我们在新创建的位置q并行运行M和N的编码，并让（短暂的）链接过程qDpMM84A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-M<$N<$= λN<$M（M<$N）<$P<$=λM<$（N<$P）（λ x. M）N=λM[N/x]M=λMVVJ=λVVJ（M<$N）<$P<$=λM<$（N<$P）M<$M<$=λM对于M闭合见图4。 amb的一些性质在p上转发任何成功终止的评估。一旦其中一个组件触发了qDp，另一个组件就会从上下文中隔离出来，这可能是因为它试图在专用通道q上进行交互，也可能是因为它是不同的。 Modulon=π，这对应于weexpecttfromamb。注意变量编码中额外的间接pJDp在将按值调用编码为（无类型）π演算时需要类似的间接，并且可以使用能力类型[19]来删除。我们不知道如何避免使用类型或其它手段的图4的编码中的间接下面是[][][]的可靠性结果。为了证明这一点，我们首先建立操作对应，其中λ[]中的每个<$→约简都与（直到扩展，与弱双相似性相关的行为前序）相关联（非empty）序列f−→τ在编码π-C文化中，减少了步骤。TheoreM4. 1（可靠性）对于λ [ ]中的nyM，N和名称p，[[M]]p = π[[N]] p意味着M=λN。5导出amb图4展示了我们已经能够建立的一组amb这些结果的证明都是基于相同的方法：我们计算两个λ[]-项的Aπ编码，构造一个（弱或耦合）互模拟来显示（可能使用高达技术，Aπ）的算法，这两个过程都与dy=π相关定理4.1，并得出结论我们给出了这种方法的一个例子，M=λM，amb的关键公平性之一。 我们首先需要一个技术成果：引理5.1对于λ[]的任意项M和名p，[[M]] p <$ν q（[[M]] q|q Dp）。A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-85ν现在我们知道，对于任意项M，M=λM：[[M]]pdef=q（[[M]] q|[[]] q|q Dp）v q（[[M]] q|q Dp）因为[[]] q<$0使用引理5.1，沿着这条思路，我们证明了amb的结合性和交换性，并证明了λv=λv满足β规则. 我们有一个社会性的选择：必须强调的是，对于这个证明，我们不得不推理，4（而不是4），因为在选择的执行中存在我们建立了如下方程：I_∞=λFi_x（λ x. （Ix）），这是因为我们只考虑强发散（该定律在设置中无效[13]，10）。衍生技术。我们还可以使用π演算编码来推导类似于文献中用于证明λ[][13，10]定律的证明技术例如，下面我们推导出一种类似于“Kleene等价”技术的技术定义5.2（=）对于两个λ[]项M和N，M=Ni(i) 如果M <$→ +V，则存在VJs. t。 N <$→ +VJ，对任意p，[[V]]p4 [[VJ]]p;(ii) M ² iN ²。5.我的朋友3（S_s_o_f=）= λ=λ。除了使用π演算之外，与“Kleene等价”的主要区别作为这种差异的结果的一个例子，命题5.3允许我们证明这个λ x （x_i）λ_i=λ_I，其中不能使用“K_（leen）e_qui v a l ence”来表示法完全抽象。预期，我们的方法不完全是一个要求λ =λ（例如，我们在π-演算法中使用相似性，其中λ=λ是纯文本的;这这种情况是将λ-演算编码为π-演算的标准）。 我们可以86A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-ννλλλλλλ[[λx.M]]p[[letx=MinN]]pdef=l（p<$l|啊！l（x，q）。[[M]]q）def=q（[[M]]q|q（v）。（[[N]]p|啊！x（r）。r<$v））图五. 局部按值调用的λ[]的π然而，对于应用性双相似性的“开放”版本，导出部分完全抽象结果（在我们仅比较纯λ项的意义上是部分的）（see[19，PartVI]）。这是一种关系，当n=op时，由扩展关系定义→打开项，并说在头部位置具有自由变量的项被卡住。在下面的定义中，我们为操作语义的扩展版本保留相同的符号→5.第五章4（Openapplicative相似）是最大的对称在λ[]上的一个三角形，当M=0pN时，(i) M→λ x。 MJ表示N→λ x。NJwthMj=opNJ;(ii) M→xM1. . . 当hn≥0时，M n表示N→xN1. . Nn和Mi=opNi对于所有1 ≤i≤ n。定理5.5（部分全抽象）设M，N是两个纯λ-项，p是一个名字. 然后[[M]]p<$[[N]]pi <$M<$=opN 。可以注意到，对于具有内部选择的λ-演算扩展，整个演算的完全抽象问题（π-演算编码是否是完全抽象的开放应用双相似性）仍然是开放的。在λ[]中，同样的问题似乎至少是困难的。6按值λ []的一个重要的丰富是，与熟悉的让.在构造中，它在语言中引入了一种按值进行局部调用的形式。相应的附加归约规则为：LETM <$→V设x=M，N<$→N[V/x]结果演算的编码是通过修改上面给出的编码来获得的，如图6所示（未提及保持不变的子句）。一封信的翻译…在建筑物中 ，A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-87在局部声明项的求值中，接着是在“in“之后的项的求值我们还添加持久性，使用复制，在编码的抽象，因为在存在让…在中，一个函数的几个副本可以在一次计算中被触发。前面几节中给出的结果也适用于λ[]和let。例如，健全性变成：定理6.1对于λ[]中的任意项M，N，且f或任何名称p，[[M]]p=π[[N]]p 意味着M=λN。同样，使用简单的互模拟推理，我们已经推导出λ[]的这些示例定律，其中let：在M中，letx=V=λ（λ x. M）V对于M闭合，x=Min xx= λMletx=λinMλ=λλ设x=Min N= λN，若M∈N且x/∈fn（N）.7进一步的结果和评论在本文中，我们区分了强发散和弱发散，并证明了只有强发散才应该计数，以便使用π-演算获得λ[]我们认为，这两个结果的语义然而，有人可能会说，在带有像amb这样的运算符的语言中，一个一般的公平性要求，即计算不应该在λ演算中研究的与amb相似的并行算子是[4]和[1]中的并行算子。这些是实际上，从语义上讲，这些操作符比amb简单得多。(The编码到π演算中是直接的，参见[19]。在全文[3]中，我们讨论了第4节的π演算编码的几个变体。例如，我们讨论了为什么编码的某些简化不允许我们获得第4-6节中的一些结果。我们建立的一些定律表达了amb在Aπ中的公平性，并且在我们的设置中是利用互模拟导出的为了更好地理解互模拟所带来的公平性，在这个方向上走得更远是很有趣的。 这样做的一种方法是研究其他公平运算符的π演算语义，例如。公平合并，这比88A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-amb[16，5]。该运算符以公平的方式计算两个（有限或无限）列表的合并，也适用于列表包含分歧的情况。我们采用了[16]的一个论点，并证明了在操作层面上不可能将公平合并表示为π演算;参见全文[3]。一个有趣的问题是公平合并模互模拟的可定义性，即在行为层面。确认我们要感谢Mariangiola Dezani进行了富有洞察力的讨论，以及匿名裁判的有益评论。这项工作得到了欧洲FET -全球计算项目PROFUNDIS的支持。引用[1] G.布多（严格）并行函数的Lambda演算。信息与计算，第108卷，第51-127页，1994年[2] G. Boudol和C. Laneve.λ演算，多重性和π演算。在证明，语言和互动，纪念罗宾米尔纳的论文。麻省理工学院出版社，2000年。[3] A. Carayol，D. Hirschko，D.桑吉奥吉关于麦卡锡琥珀的π-演算观点。 完整版，正在编写中http://www.irisa.fr/galion/acarayol/RR.ps网站，2003年。[4] M. Dezani-Ciancaglini，U.de你好并发λ-演算的一个过滤器模型SIAM J. Comput. ，27（5）：1376[5] 玛丽贝尔·费尔南德斯和莱昂内尔·哈利勒 交互网 与 麦卡锡的 琥珀色 在理论计算机科学电子笔记，卷68。Elsevier，2002年，网址：http://www.elsevier.nl/locate/entcs/volume68.html[6] P·亨德森。python功能操作系统。函数式编程及其应用，第177-192页。剑桥大学出版社，1982年。[7] D. J. 豪证明同余 互模拟 在功能 编程语言。信息与计算，124（2）：103[8] J·休斯和 J· 奥唐纳非确定性函数程序的表示与推理。在Proc. Glasgow 1989 Workshop onFunctional Programming，Workshops in Computing. Springer Verlag，1990年。[9] S.拉森关于函数和非决定论的关系推理。奥胡斯大学博士论文，1998年。[10] S. Lassen和A.莫兰McCarthy's Amb的独特定点感应。在MFCS'99的Proc.Springer Verlag，1999年。[11] J·麦卡锡计算的数学理论的基础。 计算机程序设计和形式系统，第33-70页。1963年北荷兰[12] R.米尔纳作为过程的功能。技术报告1154，INRIA Sophia Antipolis，1990年。A. Carayol et al. / Electronic Notes in Theoretical Computer Science 96（2004）73-89[13] A.莫兰按名称呼叫，按需要呼叫，以及麦卡锡博士论文，查尔姆斯理工大学和哥德堡大学，1998年。[14] V. Natarajan和R.克里夫兰分歧和公平测试。在Proc.ICALP95，LNCS的第944卷，第648-659页中。Springer Verlag，1995年。[15] 联合Nestmann和B.皮尔斯解码选择编码。并发理论国际会议，第179-194页，1996年[16] P. Panangeli和V. Shanbhogue。 麦卡锡的amb无法实现公平合并。 在Proc. of FST-TCS，Volume 338 ofLNCS，pages 348-363中。Springer Verlag，1988年。[17] C. 投手函数式编程和不稳定的非确定性。博士论文，牛津大学，2001年。[18] D.桑吉奥吉并发场景中的lazy lambda演算。第七届LICS会议，第102-109页。IEEE ComputerSociety Press，1992.[19] D. Sangiorgi和D.沃克π演算：移动过程理论。剑桥大学出版社，2001年。[20] D.特纳功能性操作系统的一种方法。函数式编程中的研究主题。艾迪森·韦斯利1990年