拓扑Domain理论中的计算效应：建立可数基空间范畴QCB及其子范畴TP的灵活框架

理论计算机科学电子笔记158（2006）59-80www.elsevier.com/locate/entcs拓扑Domain理论中的计算效应Ingo Battenfeld英戈·巴滕菲尔德1，2英国爱丁堡大学信息学院LFCS摘要本文致力于建立可数基空间范畴QCB及其子范畴TP，作为程序设计语言指称语义的一个灵活框架特别是，我们表明，这两个类别的自由代数任意可数参数化方程理论，因此，以下的思想Plotkin和电源，能够模拟广泛的计算ececonects。此外，我们给出了自由代数的一个显式构造关键词：拓扑论域理论，论域理论，计算效应，指称语义。1引言指称语义学的主要任务之一是为建模编程语言提供一个抽象的框架，该框架支持许多类型构造并对各种各样的计算现象建模。对此最流行的方法是（经典）域理论（见[1]），其中考虑了有向完全偏序集（dcpos）和连续映射的范畴Domain理论已经成功地提供了范畴是Carnival封闭的（因此允许类型构造，如产品和功能空间），范畴模型不终止，递归1本研究由EPSRC研究基金“计算元语言的拓扑模型”支持。2电子邮件：I.D. sms.ed.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.04.00560I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）59P以及递归类型、允许多态类型构造的类别和支持诸如非确定性或概率计算（通过幂域构造）的其它计算现象的类别。然而，域理论并没有成功地提供一个单一的类别结合所有这些积极的结果。Smyth [19]提出了另一种更简单的指称语义方法，该方法基于将数据集类比为拓扑空间，将程序类比为连续函数。拓扑域理论的目标是将这些方法结合起来，并提供一个拓扑空间的类别，模型的所有上述功能。我们所提出的框架的基础范畴是QCB，可数拓扑空间的拓扑等价物的范畴，它已被证明是笛卡尔闭的（见[4，8]），并具有拓扑前域的完全相关指数理想TP（见[2，18]），这允许在拓扑环境中进行Domain理论的构造。一个显著的性质是，这些范畴可以被看作是Scott组合代数ω上的可实现拓扑中的子范畴本文的目标是展示如何通过基于Plotkin和Power [12，13，14]的工作的自由代数方法在QCB和TP中建模Moggi [9，10]意义上的计算效应一般来说，函数式编程语言的基本概念是由一个干净的数学演算给出的，λ演算，它丰富了一些基本特征，如基本类型，常量或函数。然而，在计算中会出现非功能性行为，例如非确定性选择、非终止、异常、副事件或输入/输出，而这些所谓的计算事件通常不被纯λ演算所覆盖。因此，如果一个人的目标是给语义的实际实现的编程语言，相关的计算效果必须考虑在内。最初的方法是由Moggi [9，10]采用的，他区分了值的类型和计算的类型对于语言中的每种类型的值X，都有相应类型的计算TX，可以在其上对计算结果进行建模。在MoggiC. 最近，Plotkin和Power [12，13，14]表明，令人惊讶的计算上有趣的单子的数量是作为自由代数生成的方程理论在泛代数的意义。这种方法的惊人之处在于，相关的代数运算恰好是用于生成相关结果的自然计算原语。例如，如果考虑二进制运算，则选择：TX2→TX服从I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）5961表示幂等性、交换性和结合性的方程，则相应的自由代数函子就是非决定单子的函子因此，Plotkin和Power重新表述了Moggi鉴于Plotkin和Power因此，我们证明了范畴QCB和它的子范畴TP具有可数参数化方程理论的自由代数，因此许多计算结果确实可以在其中建模由于QCB的对象是拓扑空间，我们首先研究拓扑空间和连续映射的范畴Top中的自由代数Top中的无穷（非参数化）方程理论的自由代数的工作已经由Malcev [7]和Taylor [20]完成然而，即使方程理论的自由代数存在于Top中，一个著名的范畴上极限构造在这里不起作用。方程引起特殊的问题，由于缺乏carnival封闭性的顶部。因此，Porst [15]研究了Top的核心有效carnival闭子范畴的自由代数，并证明了这里的情况有所改善。在[8]中，QCB被引入作为序列空间和连续映射范畴Seq的一个子范畴，而Seq是Top的一个核心有效的Caribbean闭子范畴。我们将证明QCB在Seq中的自由代数构造下是封闭的，并且TP中的自由代数是使用反射函子获得的。本文中我们关于Top和Seq的自由代数的一些结果是将有限个方程理论的已知结果推广引理3.3以下。其他结果，如定理3.8，似乎是新的。本文的主要结果是证明了QCB和TP中广泛的一类方程理论的自由代数的存在，这使我们能够在Plotkin和Power意义下模拟计算结果此外，我们给出了一个明确的结构的自由代数在这两个类别，这将是非常有用的结合我们的结果与其他性质的框架QCB。在第2节中，我们首先介绍QCB和拓扑前域，并将它们与Seq联系起来。然后，在例子的指导下，我们在第3节中给出可数参数化签名的定义，并在拓扑空间和序列空间范畴中考察绝对自由代数，表明可数基空间在这种构造下是保持的第4节，我们62I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）59看看代数运算（在Plotkin和Power [14]的意义上），用它们来引入方程，并证明QCB中可数参数化方程理论的自由代数的存在性。在第五节中，我们将这些自由代数转移到TP上。最后，我们在第6节中给出结论2个房间设Top表示拓扑空间和连续映射的范畴。拓扑空间X的子集U称为序列开的，如果当x∈U且序列（xn）n收敛于x时，则该序列最终在U中，即存在K∈N使得对所有n≥K，xn∈U。请注意，拓扑空间的开集总是顺序开的。空间X称为序列空间如果相反的情况成立，也就是说，如果它的所有顺序开集都是开的。用Seq表示序列空间和连续映射的范畴。Seq是Top的一个满核映射子范畴，它把空间X的所有序列开子集都加到空间X的拓扑上此外，Seq是carbohydrate封闭的，这是Top没有的属性。从计算的角度来看，Seq似乎比Top更自然，因为这里连续性的特征是序列的收敛。QCB是以第二可数拓扑空间的拓扑同分子和它们之间的连续映射为对象的范畴。我们把QCB的对象简称为qCB-空间。QCB是Top和Seq的完整子类别 。 它 在 [8] 中 被 证 明 是 双 carbohydrate 封 闭 的 ， 并 且 从 Seq 和 其 他carbohydrate封闭子类别继承了这种结构，Top的超范畴[8，4]。此外，QCB可以被解释为Scott图模型P ω上的可实现性模型中的一个范畴 为为了本文的目的，我们只考虑QCB作为一个子类，Top和Seq，并忽略其他连接。一个拓扑空间可以配备有它的专门化预序±，其中x±y如果任何包含x的开集也包含y。则±是空间上的偏序当且仅当它满足T0-分离公理。相反地，任何有序集都可以配备它的Scott拓扑（见[5]）。然后单调收敛空间是一个拓扑空间，其专门化预序是dcpo，并且其拓扑比Scott拓扑粗糙单调收敛的qcb-空间称为拓扑预域[18]，TP是拓扑预域和连续映射的全子范畴证明了TP是QCB的一个完全相关指数理想（见[3]），因此它是特殊的卡里闭的.在经典的域理论中，人们经常区分那些具有I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）5963∈×→∈⊥→⊥最小元素（DCPPOS）。专门化预序为dcppo的拓扑预域称为拓扑域，它们形成范畴TD。通过QCB与经典Domain理论的比较，我们发现TP和TD分别是DCPO和DCPPO的拓扑类似物，DCPO和DCPPO分别是DCPO和DCPPO的范畴。DCPPOS和连续映射。值得注意的是，许多区域理论的性质和结构很容易延续到拓扑设置（见例如，[18，3]）。3参数化签名和绝对自由代数我们的目标是对QCB和TP中的计算效应进行建模，我们的方法基于Plotkin和Power的工作[12，13，14]。我们首先考虑一些效应的例子，并用它们来激发我们的理论。不确定性选择：假设我们想要为数据类型X建模不确定性。然后很自然地有一个操作choose：X2→X，使得choose（x，y）表示在计算x和y之间的非确定性选择。请注意，通过连续应用choose，我们可以在任何有限数量的计算之间模拟不确定性选择。概率选择：为了对数据类型X的概率非确定性建模，我们再次需要一个选择操作choose：IX2x但是这个时间由封闭的单位间隔I参数化。这里choose（λ，x，y）表示计算x以概率λ执行，y以概率λ执行。1−λ。我们选择这种方法，其中参数对象I而不是[12]中提出的方法，其中一个操作选择λ：X2→X，每个λI有两个原因。首先，在我们的方法中，我们在参数对象I和计算类型中都捕获了可计算性（由QCB中的连续性给出），而不仅仅是后者。第二个原因是，对每个λI都有一个运算意味着有不可数的运算次数，这在下面给出的理论中是不可能的。Nontermination：为了对数据类型X的nontermination建模，我们要求它有一个元素：X，它表示某种nontermination。 这可以看作是一个空值操作或常量：1个X（其中1是我们正在工作的类别中的终端元素通常，在Domain理论中，X表示dcppoX的最小元素。全局状态：设V是一组值，L是一组内存位置，系统的全局状态是对位置s∈VL的赋值。我们64I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）59× ×→ar（σ）σ我想对一个系统建模，在这个系统中，状态可以通过更新一个位置中的值来改变，并且可以读出一个存储器位置来确定一个计算。为此，我们需要一个类型X来支持操作update：L V X X，这样update（l，v，x）将值v写入位置l并携带输出一些计算x，并且查找：L×XV→X，使得查找（l，f）读出位置l的值vl，并且依赖于此执行一些com。截尾f（vl）。我们看到，在所有这些例子中，对象的计算类型支持相应的运算，这些运算类似于泛代数中考虑的运算回想一下，在泛代数中，我们有一个签名Σ，它是一组运算，每个运算都有一个arityar（σ），由一个有限数给出。那么一个代数是一个集合，在这个集合上每个运算都可以被解释。根据Plotkin的建议，我们将这个定义推广到允许参数对象，因此我们可以像概率选择的例子中那样解释参数化操作，并且我们允许我们的arity是可数无限的，就像全局状态的例子中的查找为了尽可能地保持一般性，我们在一个固定的C类中工作，它有可数的产品。定义3.1可数参数化签名是一个可数的运算符号集，每个运算符号都有一个arityar（σ）≤ω，以及一个参数对象Pσ，它是C的对象。和泛代数一样，我们现在可以定义范畴C中的n-代数、n-同态和绝对自由n-代数。计算效应可以在其上建模的数据集然后将由签名集的代数给出，签名集的运算是引起相应计算效应的运算作为标准，下面给出的自由代数构造将产生相关单子的函子定义3.2如果A是C的可数参数化签名，则C的一个对象A与一个C态射σ A：P σ×A→A，对每个σ∈ A，给出一个C的一个代数（A，{ σ A }）。对于C-代数（A，{σA}），（B，{σB}），C-同态是一个C-同态f：A→B使得下图对所有σ∈B都是可交换的P×Aar（σ）σAAPσ×far（σ）fJJPσ×Bar（σ）σBBI. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）5965^{}→ {}×B^→__我们用C表示C-代数和C-同态的范畴。对 于C- 对 象 X ， X 上 的绝 对自 由 C-代 数 是 C- 代 数的 对 象 （ FX ，{σFX}），对它存在一个C-态射ηX：X→FX，使得对任何C-代数（A，{σA}）和C-态射f：X→A，存在唯一的C-同态f：（FX，σFX）（A，σA），使得下图（C）可转换：FXfbAηFX注意，如果C是一个carbohydrate闭范畴，Z是C的任何对象，并且（A，{σA}）是一个C-代数，那么我们可以通过设置σAZ为下式的e×p个初始transs，来赋予AZ一个C-代数结构：σA（Pσ×eval）：Pσ×（AZ）ar（σ）×Z=Pσ×（Aar（σ））Z×Z→A.那么上面的图表可以概括为ZF X_f，，_A，Z×ηXFZ×X其中f必须是它的第二个分量上的同态所以在这种情况下，自由代数自动地利用伴随函子定理，可以证明：如果C=Set，Top，Seq，则对于任意可数参数化签名n，遗忘函子C<$C有一个左伴随F，它是绝对自由代数函子。在接下来的章节中，我们证明了QCB在Seq中的绝对自由代数构造下是封闭的，我们给出了一个明确的构造，并且TP中的自由代数可以通过反射自由QCB-代数得到。在集合论的情况下，有一种归纳的方法来构造绝对自由代数，也称为项代数。设f是可数参数化签名，f是赋值给集合X的函子，{σ（p，（xi）i∈ar（σ））|σ ∈ P，p ∈ P σ，σi. x i∈ X}，，，X_66I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）59O ×→O ×→||O||O（B）生成的拓扑，T也满足这些条件。I.E. （−）σ∈<$Pσ×（−）ar（σ）. Nowinductivivey定义所有序数α，F0（X）= X，F α+1（X）= X∈Fα（X））和对于极限序数β， Fβ（X）=αβFα（X）。换句话说，为了得到Fα+1（X），将通过对Fα（X）的项应用运算而得到的所有项相加，并且对于极限序数β取Fα（X）中出现的所有项对所有α β的并集。 不难看出，对于α≤αJ，Fα（X）<$FαJ（X）。 进一步地，对于第一个不可压缩基数ω1，对所有σ ∈ ω，我们都有r（σ）<ω1，且Fω1+ 1（X）=Fω1（X），从而可以得到X上的绝对自由代数由Fω1（X）给出. 运算定义为σ FX（p，（t i）i∈ar（σ））= σ（p，（ti）i∈ar（σ））。任何术语我们用occ（t）表示X上绝对自由代数的最小序数α使得t∈Fα（X）。注意occ（t）永远不是极限序数。对于本节的其余部分，假设R2是可数参数化签名，使得任何参数对象都是基于可数的拓扑空间。然后，对于Top、Seq和QCB，R2是一个定义良好的参数化签名，因为这些类别包括所有基于可数的空间。我们证明了Top和Seq的绝对自由代数函子F保持可数基空间。为此，让|Σ|是运算符号和位置与Σ一致的集合的参数化签名，σ ∈ Σ的参数集是|P σ|得双曲余切值.|·|：Top→Set是明显的健忘函子。引理3.3给定一个拓扑空间X，绝对自由的Topα-代数（FX，{σ FX}）有绝对自由的集合论的|Σ|- 代数（FX，σ FX）在X上，和拓扑（FX）是最精细的拓扑，sat-isfying：(A) （FX）是相容的，即 所有运算σX：P σF X ar（σ）FX是连续的，(B) 包含映射ηX：X→FX是连续的。给定序列空间X，绝对自由Seq-代数（FX，{σ FX}）有绝对自由集合论|Σ|-algebra（|FX|，{σ FX}）over|X|，并且拓扑O（FX）是最精细的拓扑，满足（B）并且：（AJ）（FX）是顺序相容的，即所有运算σX：PσF Xar（σ）当FXar（σ）具有以下乘积拓扑时，FXSeq.证据请注意，该结果是众所周知的顶部的有限签名。设X是一个拓扑空间。如果T是上的拓扑集合，|FX|满足（A）因此，最精细的拓扑O（FX）在|FX|存 在 .它仍然表明，（|FX|，{σ FX}）满足自由代数的泛性质。设f：X→A是连续的，I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）5967^ ^您的位置：^OJ映射到C-代数。 然后存在一个集合论同态扩张f：|FX| → |一|.但由{f−1（V）}给出的拓扑|V∈ O（A）}满足条件（A）和（B），因此比（FX）粗，因此f是连续的，如所要求的。从集合论的结果又可以得出唯一性类似地，如果X是一个序列空间，那么只要S是一组序列结构，|FX|（具有满足某些条件的极限点的序列的集合，参见例如，[16，8]）满足（A）和（B），则由S生成的序列结构也满足这些条件，并取拓扑，关于S给出满足（AJ）和（B）的最细拓扑一个自由代数的泛性质是充分的，然后由一个与上述论点类似Q注3.4对于参数化方程理论的自由代数，具有相同证明的类似引理也成立，这将在下一节介绍我们证明了，一旦我们得到了下层集合上的绝对自由代数，我们就可以通过可数归纳极限构造来构造空间上的绝对自由拓扑代数。这种构造对于证明F保持可数基空间是至关重要的，这不能从自由代数拓扑的上述特征中推导出来所以假设X是给定的，我们构造了（|FX|，{σ FX}），并获得了映射η：|X|‹→|FX|.设Ω 0为{η（U）|U∈ O（X）}，对于给定的拓扑Ω n，设Ω n+1是由Ω n<${σ|FX|（V×U）|σ∈ Σ，V∈ O（P σ），U∈ On（FX ar（σ））}，其中On（FXar（σ））是关于Ωn的乘积拓扑。显然，我们得到Ωn+1比Ωn更小，因此我们得到图：（|FX|，Ω0），，（|FX|，Ω1），，（一）|FX|，Ω2），，· · ·所有箭头所在的位置 身份地图。 让（|FX|，Ω ∞）是这个的极限图，即Ω∞ =n∈NΩn。 然后我们得到：定理3.5对所有拓扑空间X，绝对自由上的拓扑Topα-代数（FX，{σ FX}）由Ω ∞给出.证据 我们必须证明Ω∞ 其中O（FX）表示绝对自由代数的拓扑As Ω∞ =n∈NΩn和通过构造所有Ωn满足引理3.3的条件（A）和（B），Ω∞满足这些条件时间复杂度为O（X）。因此我们只需证明O（X）Ω∞。68I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）59FX→→→我们将证明，对于所有项t∈FX，且U∈ O（FX），存在V∈Ω∞使得t∈V<$U。为此，我们在occ（t）上使用transfinite归纳法若occ（t）= 0，则t=x∈X，且当ηX：X→FX连续时，我们得到对V=η−1（U），η（V）∈Ω0且t∈η（V）<$U。所以设occ（t）=α≥ 1，对所有满足occ（TJ）<α的项TJ和包含TJ的开UJ∈ O（X），存在VJ∈Ω∞使得TJ∈Vj<$UJ. 设t=σ（p，（ti）i∈ar（σ））.因为所有运算在FX上是连续的，我们有（p，（ti）i∈ar（σ））∈σ−1（U），并且FX找到一个基本的开放W× i∈ar（σ）Ui<$σ−1（U），包含（p，（ti）i∈ar（σ）），这样Ui=FX，其中i∈ar（σ）\F，对于某个有限的F。对所有i∈F，occ（ti）<α，因此我们可以应用归纳假设，即对所有i∈F，存在Vi∈Ω∞使得ti∈Vi<$Ui。现在 ， 对 于 每 个 i ∈ F ， 存 在 ni∈ N 使 得 Vi∈Ωni ， 并 且 sso ， asFis 有 限 ，m=maxi∈Fni存在s和worV={σ（p，（s i）i∈ar（σ））|p ∈ W，n ∈ F. si ∈ Vi，i ∈ ar（σ）\F. s i∈FX）}，V∈Ωm+1<$ Ω∞和t∈V<$U，根据需要。Q注3.6该定理也适用于更一般的参数化签名，其中对操作的数量没有大小限制，参数空间这是一个令人惊讶的结果，因为它表明，无论操作的规模有多大，|Σ|是，绝对自由代数上的拓扑总是可以在一个可数过程中获得。命题3.7对于序列空间X，绝对自由的Seq-代数由绝对自由的Top-代数的核投射（到Seq）给出。证据为了证明，让TSeq：SeqSeq和TTop：TopTop表示绝对自由代数函子。然后我们必须证明恒等映射TSeqXParticipSeq（TTopX）都是序列连续的。Seq （ TTopX ） 是 一 个 Seq 代 数 ， 因 此 TSeqX 的 泛 性 质 产 生 恒 等 式TSeqX→Seq（TTopX）是连续的。对于相反的情形，通过对occ（t）的归纳并利用定理3.5证明一列项（tk）在TTopX中收敛到t当且仅当tk最终具有与t相同的结构，比如tk=σ（pk，（si，k）i∈ar（σ））和t=σ（p，（si）i∈ar（σ）），并且对于所有i∈ar（σ），（si，k）收敛到si，（pk）收敛到p。但是由于TSeqX中的所有操作都是顺序连续的，因此序列也在这里收敛。 因此，同一性映射Seq（TTopX） TSeqX也是顺序连续的，显示了声明。Q我们现在来我们的主要定理这一节，表明可数为基础的空间是封闭的绝对自由代数结构在Seq。定理3.8如果X是可数基拓扑空间，则绝对I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）5969→自由Top-代数和绝对自由Seq-代数重合，并且又是可数基拓扑空间。证据利用前一个命题的结果，证明了可数基空间X上的绝对自由Top-代数也是可数基的。为此，我们使用定理3.5。我们用归纳法证明了在3.5的构造中使用的所有Ωn都有一个可数基。由于X是基于可数的，因此可以直接看出（|TX|，Ω 0）也是基于可数的。现在假设（|TX|，Ω n）是基于可数的，因此任何可数的乘积（|TX|，Ωn）是可数基的，所以如果Bα是（|TX|，Ω n）α和B是P σ的可数基，则利用Ω的可数性，得到了（|TX|，Ω n+1）通过：B1{σ|TX|（V × U）|σ ∈ B，V ∈ B，U ∈ Bar（σ）}.因此所有的Ωn都有一个可数基，Ω∞ =n∈N Ωn也是如此，根据定理3.5，它是TX上的拓扑。Q这个定理将是证明QCB在Seq中的自由代数构造下对于参数化方程理论是封闭的主要部分。4参数化代数运算与方程理论到目前为止，我们已经介绍了可数参数化代数理论，以捕捉操作，产生计算效应，对一类拓扑空间的对象。我们还证明了，在所有参数空间都是可数基的情况下，绝对自由代数函子F：C→C保持可数基空间，C=Top，Seq。 然而，为了忠实地对效果进行建模，我们必须通过以下方式将操作关联起来：方程式，如Plotkin和Power的工作。为了激发这一点，再次考虑我们的例子。非确定性选择：非确定性是由一个二元操作choose：X2X生成的，其中choose（x，y）表示x和y之间的非确定性选择。对于真正的非决定论，我们将有以下恒等式：• 等式：choose（x，x）=x，• 交换性：choose（x，y）=choose（y，x），• 关联性：choose（choose（x，y），z）=choose（x，choose（y，z））。70I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）59−•−⊥≤⊥∈⊥±±概率选择：概率选择是由操作choose：I×X2→X生成的，因此choose（λ，x，y）表示计算x以概率λ被选择，y以概率1 λ被选择。一个真正的概率选择也将满足以下方程：• choose（1，x，y）=x，• choose（λ，x，x）=x，• choose（λ，x，y）=choose（1−λ，y，x），choose（λ，choose（λJ，x，y），z）=choose（λλJ，x，choose（（1λ（1−λJ）），y，z）.1−λλJ在一个拓扑空间范畴中，I将被赋予下连续的拓扑（等价于关于I上的通常序的Scott拓扑）。非终止性：非终止性由常数（或空运算）X给出。在传统的指称语义学中，有一个不等式x，表示一个非终止程序比一个终止程序提供更少的信息。如果我们考虑拓扑空间范畴中的非终止性，我们希望有x，其中表示X上的专门化预序。这可以实现，使用参数化方程理论，由con-引入一个辅助运算σ：S×X→X，其中S表示Sierpinski空间，二元空间{0，1}，其中单点空间{1}是开的，单点空间{0}不是开的.然后方程：• σ（0，x）= 0，• σ（1，x）=x对于X上的专门化预序，对于所有x∈X，得到<$x ±x，因为通过σ的连续性，我们得到对于任何包含<$x的开U，（0，x）=<$x ∈σ−1（U），因此（1，x）∈σ−1（U），因此x=σ（1，x）∈U。注4.1以类似的方式，我们可以对任意不等式进行建模，其中考虑到特殊化预序项。我们使用这种间接的方法来处理不等式，因为具有参数化方程的理论（如下所述）似乎比直接使用不等式的理论更容易处理全局状态：回想一下，为了建模系统的全局状态，我们使用了操作update：L×V×X→X和lookup：L×XV→X，其中L是C的对象，表示一组内存位置，V是表示一组值的对象。注意，V同时作为参数对象和元出现，因此对于我们的理论，我们必须将其解释为C的对象I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）5971→和一个可数集特别地，如果C=Top，Seq，QCB，那么我们的方法仅当V是可数离散空间时才支持这个结果，在这种情况下，它可以被解释为可数拓扑空间和可数集合。对于方程，我们参考Plotkin和Power所有这些恒等式都符合下面提出的方程理论。现在我们引入C-代数的方程，并定义C-代数A满足这样的方程意味着什么。从而得到了满足方程组E的C-代数的范畴C（E，E）.然后我们给出一个骗局-在此条件下，遗忘函子U：C（E，E）→C创建coequaliz-ers，并利用这一结果，我们构造了自由代数FX在X显式作为绝对自由C∈-代数FX的余均衡器。将这些结果应用于C=Seq将最终使我们能够证明自由代数函子F：Seq→Seq（E，E）保持qcb-空间，因此限制为自由代数函子F：QCB QCB（E，E）。 做到这一点之后，我们将能够模拟计算效应，例如上面例子中给出的效应在代数范畴QCB（E，E）中，对于相应的参数化方程理论（E，E），给出了一个新的证明.定义4.2设k是C元数α和参数对象Z的代数运算是C-态射p（−）：Z×（−）α→（−）的Ob（C）-指标族，使得对于所有C-同态f：（A，{σA}）→（B，{σB}），下图交换：Z×AαpAAZ×fαfJαJZ×BpBB有时我们称这样的代数运算为（α，Z）-运算. 代数运算的概念取自Plotkin和Power的[ 12 ]，尽管他们的代数运算的概念在某种意义上更一般，它可以在合适的代数运算的例子是所有的项映射（可以通过合成运算和投影映射来归纳定义在关于无穷非参数化签名的文献中，这种项映射也被称为多项式或导出运算。研究参数化签名的代数运算是否也可以归纳定义，这将是一件有趣的事情。72I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）59^×AAJτ→{}E定义4.3元ar（e）和参数对象Pe的方程e：（p=pJ）由一对（ar（e），Pe ） - 代 数 运 算 p ， pJ 给 出 。 一 个 Σ- 代 数 （ A ， {σA} ） 满 足 方 程 e ：（p=pJ），如果pA=pJA：Pe×Aar（e）→A。如果E是一个可数方程组，并且ar（e）≤ω，对于所有e∈ E，元组（ε，E）是叫做可数参数化方程理论。一个C（ε，E）-代数是一个满足所有方程e∈E的Cε-代数（A，{σ A}），我们用C（ε，E）表示C（ε，E）-代数和Cε-同态的范畴。对一个C-对象X，X上的自由C（E，E）-代数是C（E，E）的一个对象（FX，{σFX}），对它存在一个C -态射η X：X → FX，使得对任何C（E，E）-代数（A，{σA}）和C-态射f：X→A，存在唯一的C-同态f：（FX，{σFX}）→（A，{σA}），它使得下面的图（在C中）可交换：外汇fb，，_ηXFX对于其余的文件（E，E）将始终表示可数方程理论。注意，如果C有可数的余积，则一个C-代数（A，{σA}）是一个C（，E）-代数当且仅当映射e∈EPear（e）τA一一致，其中τA，τAJ的E。是各自的代数运算对于下面的定理，假设C有可数乘积和余乘积，且遗忘函子U：C（E，E）C有一个左伴随，即自由代数函子F存在.定理4.4如果C中可数积保持余均衡图，则健忘函子U产生余均衡器。证据设f，g：（A，{σ A}）→（B，{σ B}）是C-同态.应用遗忘函子给出C-态射f，g：A→B.我们认为，如果q：B→Q是f和g在C中的余均衡器，则Q可以具有C的代数结构，使得（Q，σQ）满足，q成为C-同态，FQ（A，{σA}）g（B，{σB}）（Q，{σQ}）I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）5973→τA--D^ ^您的位置：^，P^FX一一一0是C（E，E）中的一个均衡器图。这些权利要求的证明类似于[6]中VI.8定理1的证明，其中作为绝对余均衡器的性质被可数乘积保持所取代Q如果T=UF，则T成为单子的函子，我们可以考虑CTC.的Eilenberg-Moore代数范畴贝克推论4.5如果在C中可数乘积保持余均衡图，则C，E = CT.定理4.6设F：CC表示绝对自由代数函子，可数积在C中保持余均衡图，则：(i) 对于任意的C-代数（A，{σA}），F（e∈EPe ×Aar（e） cAτcAJ是一个C（ε，E）-代数a，其中eτ^A，τ^AJ 在此基础上，证明了在端点上唯一的C-同态，ingτA，τAJ ：e∈EPe × Aar（e）→A.(ii) 对于C的每个对象X，自由C（FX，E）-代数（FX，σFX）被获得为：以下各项的共均衡器ar（e）τFXτdFJX证据(i) 由定理4.4可知，τ A，τ j A的余均衡器q：（A，{σ A}）→（Q，{σ Q}）存在于C中，并且它的计算方法与C相同。因此，它仍然需要证明（Q，{σQ}）满足E中的所有方程。对于这一点，设e0：（p=pJ）由此可知，nasqτ^A=qτ^JA，其中qτA=qτAJ 安登塞q<$pA=q<$pJA。现在考虑下面的C中的交换图：ar（e0）pAPe0×APe0×qar（e0）JpJApQ一QJPe0Qar（e0）QpJQPe0 ×qar（e0） ：PeAar（e0） →Pe×Qar（e0）是Pe×的合格rτar（e0）ar（e0）×τ J。 但我们也有这样的问题，=qpJ余均衡×F（e∈EPe×FX）e0级一0074I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）59ar（e0）^^ ^您的位置：DBτA^ˆˆE→--e∈EPe×FXFXτdFJXB（Pe0×τ^A），（Pe0ar（e0）×τJA），因此存在唯一的中介箭头ar（e0）JQPe0×Q→Q构成平面图，给出pQ=p，且soQ满意度为0。(ii) 余均衡器（Q，{σ Q}）τ FX，τJF X满足普适性。 为此，设（A，{σ A}）是任意C（λ，E）-代数，f：X → A是任何C-态射，并且f^：（FX，σFX）→（A，{σA}）对应ar（e）τFXF（far（e）f∈E）fJ JF（e∈EPe ×Aar（e）cAτcAJ确保tf等于τFX和τFJX，同时满足所需的中介条件h：（Q，{σQ}）→（A，{σA}）。Q现在假设C=Seq，N是一个可数参数化签名，使得所有参数空间都是基于可数的，并且是一组可数方程。然后可以应用伴随函子定理，U：Seq（E，E）→Seq有一个左伴随F。此外，我们有以下结果。命题4.7在Seq中，可数乘积保持余均衡图。我的律师。Schrüder和Simps在[17]中证明了拓扑商映射的Seqcoun表积是拓扑商映射.由于拓扑商映射恰好是Seq中的余均衡器，因此可以直接证明可数乘积确实保持余均衡器图。Q现在我们可以陈述我们的主要结果。定理4.8自由代数函子F：Seq Seq（E）保持qcb-空间.证据设X是qcb-空间，（FX，σ FX）是X上的自由Seq（E，E）-代数.我们必须证明FX是一个qcb空间。为此，注意自由代数函子F是左伴随的，因此保留了余均衡器，根据定理4.4，余均衡器在代数范畴中是拓扑商映射。设q：A→X是可数基空间A的拓扑商映射。现在C-同态那么下面的图的交换性F（）I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）5975FX→E--→X关于我们我们有以下图表：FA FAFJ J其中，根据前面的定理，上映射和下映射是Seq中的正则epis，因此是拓扑商映射。由于拓扑商映射在复合下是闭的，因此我们得到FX作为FA的拓扑商，FA是3.8的可数基空间。Q5映射代数到TP我们已经看到，QCB在Seq中可数参数化方程理论的自由代数的构造下是封闭的，因此我们得到了遗忘函子QCB（E，E）→QCB的左伴随，即限制自由代数函子F：SeqSeq（Eq，E）至QCB。 然而，自由代数函子一般不保持拓扑前域，如果我们考虑非确定性选择的方程理论，就可以看出设（X，）是非确定性选择的方程理论，考虑空间X上的自由代数，由配备Alexandro拓扑（或Scott拓扑）的三元链01 2<<那么自由代数（FX，{σFX}）具有幂集PX作为基础集，并且操作是联盟 但在专业化预订中， 1、 3 = 1， 2， 3，就像绝对自由代数选择（1，选择（1， 3））±选择（1，选择（2， 3））±选择（1，选择（3，3））左项和右项将用{1， 3}标识，中间的项用1， 2， 3标识。因此，FX不是T0-空间，也不是拓扑空间。逻辑前域（类似的论点可以在[11]中关于权力域的章节中找到。为了修正这个定义，我们考虑了反射子范畴中的代数，并证明了反射函子M：QCB TP限制于相应代数范畴上的反射函子。设D是C的一个满反射子范畴，其反射函子R：C→D，两者都是可数完备和上完备的，且（E，E）是C的一个可数参数化方程理论，使得所有参数对象都在D中.然后，我们得到下面的定理，将证明两个引理。76I. Battenfeld/Electronic Notes in Theoretical Computer Science 158（2006）59σ→pJRA{}→{}定理5.1如果反射函子R：C→D保持可数乘积，则它限制于一个函子R（E，E）：C（E，E）→ D（E，E）.对于这两个引理，假设定理的假设是充分的。引理5.2对任意C（λ，E）-代数（A，{σ A}），RA都可以具有C（λ，E）-代数结构，从而成为D（λ，E）-代数，且标准映射ηA：A→RA是Cλ-同态。证据当R保持可数乘积时，对每个σ∈φ，RσA：R（Pσ×Aar（σ））R=Pσ×RAar（σ）→RA定义得很好。所以设σRA=RσA，使得（RA，{σRA}）成为一个C-代数，因此是一个D-代数。为了证明ηA是一个C-同态，观察下图对每个σ∈都是可交