终余代数与连续函数的特性与构造数学【2006年电子笔记】

理论计算机科学电子笔记164（2006）141-155www.elsevier.com/locate/entcs终余代数尼尔·加尼1彼得·汉考克2英国诺丁汉大学计算机科学与信息技术学院德克·帕丁森3莱斯特大学计算机科学系英国莱斯特摘要可以追溯到布劳威尔，StrA→B型的连续函数，其中StrA是A的元素上的无限流的类型，可以用良好建立的A-分支树来表示，其叶子是B的元素。本文将上述对应关系推广到集合和函数范畴上幂级数函子的末余代数上定义的函数。虽然我们的主要技术贡献是所有连续函数的特征，定义在最终余代数上，并通过归纳类型在离散空间中取值，但方法论的一个观点是，这些归纳类型最方便地在依赖类型理论的框架中制定关键词：连续函数，最终余代数，构造数学1介绍布劳威尔选择序列是离散对象（例如自然数）的流，其中不需要导出或生成流 的 连 续 项 的 选 择 序 列 是 “ 无 限 对 象 ” 的 范 例 [11][12][13][14][15][16][17][18][19]根据Brouwer，所有关于选择序列的函数都是连续的。函数的连续性意味着如果你想让它提供给你有限的量，1电子邮件：nxg@cs.nott.ac.uk2电子邮件：hancock@spamcop.net3 电子邮件地址：dirk@mcs.le.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.06.009142N. Ghani等人理论计算机科学电子笔记164（2006）14101b0的01B301B1B2图1.连续函数Str{0，1}→B关于函数的值的信息，那么你只需要提供它关于它的参数的有限数量的信息归结为灰烬，布劳威尔由于这种归纳结构，函数必须是连续的。具体地说，我们定义了集合RA B= μX.B+（ A→ X）其中μX表示初始代数的形成（RA实际上是自由单子由（A→_）生成），然后通过良基结构递归函数吃：RA B→StrA→Beat（ inly）α=yeat（inrf）α=e at（fα0）αJ这里α的类型为StrA，α0表示α的头，αJ表示它的尾。函数eat定义了一个表示|不|= StrA → B类型函数的eat t由RA B的元素t组成。这些对象t被解释为终止程序，它读取有限个A在图形上，我们可以用有限树来表示Str{0，1}→B类型的连续函数，如图1所示。一般来说，StrA→B型连续函数的表示将是有根据的，并且如果A是有限的，则它是有限的为了在无限比特流（an）n∈ω处计算函数的值，我们从根开始然后，根据树的第一个符号a0然后，从我们刚刚到达的节点开始，使用流（an+1）n∈ω一旦我们命中一个叶子，我们就输出B的相应元素。为例如，图1所示的树表示的函数将值b2到具有初始段（1，0，1）的每个流。不同的RA B型良基对象可以表示相同的StrA→B型函数。表现是内涵性的。然而，在意图不同的实现之间存在明显的计算差异，它们具有相同的功能：它们提供产出，对投入的需求或多或少。布劳威尔N. Ghani等人理论计算机科学电子笔记164（2006）141143关注经典上，完整性是由eat是满射的事实证明的，这给了我们一个多对一的对应关系，μ X。B+（A→X）eatz，z，cts（一）（StrA−→B）在这个意义上，μX.B+（A→X）的每个元素表示StrA→B型的连续函数，但每个这样的函数可以有多个表示。在今天的现代术语中 因此，布劳威尔它们是连续的。激发本文的一个问题是：Brouwer的分析能推广吗？我们的 回 答 是 ： 至 少 对 于 具 有 离 散 余 域 的 函 子 ， 可 以 表 示 为 幂 级 数 ：<$n∈ωAn×Xn。更详细地说，我们构造了一族（Rn）n∈ω归纳型函数，并证明了所有（νF）n→B型连续函数，其中B是离散的，都可以用Rn型元素表示.作为一个直接推论，我们得到了（νF）n→B型连续函数的集合是所有包含常数函数且在a下闭的函数的最小集合的修补操作，这将在第5节中详细讨论。我们的动机不仅仅是好奇心。上述基于流的表示的一个简单的扩展是StrA→StrB型连续函数用ν X.RA（B×X）型元素的表示。这给了我们一个分析流-处理组件，具有可直接在表示上定义的组合运算符。 如果这种分析可以推广到“分支”的函子本文件就是朝着这一方向提出的。概括。2符号和标记我们写ω={0，1，2，. }，并将n∈ω与它的前辈的集合标识，即n={0，1，...，n-1}。实数用R表示，R≥0是非负实数。我们用Set来表示集合和函数的范畴，而Setω表示从ω到Set的函子的范畴，其中我们将ω视为离散的。因此，集合ω的一个典型元素是集合An的一个ω-指标族（An）n∈ω，我们用（An）简单地表示它。从（ An）到（ Bn）的一个典型态射是一个ω-指标族（fn：An→Bn）n∈ω，记作（fn）。两个集合A和B的余积记为A+B，对于典型的注入记为inl：A→A+B和inr：B→A+B类似 地，A和 B的乘 积表示为 A×B 和π1：A×B→A和π2：A×B→B，典范投影如果（fi）i∈I是一族函数Ai→B，我们在i中写：Ai→Σi∈IAi对于144N. Ghani等人理论计算机科学电子笔记164（2006）141Σ正则注入和[f i|i ∈ I]对于唯一函数u：（满足u在i= f i.i∈IAi）→B，如果F是Set上的闭函子，我们写μF（resp.v F）对于初始代数（resp.F的最终余代数），只要它存在。初始代数的结构图（分别为最终余代数（final coalgebra）表示为：F（μF）→μF（resp. out：νF→F（νF））。有时，我们写μX.FX（resp. FX）而不是μF或νF，以使F的自变量显式。这些和其他变量绑定操作的范围是我们将νX.A×X写成StrA，并采用如下约定：如果α：StrA，则α=（α0，αJ），其中α0是它的头，αJ是它的尾。类似地，树A=νX.X×A×X。我们使用标准符号，并将A→B写为来自A的所有函数的集合CTS到B;如果A和B是拓扑空间，则A−→B表示连续函数从A到B3连续函数对于全截面，设F：Set→Set是ω-连续的闭函子，B∈Set.ω-连续性意味着F与投射链的极限交换，因此有一个最终余代数LimnFn1。我们用νF=νX.F（X）作为这个投影极限的简写，并用pn：νF→Fn1表示正则投影。 序列1<$F1<$F21的连接态射. 记为pnm：Fm1→Fn1。如有需要，我们会考虑为B提供离散拓扑众所周知[3]，最终余代数作为投射极限的表示产生了一个超度量，我们现在引入。定义3.1（Baire拓扑）让d（x，y）= 2−n其中n = max{k |p k（x）= p k（y）}对x，y∈νF.我们称诱导拓扑为Baire拓扑，并且总是假设νF是这样拓扑化的。如果n≥0，我们定义（νF）n上的度量dn，其中x=（x1，.，xn）和y=（yi，.yn）∈（νF）nbyd（x，y）=max{d（xi，yi）|i=1，.，n}。很容易看出，dn也定义了（νF）n上的超度量。事实上，我们正在处理的拓扑是由超度量是没有后果的本文。注意：超度规的定义是相当非构造性的。我们也可以把Baire拓扑描述为由νF中所有共享公共前缀p的对象的邻域基{Np}p生成。然而，这将涉及更多一点我们宁愿不这样做的机械。连续函数（对于离散空间）的直观概念是，它的值f（a）仅取决于关于其自变量的有限基于B具有离散拓扑的事实，我们有引理3.2A函数f：A→B，其中 A是度量空间， B具有N. Ghani等人理论计算机科学电子笔记164（2006）1411451离散拓扑是连续拓扑a∈f−1（b）=>0.B（a）f−1（b）对于所有a∈ A和所有 b∈ B，其中 B∈（ a）是以a为中心，半径为- 是的因此，函数值f（a）在函数的某个邻域内是恒定的。a.在流上的Baire拓扑的情况下，a的n-邻域是与a共享一个（固定和有限）前缀的流的集合。因此，函数的值仅取决于a的前缀。在一致连续的情况下，这个量不依赖于参数。下面的经典例子说明了这一点。例3.3设FX=ω×X;通常我们对νF记为Strω，对Strω的一个典型元素记为（an）n∈ω。(i) 每个常数函数f：Strω→ω是连续的。(ii) 对于任意k∈ω，函数（an）n∈ω→ak是一致连续的。(iii) 如果（fn）是连续函数序列Strω→ω，则λ（an）.fa0（an+1）：Strω→ω是连续的。(iv) 函数（an）n∈ω<$→aa0 是连续的，但不是一致连续的。.(v) 分配（a）<$→0如果k∈ω.ak= 0不定义连续n n∈ω1例其他情况功能。为了定义一个系统的可判定性所需的函数，这与毕晓普的有限全知原则相对应[ 5 ]。这当然是建设性的无效。从计算的角度来说，我们感兴趣的是函数f可能需要访问多少关于参数a的信息才能计算值f（a）。通过连续模给出了一个定量测度。在一般拓扑学中，连续模是一个函数，它对度量空间的每个点x和每个δ>0产生一个δ >0，满足在x处连续的通常δ−δ定义。由于我们只对在离散空间中取值的函数感兴趣，因此下面的定义使其适应我们的设置。定义3.4假设f：（νF）n→B是一个（不一定连续的）函数。函数m：（νF）n→R≥0是f的连续模，有时简称为模，如果对所有的x，y ∈（νF）n.dn（x，y）≤m（x）=f（x）=f（y）作为这个定义的一个小结果，我们有引理3.5函数f：（νF）n→ B是连续的，且它有模。146N. Ghani等人理论计算机科学电子笔记164（2006）141001110111101（0，0）（0，1）（1，0）b0b1b2（一、一）（0，0）（0，1）b2b1（1，0）（1，1）b0的（0，0，0，0）（1，1，1，1）B4（0，1，0，0）. . . .. . . .B4B5图2.一个连续函数树{0，1} →B图3. 无限二叉树的初始段注意，连续模决不是唯一的：如果m是f，则每个MJ都是如此，其中MJ（x）≤m（x）。通常连续模的形式为m（x）= 2−k（x），其中k：（νF）n→ω。由于ω是有序的，在这种情况下，（经典地）存在最大的连续模，其对应于需要计算特定函数的值4连续函数在这一节中，我们展示了如何通过一个归纳函数来诱导νX.FX→B型的连续函数，其中F是可表示为幂级数的集合上结构我们请读者检查一下，在导言中给出的对吃的定义的简单概括肯定会失败，例如。对于无限树的情况，或者函子FX=X×A×X的最终余代数。 消耗树的根a将给我们留下两个子树，我们不能对它们应用eat（a）。非正式地说，可以表示树A→B类型的连续函数树的分支度在每次遍历弧时都提高到2的幂，如图2所示。给定一棵树t，我们从树的根开始，根据树的根元素选择第一个分支去除这个根元素，我们剩下两棵树，（t1，t2），即t的左子树和右子树，相应地有一对根元素（a1，a2）∈A×A我们根据（a1，a2）选择下一个分支，这给我们留下了四个子树;我们继续这个过程，直到我们到达树的一个叶子，我们将其作为函数值例如，图2中表示的函数将b1分配给图3中左侧树的每一个树，并将b5分配给右侧树的每一个（无限）扩展。N. Ghani等人理论计算机科学电子笔记164（2006）141147σ这种类型的树可以方便地使用集合的索引族或依赖类型来定义，其中依赖性被用来记录分支度。从技术上讲，这将涉及从定义在集合范畴中的初始代数μX.B+（A→X）移动到范畴Setω上的内函子M的初始代数。我们将恢复连续函数的表示，例如（TreeA）n→B作为Rn的元素，其中（Rn）n∈ω是函子M，定义为M：集合ω→集合ω定义为M（（Xn）n∈ω）=（B+（An→X2n））n∈ω从我们的一般分析可以得出，R1表示树A→B型的所有连续函数，因此将对应关系（1）推广到无限二叉树这种推广的代价是，我们需要处理集值函数，也就是说，集合的索引族，而不仅仅是集合。我们的概括就变成了μ（Xn）n∈ω. （B+（An→X2n））n∈ωeatz，z，ncts（（树A）在全文中，我们固定了一个幂级数内函子，−→B）ΣA×Xi，F（ X）=i∈ωi其中（Ai）i∈ω：集合ω。注意，幂级数内函子自动是ω-连续的。在本节中，我们详细描述了（νF）n→B型连续函数的表示，它使用了归纳定义的依赖类型。为了使说明书更具可读性，我们做了以下标记约定。约定4.1如果n∈ω且 σ：n→ω，我们令 A=Σi nAσ（i）和σ<$=i< n σ（i）.用这个符号，我们用来表示类型为νF→B的连续函数的归纳定义类型族是以下函子的初始代数。定义4.2函子M：Setω→Setω，定义为M（Xn）n∈ω=（ B+σ：n→ω（Aσ→Xσ<$））n∈ω是与F相关的表示函子。若（Rn）n∈ω是M的初始代数，则Rn的元素表示（νF）n→B型连续函数.在我们继续讨论表示定理之前，我们需要建立以下事实：引理4.3函子M有初始代数。证明因为函子范畴中的上极限是逐点计算的Q对于M的初始代数，我们始终记为（R，ρ），其中R=（Rn）n∈ω，ρ=（ρn）n∈ω.148N. Ghani等人理论计算机科学电子笔记164（2006）141n为了使本文的后续部分更具有可读性，我们引入了初始M-代数的结构映射ρn的约定4.4对于本文的其余部分，我们固定构造函数constn：B→Rn和 forkn：（σ：n→ω（Aσ→Rσ<$））→Rn有一个性质：ρ n=[constn，forkn]。 换句话说，constn= ρ ninl，fork n= ρ n inr.为了在FX=A×X的eat定义之间进行类比，我们确定了以下规范同构：约定4.5对于本文的其余部分，我们固定一个规范同构nout×···×outIn=Σσ¯dn：（ νF），z（i∈ωAi×（νF）），zσ：n→ωAσ×（νF）其中右手箭头是迭代分配律4。此外，我们确定了以下构造函数族，它们与d n联合逆：cσ：Aσ×（νF）σ<$→（νF）n，其中σ：n→ω与物业在哪里[…] ]是余元组。[c σ|σ：n → ω]= d−1使用这些约定，eatn的方程：Rn→（νF）n→B现在变为：eatn（ constb）（cσ（a，t））=beatn（fork（fσ））（cσ（a，t））=eatσ<$fσ（a）（t）（二）注意，与F（X）=A×X的函子的情况相反，我们可以必须在递归调用中调用一些更高（或更低）arity的eat函数我们的下一个目标是证明上面的方程唯一地确定一个连续的（v F）n→B型函数引理4.6存在唯一的函数族（eatn）n∈ω，其中eatn：Rn→（νF）n→ B，满足方程（2）。证明我们fixZ=（Zn）∈Setω其中Zn=（νF）n→B. 请注意，Z带有一个M-代数结构n=（n），定义为n（inlb）= λx.bn（inr（f σ））=[uc f σ|σ：n → ω] nN. Ghani等人理论计算机科学电子笔记164（2006）141149[4]迭代分配律由（有限）选择公理和量化器的某些运算证明150N. Ghani等人理论计算机科学电子笔记164（2006）141其中，对于一个函数f：A→B→C，映射ucf：A×B→C是f的非卷积形式，通常定义为（a，b）<$→f（a）（b）检查诱导的通用箭头u：R→Z满足等式2是例行的。相反，满足方程2的函数族un，其中un：Rn→Zn是M-代数态射;因此eatn是唯一定义的。Q这是定理的前半部分：我们仍然需要确保eatn是连续的。根据引理3.5，这可以通过明确地提供eatn的连续性模来确保。如果我们表示StrA→B型连续函数，对于良基的A-分枝树，连续模仅仅是长度为了到达B标记的叶子，我们需要遍历树的路径。例如，图1中表示的函数的连续性模将1分配给以0开始的每个流，将3分配给具有初始段的流。（1，0，0）。 下一个定义将其转换为我们的依赖类型设置。引理4.7存在唯一的函数族（mn），其中mn：Rn→（νF）n→ω，满足方程mn（const b）（ cσ（ a，t））=0mn（fork（fσ））（cσ（a，t））=1+mσ<$（fσ（a））（t）（三）对allσ：n→ω，alla∈Aσ，allt∈（νF）σ<$.证明与前面引理的证明一样，我们将Z=（Zn），其中Zn=（νF）n→ω，并通过下式定义Z上的M-代数结构：n（inlb）= λx。0n（inr（f σ））= 1 +[uc f σ|σ：n → ω] n其中，对于函数g：X→ω，我们设1+g=λx。1+g（x）。然后证明了（mn）作为唯一的R→Z型代数态射而出现，并且满足方程（3）的每个函数族都有资格作为代数态射。Q在证明mn产生eatn的连续模之前，我们需要一个小的技术引理：引理4.8设x=cσ（a，t）和y=cτ（b，s）∈（νF）n，其中σ，τ：n→ω，（a，b）∈Aσ×Aτ和（t，s）∈（ν F）σ<$×（ν F）τ<$. Ass umek≥0。若dn（x，y）≤2−（k+1），则then σ=τ，a=b且dσ<$（s，t）≤2−k。证明注意，对于x=（x1，.，xn）和y=（yi，.，y n）我们有d n（x，y）≤ 2−li 1≤ i ≤ n. pl（x i）= pl（y i）.N. Ghani等人理论计算机科学电子笔记164（2006）141151现在的主张是从考虑图表νF，PK，pk，+，1=Fpk输出、、布雷尔我操！ ΣSk i k+1F k1，ri∈ωAi×（F1）=F1它定义了投影p k+1，其中！：F1→1是唯一的这样的箭头。Q引理4.9如果mn：Rn→（νF）n→ω与引理4.7相同，则2−mn（a）：（νF）n→R ≥0是eatn（a）的连续模。证明我们通过对k的归纳证明以下陈述：对所有n∈ω，所有x，y∈（νF）n和所有r∈Rn：若mn（r）（x）=k且dn（x，y）≤2−k，则eatn（r）（a）=eatn（r）（b）。对于k= 0，没有什么可展示的，因为在这种情况下，我们有r=constb，对于某个b∈B。现在我们建立k+1的要求，其中我们假设x=c σ（a，t）和y=cτ（b，s）对于rσ，τ：n→k，（a，b）∈Aσ×Aτ和d（s，t）∈（νF）σ。所以假设m n（r）（x）=k+1且d k+1（x，y）≤2−（k+1）。根据引理4.8，我们有av e σ=τ，a=b和dσ<$（s，t）≤2−k。 我们称之为viatez=σ<$=τ<$。通过定义mn，我们有r=fork（fσ）。设RJ=fσ（a），则RJ=fτ（b）。当dσ<$（s，t）≤2−k时，我们有一个归纳法，eatzrJs= eatzrJt并且eatn（r）（cσ（a，t））=eatn（r）（cσ（b，s））由等式推理得出。Q特别地，这表明所有函数eatn（r），其中r∈Rn，是连续的。推论4.10函数eatn（a）：（νF）n→B对所有 n∈ω连续且所有a ∈ Rn.5完整性回想一下，（Rn）n∈ω是与幂级数F：Set→Set相关联的表示函子的初始代数的载体。我们在前一节中已经看到，每个元素a∈Rn，确定一个连续函数eatna，其类型为（νF）n→B. 在这一节中，我们建立了相反的情况，即每个连续函数f：（νF）n→B都可以用Rn的一个元素表示。我们首先考察流的特殊情况。CTS公式5.1Everycontin usfunctio n harese n tive：arf：StrA−→B. 律师：μX.B+（ A→ X）.吃r = f。证明证明是非建设性的，并在任何意义上展示的代表。假设f是连续的，但没有代表。 则它不可能是常数，并且对于某个a：A，fa没有表示152N. Ghani等人理论计算机科学电子笔记164（2006）141式，其中fa（α）= f（a，α0，α1，. ）的。继续以这种方式，并应用依赖选择公理，有一个N. Ghani等人理论计算机科学电子笔记164（2006）141153stream（a0，a1，. ）：StrA使得对于所有n，（. （f a0）a1... ）an−1 不是恒定的。由此可见，在这个论证中f不可能是连续的，这与我们的假设相矛盾Q我们可以立即得出一个推论引理5.2函数f：StrA → B是连续的当且仅当它属于包含所有常数函数的最小类K（StrA→ B），并且在运算pk下是闭的。pk：（A→（StrA→B））→（StrA→B）pk（f）=λα.f（α0，αJ）证明连续函数包含常数函数，并且在pk下是闭的，因此K中的所有函数都是连续的。"only if“的方向是直接从引理。Q现在考虑方程CTSrep：（StrA−→B）→μX.B+（A→X），.inl（b）α. f（α）=b（四）f›→inr（λa. rep（fa）），否则其中，对于函数f：StrA→B，映射f a：StrA→B是其形式导数，由f a（a0， a1， . ） = f（ a， a0， a1， . ）的 。 注 意 pk 与 导 数 运 算f<$→（λa.fa）是逆运算。f的连续性的归纳特征保证了任意连续函数的表示集非空。它本身并不产生一个典型的代表。似乎几乎可以肯定（但令人惊讶的是证明起来很难），方程4有唯一的解，因此函数rep是经典定义的。如果是这样的话，我们可以加强上面的引理，说函数eat具有CTS右侧逆：eatrep=id：StrA−→B接下来，我们转向一般情况。定理5.3每个连续函数都有一个代表：nctsn∈ω。f：（νF）−→B。Rn. eatnr=f.这个证明与前面的引理基本相同假设nctsf：（νF）−→B是连续的，但在Rn中没有代表。那么f不能是对于某些σ：n→ω和a：Aσ，fa没有代表，其中函数fa（f对a的导数）由下式给出：f a：（νF）σ<$→Bt<$→ f（c σ（a，t））.154N. Ghani等人理论计算机科学电子笔记164（2006）141在流的情况下，继续以这种方式，我们得到一个收缩序列的邻域的论点，其中f不是常数。由此可见，在这个论证中f不可能是连续的，这与我们的假设相矛盾。Q在流的情况下，我们可以快速推断Σ推论5.4型函数n∈ω（（νF）n→B）连续当且仅当它属于包含所有常数函数的最小类K，并且对于每个 n∈ ω，σ： n→ ω闭于pkn，σ：（Aσ→（νF）σ<$→B）→（νF）n→Bpkn，σ（f，cσ（a，t））=f（a，t）这是我们所建立的极限。看起来这些结果很有可能被加强，以给出一个关于吃的右逆的明确描述，如下所示。在同构的ndn，z（νF） R、[cσ|σ：n→ω]σ：n→ωAσ×（νF）在第4节中介绍过，我们可以为一个函数族规定下列方程代表：nctsn∈ω成为（eatn）的右逆：（（νF）−→B）→Rn），nctsrepn：（（νF）−→B）→Rn.常数bf=λx.b（五）f›→对于k（λa.repfa）σ：n→ω否则其中，对于a∈Aσ，函数fa（f对a的导数）由下式给出：f a：（νF）σ<$→Bt<$→ f（c σ（a，t））.不一定cσ：Aσ×（νF）σ<$→（νF）n且ab中有（νF）σ<$。可以合理地推测方程（5）具有唯一解rep，使得nctseat n rep n=id：（νF）−→B。N. Ghani等人理论计算机科学电子笔记164（2006）1411556结论和进一步工作本文给出了从νF到B的连续函数的详细内涵分析，其中F是ω-连续函子，νF是F的最终余代数，具有自然拓扑，B是离散的.更确切地说，我们用归纳定义的族（Rn）的元素定义了这些函数的表示：集合ω，并确定了这种表示是完备的，尽管不是唯一的。它有一个-张力特征，反映了同一功能的不同实现的贪婪在流的情况下，情况是这给了我们一个有用的流处理组件的模型，特别是可直接在表示上定义的组合运算符。用近似相同的方法，很可能对（A×）以外的ω-连续函子的最终余代数进行分析。最后，人们可能希望从这条研究路线中产生行为良好的回溯图式同样，比较[ 10 ]《易经》中的“气”字，是指类似的评论适用于Uustalu和Vene困难主要在于如何控制所有的成分，一个简单的符号和正确的形式。似乎从定义我们的Σ幂级数A函子Σ×Xn到使用容器类型定义它们[1]s：S× P（s）（其中集合{P（s）|s：S} are finite）将简化符号并驯服一些细节。这在直觉上是有道理的，因为人们会避免将给定元数构造器与子树数粘贴在一起的必要性，从而避免了例如f σ ′的计算中涉及的算术开销。这种扩展的兴趣部分在于，有了更灵活的函子，我们可以使用流以外的潜在无限数据类型来模拟流或无限缓冲器以外的其他形式的通信。例如，摩尔机可以描述为v X.O×SI的元素，其中I和O分别是输入和输出字母。可以通过以下方式对通信进行建模：共享内存，或某种通信端口，因此带来了一些强大的技术来应对这些棘手的情况。这种应用显然是可取的。还有一些其他的自然扩展需要考虑。首先，我们不清楚是否可以将我们的结果推广到比幂级数更广泛的函子类或容器。 我们把这类函子看作是，当一个函子吃掉顶层后，对于幂级数的最终余代数，人们有一个自然的剩余碎片的概念。任何扩展都必须以某种方式计算碎片的一般概念，但目前还不清楚如何做到这一点。然而，很明显，隐藏在背景中的是一个左Kan扩张，这可能是显著扩展我们可以处理的函子类的关键，我们仍在试图理解这一点。本文对拓扑问题作了具体的探讨，nn156N. Ghani等人理论计算机科学电子笔记164（2006）14111另一个悬而未决的问题是拓扑空间范畴的一般性质在多大程度上可以被使用。相关工作在表面上，我们的结果似乎与[2]中报道的见解是对偶的，其中表明具有某些域类型的函数类型可以表示为最终余代数，而我们表明连续函数可以表示为初始代数，至少当余域是离散的时。这两个概念的核心都是幂运算和乘法之间的附加运算（A×）E（A→）文[4]中的工作与我们的结果有相似之处。这项工作涉及从经典证明中提取建设性内容的方法，重点是涉及有限序列和非建设性选择原则的定理研究的一种方法删除了对无穷序列的任何引用，并将定理转化为归纳定义系统。所研究的定理与良拟序的概念有关，而不是像我们的情况那样，我不知道你在说什么。如何（天真地）定义bothesh形式“f：StrA，n：N hd（f），. “的。在机器人中，我们将对一个1概念.正 如 在 引 言 中 所 指 出 的 ， 我 们 的 结 果 可 以 追 溯 到 BrouwerKreisel 和Troelstra为布劳威尔的分析提供了一些启发，如果不是证据的话，归纳定义集的名称是“K”。这一套是灵感的功能'吃'。霍华德[ 7 ]、[ 8 ]研究了哥德尔T通过一个类似于K的广义归纳定义的扩展确认感谢Conor McBride对这个主题的讨论，以及其他方法的建议。引用[1] 迈克尔·艾伯特，托尔斯滕·阿尔滕基奇，尼尔·加尼。 容器-构造严格正类型。理论计算机科学，342：3-27，2005年9月。 应用语义学：选定的主题。[2] T.阿尔滕基希一阶函数类型作为终端余代数的表示。在Typed Lambda Calculi and Applications，TLCA2001，2044号，计算机科学讲义，第8 - 21页[3] M. Barr.良基集合论中的终端余代数。Theoretical Computer Science，114（2）：299[4] 联合Berger和M.赛森伯格归纳定义和选择原则在程序综合中的应用。在从集合和类型拓扑和分析走向实用的基础建设性数学，第48卷牛津逻辑指南，第137-148页。牛津大学出版社，2005年。[5] E.主教 建设性分析的基础。 麦格劳-希尔，纽约，1967年。N. Ghani等人理论计算机科学电子笔记164（2006）141157[6] M.达米特直觉主义的要素。牛津逻辑指南Clarendon Press，Oxford，2nd edition，2000.[7] W.霍华德棒递归法对棒诱导的功能解释。Compositio Mathematica，20：107[8] W.霍华德零阶递归泛函项的序数赋值。 Journal of Symbolic Logic，35：345，1970.[9] 马丁·勒夫无限的数学见CONOM-88，LNCS第417号，第147-197页。Springer-Verlag，1988.[10] J. Rutten行为微分方程：流、自动机和幂级数的共归纳演算。Theoretical Computer Science，308（1）：1[11]A.S.特罗斯特拉选择序列：直觉主义数学的一章。牛津逻辑指南Clarendon Press，Oxford，1977.[12] T. Uustalu和V. Vene。数据流编程的本质。在第三届亚洲研讨会上。《编程语言与系统》，APLAS'05，第3780期，计算机科学讲义，第2-18页。Springer-Verlag，2005.