可在www.sciencedirect.com在线获取理论计算机科学电子笔记325（2016）147-168www.elsevier.com/locate/entcs完备Elgot单子和余代数恢复Sergey Goncharov1，* Stefan Milius2 Christoph Rauch3，*Lehrstuhlfur？rTheoretischeInformatik，Friedrich-AlexanderUniversit？atErlangen-N？nberg，Germany摘要Monad被用来抽象建模一系列的计算效应，如非确定性，状态和异常。完备Elgot单子是配备了满足一组自然公理的（统一）迭代算子的单子，它允许对迭代计算进行抽象建模。 最近的研究表明，扩展具有自由效应的完整Elgot单子（例如，的操作通过通道发送/接收消息）规范地导致广义的共代数恢复单子，其先前被用作非良基保护进程的语义域。本文继续研究完备Elgot单子及其与广义余代数恢复单子的关系。我们给出了后者的Eilenberg-Moore代数的一个刻划。事实上，我们的工作更一般与Uustalu这进一步用于建立完备Elgot单子的特征，即其代数一致地配备有由广义余代数恢复单子得到的参数化单子的完备Elgot代数的结构。关键词：完备Elgot单子，完备Elgot代数，恢复单子，一致迭代1引言Monad在计算机科学中的一个传统用途，源于Lawvere的开创性论文[20]，是作为代数语义的工具，其中Monad作为等式理论（克隆）的高级隐喻出现。最近，Moggi提出将monad与计算对象相关联，并将其用作指称语义的通用工具[22]，这对后来的函数式编程语言的设计产生了相当大的影响，最突出的是Haskell [1]。最后，在新千年的第一个十年，Plotkin和Power重新建立了† 完整版本可在http://arxiv.org/abs/1603.02148上获得s由德国研究共同体（DFG）根据项目SCHR 1118/8-1提供1电子邮件：Sergey. fau.de2电子邮件：mail@stefan-milius.eu由德国研究联合会（DFG）根据MI 717/5-13电子邮件：Christoph. fau.dehttp://dx.doi.org/10.1016/j.entcs.2016.09.0361571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。148S. Goncharov等人/理论计算机科学电子笔记325（2016）147计算单子和代数理论之间的联系代数学[23，24]。我们使用概述的视图来研究迭代的概念， 这是一个公认的代数意义，在计算结果的上下文中非常相关。在技术层面上，我们目前的工作可以被看作是以前关于单子的广泛工作的延续，迭代[2，5，7]在Elgot[12]和Bloom和E'sik[10]的迭代理论中有其作用。更具体地说，我们关注单子上的一个特殊构造：给定一个单子T和一个函子T，我们假设存在余代数TX = νγ。T（X + γ）对于每个对象X（这些最终余代数存在于T，和基范畴的温和假设下）。已知[28]T可拓成一个单子T，我们称后者为广义余代数恢复单子。Intuelance（）是一个通用的语义域，用于将外延（通过T）和内涵（通过T）特征与迭代相结合的系统。为了使这种直觉更精确，考虑以下简单的例1.1设A={a，b}是一个动作字母表。然后下面的方程组指定基本进程代数（BPA）的进程x1，x2，x3：x1=a·（x2+x3）x2=a·x1+b·x3x3=a·x1+C我们可以把这种特殊化看作一个映射P→T（{C}+P），其中P={x1，x2，x3}，n =A×-，T=Pω是有限幂集单子.使用标准方法[26]，我们可以通过找到一个映射P→T{C}来解决这个问题，该映射为每个xi分配可能非良基树T{C}= νγ的域上的相应语义。Pω（{C}+A×γ）。这里的关键事实是，原始系统受到保护，即。变量xi的每个递归调用之前都有一个动作。这意味着给定的递归系统有唯一的解。如果放弃守护性假设，解可能不是唯一的，但是如果单子T的Kleisli范畴在完全偏序范畴中被丰富，或者更一般地，如果T是一个完全Elgot单子，则可以引入规范解的概念。一个单子T是一个完备的埃尔戈单子，如果它配备了一个迭代算子，该算子为形式为f：X→T（Y + X）的每个态射分配一个解f<$：X→TY，该解满足一组已建立的迭代方程公理和一致性[27]（例如，Pω不是一个完备的埃尔戈单子，但可数幂集单子Pω1是）。最近的工作[14]的中心结果是，只要T是一个完整的Elgot单子，那么变换单子（）也是如此特别地，这允许过程上的递归方程的正则解（在例1.1的意义上），只要T上的递归方程是可 解的。本文研究了保护迭代和非保护迭代之间的关系，并利用广义余代数恢复实现了保护迭代和非保护迭代S. Goncharov等人/理论计算机科学电子笔记325（2016）147149monads和complete Elgot monads。作为一个辅助抽象装置，我们使用Uustalu [28]引入的参数化单子的概念，即双函子#：C×C→C使得对于每个对象X，函子-#X是单子。例如，（）中的双函子X#Y=T（X+Y）产生一个参数化单子。在[5]之后，我们引入了参数化单子#的完全Elgot代数，它们是#的代数，配备了满足完全Elgot单子公理的然而，与后者相反，完全Elgot#-代数省略了Beki'claw的一个形式，该形式说明了如何解决实际递归定义。然后，我们证明，对于每个对象X，最终余代数νγ。X#γ等价地是X上的一个自由完备Elgot #-代数，并且是随后单子νγ的Eilenberg-Moore代数范畴. --γ 同构于完备Elgotγ-代数范畴进一步，我们证明了对于每个完备Elgot单子T，每个自由T-代数TZ正则扩张到X# Y的完备Elgot #-代数 =T（X+Y）。这种情况可以大致概括如下：（νγ. γ）-代数= 完备Elgot代数⊇自由T-代数从例1.1的观点来看，这种连接可以被认为是如下的。由于Id =Id，所以一组守卫只包含一个动作，这可以理解为延迟。现在，T-代数包含到（νγ. --#γ）-代数本质上意味着完全Elgot单子通过忘记守卫来解释T上的阶段性的、可能是有限的、有守卫的过程相反地，假设我们有任何单子T，使得上述包含在T-代数相干地具有完全Elgot#-代数的结构的意义上成立. 则T配备有迭代算子，满足一组比完备Elgot单子的公理弱的公理;随后的概念是弱完备Elgot单子的概念。本文的结构如下。在范畴范畴之后（第2节），我们在第3节提出并讨论了完全Elgot单子。在第四节中，我们引入了参数化单子的代数和完备Elgot代数;在第五节中，我们证明了完备Elgot代数的范畴与单子νγ的Eilenberg-Moore范畴同构。进一步证明了X上的自由完备Elgot代数与最终余代数νγ等价. X#γ（定理5.9）。最后，在第6节中，我们应用所发展的结果来刻画完备Elgot单子，即其代数相干地装备有完备Elgot代数结构的那些单子（定理6.4和6.6）。进一步相关工作。 参数化单子的代数在 [4，6]尽管对于基的特殊情况，即有限参数化单子一个局部有限可表示的范畴。Loc.前引书还介绍了迭代基代数，这是代数的基础上有唯一的解决方案的无穷递归方程。在[ 5 ]中引入了闭函子H的完备Elgot代数，并证明了它们构成了由取最终余代数TX = νγ得到的单子T的Eilenberg-Moore 范 畴 . （ X+Hγ ） ; 这 是 H 上 的 自 由 完 全 迭 代 单 子 （ 参 见 [2] ） 。 由 于X#Y=X+HY是一个参数化单子，150S. Goncharov等人/理论计算机科学电子笔记325（2016）147→−→完全Elgot代数的概念将前面的概念推广到参数化单子的水平我们的定理5.7推广了[5，定理5.8]。带迭代算子的单子的研究受到Bloom和E'sik的启发迭代理论[10]。从Lawvere理论（即集合上的无穷单子）扩展到更一般范畴上的单子，导致了在[7]中引入的Elgot单子的概念虽然迭代理论和Elgot monads研究具有有限多个递归变量的递归方程的迭代算子，但完整的Elgot monads [14]为所有（无限和无限）递归方程配备了迭代算子。2预赛我们假设读者熟悉基本范畴理论[21];我们写道：|C|对于范畴C的对象类，f：X→Y对于C中的态射。我们经常忽略索引，例如。自然的变化，如果它们从上下文中很清楚在本文中，我们使用具有有限余积的环境范畴C我们用inl和inr表示从X和Y到X+Y的左和右余积注入，并且[f，g]：X+Y→Z是f：X→Z和g：Y→Z的余积，即唯一态射[f，g]inl=f和[f，g]inr=g。通常，共对角线表示为X= [id，id]：X+X→X我们考虑C上以Kleisli三元组T =（T，η，-η）形式给出的单子，其中T是C上的内映射，|C|，η，称为单子单位，是在上加索引的态射族ηX：X→TX，|C|，并且（Kleisli）提升给每个f：X→TY分配一个态射f：TX→TY，使得以下定律成立：η= id，f η = f，（f g）= fg。这等价于将单子定义为三元组（T，η，μ），三元组由函子T和两个自然变换组成，单子单位η：Id→T和单子乘法μ：TTT [21]。 特别是，给定Kleisli三元组， μ= id产生单子乘法，η扩展到自然变换，T扩展到具有态射映射Tf =（ηf）的 内 函 子。T的Kleisli范畴 CT由Kleisli态射X→TY构成，即 CT（X，Y）= C（X，TY），其中ηX是X上的单位态射和Kleisli复合：给定Kleisli态射f：X→TY和g：Y→TZ，我们有fg=.XfT Y−gsTZ−→Werief：X −n→Y对于Kleisli态射f：X→T Y.从CT到C的遗忘函子有一个左伴随，使任意f：X→Y到f= ηf：X→TY。像任何左伴随一样，这个函子保持上极限，特别是上积。以来|C|为|CT|，这意味着CT中的余积存在，且C T中的余积是独立的。显式y，inl=ηinl：X−n→X+Y，inr=ηinr：Y−n→X+YS. Goncharov等人/理论计算机科学电子笔记325（2016）147151固定点：=自然性：Z=共对角线：=均匀性：=X⇓=Fig. 1. 完备Elgot单子的公理。[f，g] ：A+B−H→C（在C中形成）是f：A−H→C和g：B −H→C在TT中的共射。 We表示byfg：A+B−→AJ+Bj是CT中态射f：A−→AJ和g：B−→BJ的共导。 除了CT之外，我们还考虑了T的（Eilenberg-Moore）代数范畴C T，其对象是对（A，a：TA→A），满足两个定律：aη = id和a（Ta）= aμ，从（A，a）到（A，b）的T -代数态射f是态射f：A→B使得fa= bTf. [21]详情请见。我们将利用关于闭函子的余代数的标准事实[25]。给定一个内函子F：C→C，一个F-余代数是一个对（X，c），其中X是C的一个对象，称为余代数的载体，c：X→FX是一个态射，称为（转移）结构。 从（X，c）到（Y，d）的余代数态射f是态射 f：X→Y，使得df=（Ff）c。余代数和它们的态射形成一个范畴。最终的F-余代数，如果它存在的话，是该范畴中的终端对象，并表示为：νF−−o−ut→F（νF）。根据LambekYXFXYXYFXXFYXFXGYZXFXGXXXGYXXXGYZYXZHGYZXFHYZXFXHYZGZ152S. Goncharov等人/理论计算机科学电子笔记325（2016）147.3用于迭代的完全Elgot单子是[7，8]中Elgot单子的轻微推广，反过来，对于基范畴为Set，它精确地对应于Bloom和E′sik[10]中满足基态射的函子匕首蕴涵的迭代理论在[14]引用的以下定义中（为了简单起见，我们在这里不考虑强单子，因为可能存在的强度对我们的结果没有影响），我们遵循[9，27]的术语，其中在一般参数化递归的对偶设置中考虑了相同的公理定义3.1（完全Elgot单子）一个完全Elgot单子是一个单子T，它配备了一个称为迭代的运算符--<$，它为每个态射f：X−H→Y+X分配一个态射f<$：X−H→Y，使得以下公理成立：fixpoint：f<$=[η，f<$]f，f或任何f：X−→Y+X;自然y：gf<$=（（gη）f）<$，对于任意f：X−→Y+X和g：Y−→Z;codiagonal4：（[η，inr]g）<$=g<$<$对于任意g：X−→（Y+X） +X;均匀y：fh=（ηh）g意味着f<$h=g<$对于任意f：X−→Y+X，g：Z−→Y+Z和h：Z→X。上面的迭代公理可以用一个简单的图表形式表示，如图1所示.这里的反馈循环对应于迭代，彩色框表示正在迭代的构造的范围。我们相信，这种介绍与直觉有着相当好的联系。例如，自然性公理表达了这样一个事实，即迭代的范围可以扩展到包含一个对终止分支的输出进行后处理的函数图1中的公理与图2中的公理[18]第18话被事实上，Hasegawa [16]证明了满足上述公理的匕首运算存在关于一致迹算子w.r.t.副产品（实际上，长谷川在产品的双重设置中工作）。注意，本公理利用了余积注入和余对角态射，而迹公理可以更一般地表示为任何monoidal积。完备Elgot单子的例子的一个标准来源是完备偏序上Kleisli范畴CT的例3.2（ω-连续单子）一个ω-连续单子是一个单子T，使得Kleisli范畴CT在具有底连续和（非严格）连续映射的ω -完全偏序的范畴Cppo上是丰富的;此外，C中的复合需要是左严格的，C中的复合需要是右严格的： f=;等价地，是T的常数。 我们还假设， 在CT中，Cppo-富集; 2因此，在这两种情况下，共传播是单调。因此，它也是连续的，因为i[fi，g]是一个态射[4]共对角公理通常写为（（η）og）<$= g <$<$暗示着规范同构Y+（X+X）<$=（Y+X）+X。S. Goncharov等人/理论计算机科学电子笔记325（2016）147153哪里i[fi，g] = [ifi，g]。同样，第二个论点也显示了一致性-满意;满意;g（.i[fi，g]）i.nl=.ifi和（.i[fi，g]）inr=gby，我不知道。（注意，使用单调性y仅使得[fi，g]形成ω-c链，前提是fi确实如此。在[14]中证明了一个ω-连续单子是一个完备的Elgot单子，其中e<$被计算为映射f<$→[η，f]e的最小不动点。这就产生了幂集单子P、Maybe-单子（-- +1）或不确定状态单子P（-- ×S）S作为集合上的完备Elgot单子的例子。提升单子（--）是完全偏序范畴上的一个完全Elgot单子.另一个例子的主要来源是自由完备的Elgot单子，其中保护态射的迭代是唯一定义的。例3.3（自由完备Elgot单子）假设T是初始完备Elgot单子。在[14]中表明，无论何时由（）定义的函子T存在，它都会产生上的自由完全Elgot单子（注意，原始T是C的初始对象上的常数函子上的自由完全Elgot单子）。在Set中（更一般地，在任何超伸展范畴中[3]），最初的完全Elgot单子T是Maybe-单子-+1。例3.4（Capretta的复单子）一个有启发性的例子，上面的例子没有包括在内，是共代数复单子νγ。-- +γ，由Capretta研究，用于在内涵类型理论[11]中建模。注意，例3.3中没有包含这个例子，因为例3.3只说明了νγ。T（X + γ）是一个完整的Elgot单子，只要T是1（例如，它遵循νγ。X +1 + γ是集合上的完备Elgot单子），但T = Id在任何相关例子中都不是完备Elgot单子。我们猜想T = νγ。-- +γ可以被证明在任何充分丰富的（类型论的）论域上是一个完全的Elgot单子;特别是，这可以在Set中很容易地看到：这里TX显式地求值为X×N+{x}，因此每个TX可以被排序为一个Cppo域，即x±yi =x=y或x=y;这很容易扩展到例3.2中所要求的Cppo-富集，因此在T上产生一个完全的Elgot单子结构。直观地说，每个函数f：X→T（Y+X）要么发散，要么给出一个结果以及计算它所需的步骤数。迭代f†对整个循环中出现的数字求和，在收敛的情况下，将注意，在这个过程中f<$的展开次数对结果没有贡献，这解释了为什么定点恒等式确实对T成立。与以前的工作[14]相比，定义3.1显著地放弃了二元性公理（见图2）。原因是这个公理原来是可推导的，这是最近发现的事实，并在迭代理论的水平上形式化[13]。推论6引自同前。可以用现在的术语表述如下（模术语变化：参数恒等式而不是自然性，双匕首而不是共对角，基本态射的匕首蕴涵而不是一致性）：154S. Goncharov等人/理论计算机科学电子笔记325（2016）147一一=图二. Dinaturality公理命题3.5（Dinaturality）给定g：X−ε→Y+Z和h：Z−ε→Y+X，（[inl，h] g）<$=[η，（[inl，g] h）<$] g。定义3.1中的共对角公理可以等价地用well-kn ownBek i′c恒等式的一种形式来代替，见[10]。命题3.6（Beki′cidentity）一个完备的Elgot单子T是一个满足定点、自然性和一致性公理（如定义3.1）的单子，而Beki′cidentity（Tα[f，g]）<$=[η，h<$]<$[inr，g<$]，其中reg：X −n→（Z+Y）+X，f：Y−n→（Z+Y）+X，h=[η，g<$]f：Y −n→Z+Y，其中α：（A + B）+C→A+（B + C）是明显的结合同构.4完备Elgot代数的参数化单子为了研究完备的Elgot单子和它们的代数，做进一步的抽象步骤并从单子推广到参数化单子[28]是有帮助的（无穷参数化单子也称为基[4]），这是独立的兴趣。定义4.1（参数化单子）C上的参数化单子是从C到C上单子范畴和单子态射的函数 更明确地说，一个参数化单子是一个双函子#：C×C → C，使得对于任何X∈ |C|、--#X：C→C是一个单子，并且对于任何f：X→Y，id#f：Z#X→Z#Y是从-#X到-#Y的单子态射的Z-分量。注4.2X#Y中的参数顺序与[28]和[4]中的不同之处一致，其中使用了与当前X#Y等效的符号YQX我们选择了参数的顺序，以确保与迭代运算符-<$的类型轮廓一致，这反过来又与表达式（）一致在[4]之后，我们将从现在开始表示单子的单位和乘法--#X分别通过uX：A→A#X和mX：（A#X）#X→A#X。例4.3（参数化的monads）我们可以从[28]中回忆一些参数化 monads的标准例子;可以找到更多的例子，例如在[6]中。YXYZXHGYXYYZXZGGHS. Goncharov等人/理论计算机科学电子笔记325（2016）147155一uMmA=T（T（A+<$X）+<$X）−−→T（A+<$X）一一一一一一B(i) 当T=（T，η，--η）是单子且η是函子时，A#X=T（A+ ηX）是参数化单子，单位为X=0。A−in→l然后乘以ηA+ ηXA+X−→T（A+X）X.[id，ηA+<$Xin r]s<$具体地说，如果X是对象E上的常量函子，那么X#Y是例外单子Transformer，例外来自E[22]。另一个有趣的特殊情况是当T是单位单子时（参见。注4.8）。(ii) A#X=A×X是一个参数化的单子，其单位和乘法由下式给出：uX：a<$→（a，ε）和mX：（a，w，v）<$→（a，wv），其中ε表示空单词和单词的wv(iii) 给定一个逆变内函子H，A#X=AHX是一个参数化单子，其单位和乘法由下式给出：uX：a<$→ λx。 a和mX：（f：HX→（HX→A））<$→λx。f（x）（x）.这是著名的读者单子的推广，它可以通过用常数函子实例化H来以下是[4]中研究的基的代数的概念到任意参数化单子的直接扩展。定义4.4（#-代数）给定一个参数化的单子#：C×C→C，一个#-代数是由C的对象A和单子-#A的代数组成的对（A，a），即a态射a：A#A→A满足一AAA#A（A#A）#Aa#idA#AaAaIDAAA#A A#-代数（A，a）和（B，b）之间的态射是C-态射f：A→B使得A#A Af# ffB#B B对于我们的主要例子X#Y=T（X+Y），可以明确地描述#回想一下，Kelly [19]意义下的T-双代数是三元组（A，a，f），其中a：TA→A是T-代数，f：TA→A是A-代数。.156S. Goncharov等人/理论计算机科学电子笔记325（2016）147e†−−−−−→f†e命题4.5设X#Y = T（X +<$Y），对C上的一个单子T和一个函子T。则#-代数恰是T-双代数.草图（Sketch）给定一个#-代数α：T（A+<$A）→A，它形成两个代数结构a=.TA−T−i→nlT（A+<$A）−α→A<$b=。<$A−in→rA+<$AηT（A+<$A）−α→A<$。−→一个简单的计算表明，a是一个T-代数结构，而（A，a，b）是一个T-双代数.相反，给定任何T-双代数a：TA→A←A：b，α=.T（A + A）T [id，b] TA−a→A.另一个简单的计算确定这是一个#-代数的结构。最后，很容易看出，上述两种构造是相互逆的，并推广到#-代数和T-双代数范畴之间的（态射上的恒等式）同构。Q推论4.6对于C上的单子T，设X#Y = T（X + Y）。T -代数的范畴CT同构于那些#-代数a：T（A + A）→A的满子范畴，它们通过T → T（A + A）→TA因式分解.类似于完备Elgot单子，我们引入了带迭代的#-代数。这推广了[5]中函子的完备Elgot代数的定义定义4.7（完备Elgot#-代数）完备Elgot#-代数是#-代数a：A#A→A配备迭代算子e：X→A#Xe†：X→A满足以下公理：解：对于每个e：X→A#X，我们有XeA# Xe†A#e†一一A# A函数性：对于每个e：X→A#X，f：Y→A#X和h：X→Y，X A#XXhA#hYfA#Y隐含hAYS. Goncharov等人/理论计算机科学电子笔记325（2016）147157−→ Y##X.eX−−−−→f h=（id#h）e蕴含f<$h=e<$;复合性：对于每个f：Y→A#Y和g：X→Y#X定义f†·g=（Xgf†id−−−→A#X）和f□g：Y+X→A#（Y+X），[uX，g]f#idY+XYY#X（A#Y）#X（id#inl）#inrA#（Y+X）Y+XA（A#（Y+X））#（Y+X）组合性表示（f□g）<$inr=（f<$·g）<$：X→A。从一个完全Elgot#-代数（A，a，--†）到一个完全Elgot#-代数（B，b，--†）的态射是一个C-态射f：A→B，使得对于所有e：X→A#X，我们有：†−−−→FA−→ B=.X−e→ A #X f #idB#X这定义了完备Elgot#-代数CElg#（C）的范畴注4.8注意，参数化单子A#X=A+<$X（即例4.3（i）中的参数化单子，T是单位单子）的完备Elgot#-代数正是[5]中引入和研究的函子<$的完备Elgot代数。与完全Elgot单子的情况类似，获得完全Elgot#-代数的标准方法例4.9（连续代数是完备Elgot代数）考虑任何范畴C，它在Cppo上是丰富的，使得复合是左严格的，即f=f，以及一个参数化单子#：C×C→C，它在这两个论点，即.i（fi#gi）=. .ifin#。.igi对任意ω-链（fi：X→Y）i ω和（gi：XJ→YJ）i ω成立.然后，当赋予每个e：X→A#X一个最小解时，每个#-代数就成为完备Elgot#-代数更详细地说，设A是一个#-代数。对于每一个e：X→A#X，我们指派e<$：X→A，由下式给出：e†=.我也是，其中e<$0=x：X→A且ei+1=a（id #e<$i）e。 这意味着e†是函数s<$→a（id#s）e在C（X，A）上的最小不动点。这一验证表明，M158S. Goncharov等人/理论计算机科学电子笔记325（2016）147×⊥−−→满足一个完整的Elgot代数的公理可以在我们的论文的完整版本中找到。例4.10前面的例子可以很容易地归纳如下。设#是任意范畴C上的参数化单子。设a：A#A→A是一个#-代数，使得(i) 对于每个对象X，C（X，A）是一个具有π的cpo(ii) 对于每个态射g：X→Y，映射C（g，A）：C（Y，A）→C（X，A），f> →fg是连续的，(iii) 映射f<$→a（id#f）是C（X，A）上的连续映射那么很明显，对于每个e：X→A#X，最小解e<$ 是存在的;事实上，映射s<$→a（id#s）e在C（X，A）上是连续的。最小解的赋值e<$→e<$使得A成为一个完备的Elgot代数。这个事实的证明与前面例子的证明注意，如果C=Set且A是一个具有π的cpo，则C（X，A）具有逐点cpo结构，然后条件（i）和（ii）自动遵循为 了 说 明 的 目 的 ， 我 们 继 续 描 述 这 个 场 景 的 一 个 具 体 实 例 。 设X#Y=X+Y×Y，C=Set。 设S是一个集合，令SJ=S+{0，j}。然后（SJ，seq or：SJ+SJ×SJ→SJ）是一个在下列赋值下的#seq or（x）= xs e q or（x，x）=seq or（s，x）= sseq或（0，x）=x，其中s∈S。此外，SJ具有双原子cpo结构，即，x±yix= 0或x = y，并且seq或是连续的。当然，所有的hom-setC（X，SJ）都是在逐点顺序下，cpos，然后很容易看到我们上面的三个条件都满足;对于条件（iii），我们使用SJ+SJSJ也是cpo（没有底部），并且seq or显然是连续的。因此SJ是一个完备的Elgot#-代数.假设我们在S上有一个谓词p：S→2和一个函数f：X→S+X×X表示节点集X上的一个图（其中每个顶点要么有两个向外的转移，要么没有，并在S中标记）。让p？：S→SJ可以由p定义吗？（s）=s如果p（s）= 1和p？（s）= 0，否则考虑映射g=.Xfp？+ IDS+X×X−→SJ+ X×X由于g：X→SJ#X，我们得到函数g<$：X→SJ，它从给定顶点开始对满足p的S的第一个元素执行深度优先搜索 SJ的结果可以解释如下：如果找到元素，则返回s∈S，如果没有找到元素，则返回0，表示发散。在给出完备Elgot代数的特征之后，我们在例5.8S. Goncharov等人/理论计算机科学电子笔记325（2016）147159一Σ注意，我们并不要求完备Elgot#-代数的态射是#-代数的态射。事实上，这是自动发生的。命题4.11设f：A→B是一个完全Elgot#-代数态射，（A，a，--t）到（B，b，--t）。 则f是# -代数的态射。草图（Sketch）其思想是将a表示为在第一次迭代后终止的循环，然后从定义所保证的f对迭代的保持推导出f对a的保持更具体地说，我们e=（id#inr）[id，uA]：（A#A）+A→A#（（A#A）+A）并证明et=[a，id]。剩下的证明等于导出b（f#f）=f a由fet=（（f#id）e）Q5作为单子代数的完备Elgot代数在这一节中，我们证明了完备Elgot#-代数可以精确地被认为是#上广义余代数选择单子的Eilenberg-Moore代数，我们将在下面介绍回想一下，Uustalu [28]表明，参数化的monads至少以两种不同的方式产生monads：命题5.1假设#是C上的参数化单子，使得最小定点μγ。X#γ（最大定点νγ。X# γ）对每个X∈|C|.然后是μγ。--#γ（νγ. --#γ）是monad的底层函子。注5.2对于参数化单子X#Y=T（X+Y），众所周知，TμX = μγ。 T（X + γ）是单子Tμ的对象映射（实际上，Tμ是单子T的余积Σ Σamd上的自由单子，见[17]）。下面我们将主要关注在μ被ν代替的情况下，即，（）的单子T已知初始代数μγ. X#γ携带X上的自由#-代数;相反，自由#-代数是初始（X#--）-代数（见[6，定理2.18]）。这里我们感兴趣的是最终余代数νγ。X# γ。本节的目标之一是证明final（X#--）-余代数携带X上的自由完备Elgot#-代数，反过来，假设X上有一个自由完备Elgot#-代数，它的载体是final（X#--）-余代数（见推论5.10）。从现在开始，我们假设最终余代数νγ。 X #γ存在，记为J#X（省略X的结构态射：J#X → X #J#X）。回想一下，coitf：X→J#Y是由余代数（X，f：X→Y#X）诱导的唯一最终态射在[28]之后，为了介绍和推理J#的单子结构，我们使用了一个更灵活的原始共递归原理，它来自于coit中体现的标准共迭代原理。160S. Goncharov等人/理论计算机科学电子笔记325（2016）147一YX命题5.3（[28]）对任何具有最终余代数νF的内函子F，以及任何f：X→F（νF+ X），存在唯一态射h：X→νF满足outh = F [id，h] f。命题5.3中的态射h可以说是由本原上递归定义的。在J#的特殊情况下，我们使用原始的corecursion来稍微推广coit构造：引理5.4对任意e：X→B#X和f：B→A#J#A，存在唯一态射h满足XHJ#Ae出来B#XM|#A（f#h）A#J #A。（一）对于任何e：X→B#X和f：B→A#J#A，我们表示为：coit（e，f）：X−→J#A唯一h使图（1）可交换。使用（1），J#上的单子结构可以如下给出：ην=out-1uJ#X=coituXXxXf=coit（（f#id）out，out）其中f：X→J#Y这也定义了μν=id=coit（out，out）。注意，根据引理5.4，f是满足以下等式outf=mJ#Y（out f#f）out.（二）引理5.5设e：X→B#X和f：B→A#J#A。 然后coit（e，f）=（out-1f）（coit e）.作为引理5.5的一个简单推论，我们得到coite=coit（e，uJ#X）;实际上，有coit（e，uJ#X）=（ou t-1uJ#X）（coite）=（ην）（coite）=coite.X xX我们在下面的引理中陈述另一个有用的性质：引理5.6设e：X→B#X和g：B→C。然后J#g（coit e）= coit（（g #id）e）。下面的定理是我们的第一个主要结果。建立了完备Elgot#-代数与J#-代数的等价关系。S. Goncharov等人/理论计算机科学电子笔记325（2016）147161一→一Y一Y定理5.7对任意参数化单子#：C × C → C，J#= νγ的Eilenberg-Moore代数。--γ是完备Elgot代数。更准确地说，CJ#和CElg#（C）是同构的C原子，由以下构造证明（在两个方向上，态射都映射到它们自己）：CJ#→C elg#（C）：对于J#-代数a（A，χ：J#A→A），我们定义了一个#-代数a（A，χout-1（id# ην）：A#A→A，--χ），其中对任意e：X → A #X，et= χ（coite）：X→A.CElg#（C）→CJ#：对于a#-代数a（A，a：A#A→A，--<$）我们定义一个J#-代数（A，out<$：J#A → A）.（S ket ch）的Pr。 从CJ#到CElg#（C）的方向上，给出了完备Elgot #-代数的公理.最困难的情况是组成同一性.我们一方面有（f<$·g）<$=χcoit（f<$·g）=χcoit（（χ（coitf）#id）g）=χcoit（（χ#id）（（coitf）#id）g）=χ（J#χ）coit（（（coitf）#id）g）//引理5.6=χ μνcoit（coitf）#id）g）//χ是J#-代数=χcoit（coitf）#id）g，out），//引理5.5另一方面，根据定义，（f □ g）<$inr = χ coit（mY+ X（id #inl）f）#inr）[uX，g]）inr。让我们用h表示mY+ X（id#inl）f）#inr）[uX，g]。根据引理5.4，为了显示出（coith）in r =mJ#A（out #（（coith）in r））（coitf#id）g. 后者很容易从辅助方程（coit h）inl = coit f得到，其证明是一个例行程序。在从CElg#（C）到CJ#的方向上，我们对Eilenberg-Moore代数的两个顶点进行了迭代.较难的一个是out<$J#（out<$）=out <$μν，它是从组合性的实例（out □out）<$inr =（out <$·out）<$$>通过建立ou t<$[id，μν] =（out □out）<$和ou t<$J#（ou t<$） =（ou t<$·out）<$ 而获得的。 进一步的计算保证了CElg#（C）和CJ#之间的对应是函式的，而且是同构的。Q让我们重新讨论例4 - 10来说明定理5 - 7。例5.8回想一下，我们考虑参数化单子X#Y = X + Y ×Y，使得J#X是其叶子被标记在X中的有限和无限二叉树的集合。（SJ，seq or：SJ+SJ×SJ→SJ，--†）是一个#-代数的事实等价地意味着SJ是一个J#-代数。具体地，J#-代数结构是函数Seq或：J#SJSJ，其将SJ上的给定二叉树变换为SJ的单个元素，该单个元素通过使用深度优先搜索策略寻找由S标记的给定树的第一叶来计算：在成功的情况下，答案在S中，162S. Goncharov等人/理论计算机科学电子笔记325（2016）147XJ#否则，答案是0∈SJ，这意味着没有发现来自S的元素，并且在发散的情况下是0（即，在检测到来自S的还要注意，任何函数f：X→S+X×X=S#X都表示一个如例4.10所述的图形。唯一映射coitf：X→J#S到最终余代数，然后计算每个节点x∈X的树展开。现在，从谓词p：S→2开始，例4.10中定义的函数g<$：X→SJ等于组合科伊特fXJ#（p？）J序列或J−−−−−−→#S−→J#S−−→S实际上，根据定理5.7，gt=Seq或（coitg）=Seq或coit（（p？+id）f），其余的由引理5.6得出。我们的目标是证明最终余代数νγ。等价地，X# γ是自由完备Elgot #-代数。事实上，给定一个最终的（X#--）-余代数出X：J#X → X #J#X，由定理5.7（的证明）得出J#X携带X上的自由J#-代数，因此它携带X上的自由完备Elgot#-代数（因为范畴的同构保持了代数的自由性）。不难看出，下列态射出来#idm|#X输出-1和J#X#J#XX（X#J#X）#J#XXX#J#XXJ#Xu|#XXX#J#X外t-1J#X构造了X上的自由完备Elgot代数的代数结构和泛态射。J#Y上的迭代算子如下获得。给定e：X→J#Y#X，则形成以下余代数c：J#Y+X→Y#（J#Y+X），Y编号--：J#Y+XX|#Y ，e]J#Y#XM|#Y+ Xout#id（Y#J#Y）#X（id#inl）#inrY#（J#Y+X）Y然后我们把e†=（coitc）代入r中。（Y#（J#Y+X））#（J#Y+X）相反，我们有以下结果。定理5.9设ηX：FX#FX→FX与ηX：X→FX构成X上的自由完备Elgot#-代数。然后X#FXηX#idXFX FX FX是一个同构，它的逆是最终（X #--）-余代数的结构.X[uS. Goncharov等人/理论计算机科学电子笔记325（2016）147163Y#Y#FY−−−−→FY最终（X#--）-余代数与自由完备El
我的内容管理
展开
