（计算机软件与理论专业论文）共代数逻辑及其应用的初步研究.pdf

论文题目： 专业： 硕士生： 指导教师： 共代数逻辑及其应用的初步研究 计算机软件与理论 杨应宝 周晓聪副教授 摘要 共代数是代数的对偶概念，基于观察的角度考察集合及其上操作。计算机科 学中很多系统都可以归结为共代数，如自动机、抽象数据类型、面向对象设计语 言等。目前，共代数方法已经被证明是研究状态系统的行为性质的可行途径。 模态逻辑是经典逻辑的扩充。由于添加了模态词，使得模态逻辑适合于描述 动态系统的行为。模态逻辑的一些分支，如时态逻辑、认知逻辑等，已经广泛应 用予模型检测、人工智能等计算机科学领域。 共代数逻辑是适合于描述共代数系统的逻辑。把模态逻辑作为共代数逻辑是 共代数研究领域中一个新的研究方向。模态逻辑与共代数都与状态系统紧密相 连，可以利用共代数对动态系统建立模型，然后利用模态逻辑描述共代数模型的 行为性质，因此将共代数和模态逻辑融合在一起是自然的。而如何从共代数生成 合适的模态逻辑则是共代数逻辑研究的重点。l m o s s ，b j a c o b s ，a k u r z 等人都在 这方面作出了很大的贡献。 本文首先探讨了共代数与系统的关系，以及共代数与模态逻辑的内在联系， 分析了几种共代数逻辑的特点，在此基础上研究了有限k r i p k e 多项式函予上的模 态逻辑，并证明该模态逻辑保持共代数的互模拟特性，具有充分性和可表达性。 文章最后利用共代数逻辑方面的研究，给出内存管理系统的一个共代数规范，说 明如何将共代数逻辑应用于计算机领域。 关键词：共代数、模态逻辑、有限k r i p k e 多项式函子、可表达性 t i t l e m a j o r ： n a l e ： s u p e r v i s o r ： ap r e l i m i n a r yr e s e a r c ho nc o a l g e b r a i c l o g i ca n di t sa p p l i c a t i o n c o m p u t e rs o f t w a r ea n dt h e o r y y a n gy i n g b a o z h o ux i a o c o n g ，a s s o c i a t ep r o f e s s o r a b s t r a c t i i i c o a l g e b r a i st h ed u a lc o n c e p to fa l g e b r a ，w h i c hd e a l sw i t ht h es y s t e m sf r o m a no b s e r v a t i o n a lv i e w i nc o m p u t e rs c i e n c e ，l o t so fs t a t e - b a s e ds y s t e m sc a nb em o d - e l l e db yc o a l g e b r a s ，s u c h8 sa u t o m a t o n ，a b s t r a c td a t at y p ea n do b j e c t - o r i e n t e dp r o - g r a m c o a l g e b r ah a sp r o v e dt ob ea na p p r o p r i a t ew a yt oe x p l o r et h eb e h a v i o u r p r o p e r t i e so ft h es t a t e - b a s e ds y s t e m s m o d a ll o g i ci st h ee x t e n s i o no fc l a s s i cl o g i c w i t ht h em o d a lo p e r a t o r s ，m o d a l l o g i ci sa p p r o p r i a t et od e s c r i b et h es t a t e - b a s e ds y s t e m s s o m eb r a n c h e so fm o d m l o g i c ，s u c ha st e m p o r a ll o g i ca n dd y n a m i cl o g i c ，h a v eb e e nw i d e l yu s e di nm o d e l c h e c k i n g ，a r t i f i c i a li n t e l l i g e n c ee t c t h e 蛔c o fc o a l g e b r a si st h el o g i ct h a ti sa p p r o p r i a t et od e s i r et h es y s t e m s w h i c ha r em o d e l l e db yc o a l g e b r a s b e c a u s em o d a ll o g i ca n dc o a l g e b r a sb o t hc o n n e c t w i t hs t a t e - b a s e ds y s t e m sc l o s e l y , m o d a ll o g i cc a nb eu s e da st h el o g i co fe o a l g e b r a c o a l g e b r a sf a i lb ea s c i it om o d c lt h es t a t e - b a s ( 酒s y s t e m sa tf i r s t ，a n dt h e n ，t a o d a l l o g i cc 8 nb eu s e dt os p e c i f yt h eb e h a v i o u ro fc o a l g e b r a t h eq u e s t i o ni sh o wt o g e n e r a t ea na p p r o p r i a t em o d a ll o g i cf r o mc o a l g e b r a s l m o s s ，b j a c o b s ，a k u r zh a v e m a k ec o n t r i b u t i o ni nt h er e s e a r c ho ft h i sq u e s t i o n t h i st h e s i sd i s c u s s e st h er e l a t i o n s h i pb e t w e e nc o a l g e b r aa n ds y s t e m ，a n dt h e i n n e rr e l a t i o n s h i pb e t w e e ne o a l g e b r aa n dm o d a ll o g i c a n dt h e n8 0 m ea p p r o a c h e st o g e n e r a t em o d a ll o g i cf r o mc o a l g e b r a sw i l lb ei n t r o d u c e d b a s e do nt h e s ew o r k s ，w e s t u d yt h em o d a ll o g i co fe o a l g e b r a so ft h ef i n i t ek r i p k ep o l y n o m i a lf u n c t o r ，a n d p r o v et h i sm o d a ll o g i cp r e s e r v et h ec o a l g e b r a i cb i s i m u l a t i o nw h i c hm e a n 8t h e i v m o d a ll o g i ci sa d e q u a t ea n de x p r e s s i v e a tt h ee n do ft h i st h e s i s ac l s es t u d yi s u s e dt os h o wh o wt ou s ec o a l g e b r a sa n dm o d a ll o g i c si nt h ec o m p l i c a t e ds y s t e m s k e yw o r d s ：c o a l g e b r a 、m o d a ll o g i c 、f i n i t ek r i p k ep o l y n o m i a lf u n c t o r 、e x p r e s s i v e 第一章前言弟一早月ui 本章首先介绍一些背景知识，包括共代数理论及其应用、模态逻辑基本理论以及两 者关系的研究，随后给出本文研究的主要内容、方法与意义，最后是论文的结构安捧。 1 1 研究背景 作为对偶的两个概念，代数方法( a l g e b r a i cm e t h o d s ) 主要从构造的角度研究集合及 其上的操作，目前已经在抽象数据类型、计算机语言的形式语义等领域得到了广泛的应 用。而从观察角度上考察集合及其上操作的共代数方法( c o a l g e b r a i cm e t h o d s ) 则直到二 十世纪九十年代中后期才引起计算机科学工作者的广泛关注与研究，目前已经逐步应用 在对自动机、进程、对象等基于状态的系统的研究之中 模态逻辑是经典逻辑的扩张。由于添加了模态词，使得模态逻辑适合于描述动态系 统的行为。模态逻辑的一些分支，如时态逻辑、认知逻辑等，已经广泛应用于模型检测、 人工智能等计算机科学领域。 模态逻辑与共代数同样适合于描述动态系统，我们可以利用共代数对动态 系统建立模型，利用模态逻辑规范共代数模型的行为，因此将共代数和模态逻 辑融合在一起是自然的而如何从共代数生成合适的模态逻辑则是共代数研 究的重点。l m o s s ，b j a c o b s ，a k u r z ，d p a t t i n s o n 等人都在这方面作出了很大的贡 献1 1 ，2 ，3 ，4 t5 ，6 7 。 l 1 1共代数理论及其应用 计算机科学中对共代数的研究可追溯至l j l 9 8 8 年，p a c z e l 等人首次使用共代数方法给 出了进程代数c c s ( c a l c u h s o f c o m m u n i c a t i n g s y s t e m s ) 的终结语义( f i n a ls e m a n t i c s ) i s 二十世纪九十年代以来，共代数已经在计算机领域得到了广泛的研究和应用，越来 越引起人们的关注。j a d d m e k ，h p g u m m ，j p o w e r 对共代数的基础理论傲了深入研 究，考察了终结共代数的存在及性质，集合范畴上的共代数结构、代数簇( v a r i e t y ) 与共 1 2 第一章前言 代数簇( c o v a r i e t y ) 1 9 l 、代数共代数与i m o n a d ( o m o n a d 的关系等； j r u t t e n 将共代数方法应用于自动机理论和并发程序语义等的研究1 1 0 ，i i , 2 j ，并结 合偏序集、非良基集( n o n - w e l l - f c 咖d e ds e t s ) 和度量空间( m e t r i cs p a c e s ) ，探讨了终结语 义的数学基础，最终奠定了泛共代数的基础。 目前国内从事这方面研究的还比较少，但也逐渐引起了一些学者的注意与研究，如 北京大学的张乃孝教授、上海交通大学的孙永强教授以及中山大学的周晓聪副教授领 导的研究小组等陋1 6 1 7 ，1 8 l 。 1 1 2模态逻辑理论及其应用 模态逻辑作为逻辑的一个分支，早在 ：2 0 0 0 - 年前就出现了。亚里士多德在研究命题的 过程中，提出了模态命题的概念，认为模态命题研究的是命题的必然性与偶然性。另外， 麦加拉斯多葛学派也对模态逻辑做了深入的研究。麦加拉学派的菲洛、迪奥多鲁等对 模态算子做出了精确的定义。 公元9 至1 5 世纪，阿拉伯和欧洲经院派逻辑学家继承和发展了古希腊模态逻辑思想。 阿拉伯的逻辑学家把时间变项加入到模态逻辑中，因而产生了时态逻辑。经院派对模态 命题的推导，模态命题的结构进行了深入的研究，提出了命题模态与事物模态的区别， 推动了传统模态逻辑的发展。 传统模态逻辑由于没有形式化。只能处理简单的命题。随着数理逻辑的出现，模 态逻辑的发展进入一个新的阶段。现代模态逻辑是建立在数理逻辑的基础上。莱布尼 兹开创了数理逻辑，提出了思维可以计算的思想，由此开始的符号化、公理化被应用 于模态逻辑。另外，莱布尼兹提出的可能世界理论成为解释模态逻辑的重要工具。最 先开始这方面研究的是1 9 世纪末的h m a c c o l l , ，在他的影响下，美国哲学家、逻辑学 家c i l e w i s 于1 9 1 4 年构造了一个模态命题演算系统。4 0 年代末，卡尔纳普开始从语义方 面研究模态逻辑。5 0 年代末6 0 年代初，s k a n g e r 、s a k r i p k e 等人发展了卡尔纳普的理 论，提出了比较完整的模态逻辑的模型理论。6 0 年代以后模态逻辑有很大发展。出现了 许多新的系统，特别出现了许多非标准的模态逻辑系统。如认知逻辑( e p i s t e m i cl o g i c 、j l 、 道义逻辑( d e o n t i c1 0 9 i c ) 、时态逻辑( t e i n p o r a l1 0 舀c ) 、动态逻辑( d y n a m i cl o 西c ) 等。 模态逻辑在计算机领域有着广泛的应用，时态逻辑被广泛应用于模型检测、程序验 证等；认知逻辑用于人工智能、知识推理等。 1 1 3 模态逻辑与共代数的结合 共代数适合于对状态系统( s t a t eb a s e ( 1s y s t e i n s ) 进行建模已经得到了广泛的认同。 但是共代数的逻辑是什么并没有定论，人们开始研究怎样的逻辑适合于描述共代数的模 1 2 本文的主要研究内容 3 型。 l m o $ 提出可以通过模态逻辑描述共代数的行为。1 9 9 9 年，l m o s s 在论文中提出一 种方法，可以从函子t 生成共代数的逻辑，称为共代数逻辑( c o a l g e b r a i cl o g i c ) 。共代数 逻辑的公式通过函子t 递归定义而得。l m o s s 的方法对函子限制很小，适用范围很广， 但是过于抽象，缺乏模态词的具体定义，使得难以应用于实际。 由于l m o s s 的共代数逻辑过于抽象，a k u r z 针对多项式函子提出了具体的模态 逻辑，原子命题和模态词通过多项式函子的各分量定义，直观明了，但是缺乏普遍 性。d p a t t i n s o n 结合两者的优点，提出通过谓词提升( p r e d i c a t el i f t i i l g ) 定义函子共代数 的模态逻辑，既有普遍性，又有实用性。 此外，a k u r z 提出了共代数和模态逻辑的关系可以通过斯通对偶( s t o n ed u a l i t y ) 刻 画1 1 9 2 0 , 2 1 ，铆c c i m t e a 提出利用模块化方法定义复杂函子的模态逻辑【嚣，2 4 ，2 5 t 删。 r g o l d b l a t t ，a c o r r a d i n i 等人则提出利用等式逻辑描述共代数的行为性质，冽。 1 2 本文的主要研究内容 把模态逻辑作为共代数逻辑是计算机科学中共代数方法研究的重要课题之一，具有 十分重要的理论意义和应用价值。l m o s s ，a k u r z 等人的工作奠定了其理论基础，证明 了共代数与模态逻辑的融合是可行的。 同时，我们也看到，虽然l m o s s 、a k u r z 等人对基于共代数的模态逻辑生成提出了 不同的方法，并傲了理论上的探讨。但是由于他们的工作主要注重理论的探讨，并没有 深入讨论其在计算机科学中的具体应用。 l m o 和d p a t t i n s o n 的理论过于抽象，模态逻辑需要哪些模态词和原子公式都需 要自行判断。a k u r z 主要致力于多项式函子逻辑的理论研究，并把其应用于简单的数据 类型中，但并没有深入探讨其在复杂模型中的应用，而且，计算机科学领域中的很多非 确定性系统并不能通过多项式函子来抽象，因此，不熊利用a k u r z 的理论研究非确定性 系统的模态逻辑 本文以l m o s s 、a k u r z 、b j a c o b s 等人的工作为基础，研究有限k f i p k e 多项式函子 上的模态逻辑，并通过实例研究探讨模态逻辑在复杂系统中的应用。论文的主要研究内 容包括： 1 共代数方法研究：研究共代数方法在计算机领域中应用的可行性和必要性，探讨 共代数与状态系统的关系，其中包括互模拟与行为等价的关系，终结共代数与共 归纳原理的关系，变迁系统与共代数的关系等。 4第一章前言 2 共代数与模态逻辑关系的研究：探讨共代数与模态逻辑的内在关系，包括k r i p k e 语 义模型与共代数的关系，模态逻辑与等式逻辑的关系，代数与共代数的关系等。 3 共代数逻辑的研究：分析了几种共代数逻辑的特点。在此基础上研究有限k r i p k e 多 项式函子上的模态逻辑，并证明了该模态逻辑的科学性，即模态逻辑保持共代数 的互模拟特性。 4 共代数逻辑在计算机领域应用的研究：利用在共代数辑方面的研究，给出一个简 单的内存管理系统的共代数规范，说明如何将模态逻辑与共代数应用于计算机领 域。 1 3 研究意义 j r u t t e n ，l m o s s ，a k u r z ，bj a c o b s 等人的工作表明，利用共代数与模态逻辑研究 状态系统的行为与特性，具有十分重要的意义： 1 共代数方法是计算机科学中理论研究的一个热门方向，它为研究状态系统行为提 供了一致的数学理论基础。利用共代数方法研究状态系统以及抽象数据类型等， 可以提供一种新的研究思路，与传统的代数研究方法互补。 2 模态逻辑，特别是时态逻辑，已经在计算机科学领域得到了广泛应用。把模态逻辑 与共代数结合起来，共同研究状态系统的行为，可以更好地发挥两者的优势。 3 计算机领域中很多非确定性系统都可以归结为有限k r i p k e 多项式函子上的共代数 研究k r i p k e ! 多项式函子上的模态逻辑，为研究非确定性系统提供了理论工具。 1 4 论文的总体结构 本文共分为六章，各章的主要内容为： 第一章引言：给出本文的研究背景、研究内容、研究意义及论文的总体结构。 第二章范畴理论：简单介绍本文所涉及的各种范畴概念。 第三章共代数：介绍共代数的相关知识，包括共代数与系统的关系，共代数的定 义，互模拟与行为等价，终结共代数与共归纳原理。 第四章模态逻辑：主要介绍模态逻辑的基本知识，包括模态逻辑的历史，模态逻 辑的语法构成与语义解析，多模态逻辑，模态逻辑与共代数的关系等。 1 4 论文的总体结构5 第五章模态逻辑与共代数：为本文的核心部分，分别介绍了三种共代数逻辑的特 点，并比较了三种方法的优缺点。然后研究了有限k r i p k e 多项式函子上的模态逻辑生成 的定义与应用，并证明其正确性。 第六章实例研究：把模态逻辑与共代数应用于内存管理系统，并利用模态逻辑证 明该系统的一些特性。通过这个例子说明如何把模态逻辑与共代数应用于复杂系统。 第二章范畴理论 范畴理论( c a t e g o r yt h e r w ) 是& - - 世纪4 0 年代中后期，由s e i l e n b e r g 和s m a c l a n e 等 为研究同调代数而创立的一个抽象代数分支【凹l ，它以范畴、函子、自然变换等为基本 概念统一地研究某些数学结构( 如群、环、代数，共代数、拓扑空间、域等) 及其性 质【”，3 1 , 3 2 , 1 7 i 。 范畴理论可以说是一种语言，一种描述数学结构的抽象语言。以范畴理论为工具， 可以将某些数学结构的性质加以泛化而推广到其他数学结构，也可以将某些数学性质 具体化从而丰富到某些数学结构以推广该数学结构的应用范围。进一步，通过范畴理论 中的通用概念，可以将许多不同数学分支联系在一起结合起来进行研究。作为一门抽 象的数学工具性的理论，范畴理论已经广泛应用在各个数学分支，如同调代数。代数几 何。代数拓扑以及共代数理论等。随着理论计算机科学的发展，特别是域论理论，直觉 理论、类型理论等的深入研究，范畴理论在计算机科学领域的应用也日益广泛。 范畴由对象及对象间满足一定性质的射组成，对象和射的基本构造可以通过积、共 积、均等射、共均等射、回拉、外推等来完成，不同的范畴可以用函子相联系，函子与函 子间的映射可以通过自然交换来完成，一个函子还可能存在着对应的伴随函子。 范畴论的研究成果对许多数学和计算机科学中的分支部产生了深远的影响，本文涉 及到的代数与共代数，都可以从范畴论的角度得到清楚的解释。代数与共代数都定义在 某个函子上，任何代数以及它们之间的同态都构成了一个范畴，初始代数就是该范畴的 初始对象，任何共代数以及它们之间的同态也构成了一个范畴，终结共代数是该范畴的 终结对象。此外，代数与共代数之间的对偶性可以根据范畴论得出，共代数的许多性质 可以从代数对偶得到。 范畴理论是本文的基本要素，本章将简要介绍范畴理论的基础知识。 6 2 i 1 对象s 射 2 1 对象与射 7 2 1 1 范畴的定义 对象与射是范畴的基本元素，下面首先给出范畴的定义： 定义2 1 1 范畴( c a t e g o r y ) c 是一个数学系统，包括两类元素、一些操作和这些操作 所满足的公理。两类元素是： 1 对象( o b j e c t ) ：范畴c 的对象通常用a 口，表示； 2 射( m o r p h i s m ) ：范畴c 的射通常用，g ，表示。 范畴上的操作包括： 1 每个射，有两个操作：d o r a 和c o d ，d d m ( ，) 是范畴c 的对象，称为，的域( d o m a i n ) ，c o d ( f ) 也是范畴c 的对象，称为f 的共域( e o d o m a i n ) 。通常用，：a b 表示射，这时j 4 就是，的 城，而b 是它的共城； 2 每个对象 有一个射i d a ： 一a ，称为对象a 的恒等射( i d e n t i t ym o r p h i s m ) ； 3 对于每个射r 和g ，如果。以( r ) = 如m ( g ) ，则它们有复 ( c o m p o s i t i o n ) i 5 为g0 f ， 有时也省略中间的o 直接写成g ，。进一步，d w n ( g f ) = 耐d on ( f ) ，c o l d ( g f ) = “，c o d ( g ) 。 射的复合通常记为：设f ：a b ，g ：口一e ，则：g f ：a c 。 这些操作必须满足以下公理： 1 恒等射是复合操作的恒等元，即对任一的f ：a b ，有i d bo ，= f = f 0 如； 2 复合操作是可结合的，即对任意的f ： 一b ，g ：b c ，h ：e d ，有 h 0 0 0 f ) = ( h o g ) o f 命题2 1 2 每个对象有且只有唯一的恒等射。 有时为了方便，我们用a o b j c 表示a 是c 的对象，m o r c 表示，是c 的射， m o r c ( x ，y ) 表示，是x 到y 的射，其中x 、y o b j c 。在不影响理解的情况下，我们在给 出射时有可能并不给处它的域和共域，在给出恒等射时有可能不给出它的对象下标。不 过，当我们写g0 ，时，总是假定o d d ( ，) = 如m ( 9 ) 。 下面给出一些范畴的例子： 伢子2 1 31 集合范i i 毒s e t ：对象是集合，射是集合问的函数，复合是函数的 复合。 2 群范畴6 r p ：对象是群，射是群之间的同态射，复合是同态射的复合 8第二章范畴理论 3 。独异点范畴m o n ：对象是独异点，射是独异点之间的同态射，复合是同态射的复 合。 4 向量范畴v c t f ：对象是f 域上的向量空间，射是向量空间之间的线性变换，复合是 线性变换的复合。 5 拓扑范畴t o p ：对象是拓扑空问，射是拓扑空间之间的连续映射，复合是连续映 射的复合。 上面是一些来自数学领域的范畴，下面介绍一些来自计算机领域的例子： 例子2 1 41 给定一种程序设计语言l ，可以构造一个范畴c f l ) ，对象是该程 序设计语言所能表示的数据类型d ，射p ：d e 以类型d 的数据为输入，以类型e 的数 据为输出用语言l 写的程序p ，复合就是程序调用，即给定程序p ：d e 和q ：e f ，复 合是程序弘q ：d f ，程序p ；q 先调用p ，然后在调用q 。恒等射是空程序。 2 给定一个形式系统s ( 例如，命题逻辑形式演算系统) ，也可以构造一个范畴c ( s ) ， 对象是形式系统s o 的公式a ，射是形式系统的证明p ：a b ，即p 是以公式4 为附加前 提，利用形式系统的公理和规则能推出矧拘一个证明序列。复合是证明序列的连接。 范畴是一个非常抽象的概念，在各个领域都可找到范畴的实例。虽然范畴理论种有 很多内容是从范畴, s e t 泛化而来，但是范畴理论的许多内容已经超越了集合论，有了更 为广泛的含义和更为广泛的应用领域。 定义2 1 5 范畴c 的图式( d i a g r a m ) 是一个有向图，其中的顶点用c 的对象标记，有向 边用c 的射标记，且其源顶点是该射的域所标记的顶点，目标顶点是该射的共域所标记 的顶点。即图式中的顶点对应范畴的对象，边对应射，路径对应复合。 图式让范畴的概念和范畴上的操作更容易理解，而图式中最重要的概念是交换图。 定义21 ，6 交换图是一个图式，该图式中任意有相同源点和目标顶点的不同有向路 径对应c 的相同的射，等价地，是指这些不同有向路径所对应的射的复合在c 中相等。 通常利用交换图给出射的复合必须满足的一些性质。例如： 例子2 1 7 等式k0 h = g0 ，表示为： a lb i l h i g it ii c ! d 2 1 蜡象与射9 ll p 1 0 第二章范畴理论 2 1 2初始对象和终结对象 定义2 1 1 2 给定范畴c ，如果对象a 满足对任意对象b o b j c 都存在唯一的射，： a b ，则称a 为范畴c 的初始对象( i n i t i a lo b j e c t ) 。 定义2 1 1 3 给定范畴c ，如果对象a 蔫足对任意对象b o b j c 都存在唯一的射f ： b a ，则称a 为范畴c 的终结对象( f i n a lo b j e c t ) 。 根据定义，马上可以得出下面两个定理： 定理2 1 1 4 初始对象在同构意义下是唯一的。 定理2 1 1 5 终结对象在同构意义下是唯一的。 一个范畴不一定存在初始对象和终结对象。但因为初始对象和终结对象拥有如此 完美的性质，因此初始对象和终结对象是范畴理论中的重点研究对象。在后面的讨论 中，重点也是放在存在初始对象或终结对象的范畴上。 下面给出始对象和终结对象的一些例子； 例子2 1 1 6 集合范畴s e t 的初始对象是空集妒，它到任何集合a 都有空函数西：咖一 a 。集合范畴s e t 的终结对象是任意的单元素集合1 = ，对于任意集合4 ，都有唯一的 函数! a ：4 一l ，定义为v a a ，! a ( n ) = 。 例子2 1 1 7 对于单个偏序集( x ，s ) 作为范畴，它的初始对象如果存在就是它的最 小元，它的终结对象如果存在就是它的晟大元。 2 1 3 积与共积 定义2 1 1 8 给定范畴c ，两个对象 和b 的积( p r o d u c t ) 是三元组( a b ，7 r 1 ，丌2 ) ，其 中l 口是c 的对象， 1 ：ax 口_ i ，订2 ：axb - - * 1 3 是c 的射，称为投影射，且满足：对 任意c 的对象u 和射i ：e a ，g ：c b ，都存在唯一的射( ，g ) ：e a b 使得 7 r l0 f ，g ) = ， i f 2o ( f ，g ) = g 即下面的交换图成立： 2 1 对象与射 1 1 定义2 1 ，1 9 给定范畴c ，两个对象a 和b 的共积( c o p r o d u c t ) 是三元组( a + b ，k 1 ，) ， 其中4 + b 是c 的对象，k 1 ：a a + b ，忱：口一a + 日是c 的射，称为注入射，且满足： 对任意e 的对象c 和射，：月一g ，g ：b c ，都存在唯一的射i f ，g 】：a + b 一( j 使得 即下面的交换图成立： 【，9 jo k l = f l 厂，纠o ，吃= 9 ，4兰! a + b 竺b 积是集合的笛卡尔积的抽象在集合范畴中积等价于笛卡尔积。共积是集合上的不 相交并的抽象，在集合范畴中共积等价于不相交并。注意，不是所有范畴都存在积与共 积。 对于积与共积的性质，首先有下面的定理： 定理2 1 2 0 两个对象的积与共积在同构意义下是唯一的。 积与共积是对偶概念，它们的性质是类似的。因此接下来主要讨论共积的性质。关 于共积有下面的等式成立： 【，】刃。一t = f 沙鲥。8 2 2 岔 ( 2 1 ) 陋l ，k 2 l = i d x + y h o i f ，9 】= i h o f ，h 0 们 共积还可以作用于射上，下面给出两个射的共积： 定义2 1 2 1 设范畴c 有共积，它盼两个射f ：a 一8 和岔：e 一上) 的共积，记为，+ g ： a + g b + d ，定义为： ，+ 9 = k 茸o f ，k 口。翻 1 2第二章范畴理论 l 口k ：f b a x a a ( f ) i d a ： c a b 在集合范畴中，幂对象可以这样看待：给定两个集合x 和y ，幂对象y x = ，i ，是从x 到y 的全函数) 。因此幂对象y x 有时也称为函数空间( f t m c t i o ns p a c e ) 。 幂构造的本质可使用如下的对应关系刻划，这种对应也称为克雷化( c u r r y i n g ) ： z x y 亏：尹 2 2 ) 关于幂对象，首先有如下定理： 定理2 ，1 2 3 设范畴c 有积，它的两个对象a 和b 的幂对象在同构的意义下唯。 注意，幂对象b a 与a 口一般来说是不同构的。而且由于范畴不一定有积，故也不一 定有幂对象。 - 定义2 1 2 4 称范畴c 是笛卡尔封闭范畴( c m t e s i a nc l o s e dc a t e g o r y , c c c ) ，如果它 有有限积和幂对象；称范畴e 是双笛卡尔封闭范畴( b i c a r t e s i a nc l o s e dc a t e g o r y , b i c c c ) ， 如果它是有有限共积的笛卡尔封闭范畴。 幂对象有如下基本性质： e vo ( a ( 门j 氐) = f a ( e v ) = i d y x( 2 3 ) a ( ) 。h = a ( f0 ( h x i d x ) ) 2 2 函子 2 2 函子 定义2 2 1 任意给定两个范畴c 和d ，范畴c 到口的函子( f u n c t o r ) f 是满足如下条件 的指派( 勰s i 和m e n t ) ： 1 对苑畴c 的每一个对象a ，指派了范畴d 的一个对象与之对应，将这个对象记 为f a ； 2 对范畴c 的每个源为a 目标为b 的射，：a b ，指派了范畴口的一个源为f a 目标 为f b 的射与之对应，将这个射记为f ，。 且f 的这种指派还满足： 1 对范畴的任意对象a ，有见d a = i d f a ； 2 对范畴的任意两个可复合的射，：a b 和g ：b e ，有f ( g0 ，) = f g 0f ， 函子给出了两个范畴的对象与射的对应关系，而且保持恒等射和复合。而恒等射和 复合是范畴中最重要的结构，因此，函子实际上是保持范畴结构的指派 通常使用类似下图的形式来给出一个函予f ：e d ： 下面介绍一些特别 例子2 2 2 给定范 c 一口定义为： f a l f ， f b 固定d 中的某个对象d ，常函子( c o n s t a n tf u n c t o r ) k o d 卜 ，l 一 卜， aob酐彻a1 啪靴 1 4 第二章范畴理论 例子2 2 4 给定范畴c 和口，如果范畴口有共积，函子f 和g 是c 到口的函子，f 和g 的共积f + g 定义为： bf b + g b f 例子2 2 5 给定范畴c ，如果函子f 是范畴c 到c 的函子，称f 是范畴c 上的自函子。 下面给出自函子的一些例子 例子2 2 6 给定范畴c ，恒等函子，d 定义如下 a b 则，d 是范畴c 上的自函子。 月 l， b x f f x ) a ，l 一卜幽棚m m y ( f y ) 4 定义2 2 8 多项式函子是满足下列条件的集合范畴上的自函子类： 1 ，恒等函子是多项式函子； 2 如果函子f 和g 是多项式函子，则它们的积f x g 也是多项式函子； 3 如果函子f 和g 是多项式函子，则它们的共积f + g 也是多项式函子； 4 任意集合a ，如果函子f 是多项式函子，则常指数函子f 4 也是多项式函子。 吖 恻卜 蹦 一 ai川， 2 3 自然变换 在计算机领域中，函子通常用于对系统进行分类，不同的函子对应不同的系统行 为，而多项式函予是其中应用最广泛的，从后面的讨论可以看到，像确定型自动机、流 系统等，其行为都可以用多项式函子描述。 积函子f x g 表示系统行为由两部分组成，分别由函子f 和g 描述；共积函子f + g 表 示系统行为有两种可能情况，或者由函子f 描述，或者由函子g 描述。常函子k o 表示系 统的输出为集合d 的元素。常指数函子f a 表示系统的输入为集合a 的元素。 2 3自然变换 函子给出了范畴之问的关系，而函子之间的关系则由自然变换给出。下面首先给出 自然变换的定义： 定义2 3 1 给定从范畴c 到d 的两个函子f ，g ：c 一口。从函子f 到函子g 的一个自 然变换( n a t u r a t r a n s f o r m a t i o n ) a ，记为a ：f 辛g ，是一族射 n ) a 晰c ，即对范畴c 的 每个对象4 ，都有范畴口的一个射：f a g ，且满足对范畴c 的任意射，：a 一疗在范 畴d 由。口o e l = g ，o d ，参见下图： 范畴c范畴口 | ，f i b r 一， 下面以程序设计语言中的例子说明自然变换的含义： 例子2 3 2 求链表长度的函数l e n ：l i s t a - - * n 是链表函子l i s t 到常函子，0 的自然 变换，因为有： l i s t a ! ! 坠n l ；k 卜 1 6第二章范畴理论 例子2 3 3 二叉树的中序遍历操作m i d t r a v e l ：b i n t r e e a - 一l i s t a 是树函子b i n t r e e 到 链表函子l i s t 的自然变换，因为我们有如下交换图： b i n l - e e 以m i d t r a v e ll i s t 胁k b i n t r 些e e f 型l ；量v 第三章共代数弟二早犬1 弋鳅 共代数( c o a l g e b r a ) 是代数( a l g e b r a ) 的对偶概念。代数是集合以及集合上的一些操作， 而共代数也可以看作集合以及集合上的一些操作，但是共代数的操作与代数的操作不 一样。代数的操作一般称为构i i 抒( c o n s t r u c t o r l ，由已有的集合成员构造新的集合成员， 人们熟悉的抽象数据类型如链表、树等，就是通过代数方法构造的，代数方法体现的 是“构造”的概念而共代数的操作一般称为解构子( d e s t r u c t o r ) ，通过观察集合成员的 行为了解集合成员的内部结构，体现的是“解构”( d e s t r u c t i o n ) 和“观察”( o b s e r v a t i o n ) 的 观点，通常，共代数中的集合成员成为状态。 在计算机科学中，常用代数理论来研究抽象数据类型，因为抽象数据类型实际上也 是在一数据集合上给出一组满足某些性质的操作，本质上是一种代数。代数上的操作通 常具有一：t a 一一的形式，在抽象数据类型中，4 可看成数据类型，口可以看成构造子。 代数方法对于数据结构的研究起到了非常重要的作用，但是它对于刻划基于状态的 动态系统是比较困难的。对于这类型的系统，以往的方法大多数是用自动机或者变迁系 统来进行描述，通过多年的研究，人们发现，这种基于状态的系统可以利用共代数方法 研究。 共代数x 上的操作具有o ：x 一7 的形式。在计算机科学研究中，通常将共代数看 成具有内部状态的系统，x 可以看成是系统所有可能状态的集合，o 则看成对状态的观 察。 简单地说，代数和共代数本质上都是集合及其上满足一定性质的操作，用于抽象数 据类型理论研究的代数则从构造的角度研究集合及其操作，而用于系统理论研究的共 代数则从观察的角度探讨系统及其功能。从范畴论的角度上来看，它们是对偶的概念， 这一对偶性存在于计算机科学的许多领域之中，如自动机理论、面向对象设计、系统理 论、进程代数等。 本章介绍后文涉及到的代数与共代数的基础知识，包括代数与共代数的定义、行为 等价与互模拟，共代数的应用等。 1 7 1 8 3 1系统与共代数 第三章共代数 本小节主要介绍系统的概念，说明为何要以共代数的观点看待系统，并介绍了共代 数的一些基本概念与性质，并通过一些状态系纷i ( s t a t e db a s es y s t e m ) 的例子如流、链表 等，说明如何使用共代数方法对系统进行建模。 3 1 1系统 什么是系统? 简单地说，系统是具有一定结构，与外界相互作用而具有一定功能的 但又相对对立的一个集合体。系统是个集合体，是指它是一组东西的总称；系统具有 一定结构，这也意味着系统具有一定的复杂性；系统与外界相互作用，因而具有一定的 功能，完成某些任务；系统相对独立实际上是指根据系统所完成的功能可以将与系统有 关的东西从环境中抽象出来相对对立地加以研究。 从某种意义上说，所有系统都是基于状态的系统，所谓状态( s t a t e ) 就是系统结构在 菜一特定时刻的表现形式。之所以强调是基于状态的系统是因为我们想强调以一种黑 盒子( b l a c kb o x ) 的观点看待系统，即，外界只能通过系统所提供的接口( i n t e r f a c e ) 与系统 进行交互，而且在不通的时候同样的接口可能会表现出不同的行为( b e h a v i o r ) ，完成不 同的功能，因此需要将系统划分成不同的状态。总的来说，系统具有以下特征： 1 系统具有定的结构( s t r u c t u r e ) ，系统结构在不同时候具有不同的状态( s t a t e ) ，系 统结构和状态被隐藏在系统内部，外界不能直接对它们进行访问； 2 系统提供一定的接口( i n t e r f a c e ) 与外界进行交互，外界也只能通过这些接口与系 统进行交互，以观察系统的状态和使得系统完成某种功能( f u n c t i o n ) ； 3 系统通过接口与外界交互的过程表现出某些行( b e h a v i o r ) ，这些行为可能与系 统内部的状态有关，系统功能实际上是某些行为的总称。 通常，以这种观点为基础的系统称之为状态系统( s t a t eb a s e ds y s t e m s ) 或变迁系 统( t r a n s i t i o ns y s t e m s ) ，状态系统包括了很多常见的系统，例如流，自动机，标号变迁系 统，甚至抽象数据类型，面向对象的类与对象都可以看成是状态系统。为各种状态系统 建立统一的合适的模型是进一步研究系统的特性与系统之问关系的前提，也是本章的主 要任务。 由于状态系统的以上三个特征，用代数方法进行建模就不是太合适了，因为代数方 法体现的是“构造”的观点，而状态系统的内部结构是不可见，无法对其进行构造，只 能通过观察其行为而了解系统的当前状态。因而，共代数方法更适合于描述状态系统。 共代数所体现的“观察”的观点正是状态系统所必须的。共代数的变迁射可用于模拟系 统的接口与行为。而共代数的同态( h o m o m o r p t f i s m ) n t 用于描述系统间的关系，行为等 3 1 系统与共代数 1 9 j f ( b e h a v i o u r a le q u i v a l e n c e ) 和k 模拟( b i s i i i l i 】m i o n ) 可用于描述系统状态问的关系。这些 概念的具体含义，将在后面的章节中逐一介绍。 3 1 2 代数与共代数 在范畴论中。代数与共代数是一组对偶概念。在后面的内容中可以看到，共代数中 的很多概念都在代数中有其对偶概念。 下面首先给出范畴论中代数的定义： 定义3 1 1 给定任意范畴c 和其上的自函子f ，f 上的代数定义为一个二元组( i ，o ) ， 其中a 是范畴c