拟连续domain的相容幂构造

Domain theory is one of the important interaction research fields of mathematics and computer science. Mutual transformations and infiltration of order, topology and logic are the basic features of this theory. Powerdomain constructions proposed in domain theory provide mathematical models for semantics of non-deterministic programming languages. One fundamental problem in denotational semantics is whether there exists a powerdomain construction for a given category of nice enough domains. In this project, we are mainly concerned with some traditional powerdomain constructions and newly defined consistent Smyth (resp., consistent Hoare, consistent Plotkin) powerdomain constructions over quasicontinuous domains. Based on traditional powerdomain constructions over quasicontinuous domains, we will investigate the closedness of the classes of a quasicontinuous domain by taking these consistent powerdomain constructions. The investigation of this project will enrich the theory on powerdomain constructions over quasicontinuous domains.

Domain理论是数学与计算机科学交叉的一个重要研究领域。序，拓扑与逻辑的相互转化、相互渗透是这一理论的基本特征。幂 domain 的提出旨在为不确定性计算提供数学模型，一个 domain 范畴是否关于某种幂 domain 构造封闭将决定这个指称语义学模型能否支撑不确定性计算。拟连续 domain 是 domain 的重要推广类型，本课题主要围绕拟连续 domain 的多种幂构展开研究。一方面，进一步考察拟连续 domain 的传统幂构造；另一方面，在传统幂构造的基础上，结合新提出的多种相容幂构造：相容Hoare幂、相容Smyth幂、相容Plotkin 幂，研究拟连续 domain 在相容幂构造下的封闭性。本项目的研究将丰富拟连续 domain 的幂构造。

Domain理论是数学与计算机科学交叉的一个重要研究领域。幂domain的提出旨在为不确定性计算提供数学模型，一个domain范畴是否关于某种幂domain构造封闭将决定这个指称语义学模型能否支撑不确定性计算。拟连续domain是domain的重要推广类型，在本项目中我们主要引入并研究了拟连续domain的相容Smyth幂、相容Hoare幂构造的封闭性，主要结果有：1）相容Smyth幂：a）拓扑空间X是sober的当且仅当X的相容Smyth幂RQ_C(X)是sober的；若拓扑空间X是局部紧连通的、良滤的且coherent，则RQ_C(X)也是coherent；若拓扑空间X是有限上生成的、局部紧的、良滤的和coherent，则RQ_C(X)是Lawson紧的L-domain；上述结果推广了拓扑空间上的相容Smyth幂。b）每一个dcpo（定向完备偏序集）赋予Scott拓扑都是局部连通的，且如果dcpo L是有限上生成的、局部紧的、良滤的和coherent，则其相容Smyth幂RQ_C(L)是一个Lawson 紧的L-domain；每一个拟连续domain (相应地，Lawson 紧拟连续domain，拟代数domain)的相容Smyth幂domain是连续dcpo-Λ↑（相容交）-半格（相应地，Lawson紧L-domain，代数dcpo-Λ↑-半格），即表明拟连续domain的相容Smyth幂构造封闭；拟连续domain的相容Smyth幂存在且是一个自由代数；从而成功地将domain的相容Smyth幂推广至拟连续domain情形；2）相容Hoare幂：通过构造相关反例，说明若利用拟连续domain L上的全体非空相对相容Scott 闭集，引入拟连续domain的相容Hoare幂domain RΓ_C(L)，则RΓ_C(L)不必是一个dcpo。