ρ-演算和λ-演算中的项集合

理论计算机科学电子笔记171（2007）3-19www.elsevier.com/locate/entcsλ-演算和ρ-演算中的项集合Germain Faure1Universit′eHenriPoincar′eLORIA，BP239F-5450 6Vandouvre-l`es-Nancy，France摘要ρ演算通过定义任意模式的抽象和使用作为演算参数的模式匹配算法来推广项重写和λ演算特别地，可以使用不具有唯一主解的方程理论。在后一种情况下，匹配问题的所有主要解决方案都存储在一个“结构”中由于ρ演算中结构的定义有多种方法，本文研究了一种带有项集合的λ本文的贡献包括一个新的语法和操作语义的λ-演算与长期收集，这是相关的λ-演算与严格并行功能的Boudol和Dezani等人研究。并证明了为微积分定义的β-归约关系的连续性（这是一个合适的λ-演算中β-归约的标准规则的推广保留字：平行演算，平行算子，典范集，项集合。1介绍ρ-演算，也被称为重写演算，最初出现于与λ-演算不同的动机和不同的群体。引入它是为了明确重写的所有成分，例如规则应用和结果[7]。最后，ρ演算提供了λ演算的扩展，其中包含了源自重写和函数式编程的额外概念，即内置模式匹配，使用匹配约束和术语集合表示。到目前为止，ρ演算有几个方面已经被研究过。计算的动力学已经通过定义ρ演算的相互作用网络进行了研究[13]。我们还可以提到类型系统的研究[3，24]及其在证明理论中的应用，该证明理论处理广义演绎模[25]中的丰富证明项。1电子邮件：germain. loria.fr1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.12.0374G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）3在更实际的一面，ρ演算已经被用来编码对象演算[8]，并给出一个语义重写基础语言[7]，如ELAN [4]。最近，在ρ演算中指定Focal Project [17，18]的工作正在进行中，这是一个可以开发认证程序的编程环境。此外，ρ-演算已被用于指定有效的决策过程[21]。术语集合在ρ演算的上下文中是基础的，但在逻辑编程和Web查询语言中也是通常情况下，演算中涉及的匹配约束可能有多个解-这也是例如TOM [23]，Maude[16]，ASF+SDF [1]或ELAN [11]等编程语言的情况-从而生成结果的集合。不同的ρ演算工作提出了不同的方法来处理术语集合。它们最初是用集合表示的[7，6]。在更近的作品[9]中，它们通过结构构造来表示，其操作语义由理论（通常是结合性、交换性和/或等元性公理的组合）参数化，用户根据他想要处理微积分中的非确定性的方式来选择该理论。例如，通过考虑结构上的结合、交换和幂等（ACI）理论，恢复了“结果集”的原始语义当演算中涉及的匹配约束可能有多个解时，即当匹配问题的求解给出多个解（替换）时，这些最近的工作给出的一般性被打破。事实上，据作者所知，没有令人满意的（总）顺序来比较替换。因此，我们必须用集合（或者至少用一种结合的和交换的结构）来表示术语的集合。如果我们仔细观察ρ-演算的不同表示，我们可以说：不同的操作语义总是共享一个共同的结构：评估规则集可以分为第一个子集，由ρ-规则组成，λ-演算的β-规则的扩展，用于处理模式抽象的应用，以及处理术语集合的第二个子集（包括δ-规则，将术语集合分布在应用操作符上）。这两种规则都在同一级别处理，而前者在简单地说，微积分的计算机制，当后者只执行关于术语集合的“管理简化”时在[12]中提出的对ρ-演算的指称语义的第一次尝试启发了（严格）并行函数的ρ-演算和λ-演算之间的关系[5]。在语法上，后者是λ-演算的扩展，具有分配左w.r.t.的并行运算符。应用程序和w.r.t.λ-抽象（作为ρ -演算的结构算子）。它已经扩展到并行和非确定性λ-演算，如[10]。（严格）并行函数的ρ-演算和λ-演算的Scott模型惊人地接近：结构算子由连接算子充分表示。这表明了这些形式主义之间的明确关系：（严格）G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）35<∞i=1并行函数是具有项集合的λ演算的扩展，而ρ演算是具有项集合和内置模式匹配的λ演算的扩展作为研究具有非酉匹配理论的ρ-演算的第一步，本文提出研究具有项集合的λ-演算，以下称为λ“-演算。在规范化重写的精神[15]中，本文介绍的方法通过仅考虑规范集来管理元级别的术语集合，即针对某些规则进行规范化的集合（以前称为“管理简化”）。结果是一个连续的演算，其中计算机制变得更容易理解，因为只有β规则是一个显式的评估步骤。 虽然[5]的工作主要坚持模型（着眼于编程语言的完全抽象问题），但在这项工作中，我们提出从操作的角度来看待λ“-演算，为[5]中引入的等价关系提供明确的操作语义。同样的方法可以使用，如果一个人更喜欢考虑典型的多集，因为无论是定义还是证明都与恒等式无关。本文件的结构安排如下。第一节通过定义简单项、平行项和替换来介绍λ“-演算的语法第二部分是对λ“-演算中各项之间关系的一般性研究第三部分介绍了λ“-演算的操作语义我们最终第四部分研究了Church-Rosser性质。最后，我们对减少的可操作性发表一些评论。2λ“-演算的λ2.1预赛为了更好的可读性，关系τ也由→τ表示。它的自反性和自洽性决定了它由（τ）→→τ→τ决定。 对于关系τ，A的子集是集合{B|A→τB}。两 个关系的组合简单地用并列表示。我们用P+（X）表示X的有限非空子集。非空集合{S1，.，Sn}通常表示为{Si}n或者更简单的{Si}i。2.2方面在这一节中，我们介绍了λ“-演算的语法，它由简单项和平行项组成。平行项只是一组简单的项。简单项不同于λ-项，因为它们不能应用于一个简单项，而只能应用于一组简单项，即一个平行项。定义2.1（简单项和项）给定一个可数变量集X，我们通过k上的归纳法定义一个递增集族（Sk）。 我们设置S0 = X，并定义Sk+1如下：6G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）3<∞<∞<∞• 单调性：Sk<$Sk+1;• 抽象：若S∈Sk，则λx.S∈Sk+1;• 应用：如果S∈Sk且M∈ P+（Sk），则SM∈ Sk+1。我们用S表示所有集合Sk的并集，用M表示集合P+（S）。 我们称简单项为S的元素，称平行项或简单项为M的元素。在应用SM中，简单项S被称为处于功能位置，而项M处于应用位置。简单的 术语是S，T，U… 并且术语由M、N、P、E表示。. .我们用η表示单项到项的正则注入，即对于所有单项S，S→η{S}的关系。我们考虑项模α-卷积和Barendregt的hy g i ` ene卷积。α-卷积神经网络定义如下：M=αNS∈M，S=αT⎪⎩∀T∈N,∃S∈M,T=αS请注意，α转换不保留基数。 比如我们有{λx.x，λy.y}= α{λz.z，λz.z}={λz.z}。我们可以注意到，通过项上的归纳证明一个性质意味着通过最小k上的归纳证明每个项M的这个性质，使得M∈ P+（Sk）。这个数表示M的高度，记为h（M）。注2.2我们可以用以下等式等价地定义简单项和项：简单项S∈S：：= x|λx.S|S M项M∈M：：={S，.，S}故，一个词的长度可以定义如下：h（x）= 0h（λx.S）= 1 +h（S）h（S M）= 1+max{h（S），h（M）}h（{Si}i）=maxi {h（Si）}语法糖为了更好的可读性，λ-抽象和应用操作符经常被应用于术语。这些简单的语法糖定义如下：λx。{Si}i ={λx.Si}i{Si}iM={SiM}i例如，我们可以写λx。{x，y}或{λx.x，λx.y}。G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）37同样地，表示相同的术语。2.3取代{z，t}{y}和{z{y}，t{y}}我们将替换的应用定义为三个步骤：(i) 首先，我们定义一个变量被一个简单项中的一个简单项替换。该操作的类型为S×X ×S →S。(ii) 然后，我们定义用简单项中的项替换变量。这个操作的类型是S×X ×M→M。注意，在一个简单项中，用一个项代替变量得到一个项。(iii) 最后，我们将前面的运算扩展到term，即我们定义一个变量被一个项中的一个项替换。这个操作的类型是M×X ×M→M。定义2.3（简单替换）设x是一个变量，T是一个简单项。 我们通过归纳法在单式项S上定义代换[：= ]：S×X ×S→S如下：如果x=y，则y[x：=T]=在抽象的情况下，我们采取通常的预防措施，假设没有损失。一般性，并感谢α转换，y T。x和y不是自由的，定义2.4（简单替换）设x为变量，M为项。我们通过归纳法在单式项S上定义代换[：= ]：S×X ×M→M如下：y[x：=M]=Mifx=y定义2.5（术语替换）替换的定义可以是否则，（λy.S0）[x：=T]（S0{Si}i）[x：=T]==λy。（S0[x：=T]）（S[x：=T]）{Si[x：=T]}i（λy.S）[x：=M]=否则，将{y}λy。（S[x：=M]）（S{Ti}i）[x：=M]=（S[x：=M]）iTi[x：=M]8G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）3通过设置扩展到术语{S}n[x：=M]=，S[x：=M]，nii=1我i=1例2.6我们考虑简单项y{x}。用项{z，t}代替x得到：（y{x}）[x：={z，t}]=（y[x：={z，t}]）x[x：={z，t}]={y} x[x：={z，t}]={y}{z，t}={y{z，t}}在y{x}中用{z，t}替换y得到：（y{x}）[y：={z，t}]=（y[y：={z，t}]）x[y：={z，t}]=（y[y：={z，t}]）{x}=（{z，t}）{x}={z{x}，t{x}}替换引理是有效的。引理2.7（代换引理）设M，N和P是项，x是变量.如果x在P中不是自由的，那么我们有M[x：=N][y：=P]=M[y：=P][x：=N[y：=P]]3λ“-演算中项的关系我们将考虑两种关系：从单项到作为S×M的子集的项的关系和从项到作为M×M的子集的项的关系。为了简化阅读，我们使用以下定义：定义3.1（（单）项关系）单项关系是S × M的子集。关于项的关系是M ×M的子集。为了在λ“-演算的项上定义一个关系，我们总是按照以下两个步骤进行第二点将在3.1节中详细研究。我们专注于第一个。这项工作的特殊性在于，语法由两个不同的集合组成（简单项的集合和项的集合），并且一个简单项将被简化为一个项（从而从一个语法类别移动到另一个）。的G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）39定义高阶语言的操作语义（通常称为归约关系）的通常方法（例如参见[2]）首先定义头部位置的归约（通常称为归约概念），然后考虑其兼容闭包（给出归约关系）。在λ“-演算的框架中，同样的方法必须小心使用。因为一个简单项可以归约为一个项，所以我们必须弄清楚相容关系是什么，或者换句话说，我们必须弄清楚如何计算归约概念对于简单术语上的关系，我们采用通常的“上下文关系”概念若S→τM则C[S]→τC[M]对于任何上下文C[]。在λ“-演算中，上下文C[]可以将简单项S置于抽象之下，或者置于应用程序的功能位置，或者置于位于应用程序的应用位置的集合中。语境关系的概念（定义3.7）使这一思想形式化。对于项的关系，我们还必须说明这种关系相对于集合的行为这给出了加法关系的概念（定义3.4）。然而，在同时减少几个redexes的关系的上下文中，上下文和加法关系的概念应该适应。这导致了乘法和平行关系的概念（Def.3.5和3.8）。在下面的章节中，当定义一个新的关系时，我们总是会陈述它的相关属性（加法，乘法，上下文或并行）。这不仅有助于我们的证明，也有助于增加直觉。3.1把一个简单项上的关系推广到一个项上的关系设τ是一个简单项的关系。我们想确定不同的方式将其扩展到一个关系的条款。第一种方法是使用简单项到项的规范注入（pre-n表示为η）。如果S→τM，则{S}→τbM。这个扩展被称为单例扩展，它将只用于技术原因。让我们看看其他方法。假设给定一个项M，我们认为它是简单项（的单例）的并集。我们想通过一个扩展关系确定M的后继者。它们可以是用τ的后继项代替M的一个单式项得到的项，也可以是用τ的后继项代替M的所有单式项得到的项。通过类比线性逻辑中使用的术语，我们称前者为τ的加法扩张，后者为τ的乘法扩张。定义3.2（扩展关系）给定一个简单项的关系τ，我们10G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）3^^不好意思001˜定义thre reresτi，τi和τinterm如下：辛格尔顿S→τM{S} →τbM一种添加剂S→τM{S}E →τeMEδi，Si →τMi乘性i{Si}→τ我们将经常提到下面的评论，表示三个扩展（单元素，加法和乘法）是连续的。引理3.3设（τi）i是关于单项的递增关系序列，τ是定义为τ= τiτi的关系。 然后我们有τ=iτi，τ=iτi和τ=iτi。我们只证明了第一个等式。 另外两个是相似的。M→τiτbiN惠τi0， M→τci NM={S}且S→τi N惠M={S}且S→τiN惠M→diτiNO3.2关系我们首先定义了一个关系关于集合的两种不同行为。定义3.4（加法关系）关于项的关系τ是加法的，如果对于所有项M1，MJ使得M1→τMJ则对于所有项M2，我们有M1<$M2→τ1 12.我们可以注意到，如果τ是关于简单项的关系，则关系τ是加法关系。定义3.5（乘法关系）关于项的关系τ是乘法的，设对所有项M1，MJ，M2和Mj，使得M1→τMJ和M2→τMj，j1J21 2有M1<$M2→τM1<$M2。我们可以注意到，如果τ是关于简单项的关系，则关系τ是乘法关系。加法和乘法关系在以下意义上是对偶的：命题3.6加法关系的自反传递闭包是乘法关系。G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）31121证明设τ是一个加法关系。我们想证明（τ）是乘法的，<$M1， MJ，M2， MJM1→→τMJ，M2→→τMJ<$M 1<$M2→→τMJ<$MJ（一）1 2 1 2 1 2这足以证明，M1， MJM1→→τMJM2M1M2→→τMjM2.（二）1 1 1假设（2）为真，我们证明（1）。设M1，MJ，M2，MJ是项，使得J J1 2JM1→→τM1和M2→→τM2。（2）当M1<$M2→→τM1<$M2和thenMJ<$M2→→τMJ<$MJ。通过对（τ）τ的 迭 代，我们在M1→M2→τ中得到了一个新的结果J112MMJ. 为了证明（2），证明以下内容就足够了：MJM1→τMJM2M1M2→τMjM2。（三）1 1 1假设（3）为真，让我们证明（2）。 设M1和MJ是这样的项，1NnnnthatM1→→τM1。通过f（τ）的定义具体来说，是M1， .. . . M1 苏志达M1→τM2→τ... →τMn，其中M1=M1且Mn=MJ。 应用（3）n次111J111JwegetM1→M2→τ。 . →τM1<$M2thatisM1<$M2→→τM1<$M2. 我们找到了注意，（3）是真的，因为τ是加性的假设。O我们在下面的两个定义中引入了关于应用和抽象运算符的项上的关系的两个不同行为定义3.7（上下文关系）简单项上的关系τ是上下文的，如果它满足以下两个条件：(i) 语境性w.r.t.对于X的每一个变量x，对于每一个单式项S和每一个使得S→τM的项M，我们有λx.S→τλx.M。(ii) 语境性w.r.t. 应用程序操作员：(a) 对于所有的项M，N和对于每个使得S → τM的简单项S，我们有SN →τMN。(b) 对于所有的项M，N和每个单项S使得M → τeN，我们有SM → τSN。定义3.8（平行关系）一个关于项的关系τ是平行的，如果它是自反的，乘法的，并且满足以下两个条件：(i) 非对称性抽象算子：对所有变量x∈ X，对所有项M和MJ，使得M→τMJ，我们有λx.M→τλx.MJ。(ii) 非对称性对于所有项M1，M2，MJ和J J JJJ1M2使得M1→τ M1和M2→τ M2，M1M2→τ M1M2.我们常说一个关系具有平行性，意思是它是一个平行关系。加法关系和乘法关系之间的对偶性可以扩展到上下文关系和并行关系：12G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）3<∞<∞<∞00我0、、、命题3.9设τ是简单项上的上下文关系。 然后，该relat i on τ的响应性和反传性的闭合，即该relation（τ）τ，是并行的。证明类似于Prop。三点六O每个平行关系在以下意义上与替换应用兼容引理3.10设τ是关于项的平行关系。如果M，N，MJ是使得M→τMJ的项，则N [x：=M] →τN [x：= MJ].证明证明是通过归纳N。 如果N ∈ P+（S0），则结果是明显的.假设这个结果对P+（Sk）中的所有项都成立 设N是属于P+（Sk+1）的项. 当hS i ∈ S k + 1时，N={Si}i. 我们证明了对于所有i，Si[x：=M]→τSi[x：=M]的关系，并通过τ的多重迭代得到了新的结果。以下是四种情况：(i) 如果Si0属于Sk+1，并且它也属于Sk，则结果通过归纳成立(ii) 如果Si属于Sk+1，其中Si= λx，SJ和SJ∈ Sk.然后，通过诱导，0J0i0Ji0J假设条件下，有Si0[x：=M] →τSi0[x：=M]. 通过并行性，关系→τ，我们得到λx.SJ[x：=M] →τλx.SJ[x：=MJ]，这意味着我0我0Si[x：=M]→τSi[x：=MJ](iii) 如果Si属于Sk+1，其中Si=SJNJ，SJ且NJ∈P+（Sk）. 这0 0i0i0i0i0<∞J情形与前一情形类似：我们在Si0上应用归纳假设和NJ，我们通过τ的平行性得出结论。O下面的定义和下面的引理在证明中是至关重要的第五节教会-罗瑟的财产。他们形式化了这样一个思想，即如果简单项上的乘法关系满足多菱形性质（形式上，如果它的单例扩张满足菱形性质），那么它的乘法扩张也验证了这个性质。定义3.11（多菱形）关于项sat-的一对二元关系（τ，τ）满足多菱形性质，如果对于任何项M，对于任何m> 0，并且对于任何项M1，. ，Mm使得M→τMi，则存在一项MJ使得对所有i有Mi→τM J。M，τ，，ττ，，s J...，zM1、M.2，Mn，你好，，z.J，t，，MJG. Faure/Electronic Notes in Theoretical Computer Science 171（2007）313^JKβββββββ β˜JJJJ引理3.12设τS×M是关于单项的关系，设τM×M是关于项的乘法关系。 如果对（τ，）满足多菱形性质，则对（τ，）也满足多菱形性质。假设M和M1，…，Mn是使得对所有i有M→τMi的项。对于所有i和j，当S j → τ N i时，nM={Sj}j和dMi={N i}j。Since（τ^，τ）满足多菱形性质，存在项Ni→<$NJ。自从阿维尼翁乘法，我们有{Ni}j→<${NJ}j对于所有i，也就是说，Mi→<$MJ，J JMJ={N J}j。O4λ“-演算的运算语义为了定义λ“-演算的运算语义，我们首先在简单项上定义一步约简β1。然后我们使用加法扩展在项上扩展它：这提供了项的一步约简。接下来，我们考虑后者的自反和传递闭包，它定义了关系β。在下一节中，我们将证明这种关系是一致的。4.1β1还原的定义定义4.1我们在简单项上定义关系的递增序列（β1）k通过感应。 关系β 1是空关系，关系β 1被定义为0归纳如下：S→1MKk+1S→1k+1 M（λx.S）M→1k+1M→fMJS[x：=M]S→JS→1M1 1Mkk kλx.S→1k+1 λx.MS M→1k+1 {S MJ}S M→1k+1 MJM我们定义∞1 1Kk=0我们定义了一步归约β1，它将一个简单项归约为一个项。通过考虑β1的加法扩张即β1，得到了项的一步约化。它的自反和传递闭包是表示为β的关系，即：β（β1）我们可以把λ-演算看作是λ“-演算的子演算，其中所有的项都是单例的。下面的例子说明了这一点。βββ∗14G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）31111β˜1β1β例4.2λ-项（λz.λt.zt）（λxy.x）可以被编码到λ“-演算中，我们可以模拟λ-演算的约简：{（λt.λt. z{t}）{λx y. x}}→f{λt. （λx y. x）{t}}β→f{λt.λy. t}βλ-演算的λ-项ω=（λx.xx）λx.xx可以被编码到λ“-演算中，我们可以模拟λ-演算的约简：{（λx. x{x}）λx. x{x}}→f{（λx. x{x}）λx. x{x}}β→f.. .β注4.3在G. Boudol，λ-抽象和应用算子对项的应用不是本文所介绍的λ“-演算中的语法糖，而是语法和下面两个方程的直接组成部分λx。{Si}i ={λx.Si}i{Si}iM={SiM}i从左到右定向，用作求值规则，与λ-演算的β其结果是一个微积分，区分所有以下条款（g1“g2“g3）z（g1“g2）z“g3z g1z“g2z“g3z而在λ“演算的框架中，它们都由规范项表示{g1z，g2z，g3z}我们通过分析β1和β的关系来结束这一节。引理4.4关系β1是上下文关系。定义3.7的证明语句（i）和（ii-a）通过β1的定义获得。事实上，如果S→1MJ，则存在k使得S→1K M.J. 我们得到SN→1k+1 因此SN →β1 M JN。陈述（ii-a）以同样的方式进行陈述（ii-b）是β1的定义和continuity的性质的简单结果。事实上，我们可以通过PP来重新计算如果M→fM，则该值为βR em. 3.第三章。3和第一个iceksuchatM→fMJanddhenSM→K1k+1 SMJ（定义）β1）。O命题4.5关系式β是平行的。ββG. Faure/Electronic Notes in Theoretical Computer Science 171（2007）315kBkkBkk+1k+1由 引 理 4.4 证 明 ， 关 系 β1 是 上 下 文 关 系 。 然 后 我 们 可 以 应 用 3.9 的 提 议 。O5Church-Rosser财产为了避免与TaitanddMartin-Léofandintheseseect意义上的平行关系术语混淆。第三，上述四种关系将被称为同时的中美关系。为了证明λ“-演算的关系β的连续性，我们采用与文献[22]中基于平行关系的λ -演算的连续性证明相同的方法.我们首先定义了β1还原的一个变体（在第4节中定义），它在一个步骤中同时还原几个赎回这个关系用B表示。然后我们证明了它的平行扩张的自反传递闭包，即关系B的自反传递闭包，等于关系β。 最后，我们证明了B的连续性，然后推导出β的连续性。5.1同时减少B定义5.1（B-归约）单项关系B被定义为单项关系的递增序列（Bk）k的并集。关系式B0等于η。关系式Bk+1由归纳法定义如下：S→BkMS→BkNS→Bk+1Mλx.S→Bk+1 λx.NJS→BNJM→MJSM→BNJMJ因此，关系B被定义为：S→BNJM→MJ（λx.S）M→B NJ[x：=MJ]∞BBk.k=0请注意，在B的定义中，我们使用乘法扩展（而在β1的定义中，我们使用加法扩展），以便在一个步骤中同时减少几个赎回。我们证明关系B是平行的。这给出了一个平行关系的例子，它不是上下文关系的自反和传递闭包命题5.2关系B是平行的。证明我们首先证明关系B是自反的，也就是说，关于表示为id的项的恒等关系包含在B中。这是真的，因为B0≠B且B0=η=idJ16G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）30K˜˜1ββββββKβ1B11βK111B的乘法性是显而易见的。 让我们展示一下w.r.t. 的抽象运算符设M1和MJ是满足M1→MJ的项.这意味J1B1M1=i{Si}且M1=iNi，其中Si→BNi.那么我们有λx.Si→Bλx.Ni对所有i，证明了λx.M1→λx.MJ.现在让我们来展示一下相对论。BJ1J J应用程序操作员。 设M1，M1，M2和M2是满足M1→BM1的M2→MJ. 这意味着我们有M1=i{Si}和MJ=iNi，B2J1对于所有i，Si→BNi。然后我们有SiM2→BNiM2，这意味着M1M2→MJMJ.B12O5.2B的凝聚力引理5.3我们有以下包含：β1β2β因此B的自反传递闭包是β。为了证明第一个包含，我们通过对k的归纳证明β1<$B。k= 0的情况很明显，因为β1是空关系。对于归纳法，我们超级流行的是β11B。我们不能把它翻过来B. 设M和N为2KtermsuchtatM={S} E→1βk+1k+1PE=N且S→1k+1 P. 我们想证明了{S}<$E→BP<$E，但由于B是自反的，（特别是E→B） E）证明{S} →B是足够的 p的可以通过用于证明S→1P的最后一个规则的情况来完成：k+1• 如果S→1k+1 P与S→1K Pthen{S}→f1Panddbyinductioninnhypothesisweβk得到{S}→BP。• 如果S→1k+1 其中S =（λx.S1）M1，P = S1 [x：= M1]. 则有（λx.S1）M1→B1S1[x：= M1]和{（λx.S1）M1} →B1S1[x：= M1]。 由雷姆。 3.3适用于B、结果成立。• 如果S→1k+1 其中S = λx.S1，P= λx.P1和S1→β1P1. 通过感应假设，我们得到{S1}→BP1，然后由B的平行性，我们得出这个案子了• 如果S→1k+1 当S=S1M1时，P={S1MJ}，且dM1→fMj. ByinductionK假设，我们得到M1→B{S1M1} → {S1MJ}。M.J.再次通过B的平行性，我们得出结论• 如果S→1k+1 P，其中S=S1M1，P=PJM1且S1→β1 M1. 这个案子类似与之前的那些不同我们现在证明第二个包含。我们可以证明ηβ<$β，即η和β的复合的乘法扩张包含在β中。事实上，设M和N是满足M→ηβN的项，即存在单项S1，.，Sn和项P1，..，Pn使得M =πi{Si}和N= πiPi，其中Si→ηβPi对所有i.βG. Faure/Electronic Notes in Theoretical Computer Science 171（2007）317B2k+1通过定义ηii 由β的parallelism，我们有ve{Si}→→βiPi。 此时M→→βN。为了证明B∈β，只需证明：Bk η β。事实上，如果Bk<$ηβ，则B=<$kBk <$ηβ<$β。这就是我们在下面通过对k的归纳所做的。k= 0的情况是平凡的。假设Bk<$ηβ，我们证明Bk+1<$ηβ。设S是一个单项，M是一个满足S→Bk+1M的项. 通过最后一个用于证明S→Bk+1M的规则的情况：(i) 如果S→Bk+1M，其中S→BkM，则通过归纳，结果成立。(ii) 若S→Bk+1M其中S = S1M1且M = P1M2其中S1→BkP1且M1→BM2. 通过对这两个点的感应，可以得到：S1→ηβP1和M1→→βM2;{S1}→→βP1和M1→→βM2。 由βw有{S1M1}→→βP1M2的模式可知，此时为S1M1→ηβP1M2。(iii) 若S→Bk+1M，其中S =（λx， T1） M1，M = P1 [x：= M2]，则 T1→BkP1，M1→BkM2. 通过对这两个点的感应，我们得到了T1→ηβP1和M1→→βM2。我们想证明（λx.T1）M1→ηβP1 [x：= M2]即{（λx.T1）M1} →βP1 [x：= M2]，这显然是正确的.(iv) 若S→Bk+1P且S = λx.S1，则P = λx.P1且S1→BkP1.通过归纳，{S1}→→βP1，并由parallelismof→→βwecuu{λx. S1}→→βλx.P1thatisS→ηβM.引理5.4设x为变量，M1，MJ，M2，MJ为项.如果M1→OMJ和M2→MJ，则12B1M1[x：=M2]→MJ[x：=MJ]B12证明我们通过对k的归纳证明，如果M1→MJ且M2→MJ，则J JBk1JB2M1[x：=M2] →BM1[x：=M2]。 对于k= 0，我们有M1=M1，然后我们得出结论通过B的平行性（应用引理3.10）。O命题5.5关系B是连续的。证明我们通过对k的归纳证明了对（Bk，B）（这显然包含命题）。k= 0的情况是平凡的，因为B0只是恒等函数。因此，让我们假设（Bk，B）满足多菱形性质，让我们证明（Bk+1，B）也满足多菱形性质。通过引理3.12，可以证明t（B^，B）满足多变量概率。 这就是我们在下面所做的。设S是一个简单的术语和M1，.，Mn是使得对所有i，S →Bk+1 Mi的项. 通过对S.• 对于变量x，S=x的情况是不可能的。18G. Faure/Electronic Notes in Theoretical Computer Science 171（2007）312我我21• 如果S = λx.T，则我们有Mi= λx. Ni，其中对所有i，T→BkNi。 然后通过归纳假设存在一个NJ，使得Ni→那我们就完了• 如果S=TM，则存在两种情况因此λx.Ni→λx.NJ.·如果对于所有i，我们有Mi=M1M2，其中T→BM1→M2。然后i ikiBki通过归纳假设，存在NJ和NJ使得M1→BJ和M2→B案子NJ表示所有i。关系B（Prop5.2）的并行性得出结论：·否则，T=λx.U并且存在1≤q≤n使得(i) M1 = N1 [x：= P1]. 且Mq=Nq[x：=Pq](ii) Mq+1 =（λx.Nq+1）Pq+1. 且Mn=（λx.Nn）Pn其中λx.U→Bkλx.Ni和M→BkPi。 通过归纳假设，存在一个项NJ和项PJ使得λx.Ni→λx.NJ和Pi→PJ。然后我们J JB B通过应用引理5.4证明Mi→BN [x：= P]对于项M1，. ，Mq而ρ的定义则不然。O5.3β的凝聚力定理5.6 λ“-演算的项上的关系β具有Church-Rosser性质.证 明 由 于 B 的 自 反 和 传 递 闭 包 是 β （ 引 理 5.3 ） ， 并 且 由 于 关 系 B 是 连 续 的（Prop.5.5），因此结果显然成立。O结论我们研究了λ-演算的一个推广，其中项集合由规范集表示。这为（严格）并行函数的λ演算提供了一个清晰的操作语义，这是研究非酉匹配理论的ρA.Reilles [20，19]关于规范抽象语法树的工作与本文的方法密切相关。实际上，前者提供了（以非常有效的方式）维护重写系统中规范形式数据的内部表示在λ“-演算的情况下，用来确保规范不变量是集合在抽象和应用上的分布性的规则集。致谢A.米克尔建议作者阅读[14]。这是工作的起点。H. Cirstea对该论文的以前版本进行了深入的反馈。这很有用。我们还要感谢L. Vaux和C.基什内尔的有益的互动和评论这项工作。NBBG. Faure/Electronic Notes in Theoretical Computer Science 171（2007）319引用[1] ASF+SDF。基于组件的语言开发环境。http://www.cwi.nl/projects/MetaEnv/网站。[2] H.巴伦德雷Lambda演算，它的语法和语义。 逻辑与数学基础研究。Elsevier Science Publishers B. V.（北荷兰），阿姆斯特丹，1984年。第二版。[3] G.巴特，H。奇尔斯泰阿角Kirchner和L.利口酒纯模式类型系统。程序设计语言的原则-POPL 2003，新奥尔良，美国。ACM，2003年1月。[4] P. Borovansky'，C. Kirchner，H. Kirchner，P. -E. 莫雷奥和C。 Ringe is e n. ELAN的一个新版本。In卷15。ENTCS，1998年9月。[5] G.布多 （严格）并行函数的Lambda演算。 Inf. Comput，108（1），1994年1月。[6] H. 是的。 Calculdereecriture：fondementsetappl i cations。 PhDthes is，Univer s ite HenriPoincare-NancyI，2000.十月二十五日。[7] H. Cirstea和C.基什内尔重写演算-第一部分和第二部分。 Logic Journal of the Interest Group in Pure andApplied Logics，9（3）：427[8] H.奇尔斯泰阿角Kirchner和L.利口酒匹配功率。 在RTA'2001会议录Springer-Verlag，2001年5月。[9] H.西斯泰亚湖Liquori和B.变态用定点重写微积分：无类型和一阶系统。第3085卷。Springer，2003年。[10] M. Dezani-Ciancaglini，U. de'Liguoro和A.你好并行和非确定性微积分的滤波器模型。计算机科学的数学基础1993，第18届国际研讨会，第711卷lncs，1993年。[11] 伊兰 ELAN系统： http://elan.loria.fr/。[12] G. Faure和A.米克尔面向rho演算的指称语义学。 技术报告，LORIA，2005年。[13] M. 费南德斯岛 M ackie， anddF. -R. 没有。 Interactionnetsvs. 该ho-calculus ： 在双语法网络中。在EXPRESS'05会议录中Elsevier，2005年。[14] T. Herhard和L.瑞纳 微积分。 理论计算机科学，309，2003。[15] C.是的。 N ORM I ZEDR RR RI I NG ：AALTER NATRri N G D R R RI NGDUAS E QUATIN S。JournalSymb. Comput，21（3），1996.[16] 莫德Maude系统： http://maude.cs.uiuc.edu/。[17] Mod.Modulogic主页。 http://modulogic.inria.fr。[18] V. 请说。 CoC p o r l e d opeelope me ntd e logicie lscr i c i e e d o n e d o n e e d o n e d o n e e d o n e d on e e d o n e d o n e e d o n e e d o n e d o n e e d o n e e d o n e d o n e e d o n e d o n e e