可在www.sciencedirect.com在线获取理论计算机科学电子笔记276（2011）237-246www.elsevier.com/locate/entcs共归纳类型的实现Dexter Kozen1，2康奈尔大学美国纽约州伊萨卡市，邮编：14853摘要本文给出了集合上多项式函子的适度推广的最终余代数的一个显式组合构造。类型签名被建模为有向多重图而不是内函子。类型签名F的最终余代数涉及F中路集上的Brzozowski导数的概念。关键词：余代数，余归纳，递归类型，Brzozowski导数1引言集合上的闭函子F的最终F-余代数在定义余归纳数据集的语义方面很有用。在非常一般的条件下，最终余代数的存在性已经在几篇论文[1，2，3，4，5，7，11，12，14，15，16]中得到了研究。这些研究大多是从抽象的范畴观点进行的，通常涉及逆极限，柯西完备化，或大余积的互模拟等价物。除了一些具体的例子[7，11]，一般的具体结构似乎是缺乏的。在[2]中指出：“众所周知，一个最终余代数。. .可以被描述为所有适当标记的有序树的余代数，一个可访问的具体结构将用于任何对形式语义和逻辑感兴趣的人，用于推理共归纳数据集。较少关注但仍然是一个问题的是，将类型签名表示为Set上的多项式函子的传统表示并不总是足够的，[1]感谢Jean-Baptiste Jeannin、Bobby Kleinberg、Alexandra Silva、Navin Sivakumar和匿名评论员的深刻评论。2电子邮件：kozen@cs.cornell.edu1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.09.024238D. Kozen/Electronic Notes in Theoretical Computer Science 276（2011）237相互递归定义的类型;即使是这样，它也会引入不必要的不对称。字母表上的普通确定性有限自动机形成了一个特别简单形式的余代数族[11，13]。这种类型的最终余代数可以用Brzozowski导数显式地构造D a（A）={x|（1）A，B，A，本文给出了集合V上多项式函子对应的类型签名的最终余代数的显式Brzozowski式构造，其中V是一个类集合。然而，而不是函子，我们表示类型签名为有向多重图与节点指定为存在或普遍的。这种表示法有许多优点。通常，集合上的多项式函子是由乘积、余积、来自固定集合的全函数和部分函数、常数函子及其组合构建的;但所有这些都可以用存在和泛节点建模。许多抽象构造都强加了有限性条件以确保连续性，但我们不需要这样的限制。最重要的是，多重图为定义路径集上的Brzozowski导数提供了一个平台。2Brzozowski衍生物在进行§3中的构造之前，回顾一下Brzozowski导数[6]在构造普通确定性有限自动机的最终余代数中的作用是有指导意义的。经典上，字母表上的确定性有限自动机（DFA）由一组有限状态S、一个转移函数δ：S→S→S、一个起始状态和一组接受状态F<$S组成。正如在[11，13]中所观察到的，忽略起始状态，DFA只是多项式内函子（<$→−）×的余代数。一般来说，这个签名的余代数由一组状态S（不一定是有限的）和一个结构映射α组成：（S→S）×。值α（s）是（S→S）×中的一对，其中第一个分量决定了转移函数δ，第二个分量决定了s是否∈F。现在将每个状态s与自动机所接受的字符串集合L（s）相关联，如果s是起始状态。映射L满足两个性质：(i) 若t=δ（s）（a），则L（t）=Da（L（s）），其中Da（A）是A关于a∈A的Brzozowski导数，如（1）中所定义。也就是说，从状态si开始接受字符串ax，从状态δ（s）（a）开始接受字符串x。(ii) 空字符串ε∈L（s）i <$s是一个接受状态。本质上，ε的子集，连同Brzozowski导数Da和决定ε是否∈A的函数E，形成了这个签名的最终余代数，L是从DFA到这个最终余代数的唯一余代数同态。形式上给出了最终余代数的转移函数和接受态D. Kozen/Electronic Notes in Theoretical Computer Science 276（2011）237239B一LLDbDa一一aB aBL（a+b（aba）b）（bab+aba）baba（bab+aba）baDaDb DaDbFig. 1.一个自动机及其在最终余代数中的映象。最终状态（以较暗的颜色显示）映射到包含ε的集合。自动机中的转换对应于最终余代数中的导数通过D（A）（a）=D（A）E（A）=.1ifε∈A0，如果ε/∈A。使L成为余代数同态的相关性质是它与两个余代数的结构映射交换。这是上述性质（i）和（ii）的内容。图中示出了一个示例1.一、Brzozowski导数Da和同态E可以在正则表达式上进行语法定义：Da（e1+e2）=Da（e1）+Da（e2）E（e1+e2）=E（e1）+E（e2）Da（e1e2）=Da（e1）e2+E（e1）Da（e2）E（e1e2）=E（e1）E（e2）Da（e）=Da（e）eE（e）= 1D（b）=.1ifa=b，a，b∈NE（b）= 0，b∈ N0 ifa b，a，b∈Da（1）= 0E（1）= 1D a（0）= 0E（0）= 0.这是建立有限自动机和正则表达式等价性的Kleene定理的关键成分3主要结果3.1有向重图一个有向多重图是一个结构G=（V，E，src，tgt），其中节点V，边E，以及两个映射src，tgt：E→V，分别给出每条边的源和目标。如果s=srce和t=tgte，我们写e：s→t。当指定多重图时，我们有时会使用符号s→n从s到t的边。t表示元陈述，240D. Kozen/Electronic Notes in Theoretical Computer Science 276（2011）237不FCG图二.表示单排序代数签名的多重图。蓝色菱形代表存在节点，红色正方形代表通用节点。路径是节点和边s0e0s1e1s2···sn−1en−1sn，n≥0，使得ei：si→si+1，0≤i≤n− 1。这些是由G生成的自由范畴的箭头。路径的长度是边的数量。长度为0的路径只是一个节点。路径p的第一个和最后一个节点分别记为srcp和tgtp。与边一样，如果s=srcp且t=tgtp，我们写p：s→t。一个重图同态l：G1→G2是一个映射l：V1→V2，l：E1→E2使得如果e：s→t则l（e）：l（s）→l（t）.这提升到由G1和G2生成的自由范畴上的函子。3.2类型签名一个类型签名是一个有向多重图F，并指定F的每个节点是存在的或泛的。存在节点和泛节点分别对应于余积和积构造函数。图的有向边表示相应的析构函数。例如，考虑由二元函数符号f、一元函数符号g和常数c组成的代数签名。这通常由多项式内函子F=−2+−+表示，或者在OCaml中由类型t = F oft * t| t的G |C我们可以用一个由四个节点组成的有向多重图来表示这个签名{t，f，g，c}，其中t是存在的，f，g，c是泛的，以及边t→1 ft→1gt→1cf→2g→1t.多重图如图所示二、这里有一个更复杂的例子[8]。在那篇论文中，高阶语言与闭包的计算状态是根据递归类型定义来Val=常数+Cl值Cl=λ-Abs×Env闭合Env=Var~Val封闭环境D. Kozen/Electronic Notes in Theoretical Computer Science 276（2011）237241×ΣVal常量ClVal=Const+ClCl=λ-AbsEnvEnv=Var~Valλ-Abs环境B1B2B3比哈尔邦···Bn图3.第三章。表示多分类签名的多重图其中Const是常数的固定集合，λ-Abs是λ-抽象的固定集合，Var是变量的固定集合（这些集合的确切性质并不重要）。这组值是递归方程的解Val=Const+（λ-Abs×（Var~Val）），它通常由一个内函子来F=Const+（λ-Abs×（Var~−））onSet。在OCaml中，我们可以写type value = Const of int|关闭和关闭的关闭= labs * envenv = var-> value我们通过具有存在节点Val，Const，λ-Abs和Env以及通用节点Cl，和每个BλVar的节点的多重图来建模这种类型的签名。边缘是Val→1Cl→1Const→cEnv→1ConstVal→1λ-AbsCl→1，c= |Const|λ-Abs→dB，B <$VarB→bCl环境，d = |λ-Abs|Val，b = |B|注意，我们将固定集合Var上的部分函数Var~Val视为依赖余积B<$VarValB。这是通过一个存在节点来选择域B的值，然后是一个通用节点来选择该域上的函数ValB多重图如图所示3 .第三章。242D. Kozen/Electronic Notes in Theoretical Computer Science 276（2011）237→。Σ→srce=sΣs∈VFs∈VF3.3余代数及其实现设F是一个节点为VF的类型签名.一个F-余代数是（As，αs）对的一个VF-指标集合，其中As是集合，αs是集合函数αs：Assrce=sAtgte，如果s是存在的，srce=s Atgte，如果s是泛函数。F-余代数的态射是集映射hs的一个VF-指标集合，它与αs以通常的方式交换。 这符合传统的定义， 集合V上闭函子F的F-余代数。余代数等价于实现。一个F-实现是一个有向多重图G以及一个多重图同态l：G→F，称为类型，具有以下性质。• 如果l（u）是存在的，则G中存在一条边。• 如果l（u）是泛的，则l是G的具有源u的边和F的具有源l（u）的边之间的双射F-实现的同态是与类型交换的重图同态定理3.1 F-余代数范畴与F-实现范畴是等价的（在[10，§IV.4]的意义上）。证据 我们必须展示一对函子之间的F-余代数和F-实现，一个在每个方向，并表明，他们是逆自然同构。我们首先从一个给定的实现G构造一个余代数，其中节点为VG，类型为l：G→F。对于F的每个结点s，设As={u∈VG|l（u）= s}且定义αs如下：• 如果s是存 在的， u∈As， 设d： u→v是G 中的 唯一边 ，srcd=u， 令e=l（d），以及令t=l（v）=tgte。定义α s（u）=ine（v），其中ine：A tAtgte是自然注入到副产物中。• 如果s是泛的且u∈As，设α s（u）∈srce= sAtgte是乘积的唯一元素，使得对于任意边d：u→v且srcd=u，如果e=l（d）且t=l（v）=tgte，则π e（α s（u））=v，其中π e：srce= sAtgte→A t是乘积的自然投影。反之，给定一个具有数据（As，αs）的F-余代数，我们可以构造一个实化. 实现的节点是联产品的元素A s={ins（u）|u ∈ A s}（2）其中l（ins（u））=s，u∈As。若u∈As且s是存在的，则α s（u）= ine（v）∈srce=sAtgte，其中e：s→t且v∈At.将边<$u，e<$u添加到实现中，其中<$u，e<$u：ins（u）→int（v）和l（<$u，e <$u）=e。 如果u∈As且s是泛函数，则D. Kozen/Electronic Notes in Theoretical Computer Science 276（2011）237243SAJtgteSα s（u）∈srce=sAtgte. 对于每个e：s→t，设ve=πe（αs（u））∈At. 添加边缘u，e在这个构造中，我们可以取边u，e为有序对（u，e）。因为u和e唯一地决定v、s和t，所以每个这样的有序对最多出现一次作为边u，e，所以没有重复的危险为了完成证明，我们必须验证这两个构造是自然同构的逆。给定一个实现G，其类型为l：G→F，应用第一个构造，然后应用第二个构造，通过将节点u映射到inl（u）（u）并且将边d映射到in l（u）（u）的同构，产生一个自然同构于G的实现。1999年12月20日，很容易检查出这些映射是节点和边上的双射保持邻接，并与类型映射交换。类似地，给定一个带有数据（As，αs）的余代数，执行第二次迭代，然后执行第一次迭代，得到一个带有数据的余代数AJs ={ins（u）|u ∈ A s}αJ：AJ →。如果s是存在的，srce=s如果s是存在的，则α SJ（ins（u））=ine（int（v）），其中α s（u）=ine（v）andndt=tgt e。如果s是单向的，则πe（α sJ（ins （u）=int（v），其中πe（α s（u））=v且t=tgt e。通过与s：As→Ajs中的分量的同构，证明这两个余代数是自然同构的，是一种常规的方法。注意，AJs总是成对不相交的，而As可能不是。然而，这并不排除同构，因为F-余代数范畴中的态射由F的节点索引的集合映射的集合组成，这些映射可以在同一元素上取不同的值。Q3.4最终余代数实现允许我们给出最终余代数的具体构造，这让人想起弦集合上的Brzozowski导数（1）。在这里，导数作用于类型签名的特定路径集，而设F是一个类型签名。构造一个实现RF，lF如下。的节点RF是F中有限路的集合A，使得(i) A是非空的，是预闭的;(ii) A中的所有路径都有相同的第一个节点，我们定义为lF（A）;(iii) 如果p是A中一条长为n路，且t>p是存在的，则A中恰好有一条长为n+1的路扩张p;(iv) 如果p是A中长度为n的路，且t>p是泛路，则所有长度为n的路n+ 1扩张p在A中。RF的边定义如下。 设A是F中的一组路，e是一条边如果s是universal。244D. Kozen/Electronic Notes in Theoretical Computer Science 276（2011）237S不S不见图4。 多重排序的签名。荷兰盾定义A对e的Brzozowski导数为：D e（A）={p|（src e）ep∈A}，通过从A中以该边开始的路径中移除初始边e而获得的路径集合。如果A是RF的一个结点，且De（A）非空，则我们只包含一条边A，e在RF中，取lF（εA，eε）=e。很容易证明tgt∈A，∈E=De（A）满足性质（i）定理3.2实现R F，l F在F-实现范畴中是最终的。定理3.1所构造的相应的F-余代数在F-余代数范畴中是最终的。证据设G，l是任意实现。唯一同态h：G，l→RF，lF由下式给出：h（s）是F中的路的集合，这些路是G中从节点s开始的路的l下的像。定理的第二个陈述是由两个范畴的等价性得出的（定理3.1）。Q4讨论4.1多重排序签名与不对称性在引言中，我们提到集合上的多项式内函子似乎不足以建模一些值得被视为多项式类型的共归纳类型。我们还提到，它们可能会造成不必要的不对称。例如，如何对相互依赖的共归纳类型进行类型s= C of s *t 和t= Dof s *t在Set上使用一个内函子;看起来Set2是必需的。对应于该签名的多重图如图1B所示四、在单排序的情况下，集合上的内函子是足够的。它们在多排序示例Val=Const+Cl Cl=λ-Abs×Env Env=Var~ValD. Kozen/Electronic Notes in Theoretical Computer Science 276（2011）237245因为有一个节点满足所有循环;事实上，有三个这样的节点。然而，我们仍然必须选择在哪里打破循环，这是不可取的不对称。在这种情况下，我们可以选择三个选项FVal=Const+（λ-Abs×（Var~−））FCl=λ-Abs×（Var~（ Const+− ） ） FEnv=Var~（Const+（λ-Abs×−）），但这样一来，我们就得证明选择并不重要。我们猜想，当存在一个签名类型的节点集合A，使得每个圈只包含A的一个节点时，Set上的内函子是适当的。4.2作为标号树在本节中，我们希望扩展Ad′amek[2]的状态，即“最终余代数”. . 可以被描述为所有正确标号有序树的余代数 在那篇论文和[3]中，人们发现了一个显式的树形结构，用于单排序多项式签名，如图2所示。Worrell [16]给出了一个无序树的构造。当人们试图正式定义标记树时，一个微妙之处就出现了。问题是如何定义节点和边，以便在最终余代数中获得唯一的代表。对于涉及n元函数f：An→A的传统代数签名，可以将树的节点定义为ωi的预闭非空子集，使得如果α是节点，则αi对于所有0≤in都是节点，其中n是节点标签的arity。这种结构例如出现在[3，9]中。然而，目前还不清楚如何处理无序树或更一般的类型签名。 在[16]中，有人说，“我们认为树是同构的， 有向图。. .“是相同的，”因此树是同构类。但是怕什么？思考这个问题自然会引出类型签名作为有向多重图F的想法。这允许我们构造其节点是F中的路径的标记树。一个节点的子节点不是由自然数索引，而是由F的边索引。为了将最终余代数的元素刻画为标号树，我们可以从§3.4中构造的最终实现RF，lF开始。RF的每个节点A对应于如下的标记树τ（A）。τ（A）的根是1F（A）。τ（A）的节点是A的元素，它们是F中的路。如果p是q的前缀且它们的长度相差1，则τ（A）中存在从p到q的边。标号函数用路径p的最终节点tgtp来标号路径p。在这种构造中，τ（De（A））是τ（A）的第e个极大真子树.246D. Kozen/Electronic Notes in Theoretical Computer Science 276（2011）237引用[1] Aczel，P.和P. Mendler，A final coalgebra theorem，in：Category Theory and Computer Science，Lecture Notes in Computer Science389，Springer，1989 pp.357-365[2] Ad'amek，J.， 关于连续函子的有限代数，Theor. Comput. Sci. 294（2003），pp. 3-29号。[3] Ad'amek，J. 和v. Kou bek，Onthegratestfix edpointofasetfunctor，Theor. Comput. Sci. 150（1995），pp. 57比75[4] America ， P. 和 J. Rutten ， 在 一 类 完 备 度 量 空 间 中 求 解 可 交 换 域 方 程 ， J 。 Comput. 系 统 Sci. 39（1989），pp.343-375[5] Barr，M.，良基集合论中的终端余代数。Comput. Sci. 114（1993），pp.299-315[6] Brzozowski，J. A.，正则表达式的衍生物，J. Assoc. Comput。马赫11（1964），pp. 481-494.[7] Hausmann，D.， 论文，德累斯顿大学（2004年）。[8] Jeannin，J.- B.和D. Kozen，Computing with capsules，TechnicalReporthttp://hdl.handle.net/1813/22082，Computing and Information Science，Cornell University（2011）.[9] Kozen，D.，J. Palsberg和M.I. Schwartzbach，E. C. Recursive Subtyping，Mathematical Structuresin Computer Science5（1995），pp.113-125[10] MacLane，S.，[11] Rutten，J.，泛余代数：系统理论。Comput. Sci. 249（2000），pp.三比八十[12] 圣 卡 纳 莱 湖 最 后 余 代 数 的 逻 辑 构 造 ， 在 ： H。 P. Gumm ， editor， Proc. Workshop on CoalgebraicMethods in Computer Science ， Warsaw ， Poland ， Electronic Notes in Theoretical ComputerScience82（2003），pp.1-20[13] Silva，A.，“Kleene余代数”博士论文，奈梅亨大学（2010年）。[14] 史密斯，M. B.和G. D.张文，张文，等，递归域方程的范畴理论解，计算机工程学报，2000，24（1）：117 - 118. 11（1982），pp. 761-783。[15] Worrell，J.， 递归数据类型的余归纳：偏序，度量空间和Ω-范畴。《理论中的电子笔记》Comput. Sci.33（2000），pp.337-356[16] Worrell，J.，关于无穷集函子的最终序列，Theor。Comput. Sci. 338（2005），pp.184-199。
我的内容管理
展开
