Elgot代数：递归计算语义学中的新概念和编程实践

理论计算机科学电子笔记155（2006）87-109www.elsevier.com/locate/entcsElgot Algebras（ExtendedAbstract）Jir'Ad'amek1，2StefanMilius2德国布伦瑞克技术大学理论计算机科学研究所Jir'Velebil1，3捷克共和国布拉格技术大学电气工程学院摘要迭代代数，i.例如，将其中递归方程e有唯一解e。这个规范满足了两个简单且动机良好的公理：函数性（说明解是“一致的”）和组合性（说明如何执行同时递归）。这两个公理干规范从Elgot保留字： Elgot代数，有理单子，余代数，迭代理论如果你不是解决方案的一部分，你就是问题的一部分。埃尔德里奇·克利弗，1968年在旧金山的演讲†完整版本 的 这 纸 含有 所有 证明 可以 被 发现 在 的 网址http://www.iti.cs.tu-bs.de/1 第一和第三作者感谢捷克共和国共和国根据批准号。201/02/0148。2Em a il：{adamek，miliu s}@i ti. cs. t u-b s. De3我来了：velebil@math. 联邦调查局cv ut. cz1571-0661© 2006由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.11.05388J. Adámek等人/理论计算机科学电子笔记155（2006）871引言本文研究了Elgot代数，这是一个在递归计算语义学中有用的代数新概念在编程中，函数通常由递归应用程序方案指定，例如（一、一）（x）（x）其中F和G是给定的函数，并且由式（1.1）根据给定的函数递归地定义。我们感兴趣的是这样的计划的语义。实际上，我们必须区分未解释的语义和解释的语义。在未解释的语义中，给定不是函数，而仅仅是来自签名的函数符号。在本文中，我们预先定义了解释语义的基础，其中程序方案与适当的代数A结合在一起，该代数A给出了对所有给定函数符号的解释。Elgot代数在语义学中的实际应用将在[19]中讨论。当然，我们所说的例如，对于递归程序方案（1.1），我们只对那些代数感兴趣A，其中n ={F，G}，其中程序方案（1.1）有解，i。例如，我们可以规范地获得A上的新运算A和A，使得形式等式（1.1）成为有效恒等式。我们要解决的问题是：(1.2)什么样的代数适合于语义学？在文献中已经提出了几个答案。一个众所周知的方法是使用完全偏序集（CPO）代替集合，参见例如[14]。这里代数有一个额外的CPO结构，使所有操作连续。另一种方法适用于完备度量空间，参见[6]。这里我们有一个额外的完整指标，使所有操作都收缩。在这两种方法中，人们在代数上强加了额外的结构，使得有可能获得递归计算的语义作为有限近似的连接（或极限）。这是想法卡尔文埃尔戈尝试和工作在一个纯粹的代数设置避免额外的结构，如秩序或度量。在[10]，他介绍了迭代理论是代数理论，其中某些系统的递归方程有独特的解决方案。后来Evelyn Nelson [21]和Jerzy Tiuryn [25]研究了迭代代数，这是具有递归方程唯一解虽然避免了额外的结构，但它们仍然不是人们所希望的统一概念，因为它们不继承连续代数-最小不动点通常不是唯一的。J. Adámek等人/理论计算机科学电子笔记155（2006）8789、SS、然而，分析所有上述类型的代数，我们发现一个有趣的共同特征，使连续的，可度量的和迭代的代数适合用于递归程序模式的语义：这些代数允许无限树的解释。让我们更精确地说明这一点。对于给定的签名，考虑代数T X在X上的所有（有限和无限）树中，i。例如，有根有序树，其中具有n个孩子的内部节点由来自X的n元运算符号标记，并且叶子由来自X的常数或元素标记。代数T<$X是X上的自由连续的n-代数，也是自由可度量化的n-代数在X上。因此，对于任何连续或可度量化代数A，我们得到一个典范映射T<$A−→A，它为A上的任何树提供了它在A中的计算结果。 这样就很容易给递归程序A.例如，对于（1.1），我们可以简单地将树展开，得到无限树F，，F，，sss，，xsFss，SF GGx（x）=s，，ss，（x）=s，，ss，GxFSsSGGXGx FSsSGGX然后对于任意的自变量x∈A计算A中的这些无限树。实际上，我们不需要计算所有的无限树：所有的递归。主动的程序计划展开到代数树，见[8]（我们在总结中提到这些很快）。另一个重要的子类是有理树，它是作为有保护的有限递归方程的所有解而得到的。在[13]中，它们被描述为那些直到同构只有有限个子树的树。我们表示为R XTX中所有有理树的子代数。考虑到这一点，我们可以更正式地重述问题（1.2）：（一、三）什么样的代数对所有的树都有合适的计算或者所有的理性树？这意味着，更进一步的形式：什么是最大的范畴，其中T<$X或R<$X，分别作为自由代数，SS、S90J. Adámek等人/理论计算机科学电子笔记155（2006）87X吗？在TX的情况下，答案是：完备Elgot代数。这些是带有附加运算“匕首”的代数A，它为A中的每个递归方程组e分配一个解e †。两个（令人惊讶的简单）公理是放在（−）<$上，它源于T<$X的内部结构：函子T<$X−→T<$X是集合中单子的一部分，这是关于T的自由完全迭代理论，如[11]中所证明我们将证明，代数的单子（i.例如，T的基本的例子：连续代数或可度量化代数是Elgot代数。类似地，其中每个R<$X充当自由代数的最大类它们被精确地定义为完备的埃尔戈代数，只是这里考虑的递归方程组e必须是有限的。例如，每个迭代代数都是Elgot代数。相关工作：递归方程的解是许多计算模型的基本部分，例如：例如，在一个实施例中，C.迭代理论埃尔戈特[10]，迭代理论。Bloom和Z.E'sik[7]，追踪么半群范畴曲霉茹瓦亚尔河街和D。Verity [16]，域的固定点理论，见S。Eilenberg [9]或G. Plotkin [22]等。在这些模型中的某些模型中，给定类型的递归方程e的解e†的分配是唯一的（e. 例如，在一个实施例中，在迭代理论中，每个理想系统都有唯一解，或者在在完备度量空间给定的域上，不动点方程有唯一解，见[6]）。于是，运算e−→e<$满足了一些方程性质。在其他模型中，E。例如，在一个实施例中，在迭代理论或跟踪的范畴中，见[15]，假设一个特定的解e†的选择，以及某些性质（受具有唯一解的模型的都被公式化为公理本文的方法在求具体代数A中的解e−→e<$方面更为初等。这里我们用A，i中的可解方程e。例如， 形式e：X−→HX+A的态射，但不对称性只是一个技术限制：在未来的研究中，我们将证明更一般的非线性方程“自动”求解。事实上，我们的工作与一个固定的代数A（并让只有X和e变化）是部分负责我们的公理简单的工作相比，理论（其中A也变化），见e。G. [7]或[23]。Evelyn Nelson的迭代代数[21]和Jerzy Tiuryn [25]，其中要求解et是唯一的，与proa ch相似。ZoltanE′sik[12]的代数也是一个特例。不幸的是，公理的数量（7个）和它们的复杂性使得这个概念与埃尔戈代数的关系成为一个非平凡的问题。我们打算今后研究这个问题J. Adámek等人/理论计算机科学电子笔记155（2006）8791一我们处理两种变体：与R<$X相关的埃尔戈代数，其中函数（−）<$t仅将解分配给无穷大递归系统;与T<$X相关的完全埃尔戈代数，其中函数（−）<$t将解分配给所有无穷大递归系统。这与我们之前的重-搜索[1，18，2，3]，其中我们证明了每个有限的内函子H生成一个自由的迭代单子R和一个自由的完全迭代单子T。在本文中，我们研究单子R和T的这里H是一个范畴的内函子，它满足一些相当温和的条件（不仅仅是Set）：这种一般性并没有使证明变得更加复杂，稍后我们使用了Set以外的其他范畴（见总结）。由于篇幅有限，我们省略了一些证明，读者可以在本文的完整版中找到它们[4]。第2章迭代代数和CIA假设2.1在整个文件H表示一个endofunctor的范畴ffi有二进制余产品。我们用inl：A−→A+B和inr：B−→A+B表示相应的注入。在某个阶段，我们假设ffi是局部有限可表示的，H是无穷的，i。例如，过滤的蜜饯但是我们明确地做出这些假设回想一下，一个对象X被称为有限可表示的，因为hom-functorffi（X，−）：ffi−→Set是无限的。(In这些，都是真正意义上的集合。在代数的等式类中，这些代数正是通常意义上的有限可表示代数。）进一步回想一下，一个范畴ffi被称为局部有限可表示的，如果它有上极限和有限可表示对象的一个小集合，这些对象在过滤上极限下的闭包是ffi的全部，见[5]。定义2.2设α：HA−→A是H-代数。通过A中的一个齐次方程态射，我们理解了ffi中的一个态射e：X−→HX+A。我们称之为无穷的，前提是X是无穷可表示的。e的解是态射e<$：X−→A，使得平方（2.1）是的，，，e[α，A]、HXz，上下班+AHe+AHA+A如果每一个无穷维代数方程态射都有唯一解，则称A是一个迭代代数。称A为完全迭代代数（CIA），如果A的每一个非线性方程态射都有唯一解.注2.3介绍了集合的多项式内函子的迭代代数X92J. Adámek等人/理论计算机科学电子笔记155（2006）87由Evelyn Nelson介绍和研究[21]。她证明了X上的有理树的代数R<$X形成自由迭代代数，并且由此得到的理论是Calvin Elgot的自由迭代理论[10]。我们最近在更一般的背景下研究了迭代代数;研究了局部有限可表示范畴的有限内函子。Stefan Milius在[18]中研究了完全迭代代数例2.4考虑具有一个二元运算的集合中的代数例如，函子是HX=X×X。一个代数A中的代数方程态射e给每个变量x赋一个代数项y<$z（y和z都是变量）或A的一个元素。解e<$：X−→A给x∈X赋与e相同的元素，如果e（x）∈A，或者赋e<$（y）<$e <$<$（z）的结果，如果e（x）=y<$z。例如，以下递归方程xxx，由明显的态射e：{x} −→ {x}× {x}+ A表示，有一个元素a = e<$（x）作为解e<$，它是幂等的。因此，每个迭代代数都有唯一的幂等元。如果A是完全迭代的，那么对于每个序列，它有一个0，一个1，一个2，. 的元素，一个独特的解释0（一个1（一个2· ··），i。e. ，a唯一地等于b0，b1，b2， . . withb0=a0<$b1，b1=a1<$b2，等等。事实上，我们在这里考虑方程xnanxn+1（n∈）的。迭代代数中许多非线性方程的解是唯一的，因为它们是可解的.例如，以下递归方程x1（x2a）bx2x1b不被忽视。 但他们可以很容易地得到一个系统x1z1z2x2x1z2z1x2z3z2bz3a由态射e表示：X−→X×X+A，其中X={x1，x2，z1，z2，z3}。它的解是一个映射e<$：X−→A，产生一对元素s =e<$（x1）和t = e<$（x2），满足s =（t <$a）<$b和t = s <$a。例2.5迭代的代数。对于每一个有限签名<$n =（<$n）n∈，我们可以将λ-代数与多项式内函子Hλ的代数等同起来，J. Adámek等人/理论计算机科学电子笔记155（2006）8793在对象X上定义为HX = 0+ 1× X +2× X × X +...具有形式σ（x1，. ，xk），且对变量x1，.，X，k则代数A中的一个非线性方程态射e：X−→H<$X+A表示一个系统xtx递归方程组，每个变量x∈X都有一个递归方程组，其中每个tx要么是X中的一个递归项，要么是A中的一个元素。 一个解决方案e†分配给每个变量 x，其中tx= a，a∈A，元素a，并且如果tx= σ（x1，.，xk），则et（x）= σA（et（x1），.，et（xk））。注意，对于每个σ∈Σk，每个迭代的Σ-代数A都有唯一的幂等元（即，一个唯一元素a∈A，其中σ（a，...，a）= a）。事实上，考虑到方程x<$σ（x，.，x）。更一般地说，每个多项式在A中有唯一的幂等元。例如，对于深度为2的多项式，，τk），其中σ∈ τ k且τ1，.，τk ∈ n考虑递归方程x0<$σ（x1，x2，.（xk）xiτi（x0，x0，. ，x0） （i = 1，.，k）。一个迭代代数的例子是所有（有限和无限）树的代数T所有有理树的T的子代数R也是迭代的，见[21]。例2.6特别地，对于一元代数（H=Id），代数α：A−→A是迭代的i <$αk有唯一的不动点（k≥1），参见[3]。 和A是一个CIA i ∈，而且在ffi中不存在无穷序列（an）n∈，使得αan+1=an，见[18]。注2.7在[3]中，我们证明了对于局部有限可表示范畴ffi的每一个无穷函子H，在每一个对象Y上存在一个自由迭代代数RY。此外，我们还给出了RY作为由有限可表示对象携带的所有余代数X−→HX+Y的余极限，换句话说，对于ffi的每个对象Y，RY是Y中所有有限可表示方程的余极限。例如，对于Setthe free的多项式函子H集合Y上的迭代代数是Y上所有有理树的代数R∈Y。一般来说，我们称自由迭代代数的单子R为由H生成的有理单子。我们在[3]中证明了有理单子R是H上的自由迭代单子。94J. Adámek等人/理论计算机科学电子笔记155（2006）87n0nn+1个nnn+1个n例2.8完全度量化代数 完备度量空间被认为是语义学的合适基础。完备度量空间在语义上的第一个范畴化处理是由P。America和J.Rutten [6].让CMS表示所有完备度量空间的范畴（即，这样每个柯西序列都有一个极限），度量在区间[0， 1]。同态是非扩张映射f：（X，dX）−→（Y，dY），i.例如，的不平等dY（f（x），f（XJ））≤dX（x，XJ）对X中的所有x，XJ成立.给定完备度量空间X和Y，hom-setCMS（X，Y）携带逐点度量dX，Y定义如下：dX，Y（f，g）= supdY（f（x），g（x））x∈ XAmerica和Rutten称函子H：CMS−→CMS收缩，如果存在常数ε1，使得对于任意态射f，g：X−→Y，我们有dHX，HY（Hf，Hg）≤ε·dX，Y（f，g）.引理2.9如果H：CMS−→CMS是收缩函子，则每个非空H-代数是CIA。证据 设α：HA−→A是非空H-代数. 选择元素a曲霉 对每个方程态射e：X −→ HX + A定义一个序列e<$在CMS（X，A）中，如下：(i) e†= consta，值a的常数函数。(ii) Givene†然后，定义如下（比较（2.1））：e†Xn+1zA，、（2.2）e、HXz，[α，A]+AHe+AHA+A证明了（e†）是CMS（X，A）中的Cauchy序列. 事实上，z=d（e0t，e1t），然后我们通过归纳证明，d（e<$，e<$）≤z·εn。n n+1对于来自上述不等式的归纳步骤，导出d（Het，Het）≤z·εn+1，然后使用e<$和e<$的定义见（2.2）。因此n n+1、J. Adámek等人/理论计算机科学电子笔记155（2006）8795n2sequence（e†）isCauchy：对于numberδ>0chosek，具有hz·εk<δ·（1−ε）。则对于所有n个不等式，d（ek<$，ek+n<$）≤乌斯季-1i=0时†K+I†k+i+1）≤z· 乌斯季-1i=0时εk+i

下载后可阅读完整内容，剩余1页未读，立即下载