观测诱导的E-检验单子：上、下幂空间构造的拓扑理论计算科学研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记276（2011）105-119www.elsevier.com/locate/entcs观测诱导的E-检验单子：上、下幂空间构造Ingo Battenfeld1FakultaütfurInformatikTU Dortmund多特蒙德，德国MatthiasSchr¨oder2德国慕尼黑联邦国防军信息大学摘要Alex Simpson建议使用一种观察诱导的方法来模拟指称语义中的计算效果。其主要思想是使用单个观察代数来定义计算类型结构。他主张，除了给予代数结构，这种方法还允许具体的一元类型的特征。本文证明了对于任意预选的观测诱导代数，自由观测诱导代数存在于拓扑空间之间的连续映射范畴中。此外，我们使用这种方法给出了一般拓扑空间上的一个下幂域和一个上幂域的构造，这两个构造都推广了连续dcpos上的经典特征。我们的下幂域构造是针对所有由具有下Vietoris拓扑的非空闭子集空间给出的拓扑空间。对偶地，我们的上幂域构造是针对一类广泛的拓扑空间，这类拓扑空间由其拓扑的真开滤子空间与上Vietoris拓扑给出。 我们还给出了一个反例，表明这一特征并不适用于所有的拓扑空间。关键词：指称语义，计算效应，幂域，论域理论，拓扑1介绍对计算效应进行建模已成为定义语义学的一个重要方面。Moggi [9]以计算单子的形式提出了流行的元理论，并在函数式编程语言Haskell中找到了实际应用。Moggi1电邮地址：battenfeld@ls10.cs.tu-dortmund.de2电子邮件：matthias. unibw.de1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.09.017106I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105和组合效应。最近，辛普森[13]提出了一种替代他们的方法。他没有根据方程代数理论定义效应单子，而是采用了一个预先选择的观测代数，这是手头效应的原型，并根据纯粹依赖于这个代数的性质构造了一个单子。这种方法的好处是，结果类型从预先选择的代数继承了许多理想的属性。他称这种方法为观察诱导的自由代数构造。 Simpson建议拓扑空间之间的连续映射范畴作为观测诱导方法的拟合环境范畴，遵循Smyth的工作[15]。Simpson和Schr？oder已经用这种方法定义了拓扑空间的概率power-domain构造[12，14]。他们证明了对所有的拓扑空间，他们的构造产生了具有弱拓扑的连续概率赋值空间。因此，观测方法允许将经典的概率幂域构造[8]推广到dcpos之外。在演讲的最后[13]，辛普森开始研究他的方法是否也可以应用于非决定论的经典幂域。关于不确定性，有三种经典的幂域构造：下（Hoare）幂域、上（Smyth）幂域和凸（Plotkin）幂域.在连续dcpos上，每一个都有两个截然不同的特征。一个特征是通过一个自由代数结构的代数理论给出的二元运算代表nondeterministic选择。第二个特征是由更具体的手段，在时尚的集合论幂集建设。这两种特征都有其优点：自由代数结构完全适合Plotkin和Power的计算结果代数框架，具体特征允许更好地推理语义结构。这些特征一致的事实可以追溯到连续dcpos的令人愉快的特性。在连续dcpos的世界之外，已知代数结构和各自的具体特征是不同的。本文遵循Simpson我们还表明，相应的自由代数继承理想的性质，从观察代数。随后，我们在拓扑空间上构造了一个观测诱导的上、下幂空间，它推广了连续dcpos之外的经典构造。对于所有拓扑空间X，下幂空间映射将产生具有下Vietoris拓扑的X的非空闭子集的空间。上幂空间构造将给出一个广泛的拓扑空间X，即满足Wilker条件的空间，O（X）的具有上Vietoris拓扑的真开滤子空间。此外，我们提供了一个不满足Wilker条件的空间的例子，并且在这里上幂空间的特征化失败了。我们注意到SimpsonI. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105107在函数的水平上。然而，也有一些分歧，在赫克曼2观察诱导代数我们首先给出一个观测诱导的自由代数结构的一般定义[12]。我们的定义建立在拓扑空间之间连续映射的Top范畴中。然而，原则上，抽象的机器可以被转移到任意的范畴。设f是一个有限代数签名，即一组有限的运算符号{σ∈<$}每一个都有一个arity |σ| ∈ N。则一个（拓扑）的n-代数是一个元组（A，<$A），使得A是一个拓扑空间，<$A：={σ A}σ∈<$且每个σ A：A|σ|→A是连续映射。n-代数（A，A）与（B，B）之间的同态是连续映射h：A→B，其中h<$σ A<$σB<$h|σ|持有对于所有的σ∈Σ。拓扑代数和它们之间的同态构成一个范畴<$A-Alg，并且众所周知，遗忘函子<$A-Alg→Top有一个左伴随，自由<$A-Alg函子。让我们固定一个-代数（O，O）作为观察代数。这个观察代数推导出以下定义。定义2.1设X是一个拓扑空间。X上的一个抽象（O，<$O）-结构是一个带连续映射η：X →A的n-代数（A，<$A），使得每个连续映射f：X→O沿η有唯一的同态扩张f：（A，<$A）→（O，<$O），即 f是唯一的同态，使得下面的图可交换：FA，OηFX对于一个抽象的（O，<$O）-结构，我们记为η：X→（A，<$A注意，对于每一个空间X，自由代数结构<$X：X→（FX，FX）产生一个抽象的（O，O）-结构。此外，自由代数的方程理论，其中相应的方程满足（O，<$O），产生抽象的（O，<$O）-结构。所以一般来说，X上的一个抽象（O，O）-结构不是唯一的。观察方法的本质是观察代数的理想性质转移到计算类型。抽象的（O，O）-结构确实满足初始性要求，但它们肯定不共享观察代数的所有期望性质。一个强加了以下的最终要求来获得它们。定义2.2一个n-代数（B，nB）称为完备（O，nO）-代数，如果对每个抽象（O，nO）-结构η：X→（A，nA），每个连续映射f：X→B108I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105唯一地扩展到同态f：（A，<$A）→（B，<$B），如：FA、BηFX特别地，（O，<$O）本身是一个完备的（O，<$O）-代数。下面的结果表明完备代数确实共享（O，<$O）的许多性质引理2.3设E是一组n-方程，使得（n，E）是泛代数意义下的方程代数理论。 如果（O，<$O）满足E中的所有方程，那么每个完备的（O，<$O）-代数（A，<$A）也满足。证明（略）设V是可数离散的“变量”空间则拓扑代数（A，A）满足E的所有方程，如果每个连续映射V→A沿着自由代数包含IV：V→FEV有唯一的同态扩张（FEV，FEV）→（A，A）.由于iV形成了一个抽象的（O，O，O）-结构，完整性属性正好保证了这个要求。Q例如，如果（O，<$O）是一个拓扑群，即具有一个连续的二元运算和一个满足通常公理的单位元，并且<$O是由一个二元运算和一个常数组成的相应签名，则每个完备（O，<$O）-代数都是一个拓扑群。若加法（O，<$O）是交换群，则每个完备（O，<$O）-代数的连续二元运算是交换的。引理2.4设C是Top的一个满反射子范畴，对它，反射函子R：Top → C保持有限积。如果O是C的一个对象，那么每个完备（O，<$O）-代数（A，<$A）的底层空间A也是C的一个对象。证明（略）设（A，<$A）是完备（O，<$O）-代数，F表示自由<$-代数函子.文[2]证明了一个保积反射函子提升到代数的范畴上，并且F<$R <$=R<$F。这类例子可以用来证明，对于任意拓扑空间X，自由代数的单位和反射函子产生一个抽象的（O，<$O）-结构X→（FRX，<$FRX）。 因此，人们可以得到地图之间的一一对应关系，X→A和RX→A沿着反射的单位。 用A实例化X会产生所需的结果。Q因此，如果（O，<$O）的底空间是T0-空间，单调收敛空间或sober，则每个完备（O，<$O）-代数的底空间也是T 0-这些结果促使我们将观测诱导代数定义如下。定义2.5对于拓扑空间X，X上的自由（O，<$O）-代数由抽象（O，<$O）-结构η给出：X→（A，<$A）使得（A，<$A）是完备的 （O，O）-代数I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105109→^ ^您的位置：是的。通过定理2.6，我们发现（F^X，<$F^X）构成一个完备的（O，<$O）-代数很容易看出，自由（O，<$O）-代数（直到同构）由这个定义唯一确定，并且它们对任意空间存在当且仅当来自完全（O，<$O）-代数和同态范畴的遗忘函子Comp（O，<$O）→Top有左伴随。注意，sobrification是这样一个观察诱导自由代数构造的实例，即对于由Sierpinski空间S给出的没有代数结构的观察代数[16]。另一个例子是Simpson和Schröder[12，14]的观测诱导概率波域构造。他们证明了，如果用（I，I）作为观测代数，其中I是通常序的Scott-拓扑下的单位区间，I：I2→I是平均映射，则任意拓扑空间X上的自由（I，I）-代数是X上的概率赋值空间，它具有弱拓扑。我们接着证明了Top中自由（O，O）-代数的普遍存在性。下面的结果本质上是由这样一个事实得出的，那就是，n-代数的范畴是完备的。引理2.6完备（O，<$O）-代数和同态的范畴Comp（O，<$O）具有所有极限.给定一个任意拓扑空间X，我们定义H（X，O）为连续映射X O的集合。前面的引理给出了O的H（X，O）-重积O H（X，O）上的点态运算的一个代数结构，使得（OH（X，O），<$OH（X，O））成为完备的（O，<$O）-代数.下面的结果是微不足道的。引理2.7对于每个拓扑空间X，映射<$X：X→OH（X，O），由下式给出：x<$→（f（x））f ∈H（X，O）连续。推论2.8设η X：X→（FX，<$FX）表示X上的自由X-代数，则<$X：X→OH（X，O）扩张为唯一同态<$X：（FX，<$FX）→（OH（X，O），<$OH（X，O））.设一个给定的完备（O，<$O）-代数的完备（O，<$O）-子代数是一个自身满足定义2.2的完备性的子代数。我们现在把X上的自由（O，<$O）-代数作为（OH（X，O），<$OH（X，O））的包含<$X的象的最小完备（O，<$O）-子代数.命题2.9（OH（X，O），OH（X，O））的子代数定义为：F^X：={A→OH（X，O）}|<$X（FX）<$A，A是完全（O，<$O）-子代数a}与限制映射<$X：X→（FX，<$FX）形成自由（O，<$O）- 代数X.对于从（OH（X，O），<$OH（X，O））继承的操作，则<$X：X→F^X是定义良好，由推论2.8，并且对于每个连续f：X→ 噢命运投影πf：（OH（X，O），<$OH（X，O））→（O，<$O）是f的同态扩张110I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105^^^^行动J沿X → X：X→（O H（X，O），OH（X，O）），但不一定唯一。因此，投影π f的限制|FX：（F X，<$F X）→（O，<$O）也是f沿<$X的同态扩张，唯一性有待证明。因此，l∈g是f沿X的同态扩张：X→F^X。那么π f的均衡器|F^X和g定义一个完备（O，<$O）-子代数（E，<$E）的，因此也有f（OH （X，O），ωOH（X，O）），并且we可以进一步限制FXX到连续映射X→ E，可以扩展为同态（FX，FX）→（E，E）沿η X：X→FX。 但是，然后E形成（OH（X，O），<$OH（X，O））的子代数，包含图像<$X（FX），因此它必须等于F X，根据它的定义，我们得出g<$π f|FXQ因此，我们确定了以下内容。定理2.10对每个观察代数（O，<$O）和每个拓扑空间X，X上的自由（O，<$O）-代数存在，并且是（OH（X，O），<$OH（X，O））的完备（O，<$O）-子代数。我们猜想，上面的推理路线，与自由代数作为一个子集的幂O的特征，可以适用于证明更强的结果，即Comp（O，O）是一个完整的反射子范畴的-Alg。2.1变化让我们给出抽象（O，<$O）-结构和完备（O，<$O）-代数定义的一些变化。第一个变化转移设置完全进入世界的代数以下的想法辛普森。为了便于阅读，我们隐式地保留代数结构。回想一下，对于每个态射f：X→O，存在唯一的同态f：FX→O，其中FX是X上的自由π-代数。 考虑函子Hom（−，A）：A-Alg→Set，称同态h：B→B为A-iso，如果Hom（h，A）是同构。然后，我们得到以下的重新定义，它们等价于上面给出的定义定义2.11一个抽象O-结构由O-isoh：FX→A给出，其定义域是一个自由X-代数。一个完备O-代数是一个定义域为自由代数的O-isoh是一个B-iso的n-代数B另一种可能性是放弃定义域要求，将抽象O-结构定义为O-isos，将完备O-代数定义为O-isos是B-isos的代数B注意，在这个定义（主要是更一般的定义）中，完备O-代数范畴仍然具有所有极限，因此我们上面的构造在这个变体中仍然有效，所以它在拓扑环境中没有区别第二个变化是将参数化注入我们的定义中。 如果Z是拓扑空间和（A，A），（B，B）是拓扑代数，连续映射h：Z×A→B称为右同态，如果对任意z∈Z，映射hz：（A，A）→（B，B）定义为a <$→h（z，a）是同态.I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105111定义2.12 X上的参数化抽象（O，<$O）-结构是一个带连续映射η：X → A的n-代数（A，<$A），使得对每个拓扑空间Z，每个连续映射f：Z×X→O有唯一的沿id Z × η的右同态扩张f：Z×A→O。一个n-代数（B，n B）称为完备（O，n O）-代数，如果对每个参数化抽象（O，n O）-结构η：X→A，每个连续映射f：Z×X→B唯一扩张到一个右同态f：Z×A→ B.这个定义似乎需要完备（O，O）-代数上更强的性质。在许多具体的情况下，如Simpson和Schrüoder然而，我们对拓扑空间的一般存在性证明不能容易地转移到参数化设置。3低功率空间结构在经典Domain理论中，下幂Domain由包含序的非空Scott闭集对于连续的dcpoX，这证明等价于方程理论的自由代数，由二元运算·给出，表示交换性、结合性、恒等式和不等式a≤a·b的方程[1，6.2节]。这种构造的原型空间是（S，S），以连接为操作的谢尔宾斯基空间，它将作为我们的低幂空间构造的定义3.1对于一个拓扑空间X，X上的观测诱导下幂空间由X上的自由（S，S）-代数给出。我们的目的是证明X上的观测诱导下幂空间是由X在下Vietoris拓扑下的非空闭子集的集合给出的，其中集并运算是相应的运算。定义3.2设X是一个拓扑空间。 对于子集A<$X，我们将A在X中的闭包写成cl（A）。X的非空闭子集在包含序下形成格。通过C（X），我们表示X的非空闭子集的集合，其配备有由以下形式的集合生成的下Vietoris拓扑{B∈ C（X）} |BU/=}，为UX打开。在我们继续研究代数（C（X），n）的性质之前，我们给出一些关于抽象（S，n）结构的一般结果.首先，观察同态扩张在以下意义上是单调的引理3.3设η：X →（A，λ）是一个抽象（S，λ）-结构。 则对连续f，FJ：X →S，f ≤ FJ蕴涵f ≤ FJ（按逐点顺序）。112I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105接下来，我们定义一个给定的抽象（S，S）-结构上的辅助序，并证明这个序使我们能够从理论上定义同态扩张序。定义3.4设η：X→（A，λ）是一个抽象（S，λ）-结构。定义A上的关系≤η为a≤ηAJ当且仅当对所有f：X → S，对于相应的同态扩张，f（a）≤f（AJ）成立。很容易看出，≤η总是代数（A，n）上的一个预序。我们可以把它解释为同态给出的特殊化预序。下面结果的直接证明留给有兴趣的读者去做.引理3.5设η：Y→（A，λ）是一个抽象（S，λ）-结构.则对于≤η，以下成立：(i) 对于每个a0∈A，集合{a∈A|a≤ηa0}在相应的拓扑中是闭的，(ii) 对于每个a0∈A，集合{a∈A|a≤ηa0}和{a∈A|a0≤ηa}在θ下是闭的，(iii) 对所有的a，aJ∈A，有a，aJ ≤ηa <$aJ，(iv) 对于x∈X，有η（x）≤ηa∈aJ当且仅当η（x）≤ηa或η（x）≤ηaJ，(v) 对给定的连续f：Y→S及其唯一同态扩张f：A → S，则f（a）<$η（x）≤ηaf（x）成立.现在，我们再次将注意力转向代数（C（X），λ），并证明它是一种抽象的（S，S）结构。为此，我们必须做以下相当简单的观察。引理3.6 C （ X ） 上 的特化序是包含序，并且C（X）的每个开集都是关于它的Scott-开的。命题3.7对任何拓扑空间X，具有包含映射{·}：X →（C（X），X），将x ∈ X映射到它的点闭包的代数（C（X），X）是一个抽象（S，X）-结构。证据 首先通过定义下Vietoris拓扑观察包含映射是连续的。所以假设f：X→S是给定的。我们必须证明它唯一地扩张到一个连续同态f：C（X）→S。受Lemma3.5（v）的启发，我们定义f（B）：=x∈Bf（x）. 显然，F沿着{·}扩展f，并且可以直接证明f（B<$BJ）=f（B）<$f（BJ），因此它是同态。因此，如果f=1（是连续的。）=10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105113），因此，对于唯一性，我们认为，根据引理3.6，C（X）的每个开子集都是Scott-开的，因此任何连续映射C（X）→S都必须是Scott-连续的。但后来f（B）={f（cl（F））|FB finite}={f（x）|x∈ F<$B}= f（x）x∈B114I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105”这是一个独特的定义，并遵循索赔Q最后证明了（C（X），n）是完备的（S，n）-代数.命题3.8对任何拓扑空间X，代数（C（X），n）是完备的（S，S）-代数证据 设η：Y→（A，λ）是一个抽象（S，λ）-结构，g：Y→ C（X）是连续的地图我们必须证明g唯一地延伸到同态g：A→ C（X），我们定义为a<$→ cl（{g（y）|η（y）≤ηa}）。我们必须证明：（i）g沿着η扩张g，（ii）它是连续的，（iii）它是一个同态，（iv）它本身是唯一的：(i) 这由引理3.6和≤η反映了Y在包含映射η下的特殊化预序。(ii)我们必须证明，对于一个开集U<$X，集合g−1（<$U<$）在中是开的，A.映射χ<$U<$<$g：Y→S有连续同态扩张h：A→ S，并且根据引理3.5（v），h（a）={x <$U<$g（y）|η（y）≤ηa}。因此h（a）= 当且仅当存在某个y∈Y且η（y）≤ηa且g（y）∈ <$U<$。但这意味着h（a）=当且仅当{g（y）|η（y）≤ηa}<$U，[4，推论1.1.2]，等价于g（a）∈ <$U<$。 因此，g−1（U）=h−1（），显示索赔。(iii) [4，定理1.1.3]证明了对于拓扑空间的子集A，B<$X，有cl（A<$B）= cl（A）<$cl（B）。因此，引理3.5（iv）得到：2）A = A（ {g（y）|η（y）≤ηaaJ}）= c1（ {g（y）|η（y）≤ηa}<${g（y）|η（y）≤ηaJ}）= g（a）<$g（AJ）.(iv) 假设一个矛盾，g和g都是g的扩张，但存在一些a∈A，其中g（a）=/g<$（a）。然后，我们发现一些open子集U正好相交g（a），g（a）之一，因此是χ<$U<$$>g（a） χ <$U<$$>g <$（a）。但χ<$U<$：（C（X），<$）→（S，<$）是连续同态，因此χg，χg都是连续的同态扩展了χ<$U<$<$g，与抽象（S，S）-结构的唯一扩展Q这产生了以下特征的观察诱导的较低的功率域。定理3.9对任意拓扑空间X，X上的观测诱导下幂整环由（C（X），n）给出.特别是，这概括了从经典域理论的建设。在那里，连续dcpo上的上幂域由Scott拓扑下的非空（Scott-）闭子集空间给出，其中包含阶已知与下Vietoris拓扑一致I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105115注3.10我们可以证明，代数（C（X），n）也满足定义2.12中给出的参数化变分中X上观测诱导的下幂域的条件。4上部动力空间结构在经典Domain理论中，上幂Domain的构造是由非空紧饱和集的集合在包含序的逆下给出的。在连续dcpo上，这等价于不等式理论的自由代数构造，类似于低幂域的自由代数构造，但不等式被a·b≤a所取代[1，6.2节]。这种构造的原型空间是空间（S，S），它充当观察代数。定义4.1对于一个拓扑空间X，X上的观测诱导上幂空间由X上的自由（S，S）-代数给出。与上一节的发展相对应，我们得到以下结果。引理4.2设η：X →（A，λ）是一个抽象（S，λ）-结构。 则对连续f，FJ：X →S，f ≤ FJ蕴涵f ≤ FJ（按逐点顺序）。定义4.3设η：X→（A，λ）是一个抽象（S，λ）-结构。定义A上的关系≤η为a≤ηAJ当且仅当对所有f：X → S，对于相应的唯一同态扩张f（a）≤f（AJ）成立。引理4.4设η：Y→（A，λ）是一个抽象（S，λ）-结构.则对于≤η，以下成立：(i) 对于每个a0∈A，集合{a∈A|a≤ηa0}在相应的拓扑中是闭的，(ii) 对于每个a0∈A，集合{a∈A|a≤ηa0}和{a∈A|a0≤ηa}在θ下是闭的，(iii) 对所有的a，aJ∈A，有a ∈aJ ≤ηa，aJ，(iv) 对于x∈X，有a_J≤ηη（x）当且仅当a≤ηη（x）或a_J≤ηη（x），注4.5注意我们没有引理3.5（v）的类似物。 原因是，尽管连续性和（S，S）-同态在上面是和谐的，但这里的情况并非如此。下面的引理的证明很简单。引理4.6假设{fi}i∈I是连续同态的有向族（A，）→（S，），则它的点态方向也是supremum↑i同态fi是连续的回想一下，霍夫曼-米斯洛夫定理[6]说，对于一个清醒的空间X，X的非空紧饱和子集的偏序集与拓扑O（X）的（真）斯科特开滤子之间存在同构当我们处理一般拓扑空间时，后者是更可取的因此，与116I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105记住定理2.10，我们的目标应该是证明X上的观测诱导上幂空间是由O（X）的Scott开滤波器空间给出的，其中交集λ作为相应的运算。与下幂空间构造对应的，相关拓扑是这里的上Vietoris拓扑定义4.7设X是一个拓扑空间。一个O（X）的（真）开滤子是一个真子集F;O（X），它在Scott-拓扑中关于包含阶是开的，在交阶下是闭的。通过F（X），我们表示O（X）的真开滤波器的集合，其配备有由以下形式的集合生成的上Vietoris拓扑：为UX打开。[U]：={F∈ F（X）|U∈F}，对每个空间X，存在连续嵌入X→ F（X），映射一个指向其邻域过滤器的点。然而，事实证明邻域过滤映射X→（F（X），F（X））一般不满足抽象（S，F）-结构的唯一性要求，我们在下面给出一个反例。然而，对于一个足够大的空间类，我们可以证明邻域滤波器映射确实满足唯一性条件。这个类包含所有满足Wilker条件的空间[17]，其定义我们还记得。定义4.8拓扑空间X是Wilker空间，如果所有开滤波器F∈ F（X）满足Wilker条件，该条件如下所示。设对于开子集U1，U2<$X，U1<$U2∈F，则存在开滤波器F1，F2∈ F（X）使得U1∈F1，U2∈F2且F1<$F2<$F.Wilker空间类确实很大。它包含所有Hausdor空间和所有局部紧拓扑空间。反例似乎有一个相当人为的解释，如下面4.1尽管如此，据我们所知，我们还不知道威尔克条件是否被指称语义学的标准结构所保留。引理4.9设X是Wilker空间，则邻域滤波映射η：X→（F（X），X）构成一个抽象的（S，X）-结构。证据 假设f：X → S是连续的。设扩张f：F（X）→S为[f-1（）]的特征映射，即 f（F）=当且仅当f −1（）∈ F。明确这个映射是定义良好的，沿着η延伸f，并且它是连续的。很容易证明它是一个同态，所以我们必须证明它本身是唯一的假设f也沿η延拓f。根据上越南人的定义证明了对于一个子集集，f∈Ch，f∈1（） =j∈J[Vj]j∈JVj=f−1（），因此j∈J[Vj]<$[f−1（）]。当verj∈JVj∈F存在一个有限的GJ，j∈GVj∈F，sInceFScott-open. 因为X满足Wilker条件，这产生o个限定符Fj，对于orj∈G，其中ithVj∈Fj和j∈GF j<$F. 因此，对于所有j ∈ G，我们有f <$（F j）=，并且由于f<$是a，这是一个函数，它的值为f（，且f（F）=立即跟进Qj∈GFj）=它仍然需要证明（F（X），f）满足完备性。I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105117−f（[V]）i一个abstract（S，n）-结构的性质，我们得到↑χf−1（[Vi]）<$χf−1（[Vi]），命题4.10对每个拓扑空间X，（F（X），F（X））是完备（S，F（X））-代数。证据 假设η：Y→（A，λ）是一个抽象（S，λ）-结构，f：Y→ F（X）连续映射。 我们定义f：A→ F（X）为：O（X）=O（X）|χf−1（[U]）（a）= }，其中χ f −1（[U]）是特征映射χ f−1（[U]）：Y→ S的唯一同态扩张。我们必须证明：（i）f是良好定义的;（ii）它是f沿η的连续同态扩张;（iii）它本身是唯一的。(i) 重要的部分是证明f（a）总是Scott-开的。 所以假设i∈IV i∈f（a）且{Vi}i∈I是有向的。由引理4.2，{χf−1（[Vi]）}i∈I形成连续同态的有向族，因此，由引理4.6，我们有也是连续同态。 由通用且thusfrom↑χf−1（[Vi]）（a）=我们得出结论，存在某个i0∈I其中χf−1（[Vi0]）（a）=，根据需要。(ii) 直截了当。(iii) 假设f也沿η扩展f。则对每个U∈ O（X），我们计算出f −1（[U]）和f−1（[U]）的特征映射是连续的同态（A，S）→（S，S）.由于它们都是f（f<$$> η）−1（[U]）<$（f<$η）−1（[U]）的特征模沿η的延拓，所以它们必须由抽象（S，S）-结构的泛性质等价。Q定理4.11如果X是Wilker空间，则映射η：X→（F（X），F），将一个点映射到它的邻域滤波器，形成X上的观测诱导上幂空间。对于sober空间，可以等价地使用非空紧饱和集的空间，其中包含映射一个点到其特殊化顺序中的向上闭包。由于所有的局部紧空间，特别是连续dcpos，都是Wilker空间，因此观察诱导方法真正地扩展了经典的上幂域构造。注4.12这里还可以证明，上述结果对定义2.12中给出的参数化变分也成立。4.1反例本文给出了一个拓扑空间X<$，其中η：X<$→（F（X<$），<$）不满足抽象（S，<$）-结构的唯一扩张性质.所考虑的空间将被表示为序列空间[5，11]。我们从定义如下的空间X构造X基本集合由N给出。设N·，·，·，···：N4→ N是一个双射，并定义了一个收敛118I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105.›→序贯L空间Fi是闭子集，Xi的不可约性产生X的关系如下。一个序列{xn}n∈N={an，bn，cn，dn<$}n∈N收敛于x=a，b，c，d如果满足以下所有条件(1) 对几乎所有的n∈N，成立：xn=x或cn=x或dn=x，(2) 如果I：={n∈ N |Cn = x且xn/= x}是无穷的，则相应的子序列{an}n∈I趋于∞，(3) 如果J：={n∈ N |d n= x，x n x和c n/= x}是无限的，则相应的子序列{bn}n∈J趋于∞，集合{an}n∈J是有限的。这个收敛关系满足L-空间的公理，见[4，练习1.7.18]。对于集合N上的这种收敛关系，我们赋予X序列开集的拓扑通过[4，练习1.7.19]，收敛关系由这个拓扑导出。引理4.13任何两个非空开子集U，V ∈ X有一个非空交。证据假设x∈U，y∈V。我们认为存在某个a0∈ N使得对所有的b∈ N，成立<$a0，b，x，y <$∈U. 如果不是这种情况，那么对于所有n∈N，我们可以找到bn∈N，使得n∈N，x，y∈/U。但相应的数列{n ∈n，bn，x，y∈ n}n∈N收敛于x，这就产生了一个矛盾.另一方面，序列{a0，n，x，y<$}n∈N收敛于y，因此必然存在某个b0∈N，且a0，b0，x，y<$∈V，从而证明了这一点。Q现在清楚的是，整个空间X形成自身的不可约闭子集，即它不能分解成两个闭真子集。特别是空间不清醒。设X是X的Alexandro单点分解。我们很容易证明X是一个序列L空间，也满足引理4.13，并且{X}是一个开滤波器。现在考虑常数映射：X→S。 这是一个明显的同性恋-物理延拓跟随映射：（F（X），）→（S，）沿η：X→（F（X），）。 而且FifF={X}否则，请执行以下操作。是一个连续的同态扩张，因为下面的推理。如果F1，F2是滤波器，其中F1<$F2 ={X <$}，则F1<$F2 = X<$。 因为X是一个结果。因此，η：X→（F（X），）不是抽象（S，）-结构。推论4.14存在一个拓扑空间X，对于X，映射η： X→（F（X），），将一个点映射到它的邻域滤波器，不形成观测诱导的上幂空间。I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）1051195结论我们证明了对于任意的预选观测代数（O，O），在拓扑空间上存在观测诱导自由代数，并在定理2.10中刻画了它们。此外，我们还证明了自由（O，<$O）-代数继承了（O，<$O）的许多理想性质，如满足代数方程或属于引理2.3和2.4中的相应子范畴.此外，我们还研究了由观测代数（S，S）和（S，S）诱导的观测诱导的上、下幂空间构造在多大程度上推广了经典的证明了对每个拓扑空间X，观测诱导下幂域由下Vietoris拓扑下的非空闭子集空间以集并运算给出.进一步地，对于大类Wilker空间，X上的观测诱导上幂域由O（X）的Scott-开滤子空间在Vietoris上拓扑下以集交为运算给出. 然而，我们也给出了一个拓扑空间的例子，在这个拓扑空间中，这个特征并不成立。然而，我们可以说，在这两种情况下，这些观察诱导的幂空间构造将经典的幂空间构造真正地推广到了所有的拓扑空间。有一些有趣的开放性问题的观察诱导代数结构超出了本文的范围第一个问题是凸幂域和其他计算对象是否存在观测代数辛普森提出了一些可能性[13]。第二个问题是，在其他范畴中，例如经典范畴、综合范畴或拓扑范畴，情况是怎样的。抽象机制在这些设置中是适用的，并且在拓扑域理论中已经研究了观察诱导的概率功率域[3]。最后，人们可能会问，从范畴论的观点来看，上面给出的定义是否是最合适的定义，正如我们在2.1节中所暗示的那样，是否可以证明从观察代数继承了更多的性质，以及这些构造在应用中如何表现，即它们是否产生了用于证明程序正确性、程序等价性等的方法。确认这项工作是强烈的影响，由亚历克斯辛普森的工作和作者要感谢他的许多有益的意见 和 他 的 道 歉 。 作 者 还 希 望 对 Klaus Keimel 、 Christoph Schubert 和 ThomasStreicher进行的有益讨论表示感谢。引用[1] Abramsky，S.和A. Jung，Domain theory，Handbook of Logic in Computer Science3，ClarendonPress，Oxford，1994 pp. 1-168[2] 巴滕菲尔德岛，“拓扑域理论”，博士论文，LFCS，爱丁堡大学（2008年）。120I. Battenfeld，M.Schröder/Electronic Notes in Theoretical Computer Science 276（2011）105[3] 巴滕菲尔德岛和A. Simpson，Two probabilistic powerdomains in topological domain theory（2006），manuscripts，available at：http://homepages.inf.ed.ac.uk/als/Research/topological-domain-theory.html.[4] 恩格尔金河，[5] Franklin，S.P.，序列在其中存在的空间。，Fundamenta Mathematicae57（1965），pp.107比115[6] Gierz，G.，K. H. Hofmann，K.作者：John，M. Mislove和D. S. Scott，[7] Heckmann，R.，幂域和二阶谓词，Theor。Comput. Sci. 111（1993），pp. 59比88[8] 琼斯角，澳-地 “概率非决定论”博士 论文，爱丁堡大学LFCS（1989年）。[9] Moggi，E.，计算和单子的概念，Inf.Comput. 93（1991），pp.55比92[10] Plotkin，G. D.和J. Power，计算效应和操作：概述。，电笔记理论。Comput. Sci. 73（2004），pp.149比163[11] S