余代数单子：项代数统一模型与函数式编程语言实现

71理论计算机科学电子笔记65第1期（2002）URL：http://www.elsevier.nl/locate/entcs/volume 65. html21页s余代数单子NeilGhania，1，4ChristophhLüthb，2Fe dericoDeMarchia，3，4a英国莱斯特大学数学与计算机科学系bFB3摘要本文引入了余代数单子作为项代数的统一模型，涵盖了初始代数、最终余代数、有理项和项图等基本例子。我们开发了一个一般的方法，获得有限的coalgebraic单子，使我们能够概括的概念，合理的长期和长期图的其他类别集。作为一个应用程序，我们概述了部分的正确性，函数式编程语言的术语图实现1介绍初始代数语义一直被认为是程序设计语言语义的基石之一在这种范式中，语言的语法被建模为初始代数，由语言的有限项组成，而语言的语义则是从初始代数到其他代数的唯一类似的情况出现在数据类型理论中，其中初始代数由从数据类型的构造函数构建的有限项组成，而初始性允许通过结构递归在数据类型上定义函数在范畴上，我们把这样的初始代数看作是表示语言或数据类型的内函子F的初始代数为了将基本特征，如变量和替换，纳入框架，人们考虑的不是一个单一的初始代数，而是，对于每个对象X，X上的初始F-代数，即初始X+F-代数。将一个对象X（被认为是变量的对象）发送到初始X+F-代数（的载体）的映射定义了F上的自由单子。乘法1电子邮件地址：ng13@mcs.le.ac.uk2电子邮件地址：cxl@informatik.uni-bremen.de3电子邮件地址：fdm2@mcs.le.ac.uk4由EPSRC资助的研究GRM 96230/01：分类重写：Monads和模块化·2002年由ElsevierSc ie nceB出版。 V. 操作访问根据C CB Y-NC-N D许可证进行。GHANI，LÜTH和DEMARCHI72monad的自由度提供了一个替代的抽象表示，单位模型的变量，而monad的自由度模型的归纳性质的初始代数。对集合以外的基范畴的应用在许多场合都取得了丰硕的成果，例如，S-排序代数理论作为集合S上的单子的研究，用图或Cat上的单子研究具有结构的范畴，用图或Cat上的单子研究重写，Pre或Cat[14]和用单子研究高阶抽象句法F在集合[10]上（其中F是有限集合范畴的骨架当然，除了有限项的初始代数之外，还有其他项代数。例如，如果不是有限的术语，那么在有限的术语中呢？从计算的角度来看，人们可能会争辩说，应该只考虑那些在某种意义上可计算的或者，从递归论的角度来看，有理项是那些可以由某种形式的递归方程定义的项呢从函数式语言实现的角度来看，术语图是该领域的主要语法模型。这些问题是明确的实际重要性和上述论文建议推广这些长期代数范畴以外的集。在这个方向上，余代数社区已经做了一些工作。事实上，Moss[15]通过证明它们形成最终的X+F-余代数，从而优雅地对偶了有限语法树的初始代数特征，从而在有限项和无限项的术语代数的情况下给出了相当完整的答案此外，他表明，收集这些coalgebras也形成一个单子，从而满足我们的要求，替代考虑。这些结果是在[1]和[11]中独立发现的，尽管后者使用了更严格的设置。另一项代数，即合理的条款，已被认为是最近[2]，但作者评论的困难，推广他们的工作以外的范畴集。然而，这些结果只处理特定的项代数，我们不想逐个处理每个项代数。 本文引入余代数单子作为项代数的统一框架。具体来说，我们• 引入余代数单子的概念，并证明这个定义包含了一些重要的例子。• 给出了从余代数构造单子的一般定理，并利用该定理证明了有理项和项图的关键例子是余代数单子。• 通过展示如何在它们上求解方程来证明余代数单子具有良好的性质。这使我们能够通过术语图证明函数式编程语言实现的部分正确性我们认为，长期图单子可能是最重要的贡献，灰这项工作。函数式语言GHANI，LÜTH和DEMARCHI73∈CCC◦ − C C C C提供了一个优雅的推理框架，但函数式语言实现的语义仍然保持在相对较低的水平。虽然已经尝试使用抽象技术来建模术语图[6]，但它们尚未在函数式编程社区中产生重大影响。我们希望的自然性和简单性的coalgebraic模型的长期图，例如证明了我们的工作递归coalgebraic单子，将有助于弥合这一差距。本文件的结构如下。我们在第2节中引入了余代数单子的概念第3节包含了一个一般定理，证明语法的概念是一个单子，并将其应用于理性单子和术语图单子的情况第4节扩展了第3节，以涵盖共代数单子，而第5节包含我们的部分正确性结果。2余代数单子设F：F是一个函子，我们可以认为它是由某种形式的签名产生的。如果TX是使用一组变量X从F构建的某个项集合，则我们需要以下属性• TX应该包含所有变量X，并且在来自F的项构造函数的应用下是封闭的。因此TX应该是一个X+F-代数。• 每个termt TX都应该是一个变量，或者从F的term构造函数开始。因此TX应该带有X+F-余代数结构，它应该是代数映射的逆。• 为了有一个行为良好的替换概念，发送X的映射到TX应该是单子因此一个单子对每个X都是F-余代数i，TX是X+F-不动点，或者更抽象地说，T是（Id+F）：[，]n[，] fixed point5。虽然这是一个共代数单子的直觉基础，我们正式介绍的概念，首先注意到：引理2.1设（T，η，μ）是一个单子，F是范畴上的一个闭函子。在自然变换τ：F<$T和自然变换α：FT< $T之间存在双射，使得下图可交换FµFTT FT(1)αT α❄ ❄好的。µ5我们将忽略这里的大小问题，因为它们很容易处理GHANI，LÜTH和DEMARCHI74CC◦证据 给定τ，定义α = μ.τ T。（1）的可换性紧接着τ的自然性和μ的结合性：FT TτT TT TµT T TFµ Tµ µ❄ ❄ ❄英国广播公司。τT µ反之，给定α，定义τ=α.Fη。这两个映射很容易被证明是相互逆的。✷条件（1）只是说，如果我们认为α是将T上的F项变换为T项，那么如果我们在F上下文中将两项相乘然后变换，或者更确切地说变换上面的项然后将其与第二项相乘，它换句话说，（1）意味着μ：αT<$α是一个F-代数同态。在一个单子T上存在这样一个结构，就产生了另一个单子，这可以很容易地通过图追踪来验证因此，我们假定C具有所有有限的乘积。同样，给定一个具有共极限X的图D，我们将用d表示D中任意对象d的共极限映射d：d<$X。引理2.2设（T，η，μ）是上的单子，F是上的闭函子。设α：FT∈T是一个自然变换，使得（1）是对易的。定义η= inl：Id+ Ft;以及µ：Id+FT+FT（Id+F T）Id+F T+F T[η，ηα]Id+F T+FT2[Id+F T，Fµ]Id+ FT。故（Id + FT，η，μ）是一个单子，而[η，α]：Id + FTT是一个单子态射。我们现在可以定义一个余代数单子，然后给出一些例子。定义2.3设F是范畴C上的闭函子。C上的F-余代数单子是一个4元组（T，η，μ，τ），使得（T，η，μ）是C上的单子，τ是F和T之间的自然变换，其中单子态射[η，μ.τ T]：Id+FT<$T是同构。（T，η，μ，τ）和（TJ，ηJ，μJ，τJ）之间的F-余代数单子的态射是T和TJ之间的单子态射φ使得φτ=τJ。命题2.4（初始余代数单子）设（T μ，η，μ）是闭函子F：C<$C上的自由单子。其中，Tμ是初始的F-余代数单子。证据自由度给出了一个自然的变换τ：F<$T µ。 引理2.2的条件证明φ = [η，μ.τ T]：1 + FT μτ μ是单子态射。接下来，在rFη：FμId+ FT μ中的自然变换通过T μ的自由性诱导出一个单子态射T μ：T μId1+ FT μ。这个φGHANI，LÜTH和DEMARCHI75µµ◦ −◦ −和T μ是互逆的图追逐，证明了Tμ是F-余代数单子。给定任何其它F-余代数单子（TJ，τJ），自由性和变换τJ：F<$TJ给出唯一的单子态射！：TµTJ使得τJ=！τ。✷当对每个对象X，Tμ（X）是初始X+F-代数时，一个光滑的证明是可能的。在这样的设置中，Tμ是闭函子（Id+F−）：[C，C]<$[C，C]的初始代数，并且由于所有初始代数都是同构的，我们得到T同构于1+FT。 由于每个F-余代数单子都是一个（Id + F−）-代数，所以初始性随之而来。引理2.5（最终余代数单子）设F：C C是，令Tν是最终的（Id + F <$−）-余代数。则Tν是最终的F-余代数单子。证据文[1]证明了T ν是一个单子，使得存在同构[η，α]：Id + FT ν<$T ν. 此外，α满足条件（1）也是由它们的替换定理得出的因此Tν是F-余代数的。任何其他的F-余代数单子S都是（Id+F）-余代数，因此S和Tν之间存在唯一的（Id+F）-余代数同态。这也是一个单子态射，可以用一点图来证明，使用最终的Tv。唯一性源于终结性。✷集合上的许多余代数单子作为签名上无限项的子集而产生当研究由签名产生的集合和函子时，可以通过赋予它们替换的概念来证明一个无限项的集合是余代数单子，替换的概念是Tν的替换的限制。这样，我们可以证明以下都是集合上的余代数单子：i）只包含有限个变量的有限项; ii）局部有限项[7]，即。 有限项和无限项，具有从每个节点到叶子的有限路径的性质;iii）有理项是具有有限个子项的项，或者更正式地说，签名上的自由迭代理论[9]。然而，一个coalgebraic monad的概念也捕获其他的语法结构，如term graphs，它被用于实现函数式编程语言，通过使用循环和多重边来模拟递归和共享它们可以被认为是允许循环和多条边的标记图。我们现在发展一个一般定理，导出monads作为逐点列限制，并使用这个结果来定义有理和项图monads。3作为点态共极限的在签名、项、替换等概念中固有的是arity的概念，它绝对地意味着表示单子有秩。为了理解这个条件，在签名上建立的初始代数TX满足GHANI，LÜTH和DEMARCHI76C C CDCCCC（二）T（X）=T（X0）X0X是有限的这个方程成立，因为所有的算子都有一个有限元，因此一个建立在X上的项只能包含有限个变量。这样的单子是有限的，我们只关注它们，因为它们捕捉了大多数关键的例子。签名和它们的表示单子之间的关系可以推广到lfp-范畴[3]，即由一组可表示对象生成的共完备范畴，其中一个对象是有限可表示的，如果它的协变hom函子保持filtered colimit。如果是lfp-范畴，设fp是包含J的有限可表示对象的全子范畴：FP✲.一个函子F：✲有限，如果它保持过滤的余极限，或者等价地，如果它同构于它对Cfp的限制的沿着J的左Kan扩张。因此，从C到D的无穷函子的范畴Fin [C，D]等于任意一个函子范畴y[Cfp，D]。在D = C的情形下，无穷内函子范畴是幺半群，具有单位幂和乘法。类似地，[Cfp，C]也是么半群，包含J为单位，乘法为F<$G=LanJ F<$G。现在给出C上的一个无穷单子就是给出Fin[C，C]中的一个幺半群，其中，在等式y[Cfp，C]中使用一个幺半群[13]。通过将有理项、项图或其它项代数的结构推广到[Cfp，C]，证明了有理项、项图或其它项代数是可积的，并利用左Kan扩张得到一个单子.这样的幺半群可以得到我们称之为克莱斯利幺半群定义3.1lfp范畴C的Kleisli幺半群由以下组成：• - 函数T，将C中的对象TX分配给Cfp中的每个对象X;• 对于Cfp中的每个X，映射ηX：X<$TX在C中;• 对于Cfp中的对象X，Y，提升函数sX，Y：C（X，TY）<$C（TX，TY）;满足以下条件：s X，X（η X）= 1 TXs X，Y（f）.η X=fs X，Z（s Y，Z（g）.f）= s Y，Z（g）. s X，Y（f）.在本文的其余部分，我们将尽可能省略函数s的下标。这个定义引理3.2如果C是lfp范畴，则C的每个Kleisli么半群定义了一个在C范畴[Cfp，C]中的m。证据首先，通过设置T（f）= s（η.f），T可推广到函子T：fp∈T和自然变换η：J∈T.乘法需要地图GHANI，LÜTH和DEMARCHI77CCCCCCC我的 天|}−CµS：（TT）STS。由于（TT）S通过Kan扩展定义，∫（T<$T）S=LanJT（TS）=C（n，TS）<$Tn<$TSn∈Cfp因此，我们需要一个楔形wn：（n，TS）Tn<$TS，通过张量的泛性质，它是一族映射（n，TS）<$（Tn，TS），它由Kleisli幺半群的提升给出这些地图确实形成一个楔形遵循克莱斯利幺半群的法律自然性来自于余的参数性定理，而幺半群的定律又归结为克莱斯利幺半群的定律。✷有理单子和术语图单子都是作为逐点余极限出现的。因此，关于它们定义的大部分技术推理依赖于共极限的性质，我们使用Lax切片类别将其形式化。定义3.3设是一个2-范畴，X是的对象。Lax切片2-范畴LaxX具有对象映射f：Y<$X。 箭头由LaxX（f，g）= h，α α：f gh给出如果α：fβ：g和β：g他们更- 在LaxX中，我们将它们的合成记为β<$α：f好吧给定映射h，αg和Bleg，2-细胞Bleh，αBleg✲⊗hJ，αJ⟩co nsist sofa 2-cellθ：h在C中有αJ=gθ.α.片范畴C/X的通常定义是2-范畴上的松弛片范畴，它是通过只将单位2-胞腔加到上而得到的。Lax切片类别允许我们声明以下内容：引理3.4设C是一个范畴，考虑在2-C范畴Cat上建立的松弛片范畴Lax C。如果f∈H，α∈La ×C（F，G），则箭头族Hd，α d定义F上的一个余锥，它又在colimα中诱导一个映射：colim F∈colimG。此外，colim 1 F= 1：colimFcolim F和colim（βα）= colim β。科利姆α最后，给定一个2-胞腔α<$αJ，则colim α = colim αJ。3.1什么时候点态Colimit是Monad？设C是一个范畴，I：C是一个函子，KC是将每个对象映射到C的常数函子。本节的其余部分将找到自然变换U：IKC：C的让猫，使分配X→colimUX定义了一个无穷单子，记为T，在C上。因图什岛将每个对象X映射到（X+F）coalg的子范畴，该子范畴由我们想要在单子中捕获的那些余代数组成。自然变换U的第X个分量扮演了从这个子范畴到基范畴的遗忘函子的角色，而colimUX则将是表示我们感兴趣的集合的对象，即。我们单子T对X的作用我们通过证明T对Cfp的限制支持一个Kleisli幺半群结构来证明如上定义的T是一个单子 因为我们有行动TX=GHANI，LÜTH和DEMARCHI78Lg伊萨克湖LhU布雷格湖UF+∈I我F∈II我colimUX forX finitely presentable，我们转向我们的候选单位。 如果我们假设对于每个有限可表示对象X∈Cfp，存在一个对象iXX使得UX（iX）=X，那么我们可以定义ηX为包含iX：X=UX（iX）UX=TX。 在我们的例子中，iX将是inl：X<$X+FX的余代数，其包含将变量嵌入到余极限中。最后，我们转向提升函数，需要额外的属性。给定一个从对象X到TY（对象表示Y+F-余代数）的映射，通过将每个X+F-余代数映射到一个Y+F-余代数，然后利用ColimUX =TX的泛性质，将其推广到TX到TY的映射.这是通过首先观察X实际上可以映射到某个子对象Y0（表示变量集）的TY0来我们代入的项实际上是建立在其上的），然后加上Y0对每一个X+F-余代数的载体，使之成为一个Y+F-余代数。从形式上讲，这个过程被我们称为提升的过程所捕获定义3.5I被称为有提升L，当• 对于achbjtX∈C和eachg∈IX，存在一个uwl（g），gl ll l：UUgXinLa xC，即afunctorL（g）：IUgX与自然变换g L：U U.L（g）• 对于acharowk：g 在我看来，这是一个自然的转变kL：L（g） L（h）. IUksuchhathLIUk=UkL. GLL（g）IUgIXIUgIUkIUhCIX引理3.6设X和Y是可表示的，并且假设Y是一个过滤范畴。然后，任何映射f：X<$colim U Y，诱导映射s（f）：colim U X<$colim U Y。证据因为X是有限可表示的，Y是过滤的，所以f因子为f=if。f+forsomeifY. 这一定义是一个函数rLf=L（if）（f+），也是一个自然变换fL=iL<$1XfcolimUYIXIfIU（if）ULifIYUY（if）C因此，根据引理3.4，映射s（f）= colimfL：colimUXcolimUY。s（f）的构造似乎取决于因子分解f=if. f+。 这实际上不是这个案子。事实上，这是posef=ih。HISAnotheR一（f）+U⇒1L 我FUGHANI，LÜTH和DEMARCHI79HH我F我FHFX我我我我我XIXIXyF我我F因式分解，诱导函子和自然变换L（ih）I（h）：IXIY和iL1：UUL（ih）I（h）通过引理3.4，我们有一个映射colim（i L<$1）：TX_n。因为Y是过滤的，所以存在i，k：i fi和kJ：i h使得f分解为f= i.g，对于给定的映射g：X<$U Y（i），其中Uk.f+= g = UkJ.h。让我们在k：if上为你加油吧我是阿吉 提升L确定skL：L（if）<$L（i）。IUK. 然后iL1=iLI（Uk）I（f+）=（UkL.iL）I（f+）=UkLI（f+）.iLI（f+）Wherehefirsnotequalityycomesfromm （g）= （Uk）（f+），第三个是自然 变 换 的 水 平 分 量 相 对 于 垂 直 分 量 的 分 布 。我 们 有 iL<$1=UkL（f+）.iL<$1，通过引理3.4，我们有colim（i L<$1）= colim（i L <$1）。类似地，colim（i L <$1）= colim（i L <$1），因此s（f）不依赖于因子分解。重复使用上面的符号，我们定义了典范因子分解f = if。f+f∈L（f） =L（if）。（f+）和dfL=iL（f+）。 在得到Kleisli三元组的候选项后，我们现在验证需要进一步假设的三个定律。 对于单位的提升，首先注意有一个因式分解η X= i X。1. 因此，通过引理3.4，s（η）= colim（iL1）=colimiL colim 1 = colimiL.这证明X X引理3.7设X∈ C.如果colim i L= 1，则s（η X）= 1 UX。引理3.8设X和Y是可表示的，且f：X可表示U Y。若映射k：L（f）（iX）∈if∈IY使得Uk. fL=f+，thens（f）.η X= f.我的律师。 s（f）isdetermineddbyafactorisationf=if. f+。因为ηX是从UX（i X）到列UX，s（f）的包含，η是由f确定的上锥的UX（i X）次分量，如引理3.6所示，即s（f）.η = L（f）（i X）.f L. 由此可见：X=UX（iX）LiXUY L（f）（iX）UY（if）Uyif其中左三角形通过假设和右三角形交换，因为它是U，Y上的泛余锥的一部分。✷引理3.9设X、Y和Z是可表示的。考虑两个映射f：大肠 杆菌XmUY和g：大肠杆菌YUZ。一个sample，对于ally∈IY，IUyL（y）✲IY（克/升）❄L（g）❄U（L（g）y）ZL（L（g）y）英国❄F我GHANI，LÜTH和DEMARCHI80布雷格湖UyFIf我我我XIXy我我且g L<$y L=（L（g）y）L<$1。 则s（s（g）.f）= s（g）。s（f）LyIU yIYLgIZIU yI（fL）IU（Lg（y））L（Lg（y））IZ埃尼湖U UC100%（Lgy）LUUUC证据 映射s（g）.f可以分解如下：Xf质量s（g）✻If✻L（g）（if）Uif 单位（L（g）（if））GLIf其中f=if.f+是f在构造s（f）中使用的因式分解，并且平方与s（g）的构造互换因此，我们有s（g）.f的因式分解，函子L（s（g）.f）可以计算为：L（s（g）. f））=L（gLif）。I（gL）. I（f+）=L（g）.L（if）. I（f+）=L（g）.L（f）其中第三个等式是通过定义L（f）。由这些假设，下列等式也是可导出的：（L（g）if）L<$1 =gL<$iL：UX（if）<$Z。通过与h进行预压缩 f+，我们认为这两个2-胞元S是同相的。f）和L（g）.L（f）相等，因此s（s（g）.f）= s（g）。s（f）。✷收集到目前为止的所有结果，我们得到以下结果：定理3.10设C是lfp范畴，I：Cfp∈Cat是函子使得对Cfp中的每个X，IX是滤子. 设U：I KC：CfpCat是具有提升L的自然变换。 对于Cfp中的任意对象X、Y和Z以及C中的映射f：X≠U Y和g：Y≠U Z，假设• 存在IX中的对象i X，使得UX（iX）=X且colimiL= 1;• 这是一个pk：L（f）（iX）∈if，使得Uk。fL=f+;• 对于IY中的所有lly，gLyL=（L（g）y）L 1，IUyL（y）✲IY（克/升）❄L（g）❄U（L（g）y）<$Z.L（L（g）y）然后赋值TX = colim U X带有一个Kleisli幺半群结构。推论3.11在前一定理的假设下，T的左Kan扩张在Cfp包含于C下是C上的有限单子。我GHANI，LÜTH和DEMARCHI81CM4有理和项图单子现在我们使用我们的一般定理来证明项图和有理项形成单子。首先，我们给出了范畴的一些一般性质我们写UX：（X+F）−coalgforgettfulfunctor sending每个余代数对应于其载波。UX创建余极限，由于C是lfp，因此是余完备的，任何函子J：D从一个小范畴D中导出n（X+F）−coalg有一个colimit和U×colimJ = colimU× J。接下来，引理4.1设F：C<$C是函子。 将C的对象X赋值给范畴（X + F）−coalg定义了一个函子Φ：CCat。此外，U：ΦKC是一个自然变换。证据如果f：X<$Y是中的映射，Φ（f）将X + F-余代数（S，h）发送到X +F-余代数（S，（f +1）.h）。Φ（f）对余代数态射的作用和函子性也很容易证明。自然性成立，因为UX=UY Φ（f）。✷一般地，我们将用与Φ有各种关系的函子来实例定理3.10，它们的性质从Φ的性质得到类似地，我们定义了Φ的提升，由此可以得到其他函子的提升引理4.2设（S，g）是X + F-余代数. 将任何S + F-余代数（A，m）发送到下一个X + F-余代数的映射定义了Φ的提升。A+S[m，innn]S+F Ag+1X+F S+F A1+[Finr，Finl]X+F（A+S）证据 我们已经定义了函子L（g）的对象部分：Φ Ug<$Φ X，并且L（g）对态射的作用很容易定义。的第（A，m）个分量g L：U S<$U X.L（g）是包含g L= inl：A<$A+ S。 自然性gL是inl的自然性。给定任意X+F-余代数映射k：（S，g）<$（SJ，h），定义kL为自然变换，其在（S+F）-余代数m：A<$S+FA上的分量为下列X+F-余代数态射A+SL（g）（m）X+F（A+S）1+K❄1+F（1+Uk）❄A+SJ<$X+F（A+SJ）L（h）（Φk（m））表示2-胞腔条件的自然变换的分量是（1+ k）。inl：A<$A+SJ和inl：A<$A+SJ，因此显然相等。✷4.1理性单子给定一个签名，有理项是一组有限项和无限项，它们作为方程组的解出现，方程组的形式为e1= t1，.。，en= t n其中每个t i是从签名n构建的项，并且其变量来自固定集合X与集合E ={e1，.，e n}。为了得到一个解，我们坚持每一项ti都不是E的元素。换个说法GHANI，LÜTH和DEMARCHI82ICICXX0在分类上，有理方程是函数φ：E<$X + F<$T<$（X + E），其中F<$是与签名相关联的多项式内函子，T<$是初始（X + E）+F-代数，如（2）所示。正如我们将在第6节中看到的，所有这类方程在Tν（X）中都有唯一解例如，方程e= A（e）的解为无穷项A（A（...））.我们可以考虑一个形式为e=t（ei→x）的方程，它是一个有限的，其中有v个s→x，并且e指向系统的任何一个极点。例如，等式e=A（x，e）和e=A（x，A（x，e））可以表示如下A Ax x AX这样的树是有限集上的X+F余代数，其状态是图中的因此，理性单子是完全包含的极限。子范畴X+F-余代数与有限可表示载体。取完整的子范畴包括所有的余代数态射，因此通过互模拟得到的同元。这确保了上面的有理方程具有相同的解。形式上，我们取R：RisCat为将对象X映射到X+F-余代数的全子范畴的函子，其基础对象是有限可表示的。遗忘函子UX：R（X）提供了我们将取其逐点余极限现在我们用定理3.10证明有理项形成单子。命题4.3赋值X <$→ RX = colim U X定义了一个单子。由 于 这 个 函 子 是 无 穷 的 ， 我 们 证 明 了 它 是 一 个 单 子 ， 通 过 使 用corolary3.11对它的限制Cfp。I R的泛函性从引理4.1中引入的Φ的泛函性继承。同样，解除IR也是一种重新-提升L对Φ的约束。对于这一点至关重要的是，有限可表示对象的余积是有限可表示的，这意味着L（f），当应用于有限可表示对象上的余代数时，返回有限可表示对象上的余代数由于我们使用了完整的子范畴，所以提升L中所需的自然变换的所有分量仍然可用。最后，提升的所有方程性质仍然成立，因此我们有一个为IR做举重。为了应用推论3.11，我们仍然需要验证我们的主要定理3.10中表达的三个条件。自然转化α=inl：IdIXiL确保，通过引理a3。4、大肠杆菌miL=colimId=1。现在，给定C中的映射f：X ∈RY，其中X和Y是有限可表示的，余代数L（f）（iX）由复合X+Y0inl[f+，Y<$0]Y+FXif+FXY+F Y+FXY+[Finl，Finr]Y+F（Y0 +X）0GHANI，LÜTH和DEMARCHI83IXCy其中f=if+.如果我们让映射k：L（f）（iX）∈if到be[f+，Y0]：X+Y0<$Y0，它是一个新的周期。fL=f+.最后，设Z是有限可表示的，g：Y在地图上显示y：Y0<$Y+ FY0是Y +F-余代数.则对任意的Y0+ F-余代数α：A本文讨论了Z+F - 代数中的一个代数方程，即Z + F -代数方程的一个代数方程，并讨论了L（g）L（y）与L（L（g）y）I（gL）的关系A+Y0+Z0[α，Y0，Z0]❄Y0+Z0+FA（Y+Z0+[Finl，Finr]）[y，Z0，FA]❄Y+Z0+F（A+Y0）（Z+[Finl，Finr]）[ig[g+，Z0]，F（A+Y0）]❄Z+F（A+Y0+Z0）当g=igg+withU（ig）=Z0时，省略了和中明显的包含项，并有意地重新排列了和。自然变换gLyL和（L（g）y）LId的两个相应分量是包含AA+Y0+Z0，因此相等。✷4.2关于Graph Monad术语图是有限语法树的概括，它允许i）循环，如有理方程，以模型递归，ii）多个边缘，以模型共享。共享是获得效率的基础，因为共享子项中的计算仅需要执行一次，而不是每次出现一次传统上，项图由标号图定义[4]，但我们觉得将项图定义为X+F-余代数要清晰得多，因为在通常定义中明确的元数信息隐藏在余代数的结构图中，并且通常在处理余代数时自动我们还选择在我们的项图上施加最大可能的共享，即所有变量都被迫被最多一个状态调用。这些术语与长谷川在他的博士论文[12]中研究的术语非常接近，尽管似乎存在一些差异。从理论上讲，我们将其定义如下。定义4.4设X是一个有限签名，X是一个集合。 术语图其中X中的变量是5元组（S，V，L，A，r），其中• S是一个有限集合;GHANI，LÜTH和DEMARCHI84• V是X的有限子集;• L是从S到S的函数;• A是从S到C的函数，使得A（v）的长度等于L（v）的元数，其中C=S+V;• r是C中的一个元素，使得对于C中的任何其他状态s，都有一个有限序列a1，.。，a n使得a1= r，a n= s且a i是A（a i−1）中的元素。这里S表示我们图的状态集。表示变量的状态从S中分离出来，并整理在一个集合V中，该集合V嵌入X中，从而强制每个变量最多被调用一次。L是一个标记函数，它对于S中的每个状态，说明哪个标记与它相连表示变量的状态没有标签。最后，A将S中的每个状态映射到由L指示的转换之后的后继状态（子状态）组成的字符串。因此，字符串的长度必须与标记状态的函数符号的arity元素r是项的选定根，从它可以到达所有其他状态我们称G（X）为X中含有变量的项图的集合。这样一个复杂的语法定义以一种更好的方式进行了绝对重写。事实上，有了上面的数据，我们可以以一种非常明显的方式给S+V一个X+F-余代数结构（带有有限载体）。V内射映射到X的事实反映了变量最多出现一次的事实为了得到集G（X）作为余极限，利用我们的定理导出函子性和单子性，我们的思想是考虑这样的余代数的范畴实际上，还需要更多的改进;也就是说，我们希望在子项的共享中允许尽可能多的选择。与我们之前所做的相反，我们现在例如，我们想区分以下两个项图F F❄❄G G G❄X x因为在第一种情况下，G不是共享的。为了保持它们不相等，我们需要删除所有实现两个不同项之间互模拟的箭头另一方面，我们仍然希望识别同一项的两个副本这些考虑使我们只允许夹杂物作为映射为了以一种精确的方式表达这些思想，并从集合范畴中抽象出来，我们现在将在我们的基本范畴C上引入更多的假设，然后使用我们的主要定理来构建一个项图单子。X+F-余代数范畴的子范畴IGX将有作为对象GHANI，LÜTH和DEMARCHI8512CVSI−这些余代数有一个有限可表示的载体，使得每个变量最多出现在一个状态。换句话说，我们需要将余代数的载体分裂成两个对象的和，其中一个将嵌入X，而其余的状态将有一个标记转移到其他一些状态。这样的分裂反映了上面定义中的对象V和S，为了实现它，我们需要在一个广泛范畴的上下文中工作。定义4.5具有有限余积的范畴C被称为广延的，如果它允许沿着注入到一个余积中的回撤，以及任何对交换平方Aα1<$A<$α2g1fg2❄ ❄ ❄BB+C印度卢比是一对回调当且仅当顶行是C中的余积图。文[5]证明了扩张范畴的一些性质。 我们在这里报告我们感兴趣的那些。命题4.6设C是一个广延范畴。然后• 二元联产品中两次进样的回撤为初始目标;• 注入到余积中是monic（这两个性质表明和是不相交的）;• 进入初始对象的任何箭头都是可逆的（即，initials are strict）;• 对于C中的任意对象A，B，C，（A ×B）+（A ×C）的典范映射到A ×（B + C）是同构，即 C是分布式的。我们现在可以用这个定理来建立单子了今后我们也要考虑到它的广泛性。给定一个X+F-余代数γ：C<$X+FC，我们可以将C分解为以下对象的和：通过形成下面的两个回撤，映射到X的那些和映射到FC的CinlCinrCγV γ γS❄ ❄ ❄XX-X+FCX-FC印度卢比设G（X）是（X+F）coalg的子范畴，其对象为所有的余代数γ：C具有有限载体C的X+FC，并且使得γV是C中的一个幺半群，且作为映射的余代数态射的载体映射是C中的一个幺半群.进一步地，设函子UX是有效函子的自然限制。不难看出，Colim U X精确地给出了GHANI，LÜTH和DEMARCHI86我我我我SSSα我我⇒我SSX我们上面描述的集合G（X） 从I G（X）中 的余代数的载体到G（X）的共限映射将一个简单的元映射到包含s的最小的子余代数。这个余代数显然以s自身为根 在本节的其余部分，我们将经常省略IG中的下标，并将UX的上极限写为G（X）。为了使替换正确工作，我们现在需要使用不同的提升。 令γ：C X+FC是一个对象X. 函子L（γ）：CX的作用如下。 令α：A C+FA是一个对象 C.然后余代数L（γ）（α）由复合定义，A+CαS+γFA+X+F CX+[Finl，Finr]X+F（A+C）X+F（AS+[αV，C]）X+F（A+C）若f：（A，α）<$（B，β）是C+F-余代数态射，则L（γ）（f）是其载体映射为fS+C的余代数态射，其中fS是通过拉回定义βS的泛性质按期望的方式得到的.具体而言，AinlAfS f❄ ❄BCIBBINL因为f和inl都是monic，所以fS也必须是monic。这确保了S+C是唯一的，并且在此不是针对IX的。自然变换γL：UC<$UX.L（γ）在a计算公式α：AC+F AinIC由公式γL=AS+αV给出：一AS+C。 自然是一个简单的检查。映射φ：（C，γ）的提升作用（D，δ）inX必须是自然变换φL：L（γ）L（δ）。 我们在α上定义它的分量：AC+ FA inC作为映射AS+φ：AS+CA S+ D。自然性也很容易检验。此外，等式UX（φ L）γ L=δ L。Uφ成立，作为余代数α的两个自然变换的分量：AC+F AinICboth不再是组件AAS+αVA+CAS+φ一个S+ D。这就定义了提升。现在我们继续讨论定理3.10所要求的进一步的性质。首先，我们需要在IX中定义一个对象iX，使得UX iX=X。让 这个余代数在IX中，因为（iX）V是X上的单位元，因此是幺半群。我们还需要证明，科利姆湖= 1。为此，使用引理3.4，自然变换λ：Id<$L（iX）。我们定义λ的第（C，γ）分量为映射CS+γV：CS+CV=C<$CS+X，它是IX中的映射，因为假设γV是幺半群GHANI，LÜTH和DEMARCHI87Xyy∈现在让Xf+γCγγ Y.然后，我们需要一个映射k：L（f）（iX）<$C。通过一点计算，可以注意到余代数L（f）（iX）由复合定义，C我在这里FX+Y+F CY+[Finl，Finr]Y+F（X+C）Y+F[f+，C] Y+FCC上的恒等式显然是两个coalge- bras之间的余代数态射（这是可以接受的，因为它是monic的此外，自然变换的第i个X分量fLturn将不精确为f+，因此，通过将k= 1 C，等式k。（f L）i= f+紧随其后。最后，对于Y，Z，g和y：A<$Y+ FA，如定理中所述，我们需要证明L（g）.L（y）=L（L（g）y）。I（gL）anddgL<$yL=（L（g）y）L<$1.L etβ：B在IUy=IA中，A + F B是一个代数结构。然后，L（g）L（y）β：（BS+A）S+C<$Z+F（（BS+A）S+C）L（L（G）y）I（gL）β：BS+AS+C<$Z+F（BS+A+S+C）并且，通过一点计算，可以证明这两个余代数是相等的。至关重要的是，要做到这一点，我们需要证明（BS+A）S=BS+AS，但这需要一些简单的粘贴。最后，自然变换的两个分量都是同一个映射BS+（AS+g+αV）βV：BBS+AS+C，所有这些都将用于统计以下结果：4.我的朋友7.将X发送到行IGX定义了一个方法。4.3共代数性结果我们构造了一个将单子定义为逐点列限制的一般定理。由于我们的全部兴趣在于余代数单子，问题是是否有可能推广定理（3.10）来产生余代数单子。在这里，我们提供的初步结果表明，长期图和理性单子是共代数。引理4.8设F：C<$C是有限函子，IX是过滤范畴，H：IX<$IX是函子。若存在自然变换α：FUX <$UXH，则ColimUX是F-代数. 类似地，如果存在自然变换α：UX <$F UX H，则Colim UX是F-余代数。证 据通 过 引理 3.4， 我 们 有映射（ H ，α）LaxC （F UX， UX），因此colimα：colimF UX