无限范式：从项重写到项图重写的提升方法

电梯理论计算机科学电子笔记72（2007）17-29www.elsevier.com/locate/entcs从项重写到项图重写的提升无穷范式定义Stefan Blom1CWI荷兰阿姆斯特丹摘要无限范式是一种为非终止重写系统提供语义的方法。这个概念是一个通 用 的一个lizai onheBéohmreenh einhelambdacalcuuus。我首先在[2]中引入了一个方法，来为具有letrec项的lambda演算提供一个新的算法。 在那篇论文中，无限范式是直接在图重写系统上定义的。在[5]中，该框架通过使用术语的无限范式定义术语图的无限范式来改进。这种提升定义的方法使得由替换规则引入到术语图重写中的不连续问题更容易处理。在本文中，我们对后一种方法进行了简化介绍。我写的是： Termrewriting，normalform，termgrahrewriting，Bh？mree，lambdaclcu ulus1引言一种表示术语图的简单方法是使用letrec语法。通过使用这种语法，我们可以从术语重写系统导出术语图重写系统。例如，从lambda演算中的β规则（λx. M）N−→βM[x：=N]，我们可以推导（λx. M）N−−β→β letrecx=NinM;（一）letrecx=M，DinC[x]−−e→sletrecx=M，DinC[M];（letrecDinM）N−−→letrecDin（MN）.(See[4]详细了解这个重写系统是如何推导出来的。我们将把这些导出系统称为循环扩张。1 电子邮件地址：sccblom@cwi.nl1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2002.09.00318S. Blom/Electronic Notes in Theoretical Computer Science 72（2007）17是Bo？hmtre和L？evy-Longt re是lambda演算的一个不确定性。很容易将这些树的理论扩展到上面给出在[3]中，这些概念被推广到无穷大的概念中，并以两个更复杂的离散元为例研究了它们和L′evy-Longotres这些例子被证明是相当复杂的，因为每个循环扩张都包括替换规则的形式letrecx=M，DinC[x]−−e→s letrecx=M，DinC[M];letrecx=M，y=C[x]， DinN−→letrecx=M，y=C[M]，DinN;letrecx=C[x]， DinN−−c→s letrecx=C[C[x]]， DinN.问题是，有了这三条规则，重写系统就不再连贯了。经典的例子是：letrecx=F（x）inxletrecx=F（x）inF（x）CS CSletrecx=F（F（x））inxletrecx=F（F（x））inF（x）底部的两个项没有共同的约简。（左项的每个约简都有偶数个F符号，右项的每个约简都有奇数个F符号。这种不一致性导致了许多技术问题。不幸的是，在[2，3]中定义无限规范形式的方式意味着对于每一个定义的不同的无限规范形式，我们都必须处理这些问题。在[5]中，给出了一个改进的框架，其中与替换相关的问题与重写系统相关的问题分离这种分离是通过将项图的无限范式与项图的展开的无限范式相关联来实现的。分离的代价是我们必须假设一个图的无限标准形是该图展开的无限标准形。在建模编程语言的上下文中，这意味着letrec不能用于建模共享敏感的副作用，如赋值。然而，可以首先在非递归设置中对共享敏感侧集进行建模，然后使用letrec添加递归。概况. 在完成这些步骤之后，我们将定义无限规范形式的概念。在下一节中，我们将重写关系和无限范式从项扩展到图。使用这些扩展，我们然后确定一类术语图重写系统，我们定义了从术语到术语图的无限范式的扩展2个房间项T的集合由下式给出不 * *= x| λx。不 | F（T，···，T），S. Blom/Electronic Notes in Theoretical Computer Science 72（2007）1719其中x的范围是一组变量，F的范围是一组函数符号，包括常数Ω和二进制符号@。我们把@（s，t）写成st。组合归约系统（参见[8]）是在具有单个绑定算子的项上定义的，所以每当我们提到关于项的重写系统时，人们可能会想到CRS。我们定义项上的偏序≤Ω为最小传递、自反、相容关系，使得Ωs∈T ：Ω ≤Ωs。 也就是说，项s小于项 t如果s可以通过用Ω替换子项从t获得我们定义集合S的向下闭包为：↓S ={s∈T|sJ∈S：s≤ΩsJ}。可能无穷项的集合T∞是（T，≤Ω）的理想完备化也就是说，项S∈T∞是T的子集，使得S = ↓S和S，t∈S：<$u∈S：s≤Ωu<$t≤Ωu .项的集合通过映射被嵌入到无限项的集合中s→ ↓{ s}。我们将循环项T的集合定义为：T：：= x| λx。T|F（T，···，T）|letrecDinT;D ：：= x1= T，···，xn= T。给定一个新的系统m（T，−→），我们不需要由−→y−→k， 由− → k，由−→k和由−→k，由−→k，我们是一个很好的人，如果我们不这样做，s，sJ， t：s−→t并非所有CRS都是单调的。例如，如果我们有λ计算的η-规则，我们就有λx。（Ωy）x−→ηΩy，但λx。（xy）xcntainon-redex. 问题是η-规则要求变量不出现在子项中。通过展开Ω，我们引入了一个破坏redex的变量的出现因此，为了获得单调性，我们需要重写规则，其中不使用非发生要求。这样的重写规则在[7]中被称为完全扩展。3无限正规形式在本节中，我们给出无限规范形式的概念的简单介绍。该方法是对L'evy的Béohm重新定义的定义的一种最佳方法（See[9]）。无限规范形式概念的第一个版本在[2，3]中给出。该理论在[5]中得到了推广。在这些论文中，理论上提出的抽象减少系统的水平。为了简单起见，我们将我们的介绍限制在[5]中理论的一个子集上，并且我们在lambda项的水平上介绍理论无限范式概念背后的思想是，无限计算的结果是一个无限项，它是在计算过程中逐段构建的。对于一个简单的例子，我们证明了f（λx.λy. y（xx））（λx.λy. y（xx））是20S. Blom/Electronic Notes in Theoretical Computer Science 72（2007）17在下列项的简化中项的粗体部分的限制：（λx.λy.y（x x））（λx.λy.y（x x））−→βλy。y（（λx.λy. y（xx））（λx.λy. y（xx）−→βλy。yλy。y（（λx.λy. y（xx））（λx.λy. y（xx）.λy.y λy.y λy.y（···）如果可能进行多个计算，则收集所有可能约简的结果形式化概念的关键是近似函数。这个函数计算一个项的信息内容，它是已经计算的最终无限项的前缀。一个项的无穷范式被定义为所有前缀的集合，这些前缀可以通过减少项来计算唯一性是无限范式的一个重要性质：它指出任何两个可转换项具有相同的无限范式。uniform意味着如果一个项被约简，那么任何可以从一个项中计算出来的前缀也可以从约简中计算出来。形式上：定义3. 1设Tx∈{T，T∞，T∞}且设y∈m（Tx，−→），我们证明函数ω：Tx→ T∞是逼近函数，如果s，t∈Tx：s−→t=<$ω（s）<$ω（t）.给定一个逼近函数ω：Tx→ T∞，我们定义了无限规范形一个术语为：−→在fω（s）=<${ω（t）|s−→t}。我们说，在有限正规形式是唯一的，如果s：Infω（s）∈T∞andnds，t：s<$−→t：Infω（s）=Infω（t）.有时候，当相关性较弱时，会出现较明显的上升趋势。由于项（≤Ω）和集合（Ω）的自然序，我们可以讨论逼近函数的单调性和无限规范形。示例3.2预处理，其中对于Bo？hmTree而言，它是一种非常规形式。因此，我们必须确定Bo？mTreeinforatontetofatem如：⎧<$λx1···xn.x ωBT（s1）···ωBT（sm），如果s<$λx1···xn.x s1···smωBT（s）=Ω，否则为了证明这个函数是一个近似函数，我们使用了ωBT（s）是s的标准形式的事实，关于以下重写规则：（ λx. M ） N−−ω−B−→TΩ;λx. Ω−−ω−B−→TΩ;ΩM−−ω−B−→TΩ。S. Blom/Electronic Notes in Theoretical Computer Science 72（2007）1721≡Weal sodefine−−→Ω 通过<$M∈T：Ω−−→ΩM。不等于M≤ΩNi，如果M−−→Ω→N。通过一个简单的案例区分，我们可以证明以下图表成立：ΩωBTωBTΩ从这个微分方程和这一事实来看，有一个t−−ω−B−→T−→Ω，我们可以得出，有一个tωBT是不可能的，它要求to≤Ω。 IfC[（λx. M）N]−→βC[M[x：=N]]thenC[（λx. M）N]−−ω−B−→TC[Ω]。因此，我们有Ω BT（C [（λx.M）N]）= Ω BT（C[Ω]）≤ΩΩ BT（C [M [x：= N]]）。结论是ΩBT是一个逼近函数。下面的定理正式陈述了三个重要的事实：连续性意味着无限规范形式的唯一性，近似函数的单调性和重写关系意味着无限规范形式的单调性，如果无限规范形式是唯一的，那么它们是有限项的：在3.3节中，给定Tx∈{T，T∞，T∞}， R∞（Tx，−→）是一个近似函数ω。(i) 如果R是连续的，则有限正规形式中的Inf ω是唯一的。(ii) If−→anddωaremonotonicthenInfωismonotonic.(iii) 如果Infω有限正规形是唯一的，则λs∈Tx： Inf ω（s）∈ T∞.证据(i) Givens<$−→tanda∈Infω （ s ） .我 们 可 以 找 到 dsJ ， suchthats−→sJandda∈ω（sJ）。通过计算，我们可以找到tJ，因此thatsJ−→sjandt−→tJ。 由于ω是一个近似函数，我们有ω（sJ）<$ω（tJ）。因此，我们有：a∈ω（sJ）<$ω（tJ）<$Inf ω（t）。(ii) Givens≤Ωtanda∈Infω （ s ） .我 们 可 以 找 到 dsJ ， suchthats−→sJandda∈ω（sJ）。如果f−→wecn finddtJ，则uchthatt−→tJanddsJ≤ΩtJ。 由于ω的单调性，我们有ω（SJ）<$ω（TJ）。因此，我们有：a∈ω（sJ）<$ω（tJ）<$Inf ω（t）。(iii) 对于任何项λs∈Tx，我们必须证明集合Infω（s）是理想：• Givena∈Inf ω（s）andAJ≤Ωa. Wecandt，suchthats−→tanda∈ω（t）。因为ω（t）根据定义是向下封闭的，我们有一个J∈ ω（t），因此有一个J∈ Infω（s）。• Givena1，a2∈Infω（s），wecandt，suchthats−→tanda1∈ω（t）. Becauseof在fω（s）=Infω（t）中，我们可以找到tJ，suchtht−→tJanda2∈ω（tJ）。≡22S. Blom/Electronic Notes in Theoretical Computer Science 72（2007）17esesUNW因为ω是一个近似函数，我们也有a1∈ω（tJ）。因为ω（tJ），我们可以找到a3∈ω（tJ），使得a1≤Ωa3<$a2≤Ωa3。 我们还知道a3∈Infω（s）。Q唯一性和单调性都用于无限规范形式从项到图的扩展。如果所有这些性质都成立，那么我们讨论一个近似的正则重写系统：定义3.4具有近似的正则重写系统（RRSA）是一个结构（T，−→，ω），其中re（T，−→）是一个正则系统，−→是一个单调的近似函数，使得Inf ω是唯一的和单调的。在无穷项和项图的无穷范式的发展过程中，并非所有这些性质都是需要的，但是拥有所有这些性质可以简化表示。下面，我们将项图的展开定义为项图系统m（T，−−→）的无限标准形式。由于在此基础上，我们使用不同的符号表示无限范式：定义3. [5]给出这个系统m（T，−−→）。 LetnfωM关于重写规则的正规形UNW （M）表示letrecx1=M1，·· ·，xn=MninM−−ω−u−n→w M[x1：=Ω，·· ·，xn：=Ω]函数ωunw：T→ T∞定义为ωunw（M）= ↓ {nf ω（M）}。项M的展开由下式给出：−−e→sUnw（M）= Inf ωunw（M）。我们使用M=unwN作为Unw（M）= Unw（N）的简写。很容易用一个简单的函数来验证它。Because−−e→s 这是一种通过应用Thm来证明Unw是唯一的无限规范形式的方法。三点三4无限延伸研究无限重写的动机之一是通过无限重写给出图重写为此，Corradini定义了一个无限项的重写系统，该系统在一个步骤中完成了无限集合的完整开发[6]。我们使用他的定义的自由扩展来表达我们可以将无限范式定义从项重写扩展到图重写的要求。我们的扩展将任何重写关系从项提升到无限项，通过声明S重写为T，如果S中的每一项都可以扩展为S中的另一项，这反过来重写为T中的一项。此外，T中的每一项都是T中一项的前缀，这可以通过重写S中的一项来获得。Corradini形式上：S. Blom/Electronic Notes in Theoretical Computer Science 72（2007）1723ω定义4.1重写扩展算子[·T：2T×T→ 2T∞×T∞由下式给出：S，T∈T∞，→S[→−T⎧S∈S：⎩∧ ∀t∈T: ∃sJ∈S, tJ∈T:sJ→tJ∧t≤ΩtJ[·]的传递自反闭包是[·]。请注意，如果一个S重写到T的一个命题4.2给定S，T∈T∞，→ T×T，一个指标集I和si，ti∈T使得si→ti，其中i∈ I。S = ↓ {s i|i∈I}且T = ↓ {t i|i∈I}=<$S[→ <$T.这个简单的观察对于证明一个无穷项重写为另一个无穷项非常有用。下面的示例说明了[·]运算符的几种可能性：例4.3让我们考虑TRSA（X）−→X B（X）−→X。我们使用以下符号：A0（x）=x;B0（x）=x;AB0（x）=x;An+1（x）=A（An（x））;Bn+1（x）=B（Bn（x））;ABn+1（x）=A（B（ABn（x）;A ω={A n|n ∈ N};B ω={B n|n ∈ N};AB ω= ↓{AB n|n∈ N}。然后我们有：A（B（ABω））[−→A（ABω），becauseA（B（ABn（Ω））−→A（ABn（Ω））;ABω[−→<$Aω，b∈ABn（Ω）−→An（Ω）;Aω[−]→AΩ，可以用An（Ω）−→Ω来表示;ABω[−→ <$Bω[−→ <$Ω。我们可能会讨论在− →i的情况下执行[−→i]的情况下执行[−→i]的问题。答案是否定的，我们必须施加一些限制。例如，使用并发规则我们两样都A（A（X））−→2XAω[−→<$ΩanddAω[−→<$A（Ω）.2 2[·]运算符将重写关系从项扩展到无限项。如果在项上，我们定义了无穷规范形式Infω，那么我们也想将无穷规范形式扩展到无穷项。最简单的方法是扩展函数Infω。因为无穷项是项的集合，而Infω的余域已经是项的集合，所以我们只扩展域：第四章. 4Givena RR SA（T，−→，ω），Inf ω的直接外延定义如下：Inf ∞（S）=<${Inf ω（s）|s∈S}。24S. Blom/Electronic Notes in Theoretical Computer Science 72（2007）17ωωωω直接延拓是一个真延拓，因为对于有限项Infω和Inf∞，得到相同的结果：支持4. 5给定RRSA（T，−→，ω），我们有：t∈T ：Inf ω（t）= Inf ∞（↓ {t}）。证据 我们区分两种情况：“”： 从t∈↓ {t}这一事实得出。”⊇”:Inf ω（s）<$Inf ω（t）。因此，我们有，Inf ∞（↓ {t}）<$Inf ω（t）。Q直接延伸在以下意义上也是独特的：支持4. 6给定RRSA（T，−→，ω），我们有：<$S，T∈T∞：S[−→ <$T=<$Inf∞（S）=Inf∞（T）.ω ω证据 我们区分两种情况：““：GI V E N S ∈ S，W E C A N F N D S J ∈ S，T J ∈ T，S U C H T H A T S ≤ S J AND D SJ − → T J。分别通过单调性和唯一性，我们可以得到Inf ω（s）<$Inf ω（sJ）和Inf ω（sJ）= Inf ω（tJ）。从这两个陈述和Inf∞的定义中，我们可以得出：Inf ∞（S）<$Inf ∞（T）.ω ω“”： 类似于前一个案例。Q虽然直接扩张具有正确的性质（见前两个命题），但它并不令人满意，因为它不是通过近似函数来定义的。然而，我们需要它来证明无穷项的逼近函数（我们将在下面定义）产生唯一的无穷规范形式。第四章. 7Gi vena RR SA（T，−→，ω），我们定义了Inf ω的扩展其中hrespecto=TxTas：ω∞（S）= ↓ {ω（s）|s∈ S}=在f ω∞中（S）={ω∞（T）|S，S，S，S我们要证明直接扩张等于导出扩张。要做到这一点，我们需要将有条件的削减提升为无条件的削减。这对于单调归约关系是可能的：引理4.8给定重写系统（T，→）。 如果→是单调的，则s，t∈T，S∈T∞：s→ts∈S = T∈T∞：S[→ TT∈T.S. Blom/Electronic Notes in Theoretical Computer Science 72（2007）1725nnnωω证据给定s，t∈T，S∈T∞，使得s→t且s∈S。因为S是可数集和理想，我们可以找到一个序列s≠s0≤Ωs1≤Ω···，使得S = ↓{s i|i≥ 0}。因为→是单调的，我们可以找到一个序列ti，使得si→ti且ti≤Ωti+1。然后我们有S [→ ↓{t i|i≥ 0}。Q有了这个引理，我们可以证明两个扩张的相等性：给定RRSA（T，−→，ω），我们有在f∞（S）=Inf−→（S）中，S ∈ T ∞。ωω∞证据 我们区分两种情况：−→““：Gi v e n a ∈ In f ω ∞（S）. 根据Def。四、7我们发现了一个问题S<$S0[−→<$S1[−→ <$· ·Sn，suchthat<$sn∈Sn：a∈ω（sn）.从a∈ω（sn）我们得到a∈Infω（sn）. 通过使用def。4.1我们可以找到sn−1∈Sn−1，sJ∈Sn，使得Sn≤ΩSJ和SJ←−−sn−1. 我不知道并且唯一性我们有Infω（sn）<$Infω（sJ）和Infω（sJ）= Infω（sn−1），所以n nInfω（sn）<$Infω（sn−1）.通过重复这个论证，我们可以发现s0∈S0，使得Infω（sn）<$Infω（s0）. 我们的结论是a∈Inf ω（s n）<$Inf ω（s0）<$Inf ∞（S0）.“"：给定a ∈ Inf ∞（S）。我们可以找到一个s∈S使得a∈Inf ω（s）。因此，wecndt∈T，suchthats−→tanda∈ω（t）。 ByrepeaplyingLemma 4. 8，我们可以找到T∈T∞，因此th tt∈T和S[→−ttt]。因为我们有[→−[−→nda∈ω（t）<$ω∞（T），−→a∈Infω∞（S）.Q这个定理的一个非常简单的推论是，导出的有限规范形式是唯一的。−→Corollary4.10给定RRSA（T，−→，ω），我们在fω∞中有 无限正态形式是独一无二的。5循环扩展项重写系统的循环扩展只不过是从项重写系统导出的循环项重写系统。就本文而言，如何推导并不重要。只有派生的属性才重要。最重要的性质是无穷可靠性，它说循环项的任何约简都可以被投影为项的解绕的约简：26S. Blom/Electronic Notes in Theoretical Computer Science 72（2007）17RRR第五章. [1]一个新的系统结构（T，−−→）的循环扩展结构（T，−−→T）是一个新的结构，如果，R RM，N：M−−R−→ N=<$Unw（M）[−−→R→ <$Unw（N）.导出循环扩展的一种方法是从修改给定重写规则的右侧开始接下来，可以添加不修改展开的重写规则。最后，必须完成一些工作。在引言（1）中，lambda演算的简单循环扩展就是以这种方式导出的。如果正交CRS的循环扩张是以这种方式导出的，那么在[5]中证明的以下定理可能有助于证明无穷可靠性：定理5.2G给出了一个N-正交的CRS（T，−−→R）在R（T，−−→R）上的循环扩张. 如果f−−R−→R −=unw（=unw−→R=unw），则第n个循环的扩展是有限的声音。通过对循环项的展开，我们可以给出无限规范形式从项到循环项的直接推广：第五章. 3Gi vena RR SA（T，−−→，ω）andda cyclicextension（T，−−→ω），weR R定义Infω的直接扩张为Inf ∞（M）= Inf ∞（Unw（M））。ω ω这种扩展在以下意义上是独特的：第五点。4给定一个RRSA（T，−−→R，ω）和一个无限大的循环扩展（T，−−→R，ω），我们有R<$M，N∈T<$：M−→N=<$Inf<$（M）=In f<$（N）.证据 ”（《礼记·礼记·礼记·礼记》）四点六Q派生扩展也是可能的：第五章. 5给出一个RR SA（T，−−→R，ω）和一个基本上是一个循环的函数（T，−− → R，ω），函数ω的扩展由一个Pproximationfio n定义。ω（M）= ↓ {ω（s）|s∈ Unw（M）}.为了证明导出扩张等于直接扩张，因此是唯一的，我们需要一个完备性的概念。完美的情况是，如果循环项M的解旋的近似s重写为项t，则M重写为循环项N，使得t是N的解旋的近似。然而，我们不能期望这一点，因为循环项上的重写步骤通常对应于近似的多个步骤。 完整性问题在[5]中进行了深入讨论。在本文中，我们只是提出了解决方案。第五章. 6Gi vena RR SA（T，−−→，ω）. 一个环的外环sion（T，−→T）是一个有限的环，直到信息内容，如果s，t∈RT、MR∈T：s∈Unw（M）<$s−−→t=<$$>N∈T<$，tJ∈Unw（N）：M−→N<$ω（t）<$ω（tJ）.RRS. Blom/Electronic Notes in Theoretical Computer Science 72（2007）1727RωωRR我们可以通过用t − − → t j代替ω（t）<$ω（tJ）来加强完备性的概念。这一弱的概念足以暗示导出的和直接的无限元正常的形式是一样的。第五章. 7Gi vena RR SA（T，−−→，ω）. 一个环的外环s∈n（T∈，−→T∈）是一个环R R如果它是完全健全和完整的信息内容。给出了一个RRSAR（T，−−→，ω）和一个环的扩张（T，−−→ω），），我们有R R<$M∈T<$：Infω<$（M）=Inf<$（M）.证据 我们区分两种情况：““：FrominitarysoundnessitfollwshatInfω（M）Infω∞（Unw（M））. 因此，由Thm。4.9因此，Infω<$（M）<$Inf<$（M）.“”： 给定a∈ Inf <$（M）.通过定义，Inf ∞（M）= Inf ∞（Unw（M））= Inf（s）|ω ω ωs∈Unw（M）}，所以我们可以找到s∈Unw（M）使得a∈Infω（s）。 因此，我们可以alsofinedt∈Tsu c hthats−−→R→tanda∈ω（t）. 如果您有任何问题，我们可以找到anN∈T，tJ∈Unw（N）suchthatM−−→M N和dω（t）<$ω（tJ）。他说：a∈ω（t）<$ω（tJ）<$ω<$（N）<$Infω<$（M）.Q导出的无限规范形式的唯一性是这个定理的一个简单的推论。第五章. 9给定一个RRSAR（T，−−→R，ω）和一个r循环扩张（T，−→T），我们有一个唯一的有限正规形式。5.1句法的连续性和一致性关系。本节简要介绍如何将同余结果从项重写提升到循环项重写。由于篇幅所限，这里无法提供他们可以在[5]中找到用句法连续性的概念来证明Inf（M）=Inf（N）=Inf（C[M]）=Inf（C[N]）L′语法连续性表示，为了计算填充了一个项的上下文的无限范式，你需要知道的关于该项的一切都包含在该项的无限范式定义5.10Givenarewri tesystem（T，−−→R）anddanapproximationfunctionω：T → T∞，我们有Inf ω的句法连续性，如果Inf ω（C [s]）={Inf ω（C [a]）|a∈ Inf ω（s）}。为了将同余结果从项扩展到循环项，我们还需要替换连续性的概念，它表示计算无限法线28S. Blom/Electronic Notes in Theoretical Computer Science 72（2007）17作为应用于一个术语的替换形式，你需要知道的关于该术语的一切都包含在该术语的无限范式中：定义5.11Givenarewri teystem（T，−−→R）anddanapproximationfunctionω：T → T∞，我们有Inf ω的替代连续性，如果Inf ω（sσ）=<${Inf ω（aσ）|a∈ Inf ω（s）}。注意，如果β规则存在，替换连续性立即从句法连续性中得出，因为Infω（s[x1：=t1，···，xn：=tn]）= Infω（C[s]），其中C∈（λx1···xn. Q）t1···t n.给定一个合适的CRS的替换连续性和句法连续性，我们可以证明任何正则循环扩张都具有句法连续性：OREM5. 12给定一个RRSA（T，−−→R，ω），其中R（T，−−→R）是一个全延拓的二阶CRS，且R（T，−−→R）是一个环，我们有一个新的结构，RInf ω替换连续性隐含着Inf ω的句法连续性。6结论我们已经提出了一个框架，用于将有限范式定义从术语重写系统提升到术语图重写系统。文[1]中证明无穷正规形唯一性时必须处理的非连续性问题，现在在无穷可靠性的证明中处理。其优点是，在无限可靠性的证明中，我们可以使用关于重写规则的已知结果，这些规则保持了项的展开。该框架并没有取代斜连续性的概念（[1]）。这个概念仍然是有用的，以证明结果重写规则，保持一项的展开。致谢我们感谢Vincent van Oostrom对组合归约系统的帮助，以及Jaco van de Pol对本文的校对引用[1] Abadi，M.和T. Ito，编辑，[2] Ariola，Z. M.和S. Blom，Cyclic lambda calculi，in：Abadi and Ito [1]，pp. 77比106[3] Ariola，Z. M.和S. Blom，Skew concilience and the lambda calculus with letrec，Annals of Pure andApplied Logic 117（2002），pp. 95比168URLhttp://www.sciencedirect.com/science/article/B6TYB-45V6X48-3/1/44088914c39bfba322cebd6e8cf7ffae[4] Ariola，Z. M.和J. W. Klop，Lambda演算与显式递归，信息与计算139（1997），pp. 154-233。[5] Blom，S.， 论文，阿姆斯特丹自由大学[6] Corradini，A.，计算机科学中的术语重写，见：1993年CAAP学报（1993），pp. 468-484.S. Blom/Electronic Notes in Theoretical Computer Science 72（2007）1729[7] Hanus，M.和C. Prehofer，Higher-order narrowing with definitional trees，in：H. Ganzinger，编辑，RTA，Lecture Notes in Computer Science 1103（1996），pp. 138-152[8] Klop，J.W.，V. van Oostrom和F. van Raamsdonk，Combinatory Reduction Systems：Introductionand Survey，Theoretical Computer Science 121（1993），pp.279C orradoBéoh在他70岁的时候出现过，我想是的。 M. Dezani-Ciancaglini，S.RonchiDella Rocca和M.Venturini-Zilli。[9] 莱维，J。-J. ，“R e duc t i o n s C o r e c t e s et t O p t i m a l e s d a n s l e L a m b d a - C a l c u l，”Ph. D.这位姐姐，《联合国宪章七》（1978年）。