递归方程联合巴特·雅各布斯的共归纳解方法及其特例的研究

理论计算机科学电子笔记106（2004）145-166www.elsevier.com/locate/entcs递归方程巴特·雅各布斯奈梅亨大学计算机科学系P.O. Box 9010，6500 GL Nijmegen，The Netherlands电子邮箱：mailto：bart@cs. 坤nlURL：http：//www. CS. 坤nl/~bart摘要本文证明了[2，12]中求无穷项方程的共归纳解的方法是[4]中利用分配律的更一般的最近方法的一个特例。关键词：余归纳，余代数，递归方程。1介绍余代数理论中的最终性原理通常被称为余诱导[8]。它涉及到最终余代数的适当余代数同胚的存在性和唯一性。人们很早就认识到（见[1，5]），这种共归纳得到的同态可以理解为递归（或共递归，如果你喜欢）方程的解。方程本身被包含在交换方中，表示我们有一个从某个“源”余代数到最终余代数的同态由于这个图是由源余代数产生的，所以这个源也可以用递归方程来识别。对这类方程的解的系统研究首先出现在[12]中，然后是[2]。他们的共代数方法简化了[6，7]中无穷项递归方程的结果。最近，在[4]中提出了一种基于分配律的一般抽象方法。本文的结论是，它表明了[2]的方法如何用于无限大1571-0661 © 2004由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.02.032146B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145→、、在[4]的一般方法中，项与分配律相适应。这涉及到在底层接口函子上识别项单子的适当分配律。本文件的结构如下。第二节简要回顾了[4]基于分布律的方法。第三节介绍了与函子F有关的规范单子的两个分配律。然后在第4节中解释[2]中求解无穷项方程的方法。最后，第5节展示了这种方法是基于分布的方法的一个实例。2分配律与方程分布律在余代数领域的第一个重要应用是图里和普洛特金的工作[15]（参见[14]），提供了运算语义和指称语义的联合在这种情况下，分配律提供了句法和动态之间的适当兼容形式。它导致这样的结果：双相似性是一个同余，其中，当然，双相似性是等价的共代数概念，同余和代数概念。[15]中关于分配律对应于算子的适当规则格式的主张在[4]中得到了进一步的证实。在余归纳法的扩展形式中使用分配律（从而求解方程）的思想来自[9]，并在[4]中得到进一步发展。在本节中，我们介绍其要点。分配律是范畴C上两个内函子F，G：C→C之间的自然变换FG<$GF.这些F和G可能有额外的结构（点或余点，或单子或共单子，见[10]），然后必须由分配律保存。我们将集中讨论单子在函子上分布的情况，因为它似乎是最常见和最自然的--参见下一节的例子。我们将回顾这意味着什么。定义2.1设（T，η，μ）是范畴C上的单子，F：C C是任意函子。T在F上的分配律是一个自然变换T FλzFT使得对于每个X∈C，下面的两个图可交换。T（λX）λTXFX，F，（ηX）T2FXTFTXFT2XηFX、、、J，zµFX JF（µX）JTFXλXFTX TFXXFTX、、λB. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145147⇒−→，，FZ−→其基本思想是，单子T以某种语法描述了这些项，而函子F是状态空间上转换的接口。直觉上，分配律的存在告诉我们，术语和行为适当地相互作用。模型的相关概念是所谓的λ-双代数.定义2.2设λ：TF=FT是一个分配律，如上所述。一个λ-双代数由一个对象X∈C和一对映射组成：TX aXb、F、X其中：• a是一个Eilenberg-Moore代数，这意味着它满足两个方程，即：anX=id和aµX= a T（a）。• a和b通过λ是兼容的，这意味着下图是可互换的。TXaXT（b）bFX，，F（a）JTFXλXFTX一类λ-双几何的映射，from（TX−→aX−→bFX）too（TY−→cY−→FY）是C中的映射f：X→Y，它既是代数的映射又是余代数的映射：f<$a = c <$T（f）和d <$f = F（f）<$b。以下结果是标准的。Lemma2. 3假设分布律为λ：T FF T，设λ：Zλ=FZ是一个最终余代数。它携带一个Eilenberg-Moore代数获得finality在：F（α）自贸区_ - -- -我是，，λZTF，Z，T（）=TZ____α__=_ _Z产生的p空气（TZ−α→ZFZ）则是一个最终的λ-双代数。通过唯一性证明了α是一个Eilenberg-Moore代数。通过构造，α和λ通过λ相容。设任意λ-双代数（TX−→aX−→FX）。它诱导出唯一的余代数映射f：X→Z，DB148B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145QFY−→一BTFTXF TXFT2X一Bf=F（f）然后通过证明两个映射都是从余代数λX<$T（b）：TX→FTX到最终余代数λ X的同态，得到f <$a = α <$T（f）。下面的方程和解的概念来自[4]。定义2.4假设一个分配律λ：TFFT。一个守护递归方程是FT-余代数e：X→FTX. 解决这种λ-双代数（TY-→Y-→FY）中的方程是一个映射f：X→Y，使得下图为通勤。F T XFT（f）FTY、、F（a）（一）eJ，，BXfY在普通的余归纳法中，人们得到了方程X→FX的解。上述等式X→FTX概念的力量在于它允许条件作用。为方便起见，我们通常称这些方程为X→FTX λ-方程--尽管它们的表述不涉及分配律λ。但它们的预期用途是在分配律的背景下。这个解的概念一开始可能看起来有点奇怪，但根据下面的结果就变得更自然了。在[4]中，它是隐式的。命题2.5λ-方程之间存在双射对应e：X→FT X和λ-双代数为（T2XμXTX−→dFT X）withf reealgebra aµX。设（TY−→Y−→FY）是λ-双代数。然后有一个对于相关的λ -方程和λ -双代数，证明了（1）中的解f：X→Y与双代数映射g：TX→Y-之间的双射对应.证明给定λ-方程e：X→FTX，我们定义e=.TXT（e）λTXF（µX）B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145149这与自由代数μX：T2X→TX一起产生λ-双代数：F（μX）<$λTX<$T（e）=F（μX）<$λTX <$T（F（μX）<$λTX<$T（e））=F（µX）FT（µX）λT2XT（λTX）T2（五）=F（μX）<$F（μTX）<$λT2X<$T（λTX）<$T=F（µX）λTXµFTXT2（e）=F（µX）λTXT（e）µX=eµX。（五）反之，给定一个λ-双代数（T2X方程：TX−→dFTX），我们定义λ-d=.XηX TX dFTX这些运算e<$→e和d<$→d彼此是逆运算：e=eηX=F（μX）λTXλT（e）ληX=F（μX）λTXληFTXεe=F（µX）F（ηTX）e=e。d=F（μX）λTXλT（d）=F（μX）λTXλT（dληX）=dµXT（ηX）=d。现在假设f：X→Y，其中e：X→FT X类似于（1）。我们取f = a T（f）：TX → Y。 它形成了一个λ-双代数的映射，从（μX，e）2µX−→150B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145→→→ → →→至（a，b）：aT（f）=aT（aT（f））=aµYT2（f）=aT（f）µX= fµX。F（f）<$e=F（a<$T（f））<$F（μX）<$λTX<$T（e）=F（a）<$F（μX）<$FT2（f）<$λTX<$T（e）=F（a）<$FT（a）<$FT2（f）<$λTX<$T（e）=F（a）<$λY<$TF（a）<$TFT（f）<$T（e）=F（a）<$λY<$T（b）<$T（f）=baT（f）= bf.本文证明了一个λ-双代数映射g：TX→Yfromm（μX，d）too（a，b）. 它产生一个映射g=gηX：X→Y，它是d的解，因为：F（a）FT（g）d=F（a）FT（gηX）dηX=F（g）<$F（μX）<$FT（ηX）<$d <$ηX=F（g）dηX=bgηX=b g.最后，很明显f<$→f和g<$→g是彼此的逆。Q现在我们可以用公式表示这种基于分布的方法求解方程的主要结果。定理2.6设F：C→C是一个函子，其最终余代数Z−=Z→FZ。 对于每个具有分配律λ：TF <$FT的单子T，存在唯一的由引理2.3得到最终λ-双代数（TZ Z FZ）中λ -方程的解。证明对于λ-方程e：X→FTX，在（TZ→Z→FZ）中的解为：前一命题与λ-双代数的映射从相关联的（ T2X T X ）FTX）至（TZZFZ）。 既然后者是最终的，那么就只有一个这样的解决方案。Q在下一节的例3.3中，我们将给出一个示例。B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145151→→∈ −→______3自由单子及其分配律在这一节中，我们考虑一个内函子F：C C，它具有两个典型的结合单子F_∞和F_∞，以及F上的分配律λ_∞和λ_∞。第一个结果并不直接使用，但提供了第二个结果的设置--这构成了后面引理5.1的基础。3.1函子上的自由单子设F：C C是范畴C上的任意闭函子，其上积为（二元）余积+.我们在这个阶段所做的唯一假设是，对于每个对象X，C++F（）：C C有一个初始代数。 我们将使用以下符号。这个初始代数的载体将被写为F（X），其结构映射给出为：X+F（F<$（X））αF<$（X）=此外，我们将写所以αX=[ηX，τX]。ηX=ακ1τX=ακ2，映射X<$→F<$（X）是函子的：对于f：X→Y，我们得到：X+F（F（X））id+F（F（f））X+F（F（Y））αX=FJ[ηYf，τY]FJ（X）（Y）F（f）这意味着F<$（f）<$ηX=ηY<$fF<$（f）<$τX=τY<$F（F<$（f）），也就是说，η：id<$F<$和τ：FF<$$>F<$是自然变换。接下来我们确定F是单子。乘法μ被获得在：F（X）+F（F（F（X）αF<$（X）<$=id +F（μX）F（X）+F（F（X））[id，τX]F（FJJ_ _F（X））µX（X）152B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145→⇒⇒⇒⇒∼这 就 产 生 了 一 个 单 子 方 程 ， 即 μX<$ηF<$ （ X ） = id 。 相 关 的 方 程μX<$F<$（ηX）= id由代数映射αX→αX的唯一性得出：μX<$F<$（ηX） <$αX=μX<$[ηF<$（X）<$ηX，τF<$（X）]<$（id+F（F<$（ηX）=[ηX，τX<$F（μX）]<$（id+F（F<$（ηX）=αX<$（id + F（μX<$F <$（ηX）。同样地，得到了使F_n为单子的其它条件以下标准结果概括了这种情况。命题3.1设F：CC与诱导单子（F，η，μ）如上所述。(i) 映射X<$→（F（F<$（X）-τ→X遗忘函子U：Alg（F）→ C.F（X））形成一个左伴随的由这个附加物诱导的单子是（F，η，μ）。(ii) 映射σX=τX<$F（ηX）：F（X）→F<$（X）产生一个自然变换F <$F<$，使F<$成为F上的自由单子。Q接下来的观察表明，（有限）F-项的单子F与F的行为相适应。从一般的观察（例如在[ 4 ]中所作的观察）可以得出，分配律F<$G GF<$对应于普通的自然变换FG GF。因此，通过取G=F和恒等式FF FF，得到F<$F FF<$。但在这里，我们将提出明确的建设。命题3.2设F：C→C有自由单子F。然后有一个分布律λ：F。我们定义了λX：F（FX）→F（FX）。α−1[F（ηX），F（μX<$F<$（σX））]F（FX）FXFX+F（F（FX））F（FX）=其中σX=τX<$F（ηX）：F（X）→F<$（X）如命题3.1（ii）中所介绍的。Q例3.3令Z = RN是实数流的集合。它当然是函子F = R×（−）的最终余代数，通过头和尾运算hd，tl：Z−=→R×Z。在[13]中显示，在这种情况下，可共归纳地定义二元算子，其中，对和为n，对乘积为B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145153××公司 简介⊕×××R× R（Z）×× −⊕×满足递归方程：x<$y=（hd（x）+hd（y））·（tl（x）<$tl（y））x<$y=（hd（x）×hd（y））·（（tl（x）<$y）<$（x<$tl（y），其中·是前缀。很容易看出，我们用普通的余归纳法来定义，在：R（ZZ），，cID- -，，=Z×Z_ - -Z其中，余代数c_n定义为：c（x，y）= hd（x）+hd（y），tl（x），tl（y）.一旦我们有了λ：Z × Z → Z，我们就展示了如何获得x λ y作为λ -方程的解。我们从签名函子<$（X）= X×X开始，有一个明显的分配律<$F<$F<$由（<$r，x<$，<$s，y<$）<$−→ <$r + s，（x，y）<$给出。通过[ 4 ]的结果，它提升到一个分配律λ：FF，涉及如下-自由单子叶植物。 代数：（Z）→ Z产生一个Eilenberg-Moore代数[[−]]：（Z）→Z，这与[ 4 ]的结果相同，是一个λ-双代数。 现在，我们得到的解决方案：R（Z），，id（）___dRID[[]]JZ，，=Z×Z_Z_______________________其中λ-方程d由下式定义d（x，y）=hd（x）×hd（y），（tl（x），y）（x，tl（y）），哪里在术语语言中，是表示从Z开始的对的和的符号Z.在这里，我们利用了λ方法的表达能力，因为我们现在可以将项写为第二个分量。显然，hd（x <$y）= hd（x）× hd（y）。154B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145→并根据要求：tl（x<$y）=（[−]]<$（）<$π2<$d <$）（x，y）=（[−]]（））（tl（x），y）（x，tl（y））=[[（tl（x）<$y）<$（x<$tl（y））]=（tl（x）<$y）<$（x <$tl（y））。示例到此结束3.2函子上的自由迭代单子与前一节一样，设F：C C是范畴C上的任意闭函子，其上有（二元）余积+。我们现在假设对于每个对象X∈C，函子X+F（−）：C→C有一个最终余代数-而不是初始代数。我们将使用以下符号。这个最终代数的载体将被写为F∞（X），结构图给出为：F∞（X）<$X+F（F∞（X））=前一节中的集合F（X）被理解为具有来自X的自由变量的F型有限项的集合。这里我们将F∞（X）理解为X中具有自由变量的有限项和无限项（或树）的集合。像以前一样，我们应该写：ηX=<$−1 <$κ1τX=<$−1 <$κ2。F∞的泛函性如下所示。对于f：X→Y在C中，我们得到：Y+F（F∞（X））id+F（F∞（f））X+F（F∞（Y）），，f+idX- -- -- -我是，，=F∞（X）F∞（Y）F∞（f）这意味着F∞（f）<$ηX=ηY<$fF∞（f）<$τX=τY<$F（F∞（f）），即η：id<$F∞和τ：FF∞<$F∞是自然变换。B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145155→→→→∈∈Y∞Y+F（F（Y））在[11，3]中证明了F∞是单子1。乘法运算μ相当复杂，最好通过代入t[s/x]来引入。 我们的意思是替换变量x在项t中由项s表示，但现在可能是有限项。在大多数一般的函数中，这个子s_t[→−s/→−x]表示所有vari的所有发生。x∈X同时。 通过这种方式，替换可以被描述为一种运算，该运算告诉项sxF∞（Y）的X索引集合（sx）x∈X如何作用于项t F∞（X）。更准确地说，替换变成了函数s：XF∞（Y）的运算subst（s）：F∞（X）F∞（Y）。像往常一样，这样的替换操作应该尊重期限结构-即。 被一个同态-并且对变量是平凡的。标准地说，替代是通过对（有限）项结构的归纳来定义的。但是，由于我们在这里处理的是有限条件下的可能，我们必须使用共归纳。这使得替代更具挑战性。一般来说，它是这样做的。引理3.4设X，Y是任意集合.每个函数s：X F∞（Y）产生一个余代数替换算子subst（s）：F∞（X）F∞（Y），即F -代数的唯一同态：F（F∞（XF（subst（s））（F∞（Y））））FX，，sτXτYJ J与ηX，J，zF∞（X）F∞（Y）F∞（X）F∞（Y）subst（s）subst（s）证明我们首先定义余积F∞（Y）+F∞（X）的项，即作为左下方的垂直合数。Y+F（F∞（Y）+F∞（X）），，id+F（f）_ __，，[(idY+F（κ1））Y，κ2F（κ2）]F∞（Y）+F（F∞（X）），，[κ1，s+id]F∞（Y）+（X+F（F∞（X），，IDY +X=F∞（Y）+F∞（X）F∞（Y）F[1][2]对函数X<$→F（X+−），得到了一个类似的结果.156B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145→首先利用余代数映射的唯一性证明了f∈κ1是恒等式→然后，fκ2是所需的映射subst（s）。Q在本文的其余部分，我们将经常使用这个子化算子subst（-）。有了下面的基本结果，代入的计算就容易得多了。证明是通过替换的唯一性。引理3.5对于s：X→F∞（Y），我们有：(i) subst（ηX）= idF（X）.(ii) subst（s）<$F ∞（f）= subst（s <$f），其中f：Z → X.(iii) subst（r）<$subst（s）= subst（subst（r）<$s），其中r：Y → F ∞（Z）.(iv) F∞（f）=subst（ηZ<$f），对于f：Y→Z，因此subst（F∞（f）<$s）=F∞（f）subst（s）.(v) subst（s）=[s，τYX。Q命题3.6映射μX=subst（idF∞（X））：F∞（F∞（X））F∞（X）使三元组（F ∞，η，μ）成为单子。这个单子F ∞通过自然变换σ = τ<$Fη：F<$F ∞称为F上的迭代单子。文[2]证明了在适当的意义下，F∞实际上是一个自由这种自由与此无关。证明我们使用引理3.5检查单子方程。µX<$ηF∞X=subst（idF∞（X））<$ηF∞X= id F∞（X）。µX<$F∞（ηX）=subst（idF∞（X））<$F∞（ηX）=subst（idF∞（X）<$ηX）= id F∞（X）。µX<$F∞（µX）=subst（idF∞（X））<$F∞（µX）=subst（µX）=subst（subst（idF∞（X））_idF∞（F∞（X））=subst（idF∞（X））subst（idF∞（F∞（X）= µ X <$µF ∞（X）。Q以下是不太标准的。B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145157⇒∼FF◦→FF命题3.7考虑F：C→C及其迭代单子F ∞。(i) 有一个分配律λ∞：F∞F<$FF∞。(ii) 单子F <$F∞的诱导中介映射与分配律交换，在下面的图交换的意义上。FFλF∞Fλ∞JJ∞对于λ定义为λ∞X：F∞（FX）→F（F∞X），公式如下：F∞（FX）FX=FX+F（F∞（FX））[F（ηX），F（μX<$F∞（σX））]F（F∞X）其中σX=τXF（ηX）：F（X）F∞（X）如命题3.6中引入的。它满足，就像在命题3.2的证明中，µX<$σF∞X=subst（idF∞X）<$τF∞X<$F（ηF∞X）（二）然后又道：=τX<$F（subst（idF∞X））<$F（ηF∞X）=τX<$F（idF∞X）=τX。λ∞X<$ηFX=[F（ηX）， F（μX<$F∞（σX））]<$$><$ηFX=[F（ηX），F（μX<$F∞（σX））]<$κ1= F（ηX）。我们将使用以下两个辅助结果：（三）µX<$σF∞X<$λ∞X=µX<$F∞（σX）F（τX）<$F（λ∞X）=λ∞X <$τFX.我们首先证明第一个方程，然后立即用它来证明第二个方程。158B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145一个.µX<$σF∞X<$λ∞X=[µX <$σF∞X<$F（ηX），µX<$σF∞X<$F（µX<$F∞（σX））]FX=[µX<$F∞（ηX）<$σX，µX<$F∞（µX<$F∞（σX））<$σF∞FX]<$FX=[µX <$ηF∞X<$σX，µX<$µF∞X<$F ∞F∞（σX）<$σF∞FX]= [µX<$F∞（σX）<$ηFX，µX<$F∞（σX）<$µFX<$σF∞FX]<$FX=µX<$F∞（σX）<$[ηFX，τFX]<$FX=µX<$F ∞（σX）。F（τX）<$F（λ∞X）（2）∞=F（μX<$σF∞X<$λX）=F（μX<$F∞（σX））=[F（ηX），F（μX<$F∞（σX））]<$κ2=λ∞X <$τFX.现在我们准备证明λ∞与乘法交换。λ∞XμFX=λ∞XF∞FXby引理a3.5（v）=[λ∞X，λ∞X<$τFX<$F（μFX）]<$F∞FX（3）∞ ∞= [λX，F（τX <$λX [F∞FX）]（2）∞ ∞= [λX，F（μX<$σF∞X<$λX <$μFX）]<$λF∞FX（3）∞ ∞= [λX，F（µX<$F（σX）μFX）]F∞FX=[λ∞X， F（µXF∞FX=[λ∞X， F（μXF∞FX（3） ∞=[λX，F（μXF∞FX=[id， F（µXF∞FX=F（μX）<$[ F（ηF∞X）， F（μF∞X<$F∞（σF∞X））]<$$>F F∞X<$F∞（λ∞X）=F（μX）<$λ∞F∞X<$F∞（λ∞X）。为了证明这个命题的第二点，我们不得不对这个符号进行解释。让诱导中介B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145159X∞X+F（F X）◦FXFXFXFXX∞ →→XXFXXXXFX映射σ∞：FF∞则由下式给出：X+F（F<$X）id +F（σ∞）___αX=J，，=F∞XF X_ _ _______ _σ∞X我们已经知道（从命题3.1），σ∞是满足σ∞σ∞= σ∞的单子的同态。因此，σ∞与分配律交换：λ∞X<$σ∞FX=[F（ηX∞）， F（μ∞X<$F∞（σX∞））]<$$>FX<$σ∞FX=[F（ηX∞）， F（μ∞X<$F∞（σX∞））]id+F（σ∞FX）<$α−1=[F（η∞），F（μ∞<$F∞（σ∞）<$σ∞FX）]<$α−1=[F（ηX∞）， F（μ∞X<$σ∞F∞X<$F<$（σX∞））]<$α−1=[F（η∞），F（μ∞<$σ∞F∞X<$F<$（σ∞X<$σ <$））]<$α−1=[F（σ∞X<$ηX<$）， F（σ∞X<$µ$>X<$F<$（σX<$））]<$α−1=F（σ∞X）<$[F（ηX<$）， F（μ<$X<$F<$（σX<$））]<$α−1=F（σ∞X）<$λ<$X。Q4方程的迭代解法本节中的材料（再次）来自[2]。在定义2.4中，我们看到了λ-方程和解的抽象概念。 更具体地说，对于函子F，一组递归方程（通常简称为递归方程）首先由一组递归变量X组成。对于每个变量x∈X，我们在方程x=t中有一个对应的项t。 我们将允许这个术语是无限的。项t可以涉及来自已经给定的集合Y的变量和来自我们的递归变量的X. 因 此 t∈F∞ （ Y+X ） 。 总 而 言 之 ， 递 归 方 程 是 映 射 e ： X→F∞（Y+X ）。我们通常称这样的e 为∞-方程，与定义2.4 中的λ-方程X→FTX-相反。定义4.1设F：C→C是函子，对X∈C有一个最终余代数F∞（X）−∞=→X+F（F∞（X））.方程e：X F∞（Y+X）的解是映射sol（e）：XF∞（Y），为每个递归变量产生适当的项sol（e）（x）160B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145∈→∞∞→、、Y+Xζ−xX.这意味着将余元组[ηY，sol（e）]：Y + XF ∞（Y）在e中得到溶液sol（e），即X，，eF∞（Y+X）溶胶......在，subst（[ηY，sol（e）]）=subst（[ηY，sol（e）]）溶胶，zJF∞（Y）这表明解是subst（[ηY，−]）ε的不动点。与λ-方程一样，我们感兴趣的是λ-方程的唯一解。他们总是存在吗？而不是像x=x这样的简单方程，其中任何项都是解。这样的方程被排除在外，因为要求递归方程的项是这个概念也可以在一般的范畴设置中表达：- 方程e：X F∞（Y+X）被称为保护的，如果它的因素（在一个必然独特的方式）为：（四）Y+F（F∞（Y+X）），，，gκ1+id。，J。（Y + X）+F（F∞（Y + X））=XF∞（YJ）e+X这就是说，如果我们使用最终余代数映射分解e的项，那么我们不会从X得到变量。定理4.2（[2]）每个守护∞-方程都有唯一解。证明假设一个保护的∞-方程e：X→F∞（Y+X）因子为1Y+X◦ （κ1+id）∈ g，对于映射g：X→Y+F（F∞（Y+X）），如（4）中所示.为了找到一个解决方案，首先定义，如引理3.4的证明，一个辅助映射h：F∞（Y+X）+F∞（Y）→F∞（Y），通过一个B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145161Y∞Y+F（F（Y））→XX在下面的左手边的适当结构图。Y+F（F∞（Y+X）+F∞（Y）），，[id+F（κ1），（id+F（κ2））id +F（h）- -，，（Y+F（F∞（Y+X）+F∞（Y），，[[κ1，g]，κ2]+ id（（Y+X）+F（F∞（Y+X）+F∞（Y），，Y+X+ id=F∞（Y+X）+F∞（Y）F∞（Y）H然后证明h<$κ2是恒等式，并且h<$κ1的形式为subst（k），其中k：Y+X→F∞（Y）。然后得到唯一解为sol（e）=kκ2。Q5∞-方程及其解作为λ-方程及其解在本节中，我们将以前的结果放在一起。我们首先固定一个对象Y∈C，定义相关函子GY，TY：C→C，GY（X）=Y+F（X）TY（X）=F∞（Y+X）为什么我们要选择这些函子？那么，像（4）中那样的保护XY+F（F∞（Y+X））现在只是一个GYT-余代数。我们喜欢将它理解为λ-方程，以便在λ-方程的框架中拟合∞-方程的因此，第一个要求是建立适当的单子和分布结构。不难看出，TY又是一个单子与单位和乘法：Y=ηY∞+X◦ κ2：X−→Y+X−→F∞（Y+X）Y=subst（[ηY∞+X◦ κ1，id]）：F ∞（Y + F ∞（Y + X））−→ F ∞（Y + X）.为方便起见，在不太可能混淆的情况下，我们将去掉上标Y其次，我们注意到TY同构于（GY）∞，因为每个（GY）∞（X）通过构造形成映射的最终余代数X<$−→X+GY（−）=X+（Y+F（−））=（Y+X） +F（−）。ηµ162B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145∈→Y所以有t（GY）∞（X）= F∞（Y+X）=TY（X）. 命题3.7n产生所需的分配律。下一个引理具体描述了它。引理5.1在上述情况下，命题3.7产生一个分配律TYGYλzGYTY对于每个YC。 省略上标Y，其分量是以下形式的映射：F∞（Y+（Y+F（X）λXY+F（F∞（Y+X））此外，通过两个明显的自然变换κ2：FGY和F∞（κ2）：F∞<$TY我们得到分配律的交换图F∞Fλ∞TYGYλJ∞JFFGYT Y证明分配律可以描述为复合：TYGY =（GY）∞GYPro po si t i on3. 7GY（GY）∞= GYTY我们将明确地构造这个λX。首先应用final coalgebra map，我们得到：F∞（Y+（Y+FX）） （Y+（Y+FX））+FF∞（Y+（Y+FX））=右侧main +左侧的组件很容易给出所需目标的映射，即：Y+（Y + FX）[κ1，id+F（ηX）] Y+ F（F∞（Y + X））对于右边的组件，我们必须做更多的工作。如果我们能找到一个映射F∞（Y+（Y+FX））F∞（Y+X），我们就完成了。这样的映射可以通过从下式替换来获得：Y+（Y+FX）[ηY∞+X<$κ1，[ηY∞+X<$κ1，σY∞+X<$F（κ2）]]F∞（Y+X）B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145163∈把所有的东西放在一起，我们有下面的复杂表达式。λX=[ [κ1，id+F（ηX）]，κ2Y+（Y+FX）.正如引理末尾所声称的，不难检验分配律是否保持不变。Q引理5.2对于每个YC，对象F∞（Y）带有最终λY-双代数结构：TY（F∞（Y））YF∞ （Y）=F∞（Y+F∞（Y））Y+F（F∞（Y））其中，re_Y= subst（[ηY∞，i d]）。利用引理2.3证明了在F∞（Y）上存在一个Eilenberg-Moore代数结构τY：TY（F∞（Y））→F∞（Y），形成一个最终λY-双代数.我们确定，它是由满足条件Y=subst（[ηY∞，id]）的条件确定的，164B. Jacobs/Electronic Notes in Theoretical Computer Science 106（2004）145∗→−→→ ∞→在引理2.3中定义方程。 我们将像往常一样去掉上标。G（Y）<$λF∞Y<$T（Y）=G（Y）[，]Y+（Y+FF∞Y）F∞（id+Y）=G（Y）[，]（（id+Y）+FF∞（id+Y））Y+F∞Y=（id+F（∞Y））<$[[κ1，id+F（ηF∞Y）]<$（id+∞Y），κ2<$F（subst（））<$FF∞（id+<$Y）]<$F ∞Y+F∞Y=[[κ1，（id+F（YηF∞Y））Y]，κ2<$F（<$Y<$subst（）<$F∞（id+<$Y））]<$<$Y+F∞Y=[[κ1，（id+F（λYληY∞+F∞Yλκ2））λλY]，κ2<$F（subst（<$Y<$$>（id+<$Y）]<$<$Y+F∞Y（）下一页=[[κ1，（id+F（id））κY]，κ2<$F（subst（[ηY∞，[ηY∞，τY∞]]<$（id+<$Y）]<$<$Y+F∞Y=[ [κ1，κY]，κ2<$F（subst（[ηY∞，id]）]<$FY+F∞Y=[Y[ηY∞，id]，Y=<$Y<$[[ηY∞，id]，τY∞<$F（<$Y） ]<$Y+F∞Y根据引理3.5（v），该计算中的标记步骤（step）解释如下。<$Y<$σY∞+F∞Y<$F（κ2）=subst（[ηY∞，id]）<$τY∞+F∞Y<$F（ηY∞+F∞Y）<$F（κ2）=τY∞<$F（subst（[ηY∞，id]））<$F（ηY∞+F∞Y）<$F（κ2）=τY∞<$F（[ηY∞，id]）<$F（κ2）=τY∞。Q我们最终能够看到，∞-方程及其解是λ-方程及其解的特殊情况。这是我们的主要结果。定理5.3设F：C C是函子，其最终余代数F∞（X）=X + F（F∞（X））. 然后又道：(i) 对方程e：X-F∞（Y+），设g：XY+F（F∞（Y+XX）是一个λY-方程，对于来自引理5.1的分配律λY。