Domain的逻辑语构与逻辑语义表示

摘要

本文讨论了在逻辑框架下刻画Domain范畴所必需的方法与技巧.Domain以及它们之间的Scott-连续映射构成了计算机程序语言的指称语义的数学理论基础.一般地，Domain范畴的一个逻辑表示就是把Domain中的元素看作是逻辑演算中的理论或者是逻辑演算的Linbenbaum代数上的素滤子，并把Scott-连续映射理解为逻辑演算间的推理引擎.这种方法为Domain理论提供了一种简单而具有启发意义的直观表示，从而使Domain理论中的概念和性质变得容易理解，进而可以激发我们去寻找Domain理论中更多的概念和构造.　　为刻画有界完备domain和Scott-连续映射组成的范畴，本文构建了一种名为合取序列演算的逻辑系统，它是经典Gentzen型命题逻辑关于合取连接词的一个片段.证明了任一没有最大元的有界完备domainD都序同构于D所诱导的合取序列演算的所有逻辑点在集合包含序下构成的偏序集.随后通过在合取序列演算间定义有效序列我们得到了一种多语言序列演算，这种多语言序列演算间的推理称为是一个合取序列关系，它是和有界完备domain间的Scott-连续映射一一对应的.进一步，构建了一个以一致合取序列演算为对象以合取序列关系为态射的范畴，并证明了它是与有界完备domain带有Scott-连续映射构成的范畴等价的.这样就把有界完备domain范畴纳入到了合取序列演算的语构框架下，从而得到了它的一种具体的逻辑语构表示.　　连续L-domain中的任一主理想是一种特殊的有界完备domain.注意到这一性质，我们为连续L-domain定义了一个名为局部合取序列演算的逻辑系统，它在局部位置上满足合取序列演算的推理规则.我们证明了这种局部合取序列演算的逻辑点构成了一个连续L-domain，并且所有的连续L-domain都可由这种方式在同构意义下生成.这一结果从逻辑的角度上再现了连续L-domain所具有的局部性质.随后证明了局部合取序列演算间的合取序列关系与连续L-domain间的Scott-连续映射是可以互相生成的，从而把局部合取序列演算与连续L-domain间的关系推广成为一个范畴等价.同时，代数L-domain范畴作为连续L-domain范畴的一个子范畴也是等价于局部合取序列演算范畴的一个子范畴的.　　对于代数L-domain范畴，本文利用陈仪香等人提出的析取命题逻辑给出了它的另一种纯语构形式的逻辑刻画.证明了析取命题逻辑的一类特殊的理论恰好可以生成所有的代数L-domain.为进一步发展析取命题逻辑的表示理论，我们定义了一个以析取命题逻辑为对象的范畴，并证明了这一范畴与代数L-domain和Scott-连续映射构成的范畴是等价的.特别地，基于一类特殊的析取命题逻辑给出了Scott-domain的一种纯语构形式的逻辑刻画，从而可以从逻辑的角度上揭示代数L-domain与Scott-domain间的联系与区别.　　最后，我们把析取命题逻辑中任意维的析取连接词替换为一种二元析取连接词后提出了N-序列演算的概念，并证明了它关于FD-格是逻辑完备的.在N-序列演算的框架下给出了Lawson紧的代数L-domain的两种不同的逻辑表示方法.第一种表示是逻辑语义形式的，其研究对象为FD-格,并以FD-格的素滤子为桥梁建立了FD-格与Lawson紧的代数L-domain间的可互相生成关系.这一表示发展了陈仪香等人的代数L-domain的逻辑表示方法，但是在范畴的态射构造上与他们的方法又有着本质的区别.第二种表示是前面Domain的逻辑语构表示工作的继续，因而没有借用逻辑代数的帮助而是直接采用了N-序列演算的语构作为研究对象.这时以N-序列演算中的逻辑点为工具确定了N-序列演算和析取序列关系构成的范畴与Lawson紧的代数L-domain带有Scott-连续映射构成的范畴间的等价关系.这一部分的结果表明可以把某些Domain的逻辑语义表示和逻辑语构表示纳入到同一个逻辑框架下.

目录

第1章 绪论

1.1 研究背景

1.2 创新点和内容安排

1.3 预备知识

1.3.1 集合与范畴

1.3.2 序与Domain理论

第2章 有界完备domain的语构表示

2.1 合取序列演算

2.2 有界完备domain的表示定理

2.3 有界完备domain范畴的表示

第3章 连续L-domain的语构表示

3.1 局部合取序列演算与连续L-domain

3.2 局部合取序列演算范畴

第4章 代数L-domain的析取命题逻辑的语构表示

4.1 析取命题演算

4.2 代数L-domain的表示定理

4.2.1 析取命题演算的逻辑点

4.2.2 表示定理

4.2.3 若干特殊的析取命题演算类以及Scott-domain的逻辑表示

4.3 代数L-domain范畴的表示

4.3.1 可表达析取命题演算间的态射

4.3.2 范畴等价

第5章 Lawson紧的代数L-domain的表示

5.1 N-序列演算及其逻辑完备性

5.1.1 N-序列演算的语构

5.1.2 N-序列演算的逻辑语义

5.2 逻辑语义表示

5.2.1 FD-格的素滤子与Lawson紧的代数L-domain的关系

5.2.2 FD-格范畴

5.3 逻辑语构表示

5.3.1 N-序列演算的逻辑点

5.3.2 N-序列演算的语构范畴

结论

参考文献

致谢

附录A 范畴符号检索

附录B 攻读学位期间所完成的学术论文目录及参与的科研项目