经典Domain理论中的观察诱导：计算单子构造与powerdomain结构的研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记301（2014）21-37www.elsevier.com/locate/entcsDomain理论中的观察诱导Ingo Battenfeld1FakultéatfurürInforrmatikTU Dortmund多特蒙德，德国摘要我们研究了在经典Domain理论范畴内构造计算单子的观测诱导自由代数方法我们的研究结果表明，自由代数结构存在于所有有限代数签名和计算原型。我们还研究了经典的powerdomain结构中的观测诱导的方法。对于霍尔，史密斯和概率的powerdomain建设，我们建立在既定的结果，表明它们可以恢复观测诱导。然而，Plotkin权力领域的问题更大。在这里，我们表明，与明显的原型代数，Heckmanns代数A，一个没有得到经典的Plotkin幂域。关键词：指称语义，计算效应，幂域，拓扑域理论1介绍Eugenio Moggi的计算单子理论使用了一个数学概念，将涉及计算效果的程序（如非确定性、例外、状态或交互式I/O）与纯函数程序分开。此外，一元方法允许系统地将纯程序提升为有效的环境[17]。这个理论已经被证明是如此成功，以至于它已经被概念性地引入到Haskell [13]中，Haskell是当今使用最广泛的函数式编程语言之一后来，Gordon Plotkin和John Power改进了Moggi这个想法允许不同效应的系统组合[11]，并通过引入代数运算作为效应触发器的概念来帮助解释效应的起源[18]。然而，相比之下，1Email：ingo. battenfel l d@tu-dortmund. Dehttp://dx.doi.org/10.1016/j.entcs.2014.01.0031571-0661 © 2014 ElsevierB. V.在CC BY-NC-ND许可下开放访问。22I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）21相对于代数运算与效应触发器之间的对应关系，代数方程与计算类型的某些良好性条件之间的对应关系似乎有点人为。在2005AlexSimpsonanddMatthiasSchréoders与Plotkin和Power类似，他们使用代数运算作为效应触发器，但不是使用方程理论，他们建议通过计算观察的单个代数来定义属性，认为这是计算原型，以将一类完全代数作为计算类型。单子然后给出的自由代数结构到类的这些完全代数。这种方法在精神上接近于史密斯在[3，4]中，我们研究了连续映射范畴Top中的观测诱导自由代数方法在拓扑空间之间，并且在[2]中，在一般情况下，在carnival闭范畴中。的在前一种情况下，结果是自由观测诱导的代数映射对任意有限签名和计算原型都存在，而在后一种情况下，在环境范畴上，在相当温和的条件下，同样成立在手头的工作中，我们调查的观察诱导自由代数方法在经典域理论的范畴，特别是在DCPO。一我们的主要结果将是DCPO支持自由代数结构，任意有限签名和原型。这已经在[2]中提出，但与该工作相反，在这里我们使用[4]的定义，其将完备代数范畴展示为给定签名的代数范畴的全反射范畴。我们还研究了经典的幂域结构，即Plotkin，Hoare，Smyth和概率幂域通过自由观测诱导代数。 霍尔和史密斯的结构在形式上稍有不同，在前引书中已经考察过了。[20]中的概率幂域我们使用这些结果表明，它们可以恢复在观测诱导的方法。各个幂域的完备性证明都遵循相同的策略，为进一步的构造提供了一个系统的模板。对于Plotkin功率域，Alex Simpson [21]建议使用Reinhold Heckmann然而，我们发现，这种观察诱导的建设不产生经典的Plotkin powerdomain，给出的A-估值loc.cit. 或Goubault-Larrecq应该提到的是，手头的工作，特别是我们的一些结果与Klaus Keimel最近的工作[ 15 ]非常相似，他在DCPO范畴中将状态transformer Transformer和谓词transformer Transformer语义联系起来。本文的组织结构如下。 在第2节中，我们回顾了P-完全代数，并给出了两个条件，在这两个条件下，它们对于其下的S g n a u r e构成代数范畴的一个全反射子范畴。由Schréoder和Simpson提供的光学成像中的精细度差，但其反射率结果尚不清楚。在第3节中，我们证明了DCPO满足这两个要求，因此自由代数结构I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）2123^存在任意签名和原型。在第4节中，我们研究了在多大程度上经典的幂域结构可以恢复在ovbservationally诱导的方法。最后，在第5节中，我们给出了结论。2先决条件我们假设C是一个Carnival闭范畴，C是一个有限代数签名.我们用C表示C中的-代数之间的-同态范畴，定义同上。我们用A表示C-代数（A，{ωA}）.由于C是Carnival闭的，范畴C具有C-幂：如果A（=（A，{ωA}））是C-代数，X是C-对象，则AX上的规范运算按点定义为：ωAX：= λ（f i）i∈| ω|.λx。 ω A（（f i（x））i∈| ω|）的。此外，我们假设C是C-丰富的，即对于C-代数A和B，同态C（A，B）形成一个C-对象，我们用[A<$B]表示。我们假设这个C对象[A<$B]是指数BA的子对象，如果C有足够的极限和共极限，它可以作为均衡器从BA中最后，我们确定了一个C-代数P（=（P，{ωP}））作为计算原型.下一个定义在合成域理论中是众所周知的。定义2.1对于C-代数A，B和C，一个C-同态h：A→ B称为C-可等的，如果每个C-同态f：A→ C有唯一的沿h的同态扩张f：B→ C.在范畴论术语中，h与单位元idC正交，记为hidCX.接下来，我们将我们的计算类型类标识为以下意义上的完备代数。定义2.2一个P-完全代数是一个C-代数C，其中每个P-等同态h：A→B是C-等的，即：胡鲁德·P·胡鲁德·C.CP。我们将P-完全代数之间的C-同态范畴记为：回想一下，健忘的函子C→ C创建了极限。 事实证明这同样适用于P-完全代数的子范畴。引理2.3健忘函子U：CP→C产生极限。证据显然，健忘函子因子为CP→ C→ C，右边的部分产生极限。因此，如果D是CP中的图，且U（D）的极限存在于C中，则它这只说明24I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）21（Lim（D），{ωLim（D）}）是P-完全的，这是由一个简单的计算得出的. 细节留待有兴趣的读者去了解.✷为了给观测诱导效应单子提供一个良好的基础，我们想在范畴框架上做的进一步假设是，CP从CP继承了C-幂。这不能从我们的定义中显示出来，所以我们把它作为我们的第一个要求。要求1范畴C P从C P继承C-幂。对于下一个结果，让我们固定代数A和B。回想一下，我们假设[A<$B]是指数BA的子对象。我们用ι表示内含物。此外，我们有一个正则映射γ：A →B BA，λ-项由λx给出。λf.f（x）. 我们用η来表示复合Bι<$γ：A →B[A<$B]。为了简单起见，我们把它写成λx。λh .h（x），这里我们用h来表示它代替了一个n-同态引理2.4对所有的n-代数A和B，映射η：A → B[A<$B]是相应代数结构上的n-同态。Pr oof. 我们已经讨论了如何对所有的perationsω，mapsηωA和dωB[AB]η进行处理|ω|一致。 如果我们将ω A改写为λ（xi）i∈| ω|. ω A（（x i）i∈| ω|），我们计算第一项：ηω A =（λx.λh。（h（x））<$（λ（x i）i∈| ω|.ω A（（x i）i∈| ω|））= λ（x i）i∈| ω|.λh。（h（ωA（x i）i∈| ω|））。对于第二项，我们计算：ωB[A<$B]ωη|ω|=（λ（fi）i∈|ω|. λ h。 ωB（（fi（h））i∈|ω|））<$（λ（xi）i∈|ω|. λ（hi）i∈|ω|. （hi（xi））i∈|ω|）=λ（x i）i∈| ω|. λh。 ω B（（λh i. （h i（x i）（h））i∈| ω|）=λ（x i）i∈| ω|. λh。ω B（（h（x i））i∈| ω|）的。因此，为了使各项相等，我们需要h（ω A（x i）i∈| ω|）= ω B（（h（x i））i∈|ω|），这恰好是h是n-同态的条件。✷因此，特别地，对于每个C-代数A，我们得到一个标准C-同态ηA：A→P[A<$P]。我们对范畴框架的第二个要求是建立在第一个要求之上的，它要求这张地图有一个方便的因式分解。要求2：对于每个C-代数A，标准C-同态η A：A→ P[A<$P]分解为P-等时h：A→ A ′，其中A ′是P-完全的，后面跟着单态A ′ → P[A<$P]。注意到对A′是P-完全的要求，刻画了这个因式分解直到同构为止是唯一的。命题2.5在要求1和要求2下，范畴CP构成C的一个全反射子范畴。I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）2125WW证据 一个η-代数A的反射是由要求2的η的因子分解得到的P-完全代数A ′。✷3Domain理论现在我们将考虑经典Domain理论中的P-完全代数范畴.我们从固定符号开始。用DCPO表示有向完全偏序集之间的Scott-连续映射范畴。众所周知，DCPO是一个Cartesian闭、完备、余完备范畴。再次假设给定有限代数签名，得到dcpo-代数之间Scott-连续的n-同态范畴DCPO n-（我们也写DCPOn-代数）.与前一节一样，我们通过下划线来表示DCPO代数：A：=（A，{ωA}）。对于一个（点态）有向的Scott连续同态族{hi：A→B} i∈I，（点态）有向上确界i∈Ihi也是一个Scott连续同态A→ B，因此范畴DCPO_n是富含DCPO我们用[A<$B]表示A和B对于DCPO-幂，若X是DCPO代数，A是DCPO代数，则记A的X-幂为AX.我们还固定了一个DCPO的P-代数P作为计算原型，得到了P-等同态和完备P-代数的概念。DCPOP表示P-完全代数之间的Scott-连续的S-同态范畴（我们也用DCPOP-代数来表示）。我们还将使用子dcpos和子代数的概念，我们给出以下形式定义。定义3.1如果X是dcpo，则X的subdcpo是子集Y <$X，使得对于每个有向{yi} i∈I<$Y，在X中计算的上确界i∈Iyi属于Y。若A=（A，{ωA}）是DCPO代数，则DCPO代数B=（B，{ωB}）给出一个DCPO子代数，使得B是A的子dcpo，相应的嵌入是一个Scott连续的子同态B→A.我们写B<$A来表示B是A的DCPO<$-子代数。如果A是DCPOP-代数，则A的一个P-完备子代数是A的一个本身是P-完备的DCPON-子代数B现在我们继续证明DCPO满足上一节的要求1和2。我们从DCPO类的一些特定结果开始。 第一个这样的观察是众所周知的，即映射f：X ×Y →Z是斯科特连续的当且仅当它在每个分量上分别连续。现在让我们定义分量同态。定义3.2设X是dcpo，A和B是DCPO代数. 则Scott-连续映射f：X × A → B是右同态，如果对所有x ∈ X，ω ∈ ψ，{ai} i∈| ω|证明了f（x，ω A（（ai）i∈| ω|））=ω B（f（x，ai）i∈| ω|）.26I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）21^^^^WW^^_g^（xi，b0）=g^（_xi，b0）.^下面的结果，其直接验证留给倾斜的读者，不是特定于DCPO，但在每个良好指向的carpet闭范畴中都成立。引理3.3设X是dcpo，A和B是DCPO代数。 则Scott-连续映射f：X × A → B是右同态当且仅当它的指数转置f <$成为A→ BX的右同态.紧接着需求1的下一个引理是DCPO范畴特有的。引理3.4在范畴DCPO中，一个n-同态h：A→ B是C-相等的，如果它是CX-相等的，且对于C的每一个DCPO-p都是.证据 设h是C-等式。我们必须证明它是CX-均衡的，DCPO-C的幂 。所以假设f：A→CX是任意的n-同态。我们考虑它的指数转置g：X ×A → C，它是相应代数结构上的右同态.因此，对于每个x ∈ X，对应的映射gx：A → C（由a <$→ g（x，a）给出）产生同态A→C，因此具有唯一扩张g x：B→ C沿h方向。因此，我们可以定义一个映射g：X ×B → C，通过（x，b）›→ g（二）明确^^x是对应代数结构上的右同态。它本身也必须是唯一的，否则我们可以找到一些x0∈X，其中gx0沿着h没有唯一的扩张，这与它的C-等式相矛盾。证明g是Scott连续。因为所有的gx都是Scott连续的，所以只要证明g在它的第一个分量上是Scott连续的就足够了。 对所有b0∈ B和有向{xi} i∈I<$X，它成立，i∈I这是因为我们知道， i∈Ig^xi=g^Wi∈Ii∈IXi. Sincei∈Ig^xi是向上的方向B→C的Scott-连续同态，它本身也是一个Scott-连续同态，homomoorphiism. AsitholdsthatWi∈Ig^xi（h（a））=^gW x（h（a）），对于所有a∈A，weWWi∈Ii得到那个Wi∈Igxi 延伸gi∈Ixi 沿着h，所以根据唯一性，它必须保持，i∈Igxi =gWi∈Ixi ，根据需要。✷推论3.5 DCPO范畴满足前一节的要求1.为了证明DCPO也满足要求2，我们使用了所谓的d-完备化[25]，它也被称为单调收敛反射[6]。 它是一种拓扑结构，应用于DCPO中，分配给子集dcpoX的S<$X，包含S的最小子dcpod（S）<$X。 Keimel和Lawson [16]证明了给定一个半拓扑n-代数（A，{ωA}）（即所有的运算都是分别连续的），这些运算可以扩展到它的d-完备化，使得（d（A），{ωd（A）}）成为一个半拓扑n-代数。我们以下面的形式使用他们的结果。I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）2127引理3.6设A=（A，{ω A}）是一个DCPO 代 数，S ∈ A是在运算ω A 下 闭 的子 集. 则（d（S），{ω A|d（S）}）是A的DCPOπ-子代数.证据考虑S ∈ A为拓扑子空间，（S，{ω A|S}）成为一个半拓扑的n-代数。因此，利用Keimel和Lawsons的结果，可以将这些运算推广到它的d-完备化，从而得到（d（S），{ω A|d（S）}）是一个半拓扑子代数，使它成为A的DCPO子代数.✷命题3.7范畴DCPO满足要求2，即对每个DCPO 代 数，Scott连续的N-同态η：A→P[A<$P]分解为h：A→ A′后跟i：A′→ P[A<$P]，使得A′是P-完全的，h是P-相等的，且A′<$P[A<$P]。证据考虑im（η）<$P [A<$P]，映射η的像。很明显，im（η）在运算{ωP[A<$P]}下是闭的，因为η是一个n-同态，通过引理二、四、 我们设置ACP[ACP]来实现fm（n）的d-cmpin，其中通过使用一个d-cPom-subaACP[ACP]来实现。现在我们可以确定这一点J：={BP[AP]|BisP -completeanddAB}.由于DCPO满足要求1，P[A<$P]∈J，因此J非空。康-边J：=TB∈JB作为P[AP]的子集. 根据引理2.3，J配备了in-⊸P[A<$P]的导出运算成为P[A<$P]的P-完全DCPO子代数，因为交可以描述为相应DCPO子代数的极限. 所以，它几乎没有什么东西可以让它成为一个令人兴奋的东西。现在，我们有一个问题-将η设为：A−→A−→J−→P[AP]，其中所有部分都是Scott-连续的π-同态，右边的映射是DCPOπ-子代数嵌入。我们还需要证明左边的两个映射的合成（记为h：A→J）是P-相等的。为此，考虑任何斯科特连续的n-同态f：A→P和以下图：P[AP]❄❄❄电子邮件*ι❄❄❄❄❄❄JzzP，，⑧⑧⑧h F⑧⑧⑧A.当Φf：P[AφP]→P是一个奇异函数F<$→F （f）时，它是一个新的奇异函数。 因此，在Φf_i上的互补性：J→P使f沿h延伸。它仍然显示出独特性。28I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）21vvv对于这种情况：J→P不是一种简单的方法。Then，theequualizerofΦfi和g 定义了一个P-完备DCPO代数J′<$J，它也是一个P-完备DCPO_n-P[A_nP]的子结构包含η的imge，并且A_n，h_ne，h_n e，J′∈J，且f（t）{\displaystylef（t）} 这是唯一的好消息，如果Φf f是零，那么它是如何运行的？P-均匀，如所需。✷因此，命题2.5适用于DCPO。定理3.8对于每个有限代数签名，P，范畴DCPOP是DCPO的一个全反射子范畴。众所周知，对于任何有限代数签名，遗忘函子DCPO<$→DCPO有一个左伴随，即存在绝对自由代数结构F：DCPO→DCPO<$。将这个绝对自由的代数函子与反射合成，得到一个自由的DCPOP-代数函子.推论3.9对每一有限代数签名n和计算原型P，遗忘函子DCPOP→DCPO有一个左伴随FP：DCPO→DCPOP。最后，我们证明了P-完全代数满足P自身所满足的所有代数不等式.该证明非常类似于拓扑框架中关于代数方程的相应证明[3]。命题3.10设t ≤ t ′是P所满足的代数不等式。 那么所有P-完全代数满足t ≤ t ′.证据设X是离散序可数集。则X是一个dcpo，我们可以形成自由Dcpo代数TX，它由所有的一般的dcpo-项组成。TX本身是离散有序的。进一步地，代数不等式t ≤ t ′导出了一个关于任意y（I，I）的不等式，并给出了在X上的任意DCPO（I，I）-algbraFX. FX不是离散有序的，因为它满足我们对所有变量的不等式实例化。利用自由代数的性质，我们得到了一个标准的正则同态h：TX→FX，即x∈Nx→TX，并且Scott连续映射X → P、正则同态TX→ P和正则同态FX→ P之间存在同构，后者是由沿h的扩张给出的.这使得h是P-等的n-同态。因此，对于每个P-完全的λ-代数B，每个λ-同态v：TX → B都可以被归结为一个λ-同态ph是vλ：FX→B. 设ttv，tv∈B是t，t ′的对应项实例，由v：TX→ B给出.设U ∈ B是Scott-开的，包含tv。 则对于相应的项t，t ′∈ FX，（一）e. tv=v（t）anddt′=v（t′）），thatt∈v−1（U），hencet′∈v−1（U），andndsot′∈U。这表明t v≤ Bt ′，如所要求的。✷I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）21294Powerdomain构造我们现在研究在多大程度上可以恢复经典的powerdomain结构的观察诱导的方法。我们从Hoare，Smyth和（扩展的）概率幂域开始。Hoare和Smyth幂域的结果已在[3，4]中的拓扑设置中得到。在手头的案例中，证明策略是相同的，所以我们省略了证明，因为读者应该没有问题通过咨询loc来填写细节。前引书.在扩展概率幂域的情况下，所需的技术细节基本上遵循Tix [23]的工作，因此我们给出了这种情况下证明的简要提示为了在观测诱导方法中构造Plotkin幂域，Simpson [21]建议使用Heckmann我们给出了一个非常简单的反例，表明这个原型的观测诱导方法不会产生经典的Plotkin幂域，但可能包含更多的元素。事实上，传统构造的代数即使在最简单的情况下也不能是A-完全的在一般非决定论的三种情况下，即Hoare，Smyth和Plotkin幂域，我们考虑由单个双-nary运算<$={<$}，并写出简笔数<$-代数（或DCPO<$-代数）和<$-同态（或DCPO<$-同态）。进一步，我们设S表示二元Sierpinski整环{ε，ε}，其中ε≤ε，但反之则不然.我们不断地将映射f：X→S与对应的斯科特开子集U：=f−1（{K}）相识别。在扩展的概率幂域的情况下，我们使用签名{λ|λ ∈ R+}，其中R+表示非负实数集，由∞扩张. 我们还使用R+表示由相同的底层集合和通常的顺序组成的dcpo。R+成为一个DCPOn-代数（实际上是一个dcpo-锥[24]），当像往常一样配备了运算x+λy：=λ·x+（1− λ）·y时4.1霍尔的权力领域霍尔幂域的原型代数是S：=（S，），其中：S2→S是通常的连接运算。斯科特连续映射f：X→S可以用开子集U <$X，通过U=f−1（{X}）来在dcpoX上的Hoare幂整环的经典刻画将其展示为X的按包含排序的非空闭子集的dcpo，我们用C（X）表示，其运算由集并给出，即（C（X），n）。我们使用一个一般的策略证明了对于每个dcpoX，（C（X），n）是一个DCPOS-代数.这里的关键是把它代数地表示为SSX的子集。这是通过以下结果序列获得的。引理4.1映射ι：C（X）→S SX是Scott-连续的，并且成为一个π-同态（C（X），π）→SπSX。引理4.2元素F∈SSX在im（i）中当且仅当它满足以下两个性质：30I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）21∧（i）F（X）=λ，（ii）F（U <$V）= F（U）<$F（V）.定理4.3对每个dcpo X，（C（X），n）是S-完全代数.对于任意dcpo X，（C（X），n）是X上的自由dcpo-代数，其不等式理论由n的自反性、交换性和结合性以及不等式x≤x <$y给出.因此，自由性来自于经典自由代数构造的普适性。定理4.4对于每个dcpoX，X上的自由 DCPOS-代数由下式给出：（C（X），n），其中自由代数包含X → C（X）是点闭包映射。4.2关于Smyth PowerdomainSmyth幂域的原型代数是S ：=（S，），其中：S2→S是通常的交运算。连续dcpoX上的Smyth幂域的经典刻画表明它是X的按逆包含排序的非空紧饱和子集的dcpo，记为K（X），其运算又由集并给出，即（K（X），n）.在清醒的假设下，我们可以再次证明（K（X），K）是一个DCPOS-代数。引理4.5对于一个sober dcpo X，i：K（X）→ S SX是Scott-连续的，并且成为一个π-同态（K（X），π）→SSX。引理4.6对于sober dcpoX，元素F∈SSX在im（i）中当且仅当它满足以下两个性质：（i）F（λ）= λ，（ii）F（U <$V）= F（U）<$F（V）.定理4.7对每个sober dcpo X，DCPO的S-代数（K（X），X）是S-完备的.对于任意连续dcpoX，（K（X），n）是X上的自由dcpo-代数，其不等式理论由n的自反性、交换性和结合性以及不等式x <$y≤x给出.这产生以下结果。定理4.8对任意连续dcpoX，X上的自由DCPOS-代数由（K（X），λ）给出，其中自由代数包含X → K（X）为x <$→↑{x}。4.3扩展的概率幂域扩展的概率幂域的原型代数是R+：=（R+，{+ λ}），如上所定义。连续dcpo X上的扩展概率幂域的经典刻画将其表现为Scott连续赋值V（X）的dcpo，即Scott-连续映射ν：O（X）→R+，其中ν（X）= 0，ν（U <$V）+ν（U <$V）=ν（U）+ν（V），逐点排序，并给出相应的逐点运算。I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）2131R2 ifx=y=2在这种情况下，我们只给出连续dcpos的结果，因为这允许我们使用[ 23 ]的拓扑结果，因为在这种情况下，Scott拓扑和弱拓扑在loc.cit.中使用。一致。另外，V（X）对于dcpo-锥的初始性也仅在这种情况下已知。在概念上，我们不区分DCPO-代数和相应的基代数的DCPO-幂上的运算。这不应该引起任何混淆，因为相应的操作提升是规范的。RX引理4.9对于连续dcpoX，映射i：V（X）→R++是Scott-RX连续的，并且成为一个n-同态（V（X），{+ λ}）→ R++。证据 这是从[ 23 ]中的Satz 4.4得出的。✷RX引理4.10对于连续dcpoX，元素F∈R+只有当它满足以下两个性质：(i) F（const0）= 0，(ii) F（f +λ g）= F（f）+λF（g）。+ 在im（i）中，如果且证据这本质上是Riesz-表示定理，即[23]中的Satz 4.19。✷定理4.11对每个连续dcpoX，（V（X），{+ λ}）是R+-完全代数.证据现在证明是纯代数的，并且完全遵循下面引理4.14的证明步骤。 细节留待有兴趣的读者去了解.✷已知对于每个连续dcpoX，（V（X），{+λ}）是X上的自由dcpo-锥，参见[12]。这产生以下结果。定理4.12对每个连续dcpoX，X上的自由DCPO-代数+由（V（X），{+λ}）给出，其中自由代数包含X →V（X）映射x∈X对应的评价点。4.4Plotkin Powerdomain设A为三元链，其基础集合为{0，1， 2}，其中0≤ 1≤ 2，反之亦然。正如Simpson[21]所建议的，对于凸幂域，我们选择原型代数A：=（A，），其中：A2→A定义为：xxy：=0，如果x=y= 0我是说，我是说，Scott连续映射f：X →A可以用开子集对来标识通过U=f−1（{2}）和V=f−1（{1}），我们可以在这些表示之间切换。32I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）21F❧我们继续在前面的部分，以代数的方式构造双指数A的一个合适的DCPOA定义4.13设X是dcpo。设A（X）是由满足以下三个性质的元素给出的AAX(i) F（const0）= 0，(ii) F（const2）= 2，(iii) F（f<$g）=F（f）<$F（g），其中，在最后一个属性中，fg对AX使用相应的操作。A（X）确实是A AX的subdcpo很容易检查，以及它在运算下是封闭的，即它是一个子代数。实际上它是一个完备子代数，如下面的结果所示。引理4.14对于每个dcpoX，DCPO的λ-代数（A（X），λ）是λ-完全的。证据我们用e表示嵌入（A（X），n）→A<$AX。设h：A→ B是A-均匀的，f：A→（A（X），X）是Scott-连续的A-同态. 请看下图：埃什多夫✐❣❞❜❴❭❩❲❯❘sAB（A（X），）/AX，，✈✈✈✈✈✈✈✈f✈✈✈A.其中e∈ f：B→A∈AX是e∈ f沿h的唯一同态扩张，b∈A∈A ∈X是A∈C-同态扩张。 对于所有b∈B，e∈f（b）满足定义4.13的性质（i）-（iii）。为此，观察到对于每个f：X→A，评估映射π：AAX→A是A-同态，因为A-完备代数的DCPO-幂上的标准运算是由逐点提升给出的从而得到πconst0εf必是πconst0εf沿h的唯一的π-同态扩张.但后者等于映射const0：A→A，因为它通过f分解，并且im（i）的所有元素都满足定义4.13的性质（i）。因此，通过同态扩张的唯一性，πconst0 ∈ e ∈ f = const0：B→ A∈ f，如果b∈B，e∈f （b）是f ∈pp（i）. 一个非常小的团队（ii）该人的姓名或名称;或为了证明性质（iii）成立，我们可以观察到：A：A2→A可以用来将同态合成为A，即。 如果g，g′是任意Scott-连续如果A是从同一个源代数生成的n-同态，则点态合成gg′也是一个Scott-连续n 因此，我们得到，eHI. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）2133对于f，g：X→A，h（π f ef）（πgef）是（πf ef）（πgef）alonggh的一个双态随机变量. 但这一点是平等的，以πf计算，因此，这一点是必要的。总之，πfgef由πfge f确定，并且可以由任意一个等式确定t（π f ef）（πge f）π fgef，这表明对于所有b ∈ B：e<$f（b）（f<$g）=πf<$g<$e<$f（b）=（（πf <$e <$f）<$（πg<$e<$f））（b）=（πf <$e<$f）（b）<$（πg<$e<$f）（b）=ef（b）（f）ef（b）（g），henceeef（b）satisf iesprperty（iii）frmDef in it i tion4. 13，其中包括证明。✷与前面几节中考察的幂域相对应，人们可能会认为定义4.13中定义的DCPOA-代数实际上是传统的凸幂域。然而，我们现在表明，即使对于非常简单的dcpos，情况也不是传统的凸幂域（或Plotkin幂域）可以在文献中找到几种不同的定义。标准参考文献[6，1]使用透镜的概念，Goubault-Larrecq [8]用准透镜的概念代替透镜以获得更一般的结果。然而，最适合我们目的的定义是由Heckmann [9]提出的，与Goubault-Larrecq的定义是等价的他使用了X上的A-赋值的概念，这是一个Scott连续映射α：O（X）→A使得α（X）= 0，α（X）= 2，α（U）= 0意味着α（U <$V）=α（V），α（U）= 2意味着α（U <$V）=α（V）。 对于每个dcpoX，我们用AVal（X）表示逐点排序的A可以直接检查函数空间AO（X）中A-赋值的有向上确界也是A-赋值，因此AVal（X）总是dcpo。此外，我们定义了一个二元运算<$：AVal（X）2→AVal（X），通过逐点应用<$，即对于所有开U <$X，（α <$α′）（U）：=α（U）<$α′（U）。很容易证明，A是Scott-连续的，因此（AVal（X），A）构成一个DCPO代数。存在（AVal（X），）到AAX中的Scott-连续-同态嵌入，由映射i：AVal（X）→AAX给出。在由开子集对给出的映射方面，由下式给出i（α）（μ U，V μ）=如果α（U）= 2，则为2如果α（V）= 0，则为0我是说，我是说，事实上，它成为一个DCPO代数嵌入。这一主张的证明留给有兴趣的读者去研究。我们简单地说，im（i）中的每个元素都满足定义的性质，34I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）21{a}，{a，b}Ssssss一{a，b}，{a，b}s▲ssss◦S▲{b}，{a，b}▲◦ ▲sssSs{a}，{a}▲▲▲▲▲▲▲▲▲sssssssss▲▲▲▲▲▲▲◦ {b}，{b}▲▲▲▲sssss▲▲▲▲sssss▲▲▲ ss s sss，{a，b}▲▲▲▲▲◦ ssss⟨∅,{a}⟩ ▲▲▲▲S⟨∅,{b}⟩▲sssss你好Fig. 1. 一个2乌尔乌尔2 1 1 22 111 11 1 21 1l c r2 12 101 11 111 20 1 21 0 1 1 0 1LL LR1 1 1 11 101 0图二. A类（2）0 1 10 1第4.13节，但在下文中，我们将表明，这些都不足以证明im（i）完全。我们现在给出一个dcpoX的例子，其中AVal（X）A（X）。事实上取X为2，即二元离散域就足够了。让我们用{a，b}表示2的元素。Val（2）是由三个元素αa，αb，αab组成的其定义为：α（U）=.2 ifa∈U类似于αb和αab（U）=0否则，2，如果U=20，如果U=0我是说，我是说，让我们也给一个草图的dcpoA2. 在打开对方面，它看起来如图1所示。A2上的操作“向中间”组合元素我们现在画出A（2）→AA2，给出A2的元素的相应图像，如图1所示。 注意，通过条件（i）和（ii），对于每个F ∈ A（2），我们有F（，）= 0和F（{a，b}，{a，b}）= 2。因此，我们可以省略top和bottom元素。因此，A（2）看起来就像图2中的那样，在图中我们省略了排序，并根据元素在图中的位置来命名元素，即：ul表示左上方等等。实际上，我们看到A（2）同构于子代数▲Ss◦▲▲◦I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）2135A2通过省略顶部和底部元素而获得，同构是同态的。有一个明显的嵌入κ：AVal（2）→ A（2），由αa < $→ l，αb <$→ r，αab < $→ c给出。通过下面的引理，κ很容易被证明是A-相等的。引理4.15每一个Scott连续映射f：2 → A都有唯一的同态扩张f：（A（2），λ）→Aλ沿着规范嵌入2 → A（2）。证据 我们通过证明映射f：2 → A的要求来证明这个证明，给定byf （a）=2anddf（b）=1。 通过a<$→landb<$→r，可以创建一个新的计算机。这立即产生f（l）=2和f（r）=1，因此：f（c）= f（l <$r）= f（l）<$f（r）= 1.由于ul ≥ 1，单调性产生f（ul）= 2。最后三个案例都遵循相同的模式，最有趣的是ll. 单调性产生f（ll）≤ f（c）= 1。但我们也得到：f（ll）=f（ll<$l）=f（ll）<$f（l）0，因此，只剩下f（ll）= 1。✷推论4.16嵌入κ：AVal（2）→ A（2）是A-相等的，DCPO一个2上的n-代数由A（2）给出.因此我们证明了DCPOA-代数（A（X），λ）一般大于A-赋值代数然而，问题仍然是它是否刻画了自由DCPOA-代数结构。我们猜想这是连续dcpos的情况，但目前还没有证据最后，我们注意到，我们不认为另一个观察诱导理论将产生传统的Plotkin功率域的建设。 这是因为代数A是Plotkin幂整环的一个非常典型的例子，即Sierpinsky空间S上的传统Plotkin幂整环。因此，对于给出Plotkin幂域的观测诱导理论，A∈但我们上面的例子表明，情况不太可能如此。5结论和进一步工作我们证明了dcpos之间的Scott-连续映射范畴DCPO对于任意有限代数签名和计算原型P都支持一个自由的观测诱导代数构造。该结构是由一个普通的绝对自由的π-代数结构，然后是一个反射函子到范畴的P-完全代数。显示反射的存在函子是通过使用P-完全代数的定义而成为可能的，第二节给出的P36I. Battenfeld/Electronic Notes in Theoretical Computer Science 301（2014）21此外，我们还研究了在观测诱导的方法中，经典的幂域可以恢复到什么程度。 对于Hoare，Smyth和（扩展的）概率幂域，我们给出了产生传统构造的对于任何dcpo，观测诱导Hoare幂域由非空Scott闭子集的dcpo给出，对于所有连续dcpo，观测诱导Smyth幂域由非空紧饱和子集的