无保护递归模型下的共感恢复的研究及其应用

一可在www.sciencedirect.com在线获取理论计算机科学电子笔记319（2015）183-198www.elsevier.com/locate/entcs无保护递归关于共感恢复1SergeyGoncharovChristophRauchLutzSchr？oder荷兰埃朗根大学计算机科学系摘要我们研究了一个模型的侧出的过程，获得了从一个单子建模基出和相邻的自由操作使用cofreile余代数建设，从而达到什么人可能认为作为类型的非良基的侧出射树，推广无限恢复单子。 类型的这类在最近的文献中已经得到了一些关注; 2特别地，已经表明它们允许保护迭代。在这里，我们表明，他们也承认无保护迭代，即形成完整的Elgot单子，提供了基础的基础效应支持无保护迭代。关键词：递归，余代数，余归纳，完备Elgot单子，选择。1介绍在Moggi [17]的开创性工作之后，monad被广泛用于表示程序语义中的计算结果，实际上在实际的编程语言中也是如此[28]。 它们的主要吸引力在于它们提供了一个接口在正确的抽象层次上，它们继承了各种各样的副作用，如状态，非确定性，随机和I/O，同时保留了足够的内部结构来支持大量的通用元理论和编程，后者见证了，例如，在Haskell基本库中实现的monad类[19]。在目前的工作中，我们研究了一个特定的建设单子的动机，部分目标是建模通用的反应过程中的语义副作用。具体地说，给定一个基单子T和对象（类型）a，b，假设T和基范畴上有足够的结构，我们有一族最终余代数。TbX= νγ。T（X + a ×γb）1由DFG支持的HighMoon项目（SCHR 1118/8-1）下http://dx.doi.org/10.1016/j.entcs.2015.12.0121571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。184S. Goncharov等人/理论计算机科学电子笔记319（2015）183一一一一一一一一一一一对于每个对象X。这些最终余代数可以被看作是以两种方式产生的：一方面，可以从发送类型a的消息和接收类型b的消息（可能以类型X的结果终止）的反应过程开始，被建模为非良基的a-标记的b-分支树（叶子标记为X），即νγ的居民。（X+a×γb），然后将T封装的通用副作用添加到模型中（例如，非确定性或对全局共享内存的访问）。另一方面，我们可以把a和b看作是未解释的旁效应的类型f：a→b加到基单子T上，例如一个I/O操作（事实上，最初被Moggi [17]认为是例子的交互式输入和输出单子可以被看作是由这种未解释的效应产生的）;如果一个人希望建模使用f以及T的副效应的非终止程序，那么他会得到完全由TbX给出的有限树。从T构造TbX是一个无限元a a由Cienciarelli和Moggi [9]引入的广义恢复Transformer版本。Pir′og和Gibbons[20，21]称之为共归纳广义恢复Transformer，他们指出在T的Kleisli范畴中，Tb是T（a × b）生成的自由完全迭代单子。的结果，Tb是一个完全迭代单子给我们带来的贡献，目前的文件。回想一下，Tb的完全迭代性意味着对于每个态射e：X→Tb（Y+X），读作定义X的居民的方程，被认为是变量，作为定义变量（来自X）和Y的参数的项，有唯一的解e†：X→TbY在明显的意义上，假设e被保护。后一个概念是根据Tb的附加结构定义的，作为一个理想化的单子，它本质上允许将以运算开始的项与单纯的变量区分开来。e的保护性意味着递归调用只能在自由操作下发生类似的关于保护递归的结果在文献中比比皆是;例如，Tb允许保护递归定义的事实也可以从Uustalu关于参数化单子的更一般的结果中推导出来[27]。本文的主要结果是消除了上述设置中的警戒性限制。也就是说，我们证明了对于每个态射e：X→Tb（X+Y）都存在解e<$：X → TbY当然，解不再是唯一的（例如，我们承认形式x=x的定义）;此外，我们显然需要对T做额外的假设。我们的结果表明，更准确地说，Tb允许有原则地选择满足递归的标准方程律的解e†，从而使Tb成为一个完整的Elgot单子[3]2。我们需要在T上假设T本身是一个Elgot monad（例如，非决定论，非决定论，或这些与状态的组合），即我们证明了[2]我们修改了Elgot monad的原始定义，它要求变量的对象X是lfp范畴中的有限可表示对象，通过承认变量的无限制对象。这一变化主要是由于我们没有假设基础类别是lfp，在我们自己的估计中，在技术上是不必要的，尽管我们还没有检查我们的结果的明显变体的细节，这些变体是通过用Elgot monads替换完整的S. Goncharov等人/理论计算机科学电子笔记319（2015）183185一一X×××Y+X×X为ohElgot单子类在上归纳广义恢复下是稳定的Transformer。 我们还证明了Tb就像埃尔戈特单胞菌一样唯一确定为T的扩展。这些结果的动机是，好吧，从标准的guardedness约束中释放非良基递归定义。例如，请注意，在[20]中，当在完全迭代的monad上解释具有Rutten [24]最初提出的动作的while语言时，相比之下，如果Tb是一个（完全）Elgot monad，现在可以只写无限制的while循环。我们将在第5节详细阐述这个例子，并在第6节回顾进程代数中无保护递归的一个标准例子。2预赛根据Moggi [17]，计算的概念可以形式化为笛卡尔范畴（即具有有限乘积的范畴）上的强单子T。为了支持在主要研究对象中出现的结构，我们在一个分布范畴C中工作，即一个具有有限乘积和上乘积（包括一个最终和一个初始对象）的范畴，使得自然变换[IDinl，idINR]−−−−−−−−−−−−→ X×（Y+Z）是一个同构[10]，其逆我们记为distX，Y，Z。这里我们用inl：A→A+B，inr：B→A+B表示二元余积的注入。二元乘积的投影记为fst：A×B→A，snd：A×B→B;配对记为fst，fnd，f：A→C，g：B→C的配对记为[f，g]：A+B→C。唯一态射A→1写入终端对象！A，或者只是！我们写|C|对于C的对象类。分布式本质上允许在case表达式中使用上下文变量，即在copairing中。我们还要求存在某些指数，即对象X是伴随的 到笛卡尔积a×X，这意味着对于任何X和Y，存在同构curryX，Y：HomC（X×a，Y）=HomC（X，Ya），自然的X和Y。对于逆映射curry-1，我们写出uncurryX，Y. 评估-本文证明了态射evX：Xa×a→X（X中自然的）为无curryXa，X（idXa）. 我们省略了自然变换的索引，这不太可能引起混淆。注2.1指数在Xa中的作用是捕捉生成结果的代数运算的arity的概念，例如：a= 2将对应于诸如非确定性选择的二元运算更一般的设置将涉及在对称monoidal闭范畴V上丰富的范畴，其对象然后被视为arity（和coarity，即用于索引操作族的对象）[13，12]。不假设存在指数Xa，而是假设存在张量a × X和余张量Xb，其中a，b ∈|V|. 余张量是伴随于186S. Goncharov等人/理论计算机科学电子笔记319（2015）183同样的方式，指数是伴随的产品与一个常数的对象。我们希望我们的主要结果扩展到这个设置。回想一下，C上的单子T可以由Kleisli三元组（T，η，η）给出，其中T是|C|（在下文中，我们总是用同一个字母表示Kleisli三元组及其函子部分，前者用黑板粗体表示），单位η是态射族ηX：X→TX，Kleisli提升映射f：X→TY到f：TX→TY，服从以下方程：η= idf η = f（f g）= f g。这等价于根据具有自然变换单位和乘法的内函子T的表示。 一个单子是强的，如果它配备了一个称为强度的自然变换τX，Y：X×TY→T（X×Y），服从一些相干条件（例如：[17]）。 强度使得能够在多个变量上解释程序，并允许Kleisli提升的内在化，从而使像λx这样的表达式合法化。（f（x））τ）。强度等价于单子在C上的富集[14];特别地，集合上的每个单子都是强的。除非另有明确说明，否则我们将使用术语对于单子T的标准直觉是把TX看作是项的集合在某些代数理论中，变量取自X。在这个视图中，单位将变量转换为项，而Kleisli提升函数将替换f：X→TY应用于X上的项。在我们的设置中，这里的一个单子T的Kleisli范畴CT具有与C相同的对象，并且C-态射X→TY作为态射X→Y。 在CT中X上的恒等式是ηX;f：X→TY和g：Y→TZ的Kleisli复合是gf。3完整的埃尔戈特单胞体正如在引言中所指出的，我们将对单子T上的递归定义感兴趣;抽象地说，这些是态射f：X→T（Y+X）被认为是将每个变量x：X与T（Y+X）中的代数项形式的定义f（x）相关联，从而使用来自Y的参数以及来自X的定义变量。后者相当于定义的递归调用。这个概念对于非终止递归的情况是不可知的。例如，T可以将所有非终止递归调用序列标识为一个表示非终止的值，而在另一个极端，T可能是一种无限树，它只显式地记录递归调用树S. Goncharov等人/理论计算机科学电子笔记319（2015）183187对于上面的递归定义f，我们希望将一个解f：X→TY，这相当于将X的元素非递归地定义为仅在Y上的项。由于我们不假设任何形式的警戒性，因此这个解一般不会是唯一的。因此，我们要求所有方程f的解f<$的一致选择，这里的一致是指选择满足一组标准的（准）方程性质。形式上：定义3.1（完备Elgot monad）完备Elgot monad是一个强monad T，它配备了一个称为迭代的运算符，它发送任何f：X→ T（Y + X）到f：X→TY满足以下条件：• 展开：[η，f<$]展开f=f<$;• 自然性：gf<$=（[Tinlg，ηinr]f）<$对于任意g：Y→TZ;• 二度性：（[ηinl，h]g）<$= [η，（[ηinl，g]h）<$]g对于任何g：X→T（Y+Z）和h：Z→T（Y+X）;• 共对角：（T[id，inr]g）<$=（g<$）<$对于任意g：X→T（（Y+X）+X）;• 均匀性：f <$h = T（id + h）<$g意味着f <$h = g<$对于任何g：Z →T（Y +Z）和h：Z→ X。此外，迭代必须在以下意义上与强度相容：对于任何f：X → T（Y + X），τ（id×f <$）=（T dist <$τ（id ×f））<$。注3.2上述定义受到参数化统一迭代公理的启发[25]，其中Bl oom和E′sik[8]是基础。Ad'ameketal.[3]通过一个稍微不同的公理系统定义了Elgot monads：用Bek i' c恒等式代替了共对角和二元公理。然而，这两个迭代化是等价的，这本质上是关于迭代理论的一个结果[8，6.8节]。此外，[3]中的迭代算子仅定义为f：X→T（Y+X），其中X是有限可表示的，假设C是局部有限可表示的;因此我们使用术语我们的印象是，这种差异在技术上并不重要，但我们没有检查结果的最终变量的细节在进一步的发展中，完全Elgot单子的例子将作为所谓的ω-连续单子（定义3.3）或作为其自由运算的扩展出现，即通过共感广义恢复Transformer。如果T支持迭代运算符<$，那么总是可以用一个额外的参数参数将其参数化，以在递归循环中进行，即我们导出一个将f：Z×X→T（Y+X）发送到f：Z×X→TY的运算符，f=<$T（snd + id）<$（T dist）<$τZ，Y+ X<$fst，f.（1）我们称导出的算子为强迭代。188S. Goncharov等人/理论计算机科学电子笔记319（2015）183如上所述，一类重要的完备Elgot单子的例子是通过Kleisli范畴的适当的序富集而产生的定义3.3（ω-连续单子）一个ω-连续单子由单子T和T的Kleisli范畴CT在ω-完全偏序范畴ωCppo上的一个扩充组成，该范畴具有底映射和（非严格）连续映射，满足以下条件：• 强度是ω-连续的：τ_n（id ×.ifi）=.i（τ（id×fi））;ó• 在两个变元中，CT中的copairing都是ω.i fi，.igi=.i[fi，gi];• 底部元件通过强度和后组合在CT中得以保留：τ（id ×）=，f =。例3.4Set[17]上的许多标准计算单子都是ω-连续的，包括非终止性（TX=X+ 1）、非确定性（TX=P（X））和非确定性状态单子（对于状态集S，TX=P（X×S）S在ωCppo上，提升（TX=X）和各种幂域单子是ω-连续的。注释3.5正如Kock [14]所观察到的，单体的强度等同于在基范畴上的富集。这个基本事实的一个结果是，如果C在具有无底ω-完全偏序和ω-连续映射的范畴ωCpo上是丰富的（即C是Wand [29]和Smyth和Plotkin [26]意义上的O-范畴），并且双Cartesian闭结构在明显意义上是丰富的，那么CT也在ωCpo上是丰富的，因为T在强单子的基础上是ωCpo-函子（也称为局部连续函子[26]）。 则T在定义3.3的意义下是ω-连续的，即每个Hom（X，TY）在CT中有一个由强度和后合成保持的底元。这允许通过将C作为前域的合适类别来合并许多域理论的例子，并且在最简单的情况下，T是提升单子TX=X（通过下面探索的构造，可以构建更复杂的例子如果T是ω-连续单子，则h<$→[η，h]πf在hom-set上，HomC（A，TB）是连续的，因为T中的配对和Kleisli合成是连续的，因此根据Kleene不动点定理有一个最小不动点我们可以通过取f<$作为这个定点来定义迭代算子;换句话说，f<$被定义为根据定义3.1的展开方程的最小解。其余身份的验证是乏味但简单的;总之，定理3.6在每一个ω-连续单子上，通过取最小不动点来定义迭代，确定了一个完备的Elgot单子结构。根据已知的所谓ω-连续理论的类似事实[8，定理8.2.15，练习8.2.17]，这个结果是不足为奇的。S. Goncharov等人/理论计算机科学电子笔记319（2015）183189一一B一一一一一一一一一注3.7每一个完整的Elgot单子T都能表达非生产性分歧作为一般效应，伊辛 雷X−−−−→ T（Y + X）。这种计算永远不会产生任何结果，即表现得像死锁。 如果T是ω-连续的，则非生产性发散与Hom（X，TY）的最小元素一致，因此我们对上述态射使用相同的符号，但一般来说，不存在非生产性发散可以是最小元素的顺序。4共归纳广义 恢复Transformer我们继续回忆共归纳广义恢复变换的定义[20];为了简单起见，我们考虑一个只有一族自由操作的版本（而不是一个完整的签名，或者更一般地，一个基范畴上的任意内函子）。然后，我们证明了我们的主要结果，在这种结构下的完全Elgot单子类的稳定性（定理4.5）。给定a，b∈|C|使得存在形式为X b的指数，且上的单子TC、我们把（）b= a × b，TbX = νγ。T（X + γb）;也就是说，TbX是T（X+（）b）的最终余代数，我们假设它存在。的a aassignment（）b显然是一个函子，也就是说，它也适用于态射。 直觉，TbXa a是一种可能的非终止计算树，每个节点由一个计算组成，该计算具有由T指定的边项，该边项要么返回X中的值，要么继续a-许多自由操作中的一个，每个自由操作组合b-许多后续计算。让outX：TbX→T（X+（TbX）b）是最终余代数结构，设coit（g）：Y→TbX表示最终余代数结构，由余代数g诱导的自同构：Y→T（X+Yb）：科伊特（克）Y，zTaXG，bz，输出X、T（X + Ya）T（X+（T bX）b）。T（X+（coit（g））b）a a直观地说，coit（g）封装（在TbX中）一个计算树，该计算树以执行g开始，如果g执行，则终止于类型X的叶子，否则（共同）递归地继续执行g，为每个递归调用形成一个新的树节点。很容易证明outX在X中是自然的。根据Lambek因此，T通过以下方式映射到Tb：ext=TTinl，zT（Id+（Tb）b） out-1 ，zTb.a a a190S. Goncharov等人/理论计算机科学电子笔记319（2015）183一一一一§b一一一一一一一一Baa一一一一一一一一一一一一我们明确地记录Tb是一个强单子：引理4.1给定一个单子T和a，b ∈ |C|，Tb是单子的函子部分Tb，具有以下列性质为特征的单子结构。(i) 单位ην：X → T bX定义为out ην= η inl（即， ην= out−1 <$η ν inl）。(ii) 给定f：X→TbY，K-leisli提升f§：TbX→TbY是唯一解一方程的解为：out_f，η_in_r（f就这样）a一◦ 出去(iii) 设f：X→TbY，l∈g=[f，<$v]：X+Y→TbY，则l∈g是最终同态一g§=coit一[T（id+（T binr）b）输出ng，η n inr]输出n g。(iv) 强度τν：X×TbY→Tb（X×Y）是出τν=T（id+（τν）b）<$Tδ<$τ<$（id×out）其中δ：X×（Y+（TbY）b）→（X×Y）+（X×a a aTbY）b是明显的分配变换：a aX×TbYτν（T δ）τ（id×out） ，zT（X×Y+（X×TbY）b）T（id+（τν）b）、、、Tb（X×Y）或tz，T（X×Y+Tb（X×Y）b）.这就可以称Tb为（ T 上 的 ） 共归纳广义恢复单子。引理4.1的证明由以下事实方便：是一个参数化的单子，这意味着Tb是单子[27，定理3.73.9）。 另外，Tb一个单子可以直接从的结果[20]。这里的新之处在于，我们证明了Tb实际上是强的，因此支持标准计算元语言的解释[17]。这等于表明，在最后一项中定义的强度满足必要的定律[17]。在（相当复杂的）这些定律的证明中使用的一个具有潜在独立利益的事实是引理4.2对任意函子G：B→C，outG：TbG→T（G+（TbG）b）是最终的[ B，C ]中的T（G + Idb）-余代数.a a a继Uustalu [27]（和其他工作[20，1]），我们接下来介绍一个概念的防范。定义4.3（守护性）态射f：X→Tb（Y+Z）是守护的，如果存在u：X→T（Y+Tb（Y+Z）b），使得out_f=T（inl+id）<$u：FX，zTa（Y+Z）ub，Bz，出来，bT（Y+Ta（Y+Z）a）T（inl+id）T（（Y + Z）+（Tb（Y + Z）。S. Goncharov等人/理论计算机科学电子笔记319（2015）183191一f：X → T b（Y + Z）的保护性直观地意味着对f中Z类型计算的任何调用都只发生在自由操作下，即，通过右被加数192S. Goncharov等人/理论计算机科学电子笔记319（2015）183一一一一一一1一1一一复合在T（（Y+Z）+（Tb（Y+Z））b）中。 这个概念的一个熟悉的例子发生在过程a a[17]《易经》中的卦，以卦为卦，以卦为卦。例4.4设T是合适范畴上的可数幂集单子，即TX= PωX ={Y<$X||Y| ≤ω}。 物体T1X= νγ。Pω（X + A×γ）可以是被认为是可能无限可数不确定过程的域，其作用于A，最终结果在X中。一个态射n→T1（X+n）可以被看作是一个由n个相互递归的进程定义组成的系统;后者在定义4.3的意义上是被保护的，即进程的每一个递归调用之前都有一个动作，这与进程代数中的保护性的标准概念相一致。我们记得在第6节中有一个在这种情况下的不加保护的定义的例子。下面的结果是本文的主要技术贡献;它本质上说明迭代算子，即Elgot单子结构，沿着扩张T→Tb唯一传播。定理4.5设T是完备Elgot单子。 给定a，b∈|C|，设Tb 是在引理4.1中确定的单子，即T上的共归纳广义恢复单子。(i) 有一个唯一的迭代算子使Tb一个完整的埃尔戈特单核细胞，在T中的迭代的意义上，对于f：X→Tb（Y+X）和g：X→T（Y+X），如果输出信号f=（输入信号T）信号g（即： f = out−1<$（T inl）<$g），则输出Δf<$=（T输入）Δg <$。(ii) 对于任何守护态射f：X→Tb（Y + X），f<$是满足开折性质[ην，f<$]§<$f=f <$的唯一态射。证据（略）Uustalu已经证明了守护态射f有唯一的迭代f <$[27，定理3.11]。然后，关键的一步是以一致的方式定义无限制f的f <$。对于f：X→Tb（Y + X），设Df：X→Tb（Y + X）为X−−w−<$−→T（Y+Tb（Y+X）b）a aT（inl+id）b b−→T（（Y+X）+Ta（Y+X）a）输出-1b−→Ta（Y+X）S. Goncharov等人/理论计算机科学电子笔记319（2015）183193一一一一DD◦一一一（由定义保护），其中w是复合的Xfb−−−→ Ta（Y+X）出B B−→T（（Y+X）+Ta（Y+X）a）Tπb b−→T（（Y+Ta（Y+X）a）+X）其中π=[inl+id，inl inr]。也就是说，Df通过迭代使f得到保护，out_f：X→T（（Y+X） +Tb（Y+X）b）(in完全Elgot单子T）在结果的中间被加数上。当f被保护时，很容易检验Df=f因此，我们可以定义ft=（Df）t(inTb）。进一步的（非平凡的）计算表明，这个定义确实满足完备埃尔戈单子的公理为了建立唯一性，我们首先证明了任何态射f：X→Tb（Y+X）可以分解为两个态射g：X→Tb（Z+X）和h：Z→Tb（Y+X），a a其中Z=Y+Tb（Y+X）b，作为a af=[h，ηνπinr]§πgg完全不设防，即对于某个gJ，out g=（Tinl）gJ;也就是说，我们将f分成一个保护部分和一个完全无保护部分，并在后者上迭代部分由Tb上的迭代的要求确定延拓迭代在T。 接下来，我们表明，对于任何选择的埃尔戈特单子结构，在Tb上，并且f<$=（h§ g<$）<$h§ g <$= Df.总之，我们得到f<$=（h§g<$）<$=（f）<$，即我们先前对f<$的定义是具有给定性质的唯一可能的定义，因为f是保护的，因此（Df）<$已经由展开性质唯一确定。□下面的结果描述了Tb在（超大）范畴CElg（C）中的特征：C上的完全Elgot单子和（强）单子态射[16]在明显意义上保持它：定义4.6一个完全Elgot单子态射<$：R→S在完全Elgot单子R之间，S是一个态射<$在底层强单子之间（即，对于f：X→RY，η=η，f=（ f），并且τ=τ（id×））另外满足对于g：X→R（Y+X）.（g）<$=g<$194S. Goncharov等人/理论计算机科学电子笔记319（2015）183一一一一一一一一一引理4.7自然变换ext：T→Tb 是一个完整的埃尔戈特单核细胞态射定理4.8设CElg（C）有一个初始对象L。 然后(i) Lb是签名函子（）b：C→C上的自由完备Elgot单子;(ii) 对任意完备Elgot单子T，单核细胞Tb是以下两个因素的副产物 T和 Lb在CElg（C）中，左侧注射ext：T →Tb （特别地，ext是CElg（C）中的态射）。证明定理4.8的关键步骤是下面的陈述，它本身是相互关联的。引理4.9设a，b∈|C|设T，S是两个完备的Elgot单子。给定一个完备Elgot单子态射ρ：T→S和一个Kleisli态射u：a→Sb，b输出bb[η∈inl，λ∈x，f ∈ f]. S（inr<$f）u（x）]s<$ρbTaX−−−−−→T（X+a×（TaX））−−−−−−−− − − − − →S（X+TaX）扩展到一个完整的Elgot单子态射。相 反 ，任何一个π：Tb → S都会诱导下一个：T→S和out-1λ η η⟩b/a−→ Tab−→ Sb。这两段话是相互对立的，因此见证了一个双射之间的COM。完全Elgot单子态射Tb→S和Kleisli态射对a→ Sb和完全Elgot单子态射T → S。定理4.8中提到的初始完备Elgot单子L的存在性和确切形状依赖于C的性质。 回想一下，如果C有可数个不相交且泛的余积（即在回调下稳定），并且余积注入在可数个不相交并下是闭的，则C是超扩张的[2例子包括集合、ωCpo、有界完备度量空间以及所有的预层范畴。定理4.10设C是超延的。 则由LX = X +1给出的单子L是ω-连续的。 根据定理3.6，当L具有生成的完备Elgot单子结构时，L是C上的初始完备Elgot单子。证据 基本范畴C更是广延范畴，在任何广延范畴中，L是定义域为余积注入的部分态射的部分映射分类器。因此，L的Kleisli范畴从部分函数上的扩张序继承了其hom-set上的序;上积注入在C中的并下是封闭的这一事实保证了这些序是ω-完全的（注意，任何作为子代数的上积注入的上升链，利用上积的普适性，都可以转化为上积注入的不相交并利用超扩展范畴的性质，我们可以证明这导致了满足定义3.3中所有附加条件的CL的ωCppo-富集。S. Goncharov等人/理论计算机科学电子笔记319（2015）183195（Ⅲ）（Ⅲ）（Ⅲ）（）（）一n1一些p：n→M1，如果<$Ai）因子通过，则为输入型。：n→1。顺序（Ⅲ）n 1要看到初始性，请注意，任何完备Elgot单子T对任何X∈ |C|具有agx元素ntX=δX<$ ：1→TX其中δX=ηπinr：1→T（X+1）。下面是通过迭代的自然性，证明了X在X中是自然的。此外，Elgot monad morphisms的完整性很容易看出，<$X= [η，<$X]产生一个完全的Elgot单子态射<$：L→T。另一方面，它是唯一这样的，因为对于任何其他完全埃尔戈单子态射θ：L→T，都有θ inl = θ η = η = θ inl和θ inr = θ = θ inr，这意味着θ =θ。□5示例：不受限制的While循环我们使用一个简单的while语言，由Rutten提出，由语法给出P，Q：：= A |P; Q|如果b那么P否则Q|而b做P继Pir'og和Gibbons[20]之后，在单子M的Kleisli范畴中得到了解释. 在这里，A的范围涵盖了被解释为Kleisli态射的原子作用A：对于某个固定对象n，n→Mn，对于原子谓词，b，解释为作为Kleisli态射b：n→M（1 + 1）（左被加数读作“假”）。我们说A是输出型的，如果A具有形式（Mfst）<$τ<$<$idn，p<$，组合物P;Q被解释为Kleisli组合物Q（P），并且ifbthenPelseQ=[Qfst，Pfst]QMdi s）tτid，b.当然，关键点是while循环的解释，在迭代的情况下，由下式给出：当b做P时）=Ä[（Minl）ηfst，（Minr）P）fst]ä◦ Mdistid，b）.（二）Pir'og和Gibbons已经观察到，如果用一个完全迭代的monad来安装M，则需要保护while循环的每次迭代，即将while的语义更改为当b做P时）=Ä[（Minl）ηfst，（Minr）P）fst]ä◦ Mdistid，<$b）γ其中γ：n→Mn被保护，否则迭代可能无法定义。如果我们用一个Elgot monad实例化M，比如用Tb来实例化Elgot monadT，那么保护就不必要了，也就是说，我们可以坚持原来的语义（2）。作为一个例子，考虑一个简单的过程形式，它从n输入和输出符号，并具有由T指定的副效应;即我们在M=（T1）n中工作，意味着使用相邻的自由效应1→n来捕获输出，使用类型n→1的自由效应来捕获输入。我们假设一个原子动作write从n输出一个符号，一个原子动作read输入一个符号。我们将write解释为输出类型，即通过write=（Mfst）<$τidn，w，其中w=ext ou t−1ηinr i dn，ην！n→（T1）n（1）٨†٨†196S. Goncharov等人/理论计算机科学电子笔记319（2015）183n（Ⅲ）一一一一n 1n 1一一n 1（ην是T1的单位），而read是输入类型，即read（Ⅲ） =r！n其中r=out−1ηνinrid1，r0：1→（T1）nn而r0：1→（T1）n（n）n是通过对ηM进行的，其中n = 1×n→（T1）n（n）（ηM是M的单位）。此外，假设一个基本谓词b，只要它可以接受两个真值，它的解释在很大程度上与例子无关;例如，b可能只是非确定性地或随机地选择一个真值，这取决于基单子T的性质。考虑该计划read;whiletruedo ifbthenskipelsewriteM其中，skip是原子动作，解释为：（skip）=η：n→Mn。 可以对于循环不执行任何写操作，因为b可能碰巧总是选择左侧分支;也就是说，循环体未能被保护。由于M是一个Elgot单子，而不仅仅是完全迭代的，因此循环的语义仍然被定义（由（2））。6示例：简单进程代数在[5，定理5.7.3]中证明了，如果允许无保护递归，一个具有有限选择和作用预固定的简单进程代数BSP可以表示所有可数转移系统。证明的思想是引入变量Xik（i），k∈N表示第i个状态的第k次跃迁，其中Xi0表示第i个状态本身，以及（无保护的）递归方程其中，第i个状态的第k个转变执行动作bik并且到达第j（i，k）状态。(It然后明确指出使用无保护递归是必要的。为了使用共归纳的一般化恢复Transformer来模拟这种现象，我们取T=Pω1，即Set上的可数幂集单子（见例4. 4），以及一个解释为act=out−1<$ηinr<$ida，ην的操作act！其中a是动作的类型。 也就是说，我们将（无界）非决定论视为基效应的一部分，并通过共归纳广义假设添加动作前缀。故《说文》云：“三者，义也。由映射g=outt−1<$f：N×N→T1（N×N）<$=T1（0+N×N）with表示f：N×N→T（（N×N）+a×T1（N×N））（省略指数1）由下式给出f（i，k）={inr（bik，nv（j（i，k），0）），inl（i，k +1）}.同样，我们的结果T1是一个Elgot单子保证了这个方程有一个解g<$;T1中解的选择唯一地确定为通过取最小不动点将T=P的通常结构扩展为Elgot单子nS. Goncharov等人/理论计算机科学电子笔记319（2015）183197×一一一7相关工作上述结果得益于以前对基于单子的公理迭代的大量工作。特别地，我们讨论了Ad′amek等人[3]研究的Elgotmonad的概念;函子上自由Elgot monad的构造[4]与定理4.8密切相关。i，我们并不认为这个结果是本文有大量的文献的解决方案（共）递归程序计划[6，1，15，11，20，21]，从我们目前的工作主要是不同的是，我们不限于保护系统的方程。特别地，如在引言中提到的，Pir'og和Gibbons[20]实际上使用相同的单子变换器，即共感广义恢复Transformer。Pir'og和Gibbons[21，推论4.6]也证明了与我们的定理4.8类似的关于上归纳广义对偶Transformer取单子的上积的一个刻画。ii;但同样，这发生在一个不同的范畴中，即完全迭代的单子（承认有保护的递归定义）而不是完全的Elgot单子（承认无限制的上递归定义）。这样做的一个结果是，我们的余积结果中的第二个被加数是一个自由的完全Elgot单子，而不是一个自由的b上的完全迭代单子，因此有一个内置的发散概念。从技术上讲，Tb是一个完全迭代单子的结果与我们关于Tb是一个完全Elgot单子的结果a a完全迭代的，对T没有任何假设。我们从保护递归方程的解构造无保护递归方程的解，因为后者主要依赖于Uustalu关于参数化单子上的保护递归的结果[27]，这特别允许我们在没有理想化单子的情况下进行通过Elgot单子的迭代的公理化处理本质上与Simpson和Plotkin [25]对递归的公理化处理是对偶的，Simpson和Plotkin [ 25 ]在范畴D中工作，具有参数化的一致递归算子HomD（Y×X，X）→HomD（Y，X）和D中严格函数的子范畴S。给定一个分配范畴C，它具有一个完备的Elgot单子，我们可以取S=Cop和D=（CT）op。 然后CT上的迭代算子发送f：X→T（Y+X）到f†：X→TY精确地导出了（D，S）对在Simpson和Plotkin意义下的参数化一致递归算子8结论和今后的工作我们以迭代的形式为非良基边导出递归定义建立了语义基础，特别是对于所谓的共归纳广 义 恢 复 Transformer 上 的 递 归 定 义 ， 该 变 换 从 基 单 子 T 构 造 单 子 Tb= νγ 。 T（+a×γb）。虽然以前对同一个单子Transformer的工作集中在保护的上递归定义上，但在完全迭代单子的框架中，我们在（完全）Elgot单子的设置中工作，它允许无限制的递归定义。我们的主要结果表明，198S. Goncharov等人/理论计算机科学电子笔记319（2015）183一一一一一• 如果T是完全Elgot单子，则Tb• Tb作为一个完全Elgot单子的结构唯一地确定为T的结构的扩张;• 如果基本范畴C允许初始完全Elgot单子L（typi-在完全Elgot单子范畴中，我们称L=+1）enTb=T+Lba a对秀丽隐特别是这需要证明方程的法律完整Elgot单子的解决方案运营商，我们建设的Tb。我们已经在Coq证明助手中对我们的结果进行了正式验证，这在技术上非常复杂，请参见https://git8.cs.fau.de/redmine/projects/corque。我们猜想我们的结果推广到形式为νγ的单子。T（X + Hγ）对于任何（强）函子H代替a×（--）b。 除了申请从共归纳恢复单子Transformer到完整的Elgot单子T再次产生完整的Elgot单子Tb，所得到的对象显然具有由邻接的自由操作提供的更丰富的结构。进一步研究的一个主题是识别（并可能公理化）这种结构。我们的目标是使用这种结构来编程自由运算的定义，作为态射TbX→TX，其精神与处理代数运算的范式类似[23]。结合迭代，这实际上产生了一个比迭代更有表达力的递归运算符。然而，这需要超越本文的一阶设置（这对于迭代来说是足够的），因为按值调用递归被认为是一个固有的高阶概念。确认作者感谢Stefan Milius和Paul Blain Levy进行了有益的讨论。引用[1] Aczel，P.， J. Ad'amek，S. Milius和J. Velebil，无限定理和完全迭代理论：一个coalgebraic视图，理论。Comput. Sci. 300（2003），pp.1[2] Ad'amek，J.，R. Borger，S. Milius和J. Velebil，iterativealgebr as：Howiterativea rethey？Cat.19（2008），pp. 61比92[3]Ad'amek，J.，S. Milius和J. Velebil，Equationalpropertiesofitativemonad s，Inf. Comput. 208（2010），pp. 1306-1348年。[4] Ad'amek，J.，S. Milius和J. 张文，张文辉，等.迭 代法 的基 本原 理.北 京： 高等 教育 出版 社，2000 ，11 （1） ：100 - 101 . 结构。Comput. Sci. 21（2011），pp.417-480[5] Baeten，J.，T. Basten和M. Reniers，[6] Bartels，F.，广义共归纳，数学。结构。Comput. Sci. 13（2003），pp.321-348[7] Bergstra，J.，A. Ponse和S.Smolka，editors，[8] 天哪，S。 和