（计算机软件与理论专业论文）基于组件的嵌入式软件系统的共代数模型.pdf

念，并对泛性质与泛构造的关系进行了深入研究； 2 、一般化软件组件共代数语义的研究。通过将组件规约分别对应f 一共代数 的基本结构，为软件组件提供了一个一般化的共代数模型： 3 、嵌入式组件共代数模型的构造。通过对嵌入式系统的领域特性进行分析， 提出了嵌入式软件组件模型必须满足的性质。通过实例化f _ 共代数的行为单 子，使得组件行为具有确定性和无穷性。通过构造针对f 一共代数载集的函数， 实现了组件整体非功能属性的表达。通过构造三个集合范畴上的幺半群及其对 应的强单子，实现了组件方法非功能属性的表达。提出了组件基于接口的显式 依赖的概念； 4 、基于嵌入式组件的软件系统模型的构造。通过三种基本方式实现了组件 的聚合，并分析和验证了其对组件非功能属性的影响。通过分析聚合组件的性 质，提出了标准输入输出接口的概念并定义了对应的输入输出转换结构。最后 通过输入输出模拟基于依赖接口的组装，并通过实例分析了这种方法的优劣。 关键词：基于组件的软件工程；嵌入式软件系统；形式化开发；共代数方法； 卜共代数； a b s t r a c t c o a l g e b r aicm o d e lln gf o r c o m p o n e n t b a s e d e m b e d d e ds o f t w a r es y s t e m m a j o r ：c o m p u t e rs o f t w a r ea n dt h e o r y n a m e ：z h a n gl v s u p e r v i s o r ：f e n gg a n g i nr e c e n ty e a r s ，t h e “a dh o c s o f t w a r ed e v e l o p m e n tm e t h o df o re m b e d d e d s o f t w a r eh a sl a g g e dm u c hb e h i n dt h em a r k e tr e q u i r e m e n t sf o rt h ei n c r e a s i n g c o m p l e x i t yo fe m b e d d e ds y s t e m t h em o r ea n dm o r es u c c e s s f u la p p l i c a t i o n so f c o m p o n e n t - b a s e ds o f t w a r ee n g i n e e rm e t h o di i lg e n e r a l - p u r p o s ea r e ah a v ei n t r o d u c e d u san e ww a yt od e v e l o pe m b e d d e ds y s t e m s d u et ot h ed o m a i nc h a r a c t e r so f e m b e d d e ds y s t e m , s u c ha sr e a l - t i m e ，r e s o u r c ec o n s t r a i n t ，d i v e r s i t yi nh a r d w a r ea n d h i g hr e l i a b i l i t y , w ea l w a y sn e e dt ou s es o m ef o r m a lt o o l st od e v e l o pe m b e d d e d s o t w a r es y s t e m s h o w e v e r , r e s e a r c h e so nc o m p o n e n t - b a s e df o r m a ld e v e m p m e n ti s m a i n l yf o c u s e do nt h ee x t e n d i n go ft h ea l r e a d ye x i s t i n gt h i n g st od e s c r i b et h en o t i o n o fs o f t w a r ec o m p o n e n t s ，a n dm o s to ft h e mi sn o tp o w e re n o u g ht oe x p r e s st h e f a s c i n a t i o no fs o f t w a r ec o m p o n e n t s o f t w a r ec o m p o n e n t sa r eh a r d l yd e f i n a b l e ( o rs i m p l yn o td e f i n a b l e ) a l g e b r a i c a l l y , i e ，i nt e r m so fac o m p l e t es e to fc o n s t r u c t o r s t h e i rs e m a n t i c si se s s e n t i a l l y o b s e r v a t i o n a l ，i nt h es e n s et h a ta l lt h a tc a nb et r a c e do ft h e i re v o l u t i o ni s t h e i r i n t e r a c t i o nw i t ht h ee n v i r o n m e n t t h e r e f o r e ，c o a l g e b r a s ，w h o s et h e o r yh a sr e c e n t l y w i t n e s s e dr e m a r k a b l ed e v e l o p m e n t s ，a p p e a ra sas u i t a b l em o d e l i n gt 0 0 1 t h eb a s i co b s e r v a t i o no fc a t e g o r yt h e o r yt h a tu n i v e r s a lc o n s t r u c t i o n sa l w a y s i i i 伽0 1脚3啪8兀 舢1舢y c o m ei np a i r s ，h a sm o t i v a t e dr e s e a r c ho nt h ed u a l i t yb e t w e e na l g e b r a sa n dc o a l g e b r a s ， w h i c h p r o v i d e sab r i d g eb e t w e e n m o d e l so fs t a t i c ( c o n s t r u c t i v e ，d a t a - o r i e n t e d ) a n d d y n a m i c a l ( o b s e r v a t i o n a lb e h a v i o r - o r i e n t e d ) s y s t e m s a t t h ep r o g r a m m i n gl e v e l ，t h e i n t u i t i v es y m m e t r yb e t w e e nd a t aa n db e h a v i o rp r o v i d e se v i d e n c eo f s u c had u a l i t y , i n i t sc a n o n i c a li n i t i a l f m a ls p e c i a l i z a t i o n e x i s t i n g r e s e a r c h e sa r em a i n l yo np r o v i d i n gab a s i sf o r m a ls e m a n t i c f o r s o f t w a r ec o m p o n e n t sa n dl a c ko fd e e pi n s i g h ti n t oe m b e d d e da r e a f r a m ei nt h i s c o n t e x t ，t h i st h e s i sa d d r e s s e dt h ef o l l o w i n gm a i nt h e m e s ： 1 t h er e s e a r c ha n dd i s c u s s i n go fc a t e g o r yt h e o r y , w h i c hi st h ef o r m a lb a s i so f c o a l g e b r a w ei n t r o d u c e dc o r ec o n c e p t so fc a t e g o r yt h e o r ya n dt h er e l a t i o n s h i p b e t w e e nu n i v e r s a l i t ya n du n i v e r s a lc o n s t r u c t i o n sw a ss p e c i a l i z e d 2 t h ei n v e s t i g a t i o no fc o a l g e b r a i cs e m a n t i cf o rg e n e r i cs o f t w a r ec o m p o n e n t w ep r o p o s e dag e n e r i cc o a l g e b r a i cm o d e lf o rs o f t w a r ec o m p o n e n tb yc o n n e c t i n g c o m p o n e n ts p e c i f i c a t i o n sw i t h s t r u c t u r eo fc o a l g e b r a 3 t h ec o n s t r u c t i o no fc o a l g e b r a i cm o d e lf o re m b e d d e dc o m p o n e n t s w ef i r s t c h a r a c t e r i z e dt h ed o m a i np r o p e r t i e so fe m b e d d e ds y s t e m b a s e do nt h i s ，w ec l a i m e d t h r e ep r o b l e m st h a ta ne m b e d d e dm o d e lm u s ts o l v e d t h ed e t e r m i n a t ea n di n f i n i t eo f c o m p o n e n tb e h a v i o rw a sr e a c h e db yb e h a v i o rm o n a di n s t a n t i a t i o n af u n c t i o nf r o m c a r r i e rs e tt os o m es i n g l e t o ns e t sw a sa l s op r o v i d e dt od e s c r i b et h en o n - f u n c t i o n a l p r o p e r t i e so fc o m p o n e n t o t h e rn o n - f u n c t i o n a lp r o p e r t i e sr e l a t e dt oe a c hm e t h o d w a s e x p r e s s e db yc o n s t r u c t i n gm o n o i d so nc a t e g o r ys e t l a s t l y , w ed e f i n e dt h ee x p l i c i t d e p e n d e n c i e sb e t w e e nc o m p o n e n t st h r o u g hi n t e r f a c e s 4 t h em o d e lo fe m b e d d e dc o m p o n e n t b a s e ds y s t e m w ed e f m e dt h r e eb a s i c c o m p o s i t i o np a t t e r n sa n d v e r i f i e dt h e i rn o n - f u n c t i o n a lp r o p e r t i e su n d e rc o m p o s i t i o n t h r o u g ha n a l y z i n gt h ep r o p e r t i e so fc o m p o u n d e dc o m p o n e n t ，w ed e f i n e d as t a n d a r d i n p u ta n do u t p u ti n t e r f a c ef o rc o m p o u n d e dc o m p o n e n t s am e t h o dt om i m i ct h e m p u t o u t p u tb e h a v i o rt oi n t e r a c t i o nt h r o u g hi n t e r f a c eh a sb e e np r o p o s e da n dw e s h o w e dt h er e l a t i v em e r i t so ft h i sm e t h o db yas i m p l ee x a m p l e k e yw o r d s ：。c o m p o n e n t b a s e ds o f t w a r ee n g i n e e r ；e m b e d d e ds o f h v a r es y s t e m ； f o r m a ld e v e l o p m e n t ；c o a l g e b r a i cm e t h o d s ；f - c o a l g e b r a ； v 目录 中文摘要i 英文摘要i i i 第1 章绪论1 1 1 课题背景1 1 2 本文研究目的2 1 3 本文主要工作3 1 4 本文组织结构3 第2 章范畴论一共代数的形式化基础5 2 1 范畴的基本概念5 2 1 1 范畴的定义5 2 1 2 初始对象与终结对象6 2 1 3 广义元素与全局元素7 2 1 4 同构态射8 2 1 5 函子8 2 1 6 自然转换9 2 1 7 伴随函子1 0 2 2 范畴中的泛结构1 1 2 2 1 积1 l 2 2 2 共积1 3 2 2 3 乘方1 4 2 3 笛卡尔闭合范畴与可分配范畴1 5 2 4 多项式函子1 6 第3 章软件组件的共代数语义1 9 3 1 基于组件的形式化开发1 9 3 1 1 软件组件的基本定义1 9 3 1 2 软件组件的形式化开发1 9 3 1 3 基于组件系统的形式化开发2 0 3 2 软件组件的一般共代数模型2 l v i i 3 2 1 型构契约作为函子2 2 3 2 2 功能契约作为迁移函数2 3 3 2 3f 一共代数2 4 3 2 4 组件作为共代数2 7 3 3 共代数规约探讨3 0 3 4 本章小结3 0 第4 章嵌入式组件的共代数模型3 3 4 1 嵌入式组件模型的领域特点3 3 4 2 组件状态的等式关系与互模拟关系3 4 4 3 组件状态的可观察性3 6 4 4 组件非功能属性的表达3 7 4 4 1 组件整体的非功能属性3 7 4 4 2 组件方法的非功能属性3 8 4 5 嵌入式组件的共代数4 0 4 6 基于接口的组件显式依赖4 2 4 6 1 组件内部行为的暴露与隐藏4 2 4 6 2 组件与依赖组件的交互4 3 4 6 3 组件依赖作为接口4 5 4 7 本章小结4 5 第5 章基于嵌入式组件的系统4 7 5 1 聚合组件4 7 5 1 1 水平组装4 7 5 1 2 并行组装5 0 5 1 3 并发组装5 1 5 1 4 聚合组件的性质5 3 5 2 有“膜 组件5 4 5 2 1 顺序组装5 4 5 2 2 接口代理5 5 5 2 3 有“膜组件的形式定义5 6 5 3 组件交互5 9 5 3 1 输出回馈5 9 5 3 2 组件显式依赖的共代数语义j 6 1 5 4 实例研究6 4 5 5 本章小结6 6 第6 章总结与展望6 9 6 1 本文工作总结6 9 6 2 未来工作展望7 0 参考文献7 1 致谢7 5 i x 华南师范大学硕士学位论文第1 章绪论 第1 章绪论 1 1 课题背景 最近十几年来，基于组件的软件工程( c o m p o n e n t b a s e ds o f t w a r ee n g i n e e r ) 及其方法使得通用领域很多大型分布式系统的开发效率得到显著提高，系统的 开发过程从代码的逐行编写转化为对第三方组件的组装。业界也出现了比较统 一的n e t 、e j b 、c o r b a 三大组件标准n 3 。相对而言，嵌入式系统的开发方法则 大大滞后于通用领域，但是嵌入式系统的结构却越来越复杂，比如在汽车工业 中，代码的数量从i o o k b 上升到了1 g b 乜1 。这就促使人们把基于组件的开发方法 应用到嵌入式系统的开发中来，提出各种开发基于组件的嵌入式软件系统 ( c o m p o n e n t - b a s e de m b e d d e ds o f t w a r es y s t e m ) 的方式和方法，如用于基于场 设备的系统开发的p e c o s 臼3 框架的提出以及s a v e c c m h l 框架在汽车工业中的应 用。 嵌入式软件系统自身有实时性、资源有限性、安全关键性等领域特点，这 使得此类系统的开发或多或少的会引入形式化开发的方法，以使得系统的安全 性可以得到验证。但就目前成功应用的各种形式化方法而言，其基础模型与所 采用的规约语言都没有针对组件这一新概念的专门描述，因此学术界和工业界 针对这一问题进行了大量的研究工作。其中大部分的工作集中在对已成功应用 的形式化方法进行扩充以描述组件及基于组件的系统，如文 5 采用代数规约语 言来描述组件和基于组件的系统、文 6 采用t l a + ( e x t e n d e dt e m p o r a ll o g i cf o r a c i t o n s ，扩展动作时态逻辑) 对组件系统的非功能属性进行了形式化分析、文 7 对b 方法进行扩充，使得可以把组件与b 语言定义的抽象状态机对应起来、 文 8 则采用v d m ( v i e n n ad e v e l o p m e n tm e t h o d ) 的形式规约语言描述了组件库 的概念、文 9 ，1 0 使用c s p ( c o m m u n i c a t i o ns e q u e n t i a lp r o c e s s ，通信顺序进 程) 来描述接口的动态行为、文 1 1 利用有限状态自动机来分析组件状态的可 达性、。文 1 2 则采用接口自动机来描述接口的动态行为、文 1 3 对构成组件间 互连的连接件进行了抽象描述，并采用时间受限自动机来描述连接件的动态行 为、文 1 4 采用可着色p e t r i 网构造了一个c o r b a 组件的可执行模型，用于功 华南师范大学硕士学位论文基于组件的嵌入式软件系统的共代数模型 能属性的实验与测试。 综上所述，基本上在嵌入式系统开发获得了成功应用的形式化开发方法都 能通过扩充或修改一些定义来描述基于组件的系统。但是，由于原方法关注点 的不同，都只能抽象描述基于组件系统的一部分。同时，大多数现有的形式化 方法其基础语义都是由代数系统推导而来，而代数的天然特性决定了这些方法 在描述基于组件的系统时需要暴露过多组件的内部状态信息，这使得通过各组 件组装后的系统状态空间过大，系统的一致性验证需要花费很多的时间或根本 不能得到验证。另外，由于组件的“黑盒”特性，其内部状态信息是不应该也 不允许暴露给外界的，这使得用基于代数系统的形式化方法变得不适用于基于 组件系统的开发。 另一方面，作为代数对偶概念存在的共代数理论从上世纪9 0 年代开始受到 了越来越多的关注。1 9 8 8 年，p a c z e l 等人首次使用共代数给出了c c s 中进程 代数的终结语义。此后，计算机科学工作者发现共代数理论对研究基于状态的 系统( 例如自动机、进程、对象、软件组件等) 有独特的优越性。使用共代数理 论作为工具的共代数形式化方法，可以对系统的行为等价、不确定性等从数学 上进行深入探讨，为这些系统建立良好的形式理论基础，并对其性质进行描述 与验证“。自1 9 9 8 年以来，国际上已经召开了l o 届有关计算机科学中的共代数 方法( c o a l g e b r a i cm e t h o d si nc o m p u t e rs c i e n c e ，c m c s 9 8 c m c s2 0 1 0 ，0 5 年后改为两年一届) 的年会。 1 2 本文研究目的 由于共代数对于基于状态系统描述的天然优越性，同时为了克服旧有方法 在基于组件系统的开发中存在的问题，人们开始关注用共代数方法研究基于组 件的系统。l s b a r b o s a 首次提出了将组件作为共代数研究的概念和方法。， 他通过模拟进程代数，把组件抽象为一个具有初始状态的共代数，从较高的抽 象层次描述了组件及组件的组装、交互，并推导出了类似于进程代数的组件交 互结构，为利用共代数来描述组件及组件系统提供了一个理论框架。基于该框 2 华南师范大学硕士学位论文 第l 章绪论 架，文 1 7 ，1 8 对组件的精化( r e f i n e m e n t ) 与组件行为的推理演算进行了研究，” 并为其提供了形式化语义基础。文 1 9 在 1 3 的基础之上采用共代数来描述连 接件的动态行为，并提出了抽象行为类型这一个概念。通过与传统方法的对比 发现，共代数作为一种用来描述基于状态的动态系统的语言，比较适合用于描 述组件及基于组件的系统。 在这些研究中，方向主要集中于为基于组件系统提供基础的共代数形式语 义，组件的行为与组件间的交互都是基于简单的输入、输出端口，这与组件定 义中的接口有着很大的不同，使得组件的组装与交互与实际情况存在较大差异， 不利于进一步的形式化开发。另一方面，对于嵌入式系统比较关心的非功能属 性，这些研究都没有提及或没有深入的研究。这两点是本课题研究的出发点， 也是本文用共代数来对基于组件的嵌入式软件系统建模的动机所在。 1 3 本文主要工作 本文所作的工作可以分为两个主要方面，一是实例化组件的共代数模型， 使其能够对嵌入式系统开发中关注的非功能属性描述提供形式语义，并描述了 各组件的非功能属性在组件组装中如何得到保持以及对由它们组装成的系统非 功能属性的影响；二是将组件间基于输入、输出端口的交互行为与接口相关联， 提出了组件显式依赖的概念，并基于输入输出交互与组装为组件的显式依赖提 供了形式语义。 1 4 本文组织结构 全文的组织结构安排如下： 第一章前言绪论，论述选题的研究背景、意义和内容； 第二章范畴论共代数的形式化基础，介绍了范畴论中与共代数相关的核心 概念与相关的定律，以统一文中出现的各种符号的意义和用法； 第三章软件组件的共代数语义，通过介绍基于组件的形式化开发的基本流 程，探讨了形式化规约的重要性。为了给组件的形式化规约提供形式语义，给 华南师范大学硕士学位论文基于组件的嵌入式软什系统的共代数模型 出了组件的一般化共代数模型并探讨了对组件进行共代数规约的可行性。 第四章嵌入式组件的共代数模型，对嵌入式系统的领域特性进行了论述， 并由此分析了嵌入式组件模型必须满足的要求，通过对组件的一般化模型进行 领域化得到了嵌入式组件的共代数模型，并分析了组件显式依赖表达的可行性； 第五章基于嵌入式组件的系统，介绍了组件如何通过组装聚合称为功能更 强的聚合组件，以及组件显式依赖的形式语义如何通过特殊组装结构来表达， 介绍了聚合组件如何通过显式依赖的解决来构成嵌入式软件系统，并通过实例 展示这种方法的可行性和可表达性： 第六章总结与展望，通过总结已做的研究工作，发现其中的不足之处指出 了未来的工作方向； 最后是参考文献和致谢。 4 华南师范大学硕士学位论文 第2 章范畴论共代数的形式化基础 第2 章范畴论一共代数的形式化基础 在文 2 0 中，c m c l a r t y 这样评述范畴论( c a t e g o r yt h e o r y ) 的发展过程： “数学应用领域的扩展使得我们需要借助一种更一般性的理论来处理各种数学 结构，特别是当对结构的描述越来越趋向于对这些结构进行定义时。2 0 世纪6 0 年代，l a w v e r e 开始尝试采用纯粹的范畴语言来对数学中的各旧有领域进 行描述并提出了多种与这些领域对应的基础范畴，而同时这些研究成果又为数学 带了新的应用领域，这一点在逻辑学和计算机科学中尤为明显。 而共代数就是 这样一种通过对旧领域的研究而得到的新理论，它的概念虽然早已普遍存在于各 种计算现象中，但只有使用范畴论对它进行描述才能充分展现它的普遍性和强大 的表达能力。因此本章首先对范畴论中的核心概念和相关定律进行简单的介绍， 它是对这些概念的简单罗列，以为共代数概念的描述和本文所要论述的内容提供 形式化框架。本文内容主要参考文 1 6 2 5 和文 2 1 ，其中的部分翻译参考文 2 2 。 2 1 范畴的基本概念 2 1 1 范畴的定义 范畴的定义实际上描述的是箭头以及箭头的复合如何构成一类一般化的幺 半群。形式化的说， 定义2 1 一个范畴( c a t e g o r y ) c 包括： 水 对象( o b j e c t ) x e z ，组成的肘象类o b j ( c ) ； 木 对于任意一对对象卿y f ：x - - 9 y 称为艇0 啪箭头，脉为箭头7 1 拘域 ( d o m a l n ) 或源( s o u r c e ) ，y 称为箭头7 1 拘共域( c o d o m a l n ) 或目标( t a r g e t ) 。域为 兄共域为啪箭头组成集合c x ，y 】，称为态射集( h o r ns e t ) ： 木 对于任意三个对象墨y 和z ，一个称作c 一复合( c c o m p o s it i o n ) 的运算 华南师范大学硕士学位论文基于组件的嵌入式软件系统的共代数模型 。：c x ，y c 【y ，z 】j c x ，z 满足结合律； 木 对于任意对象墨一个特殊的箭头坼作为复合运算的左幺元和右幺元，称作 瑚恒等箭头( i d e n t i t yo n 如。 可用图2 - 1 表示： 即 图2 - 1 可交换图1 办。g 。= 五。( g 。厂) i d yo = g o i d r = g ( 2 1 ) ( 2 2 ) ( 2 3 ) 范畴中最基本的实例是集合范畴s e t ，它的对象为集合，箭头为集合与集合 之间的全函数，常见的还有代数范畴a l g ，它的对象是基调为的代数，箭 头为同态射。另外根据已定义的范畴，我们可以通过下面两种方式得到新的范 畴，范畴c 的对偶菹踌c 叩，它的对象是范畴c 的对象，箭头为范畴c 中箭头的反 向，范畴c 和d 的积菹踌c d ，它的对象是一对范畴c 和d 中的对象( 置，五) ， 箭头是一对两个范畴中的箭头( 石，厶) ，恒等箭头和复合箭头同样都是以分量方 式定义的。 2 1 2 初始对象与终结对象 在数学的很多分支，经常用“在给定某些条件下存在唯一态射”这种形式的 性质来定义一些结构，这种性质统称为泛性质( u n i v e r s a i i t y ) 。范畴论研究泛 性质。例如，我们说在某个范畴c 中的对象腥终结对象( f i n a lo b j e c t ) ，如 6 彰 旁 华南师范大学硕士学位论文第2 章范畴论共代数的形式化基础 果它满足对于c 中的任意对象兄存在一个唯一的箭头k 指向飚一性质，这一终 结性质就是一个泛性质，而由泛性质定义的结构通常称为泛结构( u n i v e r s a l c o n s t r u c t i o n ) 。对于泛性质来说，最有用的特点是它们总是成对出现的，泛结 构的对偶依然是泛结构。根据终结性质的对偶定义，我们可以得到初始性质，范 畴c 中的对象堤初始对象( i n it i a lo b j e c t ) ，如果它满足有唯一的箭头黼 向范畴中的任意对撇一性质。 在集合范畴中，空集严格的符合初始对象的定义。空集是任何集合的子集， 用箭头表示则有唯一的箭头唧：a 寸x 指向任意集合。而任何只有一个元素的单 集符合终结对象的定义，因为对于任意集合，总有一个函数将该集合的元素一一 映射为单集中的元素。通常用接近空集的符号0 表示初始对象，而为了强调初始 对象与终结对象的对偶性，符号通常用来表示终结对象，对于任意范畴来说， 初始对象与终结对象的存在可由如下泛性质表示： 对于范畴中的任意对象x ，如果有两个唯一的箭头? x ：0 一x 和! x ：x 一1 ， 使得对于任意箭头f ：x y ，有 ! l ，。f = ! x ( 2 4 ) 厂。? x = ? y ( 2 5 ) 2 1 3 广义元素与全局元素 在范畴论中，对象的结构是原子性的，它包含的元素未知，我们可以将指向 对黝箭头x ：z x 看作是哟“元素 ，它由z 决定，这时称x 为朋拘广义元 素( g e n e r a l i z e de l e m e n t ) ，记作x zx ，z 称为x 的定义阶。范畴中如果存在终 结对象，那么由终结对象指向椭箭头称作肭全局元素( g l o b a le l e m e n t ) ，在 集合范畴中全局元素是对集合由它的元素决定这一定理的抽象解释，因此对于全 局元素x ：j x 和箭头f ：x 专y 的复合，我们可以模拟集合论中的函数f x ， 直接用厂x 表示。 华南师范大学硕十学位论文基于组件的嵌入式软件系统的共代数模型 2 1 4 同构态射 在范畴论中，通过箭头描述不能区分的对象称为同构的( i s o m o r p h i c ) 对 象。泛性质定义的对象通常是一类在同构f 招等( i d e n t i f yu pt oi s o m o r p h i s m ) 的对象，我们说唯一的箭头通常是指在同构7 c p 莹- - ( u n i q u eu pt oi s o m o r p h i s i n ) 的箭头。 定义2 2 箭头f ：x 一】，是同构态射，如果存在另一个箭头g ：】，一x 使得 fo g = i d y ( 2 g 。f = 蛾 ( 2 7 ) 那么g 称作厂的逆厂1 ，式2 6 称作厂的截面( s e c t i o n ) ，2 7 称作的收缩 ( r e t r a c t i o n ) 。 如果两个对卿y 之间存在同构态射，那么黼y 是同构的，记作x 兰y 或者说它们在同构丁相等。 同构态射在集合范畴中就是双射函数，同样存在类似于单射函数和满射函数 的定义，称作单态射( m o n o m o r p h i s m ) 和满态射( e p i m o r p h i s m ) 。 定义2 3 箭头f ：x y 是满态射，如果对于任意对象z 和z i ，z 2 ，z ，满足 刁o f = 乞o f 毛= 乞 ( 2 8 ) 定义2 4 箭头f ：x - - ) y 是单态射，如果对于任意z 和x i ，恐zx ，满足 f 五= f 恐毛= 屯( 2 9 ) 需要注意的是，虽然在集合范畴中单态射和满态射对应的就是单射函数和满 射函数，但是在其它的一些范畴中满态射表达的是门拘像覆盖y 中的大部分。 2 1 5 函子 函子( f u n c t o r ) 是范畴与范畴之问保持结构的同态射。形式化的说， 定义2 5 一个从范畴c 到d 的厮子t ：c d ，是范畴间对象与对象，箭头 与箭头的映射使得任意对象x o b j ( c ) 有t x o b j ( d ) ，任意箭头厂c 【x ，y 8 华南师范大学硕士学位论文第2 章范畴论共代数的形式化基础 有t d t x ，t y l ，并满足 1 i d x = i d t x i t f o g = t f o t g ( 2 1 0 ) ( 2 1 1 ) 任意范畴c 有一个单位函子i d c 将范畴c 中的对象与箭头映射到其自身。 两个函子t ：c 寸d ，s ：d e 同样可以复合为t s ：c j e 。把范畴作为对象， 函子作为箭头，可以构成一个范畴的范畴c a t 。 一个由范畴c 指向范畴c 的函子称为自函子，单位函子i d c 是自函子的一 个特例，还有一种自函子，将c 中的所有对象映射为某个对象咒对象间的箭 头映射为x 上的单位箭头，这样的自函子称为常数函子，记作x ( 当上下文清 晰时简记作x ) 。域为积范畴的函子t ：c x dj e 称为双函子( b i f u n c t o r ) ，通 过固定它的某个参数为范畴中的对象，可以得到一个单函子，称为t 的截面函 子。如给定范畴c 中的某个对象么，可以得到t 的彳截面函子t 。：d e 。 2 1 6 自然转换 函子与函子之间的同态射叫做自然转换( n a t u r a lt r a n s f o r m a t i o n ) 。形式化 的说， 定义2 6 给定两个函子t ，s ：c d ，自然转换仃：t js 是一族范畴d 中的 箭头p 一：t a - - sa aeo b j ( c ) ) 对应范畴c 中的每个对象，使得对于c 中的任 意箭头f ：x y ，有 o r r 。r f = s f 。仃z ( 2 1 2 ) 可用图2 2 表示 上 1 r 与s 图2 - 2 可交换图2 9 门山f 华南师范大学硕十学位论文基于组件的嵌入式软件系统的共代数模型 如果我们将函子t 看作在范畴d 中给出了范畴c 中所有对象和箭头的一幅图 像，那么自然转换仃可以看作一个将图像t 转化为图像s 的箭头集合，对应范畴c 每个对象的箭头吼称为自然转换仃在对射处的一帮分( c o m p o n e n t ) 。如果仃的 每个部分都是d 中的同构态射，那么称仃为自然同构态射，记作仃：t 兰s 。 自然转换同样可以复合，给定函子t ，s ，r ：c d 以及自然转换仃：t s ， 仃：s r ，那么仃和仃可复合，它们的复合自然转换是通过分量方式来复合各 个部分，即 ( o o 仃) 工= o xo 仃x ( 2 1 3 ) 这样的复合称为自然转换的垂直复合( v e r t i c a lc o m p o s it i o n ) 。将从范畴c 到范 畴d 的函子作为对象，自然转换作为箭头，垂直复合作为箭头的复合，我们可以 得到函子的范畴d c 。 2 1 7 伴随函子 为了一般化范畴中的泛性质，需要伴随函子( a d j u n c t i o n ) 的概念，形式的话： 定义2 7 伴随函子包括： 宰 一对范畴c 和d ； 木 一对函子t ：cjd 和s ：d c ； 术 一对自然转换“：t sji d d 和t 7 ：i d cj s t 。 它们满足如下泛性质： 对于c 中的任意对象x 和任意箭头g ：x - - 9 s z ，存在d 中的唯一箭头 g ：tx z ，使得g = sg 。7 7 x ； 对于d 中的任意对象z 和任意箭头厂：tx z ，存在c 中的唯一箭头 广：x - - ) s z ，使得厂= z 。tf 。 偶序对( t ，s ) 称作伴随函子对，t 称作s 的左伴随函子，s 称作t 的右伴随函子。 1 0 华南师范大学硕士学位论文第2 章范畴论共代数的形式化基础 自然转换町称作伴随函子的元( u n i t ) ，称作伴随函子的兴：元( c o u n n ) 。 伴随函子的意义将在下节中讲到。 2 2 范畴中的泛结构 运用范畴论的语言，许多数学分支都可以归结成一些恰当的范畴，这些范畴 里通常都存在一些如初始对象和终结对象这样的“特殊的”对象，它们是符合某 个泛性质的结构。如果将范畴当作一类特殊的数学空间，函子当作它们之间保持 结构的转换，那么伴随函子可以看作一切泛性质的来源 下面我们给出几种泛性质的定义，符合这些性质的泛结构在计算系统的模型 化中经常用到。 2 2 1 积 给定范畴c 到它自身的积范畴的函子：c 专c c ，称作对角函子( d i a g o n a l f u n c t o r ) ，将c 中的任意对揪射为偶对( x ，x ) ，将c 中的任意箭头厂：x y 映射为箭头的偶对( 厂，厂) ：( x ，x ) j ( y ，】，) 。如果存在函子s ：c c c 为的右 伴随函子，那么对于c 中的任意对象蹴存在c 中的唯一的箭头f 。：x s z 使得 图2 - 3 可交换： ( y ，r )骂( s z ，s z ) ( 死。恐) ( z i , z ：) 图2 - 3 可交换图3 即对于c 中的任意对象x 以及箭头厂：x a 和箭头g ：x b ，如果存在c 中的唯 一箭头厂：x - - s ( a ，b ) 以及箭头p 。，p ：使得a 。f 。= 厂和p 2 。f 。= g ，那么函子s 1 1 华南师范大学硕士学位论文基于组件的嵌入式软件系统的其代数模型 是对角函了的左伴随函予。伴随函了对f s 1 的存在是范畴c 的一个泛性质，在 集合范畴中，笛卡尔积五五= ( ，吃) i 五 也五) 的概念符合这一泛性 质，所以通常用表示函子s 。对这一概念进行泛化得到范畴中的积的定义，形 式化的说， 定义2 7 范畴c 有积( p r o d u c t ) ，如果对角函子：c c c 有右伴随函子 。任意两个对象a 和b 的积为对象a x b 和一对投影舒头( p r o j e c t i o n ) 万l ：a x b a ，7 r 2 ：a x b 专b 。对于任何对象c 和从c 分别指向彳、b 的箭头 厂：c 寸a ，g ：c b ，存在唯一的从c 指向a xb 的箭头( ，g ) ：cj a xb ，称 狮g 的分割，使得图2 4 可交换： ( “，。 t 每 一卜二l 。jxb 立专劈 图2 - 4 可交换图4 。具有终结对象的有积范畴称为具有有限积的范畴。 这一泛性质可以通过箭头表达为： k = (