OBJ语言中的正确和完整的策略注释方法分析

70理论计算机科学电子笔记71（2003）网址：http://www.elsevier.nl/locate/entcs/volume71.html20页OBJ*的正确和完整（积极）策略注释Mar 'ıa Alpuente1，Santiago Escobar2，Salvador Lucas3DSIC，波兰理工大学，西班牙。摘要策略注释在几种基于重写的编程语言中用于引入替换限制，旨在提高效率和/或降低不终止的风险。不幸的是，重写限制可能会对计算范式的能力产生负面影响。在本文中，我们首先确定/澄清确保使用策略注释的计算的正确性和完整性（关于规范化）的条件。然后，我们定义了一种程序转换方法，用于（正确和）完整的评估，适用于OBJ类语言。关键词： 声明式编程、OBJ、策略注释。1介绍策略注释用于OBJ语言家族4（OBJ2[6]，OBJ3[8]、CafeOBJ[7]和Maude[3]）以避免非终止（[8]，第2.4.4）。示例1.1以下OBJ程序：obj EXAMPLE issorted Nat LNat.op0：-> Nat.ops：Nat -> Nat [strat（1）]. opnil ：-> LNat.opcons：Nat LNat -> LNat [strat（1）].*工作部分得到CICYT TIC 2001 -2705-C 03 -01、Acciones Integradas HI 2000- 0161、HA2001-0059、HU 2001-0019和Generalitat Valenciana GV 01 -424的支持。1电子邮件地址：alpuente@dsic.upv.es2电子邮件地址：sescobar@dsic.upv.es3电子邮件地址：slucas@dsic.upv.es[4]在[8]中，OBJ指的是OBJ2、OBJ3、CafeOBJ或Maude。2003年3月，出版社dbyElsevierScienceB。 V. 操作访问和C CB Y-NC-N D链接。ALPUENTE ESCOBAR和LUCAS71∈P×TF {}XFX T FX{} F→F··X操作来自：Nat -> LNat [strat（1 0）]。opsel：Nat LNat-> Nat [strat（1 2 0）].op first：Nat LNat-> LNat [strat（1 2 0）]。vars X Y：Nat.var Z：LNat.等式sel（s（X），cons（Y，Z））= sel（X，Z）。等式sel（0，cons（X，Z））= X。eq first（0，Z）= nil.eq first（s（X），cons（Y，Z））= cons（Y，first（X，Z））。eq from（X）=cons（X，from（s（X）。Endo为列表构造函数cons指定一个显式的策略注释，该注释禁止第二个参数的替换。通过这种方式，我们可以确保使用该程序的计算是终止的（参见下面的示例4.4以获得该声明的正式证明策略注释下重写的终止已经在许多论文中进行了研究[5，13，14]。不幸的是，使用重写限制可能导致不完整性，即，输入表达式的标准形式可能无法通过受限的计算达到。例如，使用示例中的程序1.1 我们不能计算对应于first（s（0），from（0））的求值的整数列表。如下所示，这个表达式的求值停止产生cons（0，first（0，from（s（0）项。 另一方面，从用户我们表明，这些问题可以通过使用一个程序transfor- mation解决，而我们仍然能够保持终止的计算。2预赛给定一个集合A，（A）表示A的所有子集的集合。设R A A是关于A的二元关系。设R=为R的自回归闭包，R+为R的过渡闭包，R =为R的自回归和过渡闭包.An元素a A是R-正规形式，如果不存在b使得a R b;NFR是R-正规形集[1]。 我们说b是a的R-正规形式（记为a R！b），如果b是R-正规形且R≠b. 我们说R是终止的i.不存在无穷序列a1R a2R a3 。在本文中，表示可数变量集，表示函数符号集f，g，.. 。每 个 人都 有一个固定的arity， 由函数ar：N给出。我们表示由以下项构建的项集： 和 通过 （ 、 ）. 上下文C[]是来自（你好，），其中，是新的常量符号。如果一个变量没有多次出现，则称该项是线性的。术语通常被看作是有标签的树。 位置p，q，. 表示为ALPUENTE ESCOBAR和LUCAS72|p{|∈}P公司简介⊆±±F± ∈FpR→RRRRµµµ用于处理t的子项的正自然数链。通过Λ，我们表示空链（指项的根）。给定位置p，q，我们用p.q表示它的级联。 如果p是一个位置，Q是一个位置集合，p.Q是集合p.q q Q。 由os（t），我们表示项t的位置的集合。 t中不可变符号的位置表示为PosF（t）和PosX（t）是变量出现。t的位置p处的子项被表示为tp，并且t[s]p是项t，其中位置p处的子项被s替换。标记t的根的符号表示为root（t），root（t，p）是root（t|p）。置换是映射σ：X → T（F，X）同态扩张到映射σ：T（F，X）→ T（F，X）。重写规则是一个有序对（l，r），记为l → r，其中l，r ∈ T（F，X），l/∈ X且Var （r）<$Var （l）。规则的左边（lhs）是l，右边（rhs）是r。TRS是一对R=（F，R），其中R是一组重写规则。L（R）表示R的lhsR是左线性的，如果L（R）是线性项的集合。 给定R =（F，R），我们认为F是符号c ∈ C（称为构造函数）和符号f ∈ D（称为定义函数）的不相交并集F = C D，其中D ={f|f（l1，.，lk）→r∈R}和C =F− D。然后，）是构造函数项的集合。 让osD（t）（resp.C（t）是定义的位置的集合（分别为）。constructor）术语t的符号。lhsl∈L（R）的一个实例σ（l）是一个redex。一项t∈ T（F，X）改写为s(at位置p），写作t→Rs（或仅t→s），如果t|p= σ（l）和s = t [σ（r）] p，对某些l→r∈R，p∈Pos（t）和代换σ.如果一个项是→-范式，则它是范式。设NFR是R的正规形的集合。如果一个项t不能重写为一个redex，则它是一个头标准形式。设HNFR是R的头正规形的集合。如果→正在终止，则TRS正在终止。3带句法替换限制的一个映射μ：F→ P（N）是一个替换映射（或F-映射），如果μ（f）≥{1，.，[9]对于所有的f∈ F，P（N）上的包含序推广到一个在MF上，所有- 地图：µμJif for allf、 µ（f）µJ（f）. 这样，µ µJ意味着µ比µJ考虑更少的位置进行缩减。我们也说，μ比μJ更严格（或同样严格）。给定一个TRSR=（F，R），我们写MR而不是MF。t ∈ T（F，X）的μ-替换位置Pos（t）的集合为：Pos（t）={Λ}如果t∈ X，且Posµ（t）={Λ} μi∈µ（root（t））i.Posµ（t|i）如果t/∈ X. 在上下文中-敏感重写（CSR[9]），我们（只）重写替换赎回：t µ-rewritesµ若t→Rs且p∈ Pos（t），则为s（记为t <$→µs<$→µ-正规形式被称为微范式。NFR是的μ-正规形式的集合，。该µ-范式包括所有的范式(but反之亦然）。 的TRS如果终止，则终止规范置换映射μcan是最严格的置换映射，它确保了R规则左侧的不可变子项被置换。注意，µ可以ALPUENTE ESCOBAR和LUCAS73RR--∈ F∈ F∈ X||ϕ很容易从R得到：对于所有f∈ F和i∈{1，...，ar（f）}，i∈ μcan（f） i ∈ PosF（l），p∈PosF（l），（root（l，p）=f∈p.i∈PosF（l））设CMR={μ∈MR|[001 pdf 1st-31files]可以是替换映射的集合，R可以比µ R的限制性更小或与µR的限制性相同。4E-战略k元符号f的（正）局部策略（或E-策略）是从0，1，...， k在括号中给出（见例1.1）。将局部策略f（f）与每个f相关联的映射f称 为 E- 策略映射[19]。代数语言，如OBJ 2、OBJ 3、CafeOBJ和Maude都承认E-策略的具体化。没有显式局部策略的符号被赋予一个默认策略，其具体形状取决于所考虑的语言5。给定一个OBJ程序P，我们（分别）考虑相应的TRS，它由P中的重写规则集和对应于其策略注释的E-策略映射在给定的E-策略映射下，OBJ程序的语义通过映射eval：T（F，X）→ P（T（F，X））（从项到它们的“计算值”集合下面[17，19]我们通过使用一个归约关系→归约在标号项和位置对上设L是所有由自然数组成的列表的集合。 用Ln表示不超过n ∈ N的所有自然数列表的集合。我们使用签名FL={fL|f∈ F <$L∈Lar（f）}和标号变量XL={xnil|x∈X}。将F的一个E-策略映射推广到T（F，X）到T（FL，XL）的一个（标号）映射，如下：如果t=x，则为nil（t）=f，n（tk））ift=f（t1， . 、tk）映射erase：T（FL，XL）→ T（F，X）以明显的方式从符号中删除标记给定一个TRS R =（F，R）和一个E-策略映射F，则二元关系n→ n→nT（FL ，XL ）×Nn+ （ 即 . ， pairst ， poflabelledtermstand positionsp ） is[17，19]：t，p→s，q当且仅当p∈ Pos（t）且(i) root（t，p）=fnil，s=t andp =q.i for somei;或(ii) 不|p= fi：L（t1， . ，tk），其中thi>0，s= t[fL（t1， . ，tk）]p和q=p.i;或r(iii) tp=f0：L（t1， . ，tk），e rase（tp）不是redex，s=t[fL（t1， . ，t，k）]p，q=p;或(iv) 不|p=f0：L（t1，.，tk）=σ（lJ），erase（lJ）=l，s=t[σ（k（r））]p，对于某些l→r∈R和代换σ，q=p.设eval（t）={erase（s）∈ T（F，X）|⟨ϕ (t),Λ⟩ →！ [17，19]. 的TRS[5]例如，在Maude中，与k元符号f相关联的默认局部策略是（1 2···k 0），参见[4]。ALPUENTE ESCOBAR和LUCAS74→ ⟨⟩F∈{∈|/}∈F∈µRRµ如果对所有的t∈ T（F，X），不存在从λλ（t），Λλ开始的无限→ λ-重写序列，则R是λ-终止的。 如果相应的TRS R是终止的，则OBJ程序P是终止的[13]。4.1E-策略与上下文相关重写带有战略注解的重写与企业社会责任密切相关。给定一个E-策略图，我们定义μMF如下：μM（f）=i μ M（f）i= 0对于所有f，其中e L表示项e出现在某处在列表L中。如果没有混淆的话，我们将把上标“”从“µ”中此外，我们还写<$∈CMR，意思是μ<$∈CMR。示例4.1TRSR：sel（0，cons（x，z））→ x sel（s（x），cons（y，z））→sel（x，z）first（0，z）→nil first（s（x），cons（y，z））→cons（y，first（x，z））from（x）→cons（x，from（s（x）以及替换地图µ（s）= µ（cons）= µ（from）={1}和µ（sel）= µ（first）={1，2}对应于例1.1中的OBJ程序。在t，p上发出的每一个降阶步骤对应于在t的未标记版本erase（t）上的一个μm重写步骤（或erase（t）保持不变）。定理4.2 [13]设R是一个TRS，R是一个E-策略映射。 设t ∈T（FL，XL），且p∈Pos（erase（t））是s.t. root（t，p）= fL，对于某个子集x L，（f）. 如果p∈t，p∈ →p∈s，q∈，则q ∈ Posµ（erase（s））且erase（t）<$→= erase（s）。OBJ计划的终止和CSR的终止也是相关的。定理4.3 [13]一个具有E-策略映射的OBJ程序P是可终止的，如果相应的TRS R是可终止的。CSR的终止已经在许多论文中进行了研究，参见[12]，概述了证明CSR终止的不同方法。例4.4考虑例4.1中的和µ。[2]的μ-终止（的超集）在[2]的示例7中演示。因此，根据定理4.3，例1.1中的OBJ程序被终止。5正确性和完整性ALPUENTE ESCOBAR和LUCAS75TRSR =（F，R）的重写语义是映射S：T（F，X）→P（T（F，X））使得对所有的t ∈ T（F，X）和s ∈ S（t），t →s [15]。 注意即，给定TRSR和E-策略图，R是一种重写语义对R.语义S是确定性的（resp. 如果t ∈ T（F，X），|S（t）|≤ 1ALPUENTE ESCOBAR和LUCAS76∈ D∈∈∈ D∈B CRR∈ F-B。注意R（分别）|≥1）。| ≥ 1).一般来说，eval不是决定性的，也没有定义。注意R的n-终止意味着evaln的定义性。在函数式编程中最常考虑的语义是R能够在有限时间内产生的构造器项的集合。重写步骤数（eval（t）={s∈ T（C，X）|t→s}）。其他种类通常被认为是RR例如，所有可能约简的对于一个头正规形（hnf（t）={s ∈ HNFR|t → s}），或正规形式（nf（t）=hnf（t）<$NFR）。 因此，给定语义SR对于R（例如，S∈ {eval，hnf，nf}），R的不同重写语义（例如，eval（）是：正确（w.r.t. S）如果eval（t）<$S（t）对于所有的t∈ T（F，X），并且完成（w.r.t. S）如果，对所有的t∈ T（F，X），S（t）等价于n（t）用OBJ程序计算产生的表达式（通过求值）称为E-范式（ENF）。这些术语通常不是标准形式（即，无赎回权的条款）。因此，不能保证eval的正确性或完整性。nf.事实上，我们有以下几点：定理5.1 [13]设R=（CD，R）是一个TRS，R是一个E-策略映射，使得对所有f，f（f）以0结尾。 如果s evaln（t），则s是t的μ-正规形式。在我们的发展中，要求所有f的f都以0结尾是必不可少的（关于这个要求的相关性的彻底分析，也见[4]因此，如果这个条件成立，我们说E-策略映射是正则的如果策略注释hnf。定理5.2 [13]设R=（CD，R）是左线性TRS，R是正则E-策略映射，使得R ∈ CMR. 如果s evaln（t），则s是一个头范式。如果我们将注意力限制在值的计算上（即，构造器术语），那么CSR就足够强大来计算它们。给定TRSR =（F，R）=（C D，R）且B <$C，我们设μB为μB（c）={1，...，ar（c）}对于所有c∈ B且μB（f）=μcan（f），如果fR RµB∈CMR.定理5.3[9]设R=（F，R）=（CD，R）是左线性TRS，B <$C而M是这样的，即M是这样的，B是± μ。 设t∈ T（F，X），δ∈ T（B，X）.然后，Rt→ δit→µδ。定理5.3在排序的签名中很容易使用（如在OBJ程序中），因为给定一个项t（排序为τ），我们能够建立应该考虑的构造函数的集合（即，排序为τ的构造函数符号）。不幸的是，定理5.3并不直接适用于OBJ计算，因为它们必须遵守策略注释所表达的求值顺序然而，我们有以下几点。[6]这个术语在[20]中使用，含义略有不同ALPUENTE ESCOBAR和LUCAS77R→ ∈ T C X∈F∈D定理5.4设R =（F，R）=（CD，R）是左线性连续TRS，B ∈ C.设R是正则E-策略映射，使得R是R-终止的。设t∈ T（F，X），δ∈ T（B，X）. 如果μB±μB，则t→！ δ i <$δ∈ eval<$（t）.例如，可以使用递归计算每个表达式的值例1.1中OBJ程序中的排序Nat（由于µ{0，s}±µ）。 这是对于LNat类型的表达式不为真R如以下示例所示。例5.5使用例1.1中的程序对排序LNat的表达式t=first（s（0），from（0））得到（我们使用Maude解释器的1.0.5版本7，但其他解释器的行为类似8）：Maude>reduce first（s（0），from（0））.在示例中减少：first（s（0），from（0））。rewrites：2 in-10ms cpu（0ms real）（~rewrites/second）result LNat：cons（0，first（0，from（s（0）请注意，cons（0，first（0，from（s（0）不是范式。然而，tnil（0，nil）（，），即，cons（0，nil）是t的一个值，不能通过Maude解释器获得。OBJ计算w.r.t.的正确性也可以实现NF(i) Nagaya证明，如果f（f）包含所有索引0，1，...，ar（f）对于每个符号f，并且对于定义的符号f，f（f）以0结尾，则eval_t是正确的。 nf（[17]中定理6.1.12）。(ii) Nakamura和Ogata表明，给定一个策略图，如果eval是正确的，w.r.t. hnf，则eval_J是正确的。nf对于任意的f ∈F，由下式给出：nfJ（f）= nf（f）++（i1···in）对于所有的符号f∈ F（其中'++'附加两个列表，并且{ i 1，.，in}={1，.，ar（f）}−µ（f））（[19]中的定理3.2）。例如，例1.1中所给出的公式，相对于t. r.t. hnf（使用定理5.2）。此外，由于例1.1中的OBJ程序是以EAL-终止的，因此定义了eval EAL。因此，对每个项t的求值产生t的头标准形式（即，可以认为是头部正常化）。不幸的是，evalJ不再被定义：头部正常化的行为消失了例5.6考虑例1.1中的程序，其中对于每隔一个符号f，J（cons）=（1 2）和j（f）=（f）（将程序重命名为EXAMPLE-INF）。再次考虑t=first（s（0），from（0））的求值：Maude>reduce first（s（0），from（0））.在EXAMPLE-INF中reduce：first（s（0），from（0））。段违例7可用 在http://maude.csl.sri.com/system/。8.我们使用OBJ3解释器v重现了我们所有的实验2.0（可用）在http://www.kindsoftware.com/products/opensource/obj3/OBJ3/请参阅和咖啡馆OBJALPUENTE ESCOBAR和LUCAS78解释器 诉 1.3.1 （有 在http://www.ipa.go.jp/STC/CafeP/cafe.html）。ALPUENTE ESCOBAR和LUCAS79++R∈ XCCQC∈F×··×→他们问题是t的评估，即，评价J（t）=first（120）（s（1）（0nil），from（10）（0nil））using→bandj不会终止（我们在契约的赎回下加first（120）（s（1）（0nil），from（10）（0nil）），Λ→j first（20）（s（1）（0nil），from（10）（0nil）），1→jfirst（20）（snil（0nil），from（10）（0nil）），1. 1⟩→j first（20）（snil（0nil），from（10）（0nil）），1→j first（20）（snil（0nil），from（10）（0nil）），Λ→J 第一个（0）（snil（0nil），从（10）（0nil）），2→J第一个（0）（snil（0nil），从（0）（0nil）），2。1⟩→Jfirst（0）（snil（0nil），from（0）（0nil）），2→j first（0）（snil（0nil），cons（12）（0nil，from（10）（s（1）（0nil），2→J 首页（0）（s零（0 ），cons（2）（0 ，从（10）（s（1）（0 ），2→jfirst（0）（snil（0nil），consnil（0nil，from（10）（s（1）（0nil），2. 2⟩→J 首页（0）（s零（0 ），consnil（0 ，从（0）（s零（0 ），2. 2⟩→J···Maude解释器将这种因此，R的n-终止（见例4.4）并不能保证eval n-j的定义性，正如Nagaya和Nakamura-Ogata先前的结果所暗示的那样。此外，evalj能够获得evaljJ无法获得的头范式（比较例5.5和5.6中t的计算）。 例5.6还表明，在定理5.4中要求n-终止对于确保正确和完整的求值是必不可少的（注意，例5.6中的5.6满足定理5.4中的所有要求，除了终止）。在下面的部分中，我们提出了一个解决方案来（部分）克服这个问题，它是基于程序转换。6用于完整评估的前一节中的讨论和例子表明，要将实现项t的中心求值所需的替换约束（至少需要μcan，见定理5.2）与约束隔离开来。在构造函数中获取文本C[]∈所需的R对于某些B∈C，T（B ∈{X}，X）（这至少需要sµB，se定理5.4）。在实践中，我们只需要（并且希望）固定排序τR的输入表达式-我们想要评估的结果，以修复假设符号f被 排 序 为 ：f：τ1τkτJ。f的（输出）排序是sort（f）=τJ。 变量x也有一个sort，sort（x）。我们还假设所有项在任何地方都是有序的一个项t的排序是它最外面的符号的排序。 给定一个排序τ，设τ是可以在排序τ的构造函数项中找到的构造函数符号的集合。为例如，CNat={0，s}和CLNat={0，s，nil，cons}。 我们引进一套ALPUENTE ESCOBAR和LUCAS80RRRR∈ C×··× →{}RRR新构造函数符号的CJ：它们被重命名为计算所有参数的原始构造函数c∈ Cτ的版本cJ构造器符号c∈ Cτ的cJ∈ CJ由规则执行引用τJ（c（x1，.， （xk）） →cJ（引用τ1（x1），.， 引用τk（xk））其 中 c ， CJ ： τ1× ··· ×τk→τJ 。 设 Quote 是 包 含 所 有 这 些 符 号 的 集 合 ：Quote={quot eτ J|<$c∈Cτj，sort（c）=τJ}. 项t的评估将通过减少引号排序（t）（t）来进行。所获得的值仅通过使用C j中的符号来构建。 在评估之后，使用未引用的新符号τJ：τ J→τJ来表示重命名。对于一个ch常数b∈Cτε，我们给出了一个规则unquotesort（b）（bJ）→b对于每个Cτk使得c：τ1τkτJ，k >0，且μj（c）=一，K ，我们添加一条规则unquoteτJ（cJ（x1，...，xk））→c（未引用τ1（x1），.，最后，对于每个c∈ Cτ，使得c：τ1× ·· ×τk→τJ，k >0，且µ（c）/={1，.，k}，我们考虑一个新的符号fc：τ1×···× τk→ τ J;我们增加了两个规则unquoteτJ（cJ（x1，...，（xk）） →fc（unquoteτ1（x1），.，（不带引号的τk（xk））fc（x1，.，xk） →c（x1，...， xk）我们把这些新的符号集合在一起，形成一个新的集合.将这些规则与R的规则结合起来得到的TRS表示为Eτ（R）。变换后的TRSEτ（）包括原始TRS的规则。添加的规则管理构造函数符号的适当引用和取消引用：引用的构造函数允许计算其所有参数;在计算它们之后，符号取消引用恢复原始构造函数c。因此，我们还扩展了（原始）E-策略：令Emapτ（τ）为如下：如果f∈ F，则<$J（f）=<$（f），如果cJ∈ CJ，则<$J（cJ）=（1···ar（cJ）），<$J（引用τJ）=对于所有的排序τ j，J（unquoteτJ）=（1 0），并且对于每个c ∈ C τ，（fc）=（1···ar（c）0），使得μ（c）/={1，.，ar（c）}。在下面的结果中，evalJ使用J和Eτ（）来计算项（evalj使用和，如上所述我们的转换在一个非常一般的环境中是正确的9。定理6.1设R =（F，R）=（CD，R）是TRS.设E是一个常规的E策略图。设t∈ T（F，X）满足sort（t）= τ且δ∈ T（C）. 设RJ= Eτ（R）和Emapτ（R）。如果δ∈evalJ（unquoteτ（quoteτ（t），则t→δ。因此，当将排序为τ的t ∈ T（F，X）计算为非引号τ（引号τ（t））时，不会此外，没有构造器项（类型为τ）通过使用Emapτ（Emap）和Eτ（）获得并在使用Emap τ（）和E τ（）时丢失而不是.在本节中，我们不使用ALPUENTE ESCOBAR和LUCAS81R定理6.2设R =（F，R）=（CD、R）是TRS。让它成为一个regu-最大电子战略地图。 设t∈ T（F，X）满足sort（t）= τ且δ∈ T（C）.设RJ= Eτ（R）和Emapτ（R）。 如果δ∈eval（t），则δ∈evalJ（unquoteτ（quoteτ（t）。转换的完备性（关于构造项的计算）需要一些附加条件。定理6.3设R =（F，R）=（CD，R）是左线性连续TRS.设R是正则E-策略映射，使得R ∈ CMR，R是R-终止的.设t∈ T（F，X）满足sort（t）= τ且δ∈ T（C）.设RJ= Eτ（R），J= Emapτ（τ）。如果t→εδ，则δ∈evalεJ（unquoteτ（quoteτ（t）。请注意，与定理5.4相反，我们现在可以从任何E-策略映射开始：示例6.4OBJ程序：obj EXAMPLE-STR是Nat LNat的排序。ops00 '：- > Na t.操作s s '：Nat -> Nat [strat（1）]。opsnilnil'：-> LNat.opcons：Nat LNat -> LNat [strat（1）].opcons'：Nat LNat -> LNat [strat（12）]. op fcons：Nat LNat -> LNat [strat（12 0）]. 操作来自：Nat-> LNat [strat（10）]。opsel：Nat LNat-> Nat [strat（1 2 0）].op first：Nat LNat -> LNat [strat（1 20）]。操作引用：Nat-> Nat [strat（10）]。ops quote ' unquote'：LNat -> LNat [strat（10）]. varsX Y：Nat.var Z：LNat.等式sel（s（X），cons（Y，Z））= sel（X，Z）。等式sel（0，cons（X，Z））= X。eq first（0，Z）= nil.eq first（s（X），cons（Y，Z））= cons（Y，first（X，Z））。eq from（X）=cons（X，from（s（X）。等式引号（0）=0'。eq quote'（cons（X，Z））= cons'（quote'（X），quote'（Z））. eq quote'（nil）=nil'.等式引号（s（X））= s'（引号（X））。equnquote（0' ） =0。eq unquote（s'（X））= s（unquoteALPUENTE ESCOBAR和LUCAS82（X））。equnquote'（nil'）=nil.eq unquote'（cons'（X，Z））= fcons（unquote'（X），unquote'（Z））. 等式fcons（X，Z）= cons（X，Z）。ALPUENTE ESCOBAR和LUCAS83Endo是例1.1中OBJ程序的转换版本。现在，对term unquote '（quote'（first（s（0），from（0）的求值Maude>reduce unquote'（quote'（first（s（0），from（0）.reducein EXAMPLE-STR：unquote'（quote'（first（s（0），from（0）. 重写：11 in-10 ms cpu（0 ms real）（~重写/秒）result LNat：cons（0，nil）注意符号s'和cons'的“取消引用”规则之间的区别不引用cons'是间接的unquote（在例6.4中的程序中，cons的第二个参数不起作用：原因是在应用了这个规则之后，cons的第二个参数仍然是不可替换的。例如，通过使用这样的规则（而不是例6.4中程序的最后两个规则），对unquote '（quote'（first（s（0），from（0）的求值cons（0，unquote'（nil'））这是通过引入中间定义符号fcons来解决的，它首先计算其参数（从而执行重命名），然后还原为cons。在这个意义上，显式注释（1 2 0）对于符号fcons也是至关重要的;否则，解释器可能会关联一个不允许重命名的默认策略（例如，OBJ 3将strat- egy（0 1 2 0）关联到fcons;使用这个默认注释，我们也会获得cons（0，不幸的是，前面的转换并没有保持原程序的终止（在例4.4中证明）。例6.5t=quote '（from（0））的计算Maude> reduce quote'（from（0））.在EXAMPLE-STR：quote '（from（0））中减少。建议：关闭打开的文件。（1）>再见。我们被迫中止了无终止死刑同样，问题是t的评估，即，评价（t）=quote不会终止：引号→引用→ϕ 引用'（0）（from（0）（0 nil）），1. 1⟩→ϕ 引用→引用→引用'（0）（cons nil（0 nil，from（1 0）（s（1 0）（0nil），1. 1⟩ALPUENTE ESCOBAR和LUCAS84ϕ→→→引用→引用→cons→+cons→ϕ···6.1保持完整性和终止性例6.5显示注释J（引用τ）=（10）可能导致非终止。我们可以通过限制T的E-策略为（0）来避免这个问题。但是，在这种情况下，我们需要添加新的规则，以另一种方式进行评估在[16]中，我们引入了一个程序，这是一种能够实现类似效果的转换。在下文中，通过项t中的最外层（出现）定义符号，我们指的是在t中只有构造器符号在其上方的定义符号。新的构造器现在通过redex的收缩引入计算最外层定义的符号F。因此，我们添加了新定义的符号f J，它将在这些最外面定义的f符号出现时出现，以及定义这些符号的新规则。 新规则 FJ（l1，.，lk）→ rJ来自原始的f（l1，.，lk）r如下：在r中出现的最外面定义的符号g在rj中被重命名为gJ;在r中出现的那些g上面的构造器符号c在rj中被重命名为cJ;在r中出现的变量x在它们上面只有构造器符号，在rj中被标记为引号sort（x）（x）。 现在（与前面的变换相反）符号引用τ也旨在将最外面定义的符号f（排序为τ）重命名为它们的别名f J（排序相同）。为了化繁为简的改造，诱人不考虑被添加到变换的TRS的额外规则的数量并引入新的规则FJ（11，...，lk）rJ对于每个定义的符号f。不幸的是，这可能不必要地导致非终止。例6.6考虑规则from（x）→cons（x，from（s（x）我们的运行示例。然后我们引入规则：from’(x)例如，在例5.5中t = first（s（0），from（0））的求值中，符号from并没有出现在最外层：粗略地说，唯一的可能性是，定义first的规则的右侧包含一个只有构造器符号的排序变量LNat，或者from在某个右侧是最外层。这在我们的例子中并没有发生因此，我们不需要引入非终止性的规则，因为在反对方的两个参数上都允许减少 出于这个原因，我们通过仔细识别在给定表达式的求值过程中可能出现的最外面的定义符号来对所需的附加规则进行更准确的分析。ALPUENTE ESCOBAR和LUCAS85{∈ V|n∈ P|∧∀∈ P}下面的符号是辅助的[16]：给定f：τ1×. × τk→ τ，f的自变量的种类被收集在集合10sortarg（f）={τ1，.，τk}。给定一项t∈ T（F，X），• CVar（t）= xar（t） pos（t）， tp=xq

下载后可阅读完整内容，剩余1页未读，立即下载