余代数上的松弛不变量

《余代数上的松弛不变量》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、首都师范大学位论文原创性声明本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究工作所取得的成果．除文中已经注明引用的内容外，本论文不含任何其他个人或集体已经发表或撰写过的作品成果．对本文的研究做出重要贡献的个人和集体，均已在文中以明确方式标明．本人完全意识到本卢明的法律结果山本人承担．学位论文作者签名：办1日期：蝴年仁月7同首都师范大学位论文授权使用声明本人完全了解首都师范大学有关保留，使用学位论文的规定，学校有权保留学位论文并向国家主管部门或其指定机构送交沦文的电子版和纸质版．有权将学位论文用于非赢利目的的少量复制并允许论文进入学校图书馆被查阅．有权将学位论文的内

2、容编入有关数据库进行检索．有权将学位论文的标题和摘要汇编出版．保密的学位论文在解密后适用本规定．学位论文作者签名：砌味1日期：瀹眸明夕日余代数中的松弛不变量§o．前言一直以来，代数理论在计算机安全、程序语义以及处理有限数据类型等领域有着广泛的应用，而作为代数的对偶概念一余代数，则直到上世纪后半期才为越来越多的计算机学者所关注．在计算机科学中，代数从构造的角度研究数据类型，而余代数则从观察的角度研究系统及其性质．随着研究的深入，理论计算机科学家等逐渐发现余代数对研究基于状态的系统，如自动机、进程、对象、软件构造等有独特的优越性．利用余代数的理论以及方法，可以对系统的行为等价，不确定性

3、等从数学上进行探讨，为这些系统建立形式理论基础，并对其性质进行描述与验证．近几十年，余代数在计算机科学，特别是理论计算机科学中，发挥着越来越重要的作用，应用越来越广泛，如：余代数方法在自动机理论中的应用【2】，在并发模型及其语义研究中的应用[3，4】，在对象语言及其语义研究中的应用等等其他的应用【5，6，7，8】，更多的关于余代数的介绍可以参看[9】．余代数主要是给我们提供状态的一些信息，它允许我们观察系统的某些状态，也允许我们在特定情况下修改状态，或者移动到下一个状态，但是我们无法构造新的状态．状态的行为就是我们直接或者间接观察到的东西．在这种情况下，可能会发生这样的情况：两个状

4、态有相同的行为，但是由于我们观察有限，实际上这两状态并不完全相同，此时我们称这样的两个状态是互模拟．由于互模拟的这种性质，互模拟在模态逻辑、domain理论、范畴论等领域有很广泛的应用．而不变量本身是状态空间上的谓词，表示状态空间上关于某种性质封闭，即不变量一旦成立，则无论系统如何迁移都会成立．不变量在系统的建模中起到很重要的作用，因为不变量经常表示某种隐性的假设，如除法中除数永远不能为零，某人的岁数永远不能为负等等．因此不变量是”安全的性质”，即”坏的”情况永远不会发生．不变量的这种性质使得其在很多方面有很重要的应．3．余代数中的松弛不变量用【5，6，10，11】．互模拟和不变量

5、是余代数研究中较为重要的两个概念，关于互模拟和不变量的详细定义以及相关结论参看[11】．本文主要是基于Bart．Jacobs和Jesse．Hughcs在文献[1】中研究互模拟的基本框架研究不变量的相关性质。在本文中我们只考虑集合范畴上的情形，其他范畴上的情形类似，且本文所考虑的函子也都是Kripkc多项式函子．在此前提下，研究松弛不变量以及双向松弛不变量等的相关性质，并比较了松弛不变量与模拟之间的关系，并类似于文献⋯1的思路，研究了不变量与双向松弛不变量之间的关系，从而得到了使得它们等价的充分条件．本文分为四章，第一章是本文的预备知识，主要回顾范畴论、余代数和序的相关概念，介绍了文

6、献【1】所引入的的集合范畴上带有偏序关系的函子，及与该函子相关的谓词提升等概念．第二章引进了松弛不变量的概念，研究了松弛不变量与模拟之间的关系，并说明了松弛不变量的作用．此外我们证明了松弛不变量的一些基本性质，例如松弛不变量关于并封闭(本文中称之为最大松弛不变量)．在第三章，我们研究了松弛不变量与函子不动点之间的关系，证明了最大松弛不变量是关于一个特殊函子余代数的终结余代数。最后，第四章研究了松弛不变量与不变量之间的关系，给出了两者相同的充分条件。·4．余代数中的松弛不变量§1．预备知识本章简要介绍在阅读本文时所需要的预备知识，包括范畴论、序以及余代数中的某些基本概念和结论．除个别

7、概念和定理的叙述与通常情形略有差别外，本章的绝大多数内容都是标准的．范畴论、拟序集和单调映射的内容请参看文献[13，14】，代数和余代数的内容请参看【11】．1．1范畴范畴够由一个对象类D6(够)和一个态射类mor(够)构成，其中D6(够)中的元素称为够的对象，通常用A，B，．．．表示．对任意对象A，B∈D6够)，有子族够(A，B)∈mor(够)，其中够(A，B)称为从A到B的态射，记为

8、：A_B。对VA，B，C∈D6(够)，有一种运算称为态射的合成：够(A，B)XV