Zippers循环表示属性文法与属性求值实现的一阶函数解释及其优化规则

理论计算机科学电子笔记229（5）（2011）39-56www.elsevier.com/locate/entcsZippers循环表示上的递归属性文法Eric Badouel1INRIA雷恩-布列塔尼大区，Campus universaire de Beaulieu，F-35402 Rennes，France伯纳德Fotsing2 RodrigueTchougongIRISA，第一大学，Campus universaire de Beaulieu，F-35402 Rennes，France摘要属性评价w.r.t.可以通过归纳计算表达合成属性对继承属性的依赖性的函数来获得属性语法。这种高阶函数式的属性语法方法导致了使用高阶惰性函数式语言（如Haskell）的直接实现。然而，所得到的评价函数不容易服从优化规则。我们提出了属性文法的另一种一阶函数解释，其中输入树被替换为每个节点都知道其上下文的扩展循环树作为一个额外的子树。顺便说一下，我们证明了这些循环表示的zip-PER（具有其上下文的树）是双向链表到任意签名上的树的自然推广。保留字：属性文法，属性求值，循环数据结构，Zipper1介绍属性语法[21，24]的引入使得对上下文敏感信息的操作成为可能，比如程序中变量的作用域。这种形式主义主要用于语言处理工具的上下文中，可以用于两个目的：用属性装饰输入树（从而在每个节点上本地添加信息）或定义语法导向的计算，以便将输入树转换为某些语义域。这两个问题是相关的，因为语法定向计算的结果通常由值1电子邮件：ebadouel@irisa.fr2电子邮件地址：bfotsing@irisa.fr3电子邮件：rtchougo@irisa.fr1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.02.01540E. Badouel等人理论计算机科学电子笔记229（5）（2011）39在根节点上的特定属性;一旦计算了树的装饰，就可以提取（即使人们可能不必计算整个装饰来获得所需的结果）。另一方面，装饰树可以由特定的属性给出，即使这些属性在不同节点上的值可以共享整个子表达式。为了获得有效的实现，经常针对这两种情况提出不同的算法解决方案然而，如果使用像Haskell这样的惰性函数式语言，那么在这两种情况下都可以采用相同的解决方案。事实上，一方面，惰性计算避免了不必要的计算，另一方面，它允许在不同的地方共享子表达式输入树的集合是作为上下文无关文法的抽象语法树的集合给出的树的规则集合，或者，如果我们对具体语法不感兴趣而只对树的抽象结构感兴趣，则作为从多排序签名构建的项的集合。属性的值是由属性语法的所谓语义规则给出的一组递归定义来定义的。如果属性语法是非循环的（属性之间没有循环依赖关系），那么可以使用依赖图的拓扑排序来计算每个属性的值（其弧表示属性值之间的依赖关系然而，人们可以使用基于最小固定点的序代数方法[6，23]来计算潜在循环属性文法（以及潜在无限输入树）的属性。一般属性文法使用合成属性和继承属性，它们分别承载来自给定节点的子树和该子树的上下文的信息。只有合成属性的属性文法相当于原始递归模式[9]，并且属性值很容易通过树上的结构递归计算。由于对上下文信息的操纵，一般属性语法的情况更为复杂。然而，人们很快认识到，我们可以求助于属性语法，只有合成大小的属性，其属性是表达合成属性对继承属性的依赖关系的函数。 因此，属性文法减少了到树的结构归纳，代价是使用高阶值。这种高阶函数式的属性语法方法[19，11，2，22]导致了在高阶惰性函数式语言（如Haskell）中的高效实现。飞利浦开发的Elegant系统[1]和乌得勒支大学的UUAG系统[25]都说明了这种方法。不幸的是，所得到的评价函数不容易适用于优化技术，如基于函数的一阶表示的捷径融合因此，我们提出了一个替代的属性文法的一阶函数解释，其中输入树被替换为扩展的循环树，其中每个节点都知道它的上下文被视为一个额外的子树。付出的代价是一个预处理阶段，将树展开为它的扩展循环版本。顺便说一下，我们证明了拉链的这些循环表示（树及其上下文[16]）是双向链表到任意签名上的树的自然推广。更确切地说，有两种自然的方式来表示E. Badouel等人理论计算机科学电子笔记229（5）（2011）3941列表，以便能够在两个方向上浏览它们。我们可以用一对下推栈来表示列表及其上下文（zipper），例如：一个用于当前列表本身，另一个以相反的顺序用于其上下文;或者在每个节点上使用指向其前一个节点的指针（双向链表）。从一个给定的多排序的签名Z，我们得到一个扩展的签名Z，其对应的树与树或与它们的上下文相关联。一个拉链被引入作为一对树和它的上下文，从而推广对堆栈表示的列表树在任意签名。 我们还介绍了拉链的循环表示，其中每个树（分别上下文）都知道它的上下文（分别）。附加的子树）作为额外的参数给出;这产生了一个新的签名CZ-1，推广了列表的双链接表示在这两种情况下，我们提出了相应的算法属性评估。 第一个（与拉链表示有关）类似于Uustalu和Vene [26]提出的解决方案，尽管我们没有使用comonad的底层结构。第二个算法（与zipper的循环表示有关）是新的。本文的其余部分组织如下。在第二节中，我们回顾了属性文法的基本定义，并给出了属性文法的高阶函数解释的一个变体。在第三节中，我们介绍了拉链，和基于拉链表示的属性评估。在第四节中，我们介绍了拉链的循环表示和一棵树到它的循环表示的展开。在第5节中，我们介绍了基于树的循环表示2属性文法的高阶函数解释为了修正一些符号，我们首先非常简短地回顾了关于多排序签名及其代数的一些数学定义（我们假设读者 如果你熟悉这些概念，他可能希望查阅[14，4]以获得更详细的介绍）;然后我们继续属性语法的定义及其相关解释。我们通过引入根属性文法2.1签名与代数定义2.1一个（多重排序的）签名S =（S，Op）由一个有限的排序集合S和一个有限的算子集合Op组成每个算子op都有一个元α（op）∈S和一个排序σ（op）∈S。记op：s1× · · ·×sn→s表示op是元数α（op）=s1···sn且排序σ（op）=s的算子.运算符op的秩是其元的长度：ρ（op）= |α（op）|. 若α（op）=ε，则称op为σ（op）类常数作为一个例子，我们考虑只有一个排序树的签名，42E. Badouel等人理论计算机科学电子笔记229（5）（2011）39.Σ运算符如下：分叉：树×树→树叶标签：→树因此，我们有一组常数，由一组标签和一个二进制操作符. 它对应于以下Haskell数据类型定义。数据树a =叶子a|叉（树a）（树a）定义2.2设λ =（S，Op）是一个签名，λ-代数A由一个解释域，一个集合As，对每个 类 s ∈ S ， 和 一 个 函 数 opA ： As1 ×···×Asn →As 组 成 ， 它 与 每 个 算 子 op ：s1× · · · ×Sn→s相关联。代数f：A → B的态射是一族映射fs：As→ Bs，使得对每个ai∈ Asif s opA（a1，.，a n） = opB（f s1（a1），...，f sn（a n））当一个代数的解释域是完全偏序且算子的解释是连续函数时，称该代数是连续我们让T（T）s表示s类型的项的集合，而Tree（T）s表示s类的有限树或无限树的集合，它们建立在签名T及其近似项上。这些集合分别是自由连续代数和自由连续代数的载体集合。我们用有限树来标识项，我们将树解释为部分映射t：Nn →n，其域Dom（ t ） 是 非 空 前 缀 闭 语 言 ， 使 得 对 于 每 个u∈Dom （ t ） ， 其 中 t （ u ） =op ：s1×···×sn→s，且i∈N，有u·i∈Dom（t）惠1≤i≤n且σ（t（u.i））=si。 此外，我们让tu表示由Dom（tu）={v∈N给出的以u为根的t的子树|u·v∈Dom（t）}和t u（v）= t（u·v）.2.2属性文法一棵树的节点可以用属性来装饰，属性的值是根据语义规则计算的。定义2.3一个（抽象的）属性文法G =（S，Attr，D，sem）是一个符号G =（S，Op），它的每个语法符号（sort）都与一组属性相关联，在这组属性中我们区分继承的属性和合成的属性：Attr（s）= Inh（s） Syn（s）. 属性q∈Attr（s）的赋值域是完全偏序Dq。我们让Ds↓=q∈Inh（s）Dq和Ds↑=q∈Syn（s）Dq分别表示s类节点的继承属性和合成大小属性的解释域。此外，一组规则（所谓的语义规则）与签名的每个操作符相关联。这些规则给出了属性值之间的函数依赖关系，并由函数给出：sem（op）：Ds↓×Ds↑1×···×Ds↑n−→Ds↑×Ds↓1×···×Ds↓n一个节点u∈Dom（t）被称为语法符号s=σ（t（u）），则它具有与s相同的属性。作出区分的理由E. Badouel等人理论计算机科学电子笔记229（5）（2011）3943⎪⎩⎧⎨、⎧⎪⎨继承属性和合成属性之间的区别如下。树的给定节点中的综合相反，继承的属性表示来自该子树外部的信息（即来自其上下文）。因此，我们定义运算符op：s1···sn→s的输入属性为s的继承属性（其值来自上下文）或s i中的某些si的合成属性（1≤i≤n）（其值来自相应的子树）。其余的属性，即s的合成属性和si的继承属性（1≤i≤n）称为输出属性或定义属性。与生产操作相关联的语义规则集sem（op）实际上确实包含每个输出属性在输入属性方面作为说明，让我们考虑以下用于计算二叉树的边界（从左到右的其叶子的标签的列表）的属性语法，该边界由使用累积参数（继承的属性co_atten）的合成属性a_atten给出。coflat flatten = a：coflat叶一图1.一、计算二叉树边界的属性文法叶a：：−→树εTreeε·flatten=a：（Treeε·coflat）分叉：：Tree1×Tree2−→TreeεTreeε·flatten=Tree1·flatten树1·coflat=树2·flatten树2·coflat=树ε·coflat为了体现语义规则，我们需要区分同一语法符号（排序）的不同出现位置为了这个目的，如果op：s1×···×sn→s是一个算子，我们让op：：（s1）1×···×（sn）n→sε作为扩展的符号，其中每一次排序的出现都用它的位置来标记，并且通过稍微滥用符号，我们经常写op：：X1× ··· ×Xn→Xε，其中Xi是（si）i的一个子，并且Xε=sε。那么附加到运算符op的语义规则的形式如下op：：X1× · ·· ×Xn−→XεXε·syn=sem（op）ε，syn（Xλ·q;（λ，q）∈Inop） 其中syn∈Syn（s）<$Xi·inh=sem（op）i，inh（Xλ·q;（λ，q）∈Inop）其中1≤i≤n且inh∈Inh（si）叉左权44E. Badouel等人理论计算机科学电子笔记229（5）（2011）39.Σ.Σ哪里In op={（ε，q）|q∈Inh（s）}{（i，q）|1 ≤i ≤ n q∈ Syn（s i）}输出op={（ε，q）|q∈Syn（s）}{（i，q）|1 ≤i ≤ n q∈ Inh（s i）}分别表示输入属性和输出属性的出现集合。语义函数实际上是规则方案，其目的是定义术语（的树表示）的每个节点处的每个属性的值。例如，如果t是一棵树，并且u∈Dom（t）使得t（u）=Fork，则上述等式应解释为：flatten （ tu ） =flatten（ tu·1 ） coflat （ tu·1 ）=flatten （ tu·2 ） coflat（tu·2）=coflat（tu）因此，每棵树都与一个方程组相关联，该方程组的变量是属性V t={v t，π，q|π ∈ Dom（t）t（π）：：s1× · · ·s n→ s; q∈ Att（s）}{v t，π·i，q|π ∈ Dom（t）t（π）：：s1× · · ·s n→ s; q∈ Att（s i）}其分辨率提供了树t∈Tree（Tree）sw.r.t.的解释。把文法G归结为映射（[t]）G：Ds↓→Ds↑givenby：（[t]）G（v）（q）=vt，ε，q其中vt，π，q=sem（t（π））ε，qvt，π·λ，q′/（λ，qJ）∈Int（π），其中q∈Syn（σ（t（π）））vt，π·i，q=sem（t（π））i，qvt，π·λ，q′/（λ，qJ）∈Int（π） ，其中q∈Inh（σ（t（π·i）vt，ε，q=v（q），其中q∈Inh（σ（t（ε）其中，假设出现在“where”子句中的向量vt，λ，q我们将在每次定义中出现“where”子句时做这个假设;这符合Haskell程序的解释。图2显示了属性出现的计算流程，它产生了一个二叉树的边界，假设累积参数的初始值（根节点处的属性出现的值）是空列表。2.3与属性文法属性文法的语义规则是语法导向的，因为它们由与签名的每个运算符相关联的规则方案给出。由于这个原因，我们可以展示一个从属性文法G导出的代数AG，使得（[t]）G=tAG，也就是说，在前一节中定义的树的解释是由与代数AG相关的求值态射（分解态射）给出的。E. Badouel等人理论计算机科学电子笔记229（5）（2011）3945的G.Σ.Σ[][a、b、c、d]一DBC图二、用属性文法计算二叉树的边界定义2.4由属性文法G导出的代数AG使得（AG）s=Ds↓→Ds↑，并且运算符op的i-解释：s1×·· ·×sn→s是由下式给出的映射opopAG（f1，...，f（n）（v）（q）=vop，ε，q其中vop，ε，q=v（q），如果q∈Inh（s）vop，i，q=fi（vi）（q）其中ereq∈Syn（si）andndvi（qJ）=vop，i，q′对于qJ∈Inh（si）vop，ε，q=sem（op）ε，qvop，λ，q′/（λ，qJ）∈Inop如果q∈Syn（s）vop，i，q=sem（op）i，qvop，λ，q′/（λ，qJ）∈Inop 若q∈Inh（si）这个定义是循环的[5]，因为在“where”子句中 为qJ∈Inh（si）在定义方程的左侧和右侧都有一个点。因此，它应该被解释为向量<$v op，λ，q<$（λ，q）∈Inop<$Outop作为相应变换的最小不动点的特征。命题2.5（[t]）G=tAG证据 简单地说，细节在[3]中提供。Q上述属性文法的语义遵循[19，2]中提出的方法，它也从[23，6]中获得灵感，因为它给出了属性文法的固定点语义。我们将上述定义几乎逐字转录到Haskell语言中，因为懒惰求值的机制掩盖了结果程序的明显循环性[5]。在[11]中已经提出了将属性文法转化为退化（代数的求值函数）然而，在我们看来，我们刚才给出的演示比那里给出的演示更明确，也更基本，它导致了Haskell中的直接实现。请注意，惰性计算的另一个优点是我们可以在潜在的无限数据结构上定义属性的计算。例如，我们可以定义流上的语义规则，只要给定属性值的每个近似值都可以使用流的有限个前缀46E. Badouel等人理论计算机科学电子笔记229（5）（2011）39.Σ.Σ树的评价w.r.t.由属性文法导出的代数则由归纳定义给出（op（t1，...，t n）AG（v）（q） =vop，ε，q其中vop，ε，q=v（q），如果q∈Inh（s）vop，i，q=tAiG（vi）（q）其中req∈Syn（si）andvi（qJ）=vop，i，q′，其中qJ∈Inh（si）vop，ε，q=sem（op）ε，qvop，λ，q′/（λ，qJ）∈Inop如果q∈Syn（s）vop，i，q=sem（op）i，qvop，λ，q′/（λ，qJ）∈Inopifq∈Inh（si）回到我们的例子，我们导出以下Haskell代码：flatten：：Tree a -> [a]->[a]flatten（Leaf a）coflat= a：coflatflatten（Fork left right）coflat= flatten left（flatten right coflat）2.4根属性文法从现在开始，我们认为每个签名都有一个特定的排序a，称为它的公理。考虑一个顶级函数通常是方便的，该函数在适当初始化继承的属性之后使用属性（这些属性是相应方程组的参数）。这可以通过扩展属性文法来实现，增加一个操作符Root：a→ T，其中a是文法的公理，T是附加的排序，以及相关的语义规则。一个树的形式根（t），其中t∈树（树）a表示一个有根树，即一个树与一个空的上下文。我们假设额外的排序T没有继承的属性和一个对应于最终结果的合成属性。然后，通过一对函数给出与该附加操作符rot相关联的语义规则：init：Da↑→Da↓，初始化rootnode处的继承属性，并且result：Da↑→D其中D=D↑是最终结果的值域。我们不会明确地将这个新的操作符添加到签名中，但要考虑到这是一个指定的rammar是一个属性文法加上这两个功能。顶层函数则是与扩展属性语法所导出的代数中的（现在是隐式的）运算符Root相关联的求值函数，因此它由图3所示的表达式给出。在我们的运行示例中，结果函数是return：T（n）a−→ Dreturn t=result（val）其中val=tAG（init（val））图3.第三章。打结：有根属性文法的顶层功能而init函数是返回空列表的常量函数（初始化与继承的属性countyat相结果inittAGE. Badouel等人理论计算机科学电子笔记229（5）（2011）3947.Σ1=C[op（t1，n到空列表，而不管根节点处的合成属性的值是多少），因此它由以下函数给出return：：Tree a-> [a]return tree= flatten tree []3作为拉链Transformer的为了说明上下文相关的信息，我们操纵一个子树连同其相应的上下文。我们把注意力限制在以排序为公理的树上。一个zipper（排序为s）由一个排序为s的树与该树的上下文组成的一对给出。zipper中上下文的表示来自以下观察：所考虑的子树t的上下文要么是空的，要么是以下形式：opi（t，.，不，C，tdef···得双曲余切值.，[]，t，···，t）]其中op：s1×···×s n→s是一个算子，使得s i是t i的排序，C是一个上下文，其洞的排序是s。 对于1 ≤ j ≤ n和j/= i，树t j是t的兄弟树。因此，树和上下文由以下签名给出。定义3.1在签名Z中，我们发现了两个表示为s和sn的类，a与s中的每个类s∈ S和s n中的每个算子op：：s1×···×sn→s相关联，也是Zn中具有相同元数和类的算子;但它也产生了一族算子opi，其中1≤i≤nopi：s1×···×si−1×s×si+1×···×sn→si最后，我们有一个常量操作器Emptyofsort，它表示空的CON文本。一个s类的zipperc @ t是由一个子树t∈Tree（Z）s和它的上下文c∈Tr e e（Z）s组成的一对。语义规则Xε·syn=sem（op）ε，syn（Xλ·q;（λ，q）∈Inop）与op：：X1×···×Xn−→Xε相关的归纳法则s yn（x）=op（x1， . ，xn））=sem（op）ε，syn（q（x）ε@op（x1， . ，xn））/q∈Inh（s）;qopi（x1， . ，xi−1，x∈ε，xi+1， . ，xn）@xi/q∈Syn（si）），其解释如下。如果zipperc @t的子树t匹配模式xxε@op（x1， . ，xn），即 t=op（t1， . ，tn），则表示上下文c中的子树t的合成属性syn的值的表达式syn（c@t）由右h侧的表达式给出，其中变量x∈ε和xi分别由上下文c和由模式匹配给出的子树ti代替同样，语义规则Xi·inh=sem（op）i，inh（Xλ·q;（λ，q）∈Inop）i−1i+1，.， tn）i−1一期+148E. Badouel等人理论计算机科学电子笔记229（5）（2011）39.Σ.Σ由下式给出inho pi（x1， . ，xi−1，x∈ε，xi+1， . ，xn）@xi=se m（op）i，inh（q（x））@op（x1， . . . ，xn））/q∈Inh（s）;qopi（x1， . ，xi−1，x∈ε，xi+1， . ，xn）@xi/q∈Syn（si））在这种情况下，继承的属性显示为相对于给定子树的上下文（根据模式进行测试）的属性。如果属性语法是根的，则与（隐式）运算符Root相关联的语义规则被翻译为：inh（Empty@x）=init（q（Empty@x）/q∈Syn（a））inhreturn（x）=result（q（Empty@x）/q∈Syn（a））对应于我们运行的示例的Haskell代码如下所示。数据树a =叶子a|叉（树a）（树a）dataCxt a=空|LCxt（Cxt a）（树a）|RCxt（Tree a）（Cxt a）data Zipper a = Cxt a：> Tree aflatten：：Zipper a ->[a]flatten（cxt：> tree@（Leaf a））= a：（coflat（cxt：> tree））flatten（cxt：>（Fork left right））=flatten（（LCxt cxtright）：>left）coflat：： Zipper a -> [a]coflat（CoRoot：>tree）=[]coflat（（LCxt cxt right）：>left）=flatten（（RCxt leftcxt）：>right）coflat（（RCxt left cxt）：>right）=coflat（cxt：>（Fork left right））return：： Tree a ->[a]return tree= flatten（Empty：>tree）该代码是语义规则的直接转录，其中合成属性在树组件的结构上归纳定义，而继承属性在给出上下文的组件的结构上归纳然而，我们在每个规则的右侧相应地更新了各种参数。例如，规则coflat（（LCxt cxt right）：>left）=flatten（（RCxt leftcxt）：>right）声明继承的属性cobalat在应用于LCxt cxt right和子树left形式的上下文时由合成属性cobalat给出在相应上下文中为子树右，即RCxt左cxt。如果每个子树都知道它的上下文，我们可以使这个额外的参数隐式，作为一个额外的参数，并且对E. Badouel等人理论计算机科学电子笔记229（5）（2011）3949称地，每个上下文都知道它所应用的子树。我们使用拉链的循环表示来实现这个结果，我们将在下一节中50E. Badouel等人理论计算机科学电子笔记229（5）（2011）394作为循环数据结构的首先，我们引入了一个扩展的签名，使得相应的树是拉链的循环表示的编码。在第二部分中，我们描述了展开一个有根树（即初始空上下文）到其循环表示的过程。4.1循环数据结构定义4.1在签名CZ w中找到两个表示为s和s的类，与中的每个类s∈ S和每个算子op：s1× · ··×s n→s相关联的a产生一族算子opλ，其中λ∈{ε}<${1， . ，n}其中opε：：s×s1×· · ·×sn→s和opi：：s×s1×···×sn→si。最后我们给出了一个运算子Co Root：a→an，其中a是n的公理.树t∈Tree（CZ<$）s是s类型子树的表示，树c∈Tre（CZ<$）s<$是t类型子树的表示.然而，大多数的树建立从这个签名CZ序列不是有效的表示的子树或上下文。让我们用双向链接流的例子来说明这种现象。如果A是一个字母表，则流是一个在单排序签名上的树（排序S={st}），其中包含一个一元运算符a：：st→st，每个字母a∈A。树a（st）代表其根节点被标记为a的流，并且使得通过移除该根节点而获得的剩余流是st。签名Z提供拉链的关联结构data Stream a = Cons{val：：a，String：：Stream a}data StreamCxt a = Snoc{val：：a，pred：：StreamCxt a}|空数据StreamZipper a =（StreamCxt a）：>（Stream a）zipper的结构允许非破坏性地导航流left，right：：StreamZipper a ->StreamZipper a right（cxt：>（Consastr））=（Snoc acxt）：>str left（（Snoc a cxt）：>str）=cxt：>（Consastr）为了在两个方向上导航一个流，我们可以选择向每个节点添加一个指向前一个节点的指针，这将我们引向一个双向链接流的结构：data DStream a = Node{val：：a，prev：：CxtDStream，prev：：DStream a} data CxtDStream a = CoRoot（DStream a）|CoNode{val'：：a，val'：：CxtDStream a，suc'：：DStream a}其是与签名CZ_n相关联的归纳数据结构。如果我们考虑双向链表而不是双向流，那么我们只需要添加一个与空链表相关的常量操作符相关联的一元构造函数data DList a= Node{val：：a，prev：：CxtDList，val：：DList a}|无（CxtDList）data CxtDList a = CoRoot（DList a）E. Badouel等人理论计算机科学电子笔记229（5）（2011）3951|CoNode{val’:: a ,prev’::CxtDList a, suc’::DList a}These two data structures are isomorphic, and by identifying them we obtain amore traditional representation of doubly-linked lists as:data DList a =节点{val：：a，prev，val：：DList a}|无（DList）一个隐含的假设是，如果定义了prev xs，则prev（prev xs）= xs，如果定义了prev xs，则prev（prev xs）= xs，类似地，prev xs = Nil ys或ys需要ys=xs。 这些条件在以下列表的双链接表示中得到满足[1，2，3]dlist= node1其中node1 = node1（Nil node1）node2node2 = node2 node1 node3node3 = node3 node2（Nil node3）抽象数据类型通常由多排序签名以及根据签名的构造函数声明的等式约束表示。因此，他们限制类的有效解释属于相应的等式的代数簇。然后，抽象数据类型被标识为该类别的初始对象;即，初始代数与诱导同余的商。在本例中，等式是根据签名的选择器来陈述的它们限制了有效生成元的类，抽象数据类型可以用终结余代数的子余代数来标识。这种抽象表示的元素可以用图来表示，其树展开满足以下意义上的方程约束的集合确定了树的节点集合上的二元关系。如果两个以相关节点为根的子树相同，则树满足等式约束。抽象数据类型的载体然后被给定为满足等式约束的树的集合;并且每个这样的元素可以被看作是图的树表示，其节点是其子树的同构类。由于这种图形表示，我们使用循环数据结构的表达式来表示抽象数据类型，这些数据类型定义自多排序签名和由一组使用签名选择器的方程给出的循环基。更深入地研究循环数据结构的这种共代数表示可能是有趣的[15，20，7，13，18]。为了只生成良构的双向链表（即满足上述恒等式的双向链表），我们将使用一些流余代数专门生成它们。这样的余代数允许生成流：data StrCoalg b a = StrCoalg{out：：b->a，next：：b->b}streamGen：： StrCoalg b a -> b -> Stream astreamGen（StrCoalg out next）= build其中build gen = Cons（out gen）（build（next gen））例如，可以使用Er的筛子生成素数流52E. Badouel等人理论计算机科学电子笔记229（5）（2011）39阿托斯特尼如下：筛= StrCoalg头下一个其中next xs=filter（\n-> not（（nprimes = streamGen sieve[2..]为了从一个流余代数生成一个格式良好的双链接流，我们只需要通过添加一个新的参数来处理上下文，从而调整流生成函数的上述定义：dStreamGen：： StrCoalg b a -> b -> DStream adStreamGen（StrCoalg out next）gen =dstr其中dstr= build gen（CoRootdstr）build gen cxts = Node（out gen）cxtsdstr其中dstrdprimes = dStreamGen sieve[2..]然后我们推导出一个函数，将一个流转换为相应的双向链接流：stream2dStream：： Stream a -> DStream astream2dStream= dStreamGen（StrCoalg值为0）或者等价地通过扩展函数dStreamGen的定义：stream2dStreamstr= dstr其中dstr= buildstr（CoRootdstr）build（Cons val）cxts = Node val cxts dstr现在可以浏览一个双向链接的流：right（Node a cxts dstr）=dstrleft（Node_（CoNode b cxts dstr）_）= Node b cxtsdstrfirst：： Int-> DStream a -> [a]first0 str= []first（n+1）（Nodea cxts dstr）= a：（firstn dstr）测试=第一5（（左右右左右）dprimes）>测试[11，13，17，19，23]4.2展开一棵树在本节中，我们将对前面的双向链接流示例进行概括把树转化成拉链。为此，我们引入了一个属性语法规范与给定的签名。E. Badouel等人理论计算机科学电子笔记229（5）（2011）3953⎧⎨⎩定义4.2与签名n =（S，Op）和公理a∈ S相关联的根属性文法η n定义如下。它有一个与每个排序Inh ={cxt s}关联的继承属性|s ∈ S}表示树的给定节点处的上下文，以及一个合成属性Syn ={tree s|s ∈ S}表示以该节点为根的子树，由树s：s → s和cxts：s→s给出位置和排序。定义了Dtrees=Tree（CZ）s和Dcxts=T ree（CZ）s. 与运算符op：s1×···×sn→s相关的语义规则由下式给出：op：：X1×···×Xn→XεX ε·tree s= op ε（X·cxt s，X1·tree s1，.，X n·treesn）X i·cxt si = op i（X·cxt s，X1·tree s1，.， Xn·tree sn）和 的 辅助 功能 结果：树（CZ）a→树（CZ）a和 初始化：T re e（CZ<$）a→Tree（CZ<$）a分别是恒等式和算子Co Root。我们让U表示因此，运算符op的解释如下：opU（f1，.，f n）cxt = op ε（cxt，tree1，.，树n），其中树i= fi（op i（cxt，树1，...， tree n））我们让unfold表示相应的顶层函数：unfold：：Tree（）a→Tree（CZ）aunfold（tree）=ctree 其中ctree=tU（CoRoot（ctree））因此展开函数可以写为：展开树=ctree其中ctree=构建树（CoRoot ctree）build s（op（t1，.，t n））cxt = op ε（cxt，tree1，.，树n）其中t reei=bui ldsi tiopi（cxt，t ree1， . ，treen）在我们的二叉树例子中，展开可以给出如下：数据树a=叶子a|叉（树a）（树a）data ZTree a = ZLeaf a（ZCxt a）|ZFork（ZCxt a）（ZTree a）（ZTree a）数据ZCxta = CoRoot（ZTree a）|ZLeft（ZCxt a）（ZTree a）（ZTree a）| ZRight（ZCxta）（ZTreea）（ZTreea）54E. Badouel等人理论计算机科学电子笔记229（5）（2011）39unfold：： Tree a ->ZTree aunfold tree= ctree其中ctree=build tree（CoRootctree）build（Leaf a）cxt = ZLeaf a cxtbuild（Forkleft right）cxt= ZFork cxt cleft rightE. Badouel等人理论计算机科学电子笔记229（5）（2011）3955GGG我其中，cleft =buildleft（ZLeft cxtcleftright）right=build right（ZRight cxtcleftright）在双链表的例子中，我们引入了这个展开函数，作为从列表余代数生成双链表的函数的特殊情况。通过使用上述展开函数的适配可以完成相同的操作数据主干a b =叶a |Fork b b数据树a = In{out：：Trunk a（Tree a）}data TreeCoalg c a = TreeCoalg{next：：c-> Trunk a c}punfold：： TreeCoalg c a -> c -> ZTree apunfold coalg gen= ctree其中ctree= build gen（CoRootctree）build gen cxt = case next coalg gen ofLeaf a-> ZLeaf a cxtForkleft right-> ZForkcxt cleft right其中，cleft =buildleft（ZLeft cxtcleftright）right=build right（ZRight cxtcleftright）unfold = punfold（TreeCoalg out）更一般地，该参数展开将被给出为：punfold coalg gen=tree其中tree=builda gen（CoRoot tree）buildsgen cxt=case coalg gen ofop（gen1，.，genn）→op ε（cxt，tree1，.， 树n）其中，trei=buildsi geniopi（cxt，t ree1， . ，treen）5属性文法的一阶功能解释我们将一个根属性文法G与一个CZ-代数A哪里和.A.S =Ds↑和。A.s=Ds↓opAεG（v）（syn）=sem（op）ε，syn（v）opAG（v）（inh）=sem（op）i，inh（v）CoRootAG=init56E. Badouel等人理论计算机科学电子笔记229（5）（2011）39G.Σ其中op：s1×···×sn→s，v∈Ds↓×Ds↑1×···×Ds↑n，syn∈Syn（s），且inh∈ Inh（s i）.提案5.1（展开树）AG = Val其中val = tAG（init（val））证据 简单地说，细节可以在[3]中找到。Q因此，结果（展开树）A与由根属性语法G从给定输入树返回的值返回树一致。它给出了一个算法，通过简单的结构递归对输入树的展开来计算该值。在我们的运行示