FS-ε↑-整环的Scott连续函数与Smyth幂整环的特性及其在领域理论中的应用

∧∧可在www.sciencedirect.com在线获取理论计算机科学电子笔记333（2017）153-162www.elsevier.com/locate/entcs用FS-ε↑-整环Yayan Yuan1，2河南省大数据统计分析与优化控制工程实验室河南师范大学数学与信息科学学院，河南新乡453007惠寇三号四川大学数学学院长江数学中心，四川成都610064摘要本文引入了FS-↑-Domain，证明了以FS-↑-Domain为对象，Scott连续函数为态射的范畴是一个笛卡尔闭范畴.此外，我们利用FS -ε ↑ -整环刻画了Lawson紧整环上相容的Smyth幂整环.保留字：Domain; Consistency;FS-ε↑-domain; Consistent Smyth powerdomain1介绍在Domain理论中，幂域是一种非常重要的结构，它在非确定性程序设计语言的语义建模中起着重要的作用（[4，5，6，7，9，11，12，13，14，15]）。例如，Smyth幂整环是连续dcpo上的自由退化半格，其中退化二元算子是Scott连续满足算子[14]。然而，在许多有趣的域中，例如L-域，交算子不是完全的，而是部分的：如果两个元素是一致的，则它们有交（或最大下界），即，它们有一个上限。在这种情况下，部分交会算子称为一致交会，用↑表示。于是一个问题出现了：我们能构造一个新的自由代数吗？1国家自然科学基金（11371262，11171368）和河南省教育厅基金（15A110034）资助2电子邮件：yayanyuan@hotmail.com3电子邮件：kouhui@scu.edu.cnhttps://doi.org/10.1016/j.entcs.2017.08.0121571-0661/© 2017作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。154Y. Yuan，H.Kou/Electronic Notes in Theoretical Computer Science 333（2017）153一个连续的dcpo上的二元算子正是斯科特连续一致满足？在[16]中，我们用拓扑学和序理论的方法证明了连续dcpo上的相容Smyth幂整环存在，并且是一个连续dcpo-ε↑-半格.此外，如果连续dcpo是Lawson紧的，则它的相容Smyth幂整环是Lawson紧的L-整环.这是相容Smyth幂整环与经典Smyth幂整环的区别，因为Lawson紧整环上的经典Smyth幂整环是有界完备整环.注意，经典的幂整环，如Smyth幂整环和Hoare幂整环，都可以用幂整环结构中的基本函数分别给出的FS-整环来在文献[8]中，Huth，Jung和Keimel引入了一个新的概念：线性FS-格，它是一个完备格，并且存在一个有向族的有限可分线性函数可以逼近id，其中一个函数是线性的，如果它保持所有的上确界。他们证明了点域L上的Hoare幂域H（L）的特征在于：分配线性FS-格。在文献[10]中，Meng和Kou引进了F-S-整环，并证明了Lawson紧整环上的Smyth幂整环S（L）L是由F-S-整环刻画的.因此，从纯数学的角度出发，我们有理由相信在Lawson紧连续整环上存在一类FS本文首先利用部分Scott连续二元算子构造了一个有限分离Domain：FS-<$↑-Domain，它是一个dcpo-<$↑-半格，并且存在一个有向族的有限分离<$↑-半格同态，它能逼近idL.我们得到了以下结论：a) 以FS-R↑-Domain为对象，Scott连续函数为态射的范畴是一个范畴.b) Lawson紧连续整环L上的相容Smyth幂整环SC（L）是一个FS-ε↑-整环.此外，我们还利用FS-ε↑-刻画了一致的Smyth幂域，域.接下来，我们收集了本文所需的一些基本概念。读者也可以参考[1，3]。偏序集L称为有向完备偏序集（简称dcpo），如果L的任何有向集在L中有一个sup。对于x，y∈L，称x远低于y（记为xy）如果对于任何有向集D，y≤D，意味着存在一些d∈D，其中x≤d。 一个子集L称为连续的，如果对所有x∈L，x=<$↑↓x，即，集合↓x={a∈L：ax}是有向的，且x=<${a∈L：ax}，其中在系统结构<$↑中的“有向”是为了强调↓x的有向性。特别是，一个dcpo作为偏序集连续的域称为（连续）域。对于L的子集A，设↑A={x∈L：<$a∈A，a≤x}，↓A={x∈L：<$a∈A，x≤a}. 我们使用↑a（resp.↓a）而不是↑{a}（resp. 当A={a}时，A称为上（或下）。如果A=↑A（相应地，A=↓A）。一个元素k∈L称为紧的，如果k k.所有紧元素的子集记为K（L）。一个dcpoL称为代数的，如果对所有x∈L，x=<$↑（↓x<$K（L））。定义1.1设L是偏序集。Y. Yuan，H.Kou/Electronic Notes in Theoretical Computer Science 333（2017）153155(1) L的子集A称为相容的，如果A在L中有上界，即，对于某个x ∈ L，A <$↓ x.(2) 称L为相容交-半格（或称L ↑-半格），如果对所有相容x，y ∈ L，x ∈ y存在.为了强调x和y是一致的，我们将把x y写成x ↑ y。此外，若L是（连续）dcpo，则L称为（连续）dcpo-L ↑-半格.(3) 称L为L-整环，如果 L是整环且 L具有inf，即，对于所有x ∈ L，↓ x是完备格。设L是偏序集。 我们把由补L\↑x生成的拓扑称为作为次基开集的主滤子的下拓扑，记为ω（L）。如果（L，≤）是dcpo，我们定义Scott拓扑（记为σ（L）），它的闭集拓扑是所有有向完备下集，即，下集在有向上闭Lawson拓扑λ（L）是通过取σ（L）和ω（L）是次基的。如果L是一个<$↑-半格，则部分算子↑：L×L→L是Scott连续的。dcpo-<$↑-半格（P，<$↑）与（E，<$↑）之间的<$↑-半格同态f是从P到E的Scott连续函数，使得f（a<$↑b）=f（a）<$↑f（b），只要a，b在P中相容.注意，该函数是Scott连续的且条件乘法的（或在[2]中简称为cm），即每个<$↑-半格同态是Scott连续的cm函数。2FS-↑ -domain的分类对于dcpos L和P，令[L−→P]表示从L到P的所有具有逐点阶的Scott连续函数。对于dcpo-<$↑-半格D和E，设[D−→ <$↑E]表示从D到E的具有逐点序的<$↑-半格同态的函数空间。定义2.1 [3]一个dcpo L称为FS-domain，如果id L直接被一族有限分离函数逼近，其中Scott连续函数f：L−→L称为有限分离的，如果存在一个有限集合M f使得对于每个x∈L，存在m∈M f使得f（x）≤m≤x。定义2.2一个dcpo L称为一个FS-<$↑-domain，如果它是一个<$↑-半格，并且存在一个有向族的有限分离<$↑-半格同态，它们可以逼近id L。换句话说，FS-n↑-domain是一个连续的dcpo-n↑-半格，它的id被一个有向的有限分离的Scott连续函数族所逼近，这些函数保持了已有的有限infs。显然，每一个FS-域都是一个FS-域. 然后我们有命题2.3每个FS-整环都是Lawson紧整环.其次，我们证明了以FS-π↑-Domain为对象，Scott连续函数为态射的范畴是一个Carnival闭范畴。定理2.4设D和 E是dcpo-<$↑-半格，则[D−→<$↑E]是dcpo-<$↑-半格，156Y. Yuan，H.Kou/Electronic Notes in Theoretical Computer Science 333（2017）153j∈Jj∈Jk∈Kk∈Kk∈K半格证据首先，[D−→↑E]是dcpo。对任意有向集{f j∈[D−→E↑]：j∈J}和x∈D，集f（x）=j∈Jfj（x）.显然f是Scott连续的。如果x，y∈D是相容的，则f（x），f（y）在E中也是相容的.然后f（x↑y）= f j（x <$↑y）=（f j（x）<$↑f j（y））=（ f j（x））<$↑（f j（y））= f（x）<$↑f（y）.j∈Jj∈J所以f也是Scott连续的和一个π↑-半格同态。故[D−→↑E]为dcpo。其次，[D−→ <$↑ E]是<$↑-半格. 若f，g ∈ [D−→E↑]是相容的，则f（x），g（x）对任意x ∈ D都是相容的. 则f（x）<$↑g（x）存在。设（f<$↑g）（x）=f（x）<$↑g（x）.对于有向集{xk∈D：k∈K}，我们有（f↑g）（x k））= f（（x k））↑g（（x k））=f（xk）<$↑g（xk）=[f（xk）<$↑g（xk）]k∈Kk∈Kk∈K=[（f <$↑ g）（x k）]。k∈K则f↑g是Scott连续的。对于D中的一对相容点x，y，f（x<$↑y）和g（x<$↑y）在E中是相容的.然后（f↑g）（x↑y）=f（x<$↑y）<$↑g（x<$↑y）=（f（x）<$↑f（y））<$↑（g（x）<$↑g（y））=（f（x）<$↑g（x））<$↑（f（y）<$↑g（y））=（f <$↑ g）（x）<$↑（f <$↑ g）（y）。也就是说，f<$↑g是一个<$↑-半格同态。所以[D−→ <$↑E]是一个<$↑-半格。最后，利用运算的Scott连续性，得到如下结论.如果有向集{f j∈[D−→<$↑E]：j∈J}的sup与g∈ [D−→ <$↑E]相容，则对x∈ D，Y. Yuan，H.Kou/Electronic Notes in Theoretical Computer Science 333（2017）153157j∈Jj∈J[g↑]f j）]（x）= g（x）<$↑（（f j（x））=[g（x）<$↑fj（x）] =[（g<$↑fj）（x）]j∈J=[（g <$↑fj）]（x）.j∈Jj∈J所以，[D−→↑E]×[D−→↑E]−→[D−→↑E]是斯科特连续的。我们得到了[D−→E↑]是dcpo-ε↑-半格。Q定理2.5设D和 E是 FS-ε↑-整环，则[D-→ε↑E]和[D-→E]是FS-↑-域。证据设D和E分别是D和E的近似恒等式。那么我们声称这家人D E={δ：δ∈ D，∈E}定义为f›→δ2对于f∈[D−→<$↑E]是[D−→<$↑E]的一个近似恒等式，δ<$<$是有限分离的。证明与FS-整环的情形类似它表明δ∈[D−→↑E]−→↑[D−→↑E]。 首先，证明了δε是Scott连续的.其次，对于一对相容点f，g∈[D−→E↑E]，我们有（δ）（f），（δ）（g）是相容的，且对任意x∈ D[（δ）（f↑g）]（x）=[2（f↑g）δ2]（x）=2[fδ2（x）↑gδ2（x）]=2fδ2（x）↑2gδ2（x）=[2fδ2↑2gδ2]（x）=[（δ）（f）↑（δ）（g）]（x）。因此我们得出结论：δεε是一个ε↑-半格同态. [D-→↑E]是一个FS-↑-domain。同样，[D−→E]也是一个FS-↑-domain。Q注意，通常以FS-π↑-Domain为对象，π↑-半格同态为态射的范畴不是一个Carnival闭范畴。然而，如果范畴将Scott连续函数视为态射，则从前面的段落中我们有以下结论：定理2.6以FS-域为对象，Scott连续函数为态射的范畴是一个范畴.158Y. Yuan，H.Kou/Electronic Notes in Theoretical Computer Science 333（2017）153∧↑¯3通过FS表征一致的Smyth功率域-n↑-domain在下面的段落中，我们将把FS-ε↑-整环和相容Smyth幂整环与函数ε↑-半格同态联系起来。利用FS-幂↑-整环刻画了Lawson紧连续整环L上的相容Smyth幂整环SC（L定义3.1 [16]相容的定义半格是一个连续的dcpo L，其Scott连续二元部分算子仅定义为相容的点对，这些点对满足三个方程：交换性x <$↑ y = y <$↑ x，结合性x <$↑（y<$↑ z）=（x <$↑ y）<$↑ z，幂等性x <$↑x = x以及不等式x ≥ x <$↑ y，对于任何x，y，z ∈ L。整环L上的自由相容退化半格称为整环L上的相容Smyth幂整环。定义3.2 [16]设L是偏序集，F是L的非空子集。F中的两个元素x和y称为F中的线性连通，只要在↑ F中存在从x到y的一致路径，即无限多个x0，x1，. x n在↑ F中，使得x= x0<$x1<$. † x n= y，记为x <$Fy。称F是线性连通的，如果F的任意两个元素在F中线性连通。设L是一个连续区域，BC（L）={F<$finL：F/=<$且F是线性连通的}。设SC（L）是以↑BC（L）={↑F：F∈BC（L）}为基生成的族，即 设A ∈ SC（L），A = ↑ {↑ F：F ∈ BC（L）↑ FA}，则SC（L）是[16]中的连续dcpo-ε↑-半格.&定理3.3[16]设L是连续区域。L在SC（L）中的嵌入j由j（x）= ↑x（x ∈ L）给出。若P是dcpo-ε↑-半格，f：L−→P是Scott连续函数，则存在唯一的a-同态f使得f<$j = f。因此，SC（L）同构于L上相容的Smyth幂整环.定义3.4连续dcpo-ε ↑-半格D中的关系称为相容-乘法，如果对相容元素a，b ∈ D，xa，b蕴涵x a ε ↑ b。对于连续的L-整环L，如果满足下列条件，则L是分配的，且满足：对于任意相容点x，y，z，x<$↑（y<$z）=（x<$↑y）<$（x<$↑z）.定义3.5设L是偏序集。一个元素m ∈ L是子集A的一个极小上界（或简称mub），如果m是A的一个上界，且在A的所有上界的集合中是极小的。引理3.6设D是代数Lawson紧 L-整环，-乘法性质。 若D是分配的，且有和↑，则D是FS-↑-整环。Y. Yuan，H.Kou/Electronic Notes in Theoretical Computer Science 333（2017）153159否则，0↓z⎨（K）使得dm，则fK（↑d）=↑m：dMK证据设D={（x<$x）∈D→D：x x}，其中（x<$x）是一步函数，定义为（xx，z∈↑x，对于任意有限紧元素子集K ={x1，.，xn}<$K（D），其中n∈N，定义MG <$finmub（G）：对任意m ∈ MG，存在x ∈ <$xi ∈G↑xi使得mx.通过D的 紧 性 ， 存 在 有 限 集 MG <$mub{xi ： xi∈G} ， 使 得 mub{xi ： xi∈G} 满 足m∈MG↑m。设置Lc（K）={k↑xi∈G{xi}：kG<$K，<$xi∈G↑xi}，MLc（K）={m∈MG：GG<$Lc（K），<$xi∈G↑xi/=<$}，K=Lc（K）<$MLc（K），K1=K，K2=K1，.，Kn+1=Kn，F（K）=Kn.n∈N根据分配性质，集合F（K）是有限的。让我们定义映射fK：D→D如下：对于x∈D，f（x）=<$m，x∈↑m\↑（↑m<$F（K）），m∈F（K），否则，为0 ↓x。若G1=G2，m1，m2∈MG1且m1/=m2，则n↑m1\↑（↑m1<$F（K））<$↑m2\↑（↑m2F（K））=。否则，有x∈↑m1\↑（↑m1<$F（K））<$↑m2\↑（↑m2<$F（K））。但是m1m2.这与D是L-整环是矛盾的如果G1/=G2且mi∈MGi，其中i=1，2，则有↑m1\↑（↑m1<$F（K））<$↑m2\↑（↑m2<$F（K））=<$.否则，有x∈↑m1\↑（↑m1<$F（K））<$↑m2\↑（↑m2<$F（K））。则x∈↑（m1<$↓xm2），一个悖论。另一方面，假设m1∈MG1，m2∈MG2且G1/=G2。Ifa∈↑m1\↑（↑m1<$F（K））和b∈↑m2\↑（↑m2<$F（K）），fK（a）fK（b）. 我们必须有一个v e a/=b。否则，a∈↑（m1am2），但fK（a）=m1.这与fK的定义是矛盾的。若G1=G2，m1，m2∈MG1，m1/=m2，则a/=b，因为D是L-整环。那么fK就定义得很好了很任何d∈D，ifd=0↓d且d/∈↓m，对任意ym∈F（K），则f−1（↑d）=↑d; ifhe es∈F−1↑{↑K}f−1（↑d） =100。 所有的情形都表明f−1（↑d）是D的一个Scotto p en集。K是K K斯科特连续。很容易证明{f K：K <$K（D），|K|N}是逼近于id D的有向集. 对于任意x ∈ D，我们知道sup{f K（x）：K <$K（D），|K|n∈N}≤ x。如果x/≤sup{f K（x）：K<$K（D），|K| n {\displaystyleN}，则有ux但u/≤sup{fK （ x ） ： K<$K （ D ） ， |K| {\fn 方 正 黑 体 简 体\fs18\b1\bord1\shad1\3cH2F2F2F}.通过u x，存在某个紧元v使得u v x。一些M否则，160Y. Yuan，H.Kou/Electronic Notes in Theoretical Computer Science 333（2017）153由（v<$v）（x）=v和（v<$v）≤sup{fK：K<$Y. Yuan，H.Kou/Electronic Notes in Theoretical Computer Science 333（2017）1531611不C1不S1SeK（D），|K|{f∈N}，则u ≤ v ≤ sup{f K（x）：K <$K（D），|K|N}，一个矛盾。为了证明{f K：K <$K（D），|K|N}是D上的近似恒等式，证明这些函数也是<$↑-同态就足够了. 假设a和b是一致的，由c证明。设a↑b=x，令a∈↑m1\↑（↑m1<$F（ K ） ） ， b∈↑m2\↑（↑m2<$F（K））和x∈↑m0\↑（↑m0<$F（K）），其中mi∈MGi，i=0，1，2。 则fK （a）<$↑fK （b）存在。通过 m0x≤a和m0x≤b，如果G0= G1= G2，则m1= m0和m2= m0，然后m0= m1↑m2。否则，我们得到m0<$$><$am1a 和 m0<$$>am1∈F （ K ） ， 但 a∈↑m1\↑ （ ↑m1<$F （ K ） ） .则m0≤m1。类似地，m0≤m2。 因此，我们有m0≤m1↑m2。 另一方面，利用乘法性质，m1<$↑m2a<$↑b= x. 由f K的定义，我们得出 m0= m1<$↑m2。因此，fK （a<$↑b）=m0=m1<$↑m2=fK（a）<$↑fK（b）。Q定理3.7设D是Lawson紧L-整环，具有相容-乘法性.若D是分配的，且有和↑，则D是FS-↑-整环。证据 对于任何有限子集X ={x1，...，x n}D，Y ={y1，...，yn}D，yix i对于任何n∈N且I={1，.，n}，设置Lc（X）={λ↑i∈F{xi}：F∈Φ（I）=Φ（λX）}，U c（X）={<$↓x{xi：i∈ F}：F ∈ Φ（<$LC（X）），<$x∈ D，s.t.，{xi：i ∈ F}<$↓x}，X<$=Lc（X）<$Uc（X），X1=X1，X2=X1，...，Xn+1=Xn，F（X）=Xn，n∈N其中，Φ（I）={F∈I：<$i∈F↑xi <$}，Φk（I）={F∈Φ（I）：|F|=k}，MI = max {i∈I：<$F∈ Φ（I），s.t.，|= i }，|= i},设X=I，L（X）={i↓（i+k（2）），.， i↓（i+k（2）），.， i↓（i+k（e+1））↓... ↓（i+k（e+1））：1≤i≤n}，哪里k（2）=min{k：↑xi↑xi+k=/k（2）=max{k：↑xi<$↑xi+k162Y. Yuan，H.Kou/Electronic Notes in Theoretical Computer Science 333（2017）1530≤k≤n−i}，0≤k≤n−i}Y. Yuan，H.Kou/Electronic Notes in Theoretical Computer Science 333（2017）15316311S1Se我⎩S1SeS1Se我 i+k（e+1）i+k（e+1）k∈E且i↓（i+k（2））表示xi<↑xi+k（2）存在，且e=max{|E|：↑xi<$（↑xi+k）/=n，0 ≤k≤n−i}，k∈E{（i+k（e+1）），.，（i+k（e+1））}=max{E：↑xi（↑xi+k）=/，0≤k≤n−i}，i↓（i+k（e+1））↓... ↓（i+k（e+1））表示： x}存在。From我们知道，|C（X）|≤（Lc（X））！.则Lc（X）是有限的。同样，对于某个Xk，集合Xk是有限的。设M E为一个有限集合E，定义M E∈finmub{y i：i∈E}：对任意m∈M E，有x∈Ei∈E↑xi使得m x.通过D的紧性，存在一个有限集ME∈mub{yi：i∈E}，使得mub{xi：i∈E} 满 足 c hm∈ME↑m。设ma=<$^iF{yi}，ifa=<$^iF{xi}，其中F∈Φ（<$Xk1）. 设ma=<$↓x{yi：i∈F}，如果s∈omex∈D，则{xi：i∈F}<$↓x，对于F∈Φ（<$Xa=<$↓x{xi：i∈F}。）和根据D的分配性质和紧性，集合{ma：a∈F（X）}是有限的。让我们定义一个映射fI：D→D如下：对于x∈D，f（x）=<$ma，x∈（↑ma <$↑a）\↑（↑a<$F（X）），a∈F（X），0 ↓x，否则。则{fI：I<$finN}是D上的一个近似恒等式。Q在[16]中，我们证明了Lawson紧连续整环上的相容Smyth幂整环是Lawson紧连续L-整环。定理3.8[16]若L是Lawson紧连续整环，则一致Smyth幂整环SC（L）是满足相容-乘法性质和分配性质的Lawson紧连续L，天啊。Q根据定理3.7和定理3.8，我们得到以下结论：定理3.9若L是Lawson紧连续整环，则L上的相容Smyth幂整环SC（L）是FS-ε↑-整环.引用[1] Abramsky，S.，和Jung，A.，Domain Theory，In Handbook of Logic in Computer Science，1-168，Oxford University Press，1994.[2] 阿马迪奥河Curien，P.-L.，Domain and Lambda Calculi，Cambridge University Press，1998.[3] Gierz，G.，霍夫曼，K.H.，Keimel，K.，例如，连续格与域，剑桥大学出版社，2003年。[4] Heckmann，R.，强紧集上幂整环的构造。计算机科学讲义，598：272-293，1991。K2164Y. Yuan，H.Kou/Electronic Notes in Theoretical Computer Science 333（2017）153∧[5] Heckmann，R.，用幂域刻画FS-域。理论计算机科学，264：195-203，2001。[6] Heckmann，R.，权力领域的建设。计算机程序设计科学，17：77-117，1990。[7] Heckmann，R.，幂域和二阶谓词。理论计算机科学，111：59-88，1993。[8] Huth，M.，Jung，A.，和Keimel，K.，线性类型和近似。计算机科学中的数学结构，10：719-745，2000。[9] Liang，J.H.，和Kou，H.，凸幂域与Vietoris空间。计算机和数学与应用，47：541-548，2004。[10] 孟，H.，和Kou，H.，关于半格同态的函数空间与FS -整环。中国数学年鉴，32：107-114，2011。[11] Mislove，M.W.，在史密斯的能量领域。计算机科学讲义，298：161-172，1988。[12] Mislove，M.W.，拓扑学、域理论与理论计算机科学。拓扑学及其应用，89：3-59，1998.[13] Plotkin，G. D.，一个领域结构。SIAM Journal on Computing，5：452-487，1976。[14] Smyth，M.B.， 能量领域Journal of Computer and Systems Sciences，16：23-36，1978.[15] Smyth，M.B.，电源域和谓词变压器：拓扑视图。计算机科学讲义，154：662-676，1983。[16] 袁，Y.Y.和Kou，H.，一致的史密斯力场。拓扑及其应用，173：264-275，2014。