（计算机软件与理论专业论文）基于双代数的进程语义研究.pdf

论文题目： 专业： 硕士生： 指导教师： 基于双代数的进程语义研究 计算机软件与理论 陈鹤群 周晓聪副教授 摘要 双代数是同一基集上的代数共代数对，它结合了代数的构造和共代数的观察。计算 机科学中的许多概念都是构造与观察的结合体，如程序、进程、自动机等，都可用双代 数方法进行研究。目前，双代数方法已经被证明是研究基于状态系统的静态结构与动态 行为之间的关系及性质的可行途径。 由于程序的语法构造可以通过初始代数给出，程序的行为描述可以通过终结共代数 给出，因此可以在初始代数和终结共代数上构造双代数，组成一个双代数对，从而利用 初始代数和终结共代数的性质，研究该语言的形式语义。这种使用双代数结构研究形式 语义的的方法是共代数研究领域中一个最新的研究方向，已经应用在对进程、自动机等 的操作语义和指称语义的性质研究之中。 进程具有典型的代数与共代数性质，是一个双代数：它的语法表达式可以看成某个 基调上的项，这是代数结构；它的运行可以通过内部状态的变迁来展示其可观察行为， 这是共代数行为。因此，进程的语义也可利用双代数结构进行研究。 本文利用初始代数与终结共代数上的双代数结构，对进程的语义进行研究。文章首 先研究j r u t t e n 给出的双代数结构，探讨其成立的条件，并结合d t u r i 使用双代数研究 操作语义与指称语义间对偶性的一些成果，研究双代数结构在进程代数中的应用。文章 提出了一个能够用双代数结构描述的进程代数模型，分析了由该模型定义的进程的代数 与共代数特性，在研究变迁系统规范和定义出终结共代数上的代数操作的前提下，将这 个模型扩展到双代数结构中，并给出进程的操作语义和指称语义描述。文章最后使用初 始代数上的归纳原理、终结共代数上的共归纳原理，证明了一些进程性质，展示了双代 数语义方法的应用。 关键词：双代数、进程代数、进程语义、初始语义、终结语义 t i t l e ： m a j o r ： n a m e ： s u p e r v i s o r b i a l g e b r a i cs e m a n t i c sf o rp r o c e s s e s c o m p u t e rs o f t w a r ea n dt h e o r y c h e nh e q u n z h o ux i a o c o n g ia 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 ab i a l g e b r ac o n s i s t so fa na l g e b r a - c o a l g e b r ap a i rw i t hac o m m o nc a r r i e r i t c o m b i n et h en o t i o no fc o n s t r u c t i o na n dt h en o t i o no fo b s e r v a t i o n i nc o m p u t e r s c i e n c e ，m o s to b j e c t sa r ec o n s t r u c t i v ea n dh a v eo b s e r v a b l eb e h a v i o r s ，s u c ha sp r o - g r a m ，p r o c e s s ，a u t o m a t o n ，e t c t h e yc a lb es t u d i e dt h r o u g ht h em e t h o d so f b i a l g e b r a b i a l g e b r m cm e t h o d sw e r ep r o v e dt ob eae f f e c t i v ew a yt oi n v e s t i g a t e t h er e l a t i o n s h i pb e t w e e ns t a t i cs t r u c t u r ea n dd y n a m i c a lb e h a v i o ro fs t a t e - b a s e d s y s t e m s t h es y n t a xo fap r o g r a m m i n gl a n g u a g ei sai n i t i a la l g e b r a lw h i l et h es e m a n t i c s o f t h i sl a n g u a g ei saf i n a lc o a l g e b r a ap a i ro fb i a l g e b r ac a nb ec o n s t r u c t e db yg i v e n ac o a l g e b r ao ni n i t i a la l g e b r a ，a n daa l g e b r ao nf i n a lc o a l g e b r a i ft h eb i a l g e b r a p a i r sa r ec o n s t r u c t e du n d e rt h es a m ef u n c t o r ，t h ep r o p e r t i e so fi n i t i a la l g e b r aa n d f i n a lc o a l g e b r ac a l lb eu s e dt oi n v e s t i g a t et h es e m a n t i c so fp r o g r a m t h i sw a y i san e wi d e ai nt h et h e o r yo fc o a l g e b r a ，a n dh a sb e e na p p l i e di nt h es t u d i e so f o p e r a t i o n a ls e m a n t i c sa n dd e n o t a t i o n a ls e m a n t i c sf o rp r o c e s s ，a u t o m a t o n ，e t c p r o c e s sc a nb ec o n s i d e r e da sb i a l g e b r a ：a saa l g e b r a ，i t ss y n t a xe x p r e s s i o n s a r et e r m so fc e r t a i ns i g n a t u r e ；a sac o a l g e b r a ，i t sd y n a m i c a lb e h a v i o rc a nb e o b s e r v e dt h r o u g ht h et r a n s i t i o no fi n t e r n a ls t a t e t h u s ，t h es e m a n t i c so fp r o c e s s c a nb ei n v e s t i g a t e db yb i a l g e b r a i nt h i sp a p e r ，t h es e m a n t i c so fp r o c e s sa r es t u d i e db yu s i n gt h eb i a l g e b r a l c m e t h o d s f i r s t l y , t h eb i a l g e b r af r a m e w o r ki n t r o d u c e db yj r u t t e na r eg i v e n i n - c l u d i n gt h ec o n d i t i o n su n d e r w h i c hi n i t i a la l g e b r as e m a n t i c sa n df i n a lc o a l g e b r a s e m a n t i c sc o i n c i d e s e c o n d l y , ac c sl i k ep r o c e s sa l g e b r am o d e li sp r e s e n t e d ，a n d i v i t sa l g e b r aa n dc o m g e b r ap r o p e r t i e sa x ea n m y z e d t h i sm o d e lc a nb eu n i f i e di n t o t h ef r a m e w o r ko fb i a l g e b r aw h e nt h es p e c i f i c a t i o no ft r a n s i t i o ns y s t e mi sp u r et y f t f o r m a ti nw h i c hb i s i m n i a t i o na n dc o n g r u e n c ea r ec o i n c i d e t h i r d l y , t h ea l g e b r a o p e r a t i o n so nt h ec a r r i e ro ff i n a lc o a l g e b r aa r ed e f i n e d ，t h e nt h eo p e r a t i o n ms e - m a n t i c sa n dd e n o t a t i o n a ls e m a n t i c sw h i c he a c ho t h e rd u a la r eg i v e n a tl a s t ，t h e i n d u c t i o np r i n c i p l eg i v e nb yi n i t i a la l g e b r aa n dt h ec o i n d u c t i o n p r i n c i p l eg i v e nb y f i n a lc o a l g e b r ab y eu s e dt op r o v e dt h ep r o p e r t i e so fp r o c e s s k e yw o r d s ：b i a l g e b r a ，p r o c e s sa l g e b r a ，p r o c e s ss e m a n t i c s ，i n i t i a ls e m a n t i c s f i n a ls e m a n t i c s 第一章引言 本章首先介绍一些背景知识，包括共代数理论及其应用、双代数结构及其在形式语 义学中的研究，以及它们在进程代数领域中的应用情况和本文的项目背景；随后给出本 文研究的主要内容、方法与意义；最后是论文的结构安排。 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 em e t h o d s ) 则直到二 十世纪九十年代中后期才引起计算机科学工作者的广泛关注与研究，目前已经逐步应用 在对自动机、进程、对象等基于状态的系统的研究之中。 由于代数与共代数本质上都是集合及其上的操作，因此将代数与共代数方法融合 是一个必然的趋势，已经逐渐成为计算机科学中研究共代数方法的主流，其中对双代数 方法( b i a l g e b r a i cm e t h o d 8 1 的研究更是一种新的研究思路。双代数就是同一基集上的代 数共代数对，计算机中的很多概念都是构造与观察的整体，例如程序、进程、自动机等， 它们本质上都是双代数。因此我们可以利用代数的构造来研究这类基于状态的系统的 静态结构，以及用共代数方法来研究它们的动态行为。 1 1 1共代数理论及其应用 计算机科学中对共代数的研究可追溯到1 9 8 8 年，p a c z e l 等人首次使用共代 数方法给出了进程代数c c s ( c a l e u l u so fc o m m u n i c a t i n gs y s t e m s ) 的终结语义( f i n a l s e m a n t i c s ) t 1 】。 二十世纪九十年代以来，共代数已经在计算机领域得到了广泛的研究和应用，越来 越引起人们的关注。j a d d m e k ，h p g u r n m ，j p o w e r 2 k j 共代数的基础理论做了深入研 究，考察了终结共代数的存在及性质吼集合范畴上的共代数结构叭代数簇( v a r i e t y ) 与 2第一章引言 共代数簇( e o v a r i e t y ) 叽代数共代数与m o n a d c o m o n a d 关系【5 】等； j r u t t e n 将共代数方法应用于自动机理论和并发程序语义等的研究【6 ，7 ，8 】，并结合 偏序集、非良基集( n o n - w e l l - f o u n d e ds e t s ) 和度量空 e ( m e t r i cs p a c e s ) ，探讨了终结语义 的数学基础i o l ，最终奠定了泛共代数的基础i l o i 。 ls m o s s ，ak u r z ，d p a t t i n s o n 等关注于对共代数逻辑的研究1 2 ，1 3 ，1 4 ，1 5 ，1 6 】。h r e i c h e l ，b j a e o b s 等人则将共代数方法用于面向对象程序的规范与语义的研究旧”】。 目前国内从事这方面研究的还比较少，但也逐渐引起了一些学者的注意与研究，如 北京大学的张乃孝教授、上海交通大学的孙永强教授以及中山大学的周晓聪副教授领 导的研究小组等【1 9 ，2 0 , 2 1 , 2 2 】。 1 1 2双代数方法及其在形式语义学中的研究 与代数的广泛应用不同的是，计算机科学中的共代数方法研究仍然处于起始阶段， 其基础理论及应用方面都还需要更多的探索工作，因此难以在短期内像代数方法一样在 程序设计和软件开发中得到广泛应用。 目前一种新的研究思路是将代数与共代数融合起来，利用代数在构造上和共代数在 观察上的优势，对某个对象进行研究。由于代数与共代数都可以看成某个范畴上的对象 及射，因此在理论上这种融合是可行的。 双代数就是这样一种融合方法它涉及到两个函子( f u n c t o r ) ，其中代数函子给出了 基集元素的构造方法，而共代数函子给出基集元素的行为，这两个函子通过被称为分配 律( d i s t r i b u t i v el a w ) 的自然变换联系起来，这种分配律给出了元素的构造与产生合适行 为之间的关系。 更进一步，可以在初始代数和终结共代数上分别构造双代数结构。由于初始代数的 基集可以看成某个基调上的闭项的集合，终结共代数的基集可以看成某个语义域，因此 可以利用初始代数和终结共代数的性质，研究某种形式语言的形式语义。其中，语言的 构造可以通过初始代数给出，语义由终结共代数给出。我们可以根据初始性给出初始语 义( 指称语义) ，根据终结性给出终结语义( 操作语义) 。此外，还可以根据某个函子上 的最大互模拟关系是同余关系得到操作语义与指称语义之间的一致性。 计算机科学中对双代数的研究始于上个世纪九十年代，j r u t t e u 在其论文中【7 】利 用初始代数和终结共代数上的双代数结构给出了基本进程代数b p a ( b a s i cp r o c e s s a l g e b r a ) 的一种语义模型，并初步探讨了初始语义和终结语义的一致性。dt u r i 在 其研究的基础上从范畴论的角度上研究了程序的操作语义与指称语义之间的对偶 性盼2 4 , 2 5 】，他主要通过m o n a d 给出程序的语法和语义模型，并提出一种从语法m o n a d 导 出语义m o n a d 的方法，再证明由此得到的操作语义和指称语义是一致的。 1 。1 研究背景 3 此后，双代数经过m k i c k ，j p o w e r ，f b a r t e l s ，b j a e o b s ，b k l i n 等人的发展，在 程序和并发进程的语义、自动机与k l e e n e 代数等方面得到了应用，被证明是研究基于状 态系统的静态结构与动态行为之间关系及性质的可行途径口6 ，2 7 ，2 8 ，2 9 ，3 0 ，”】。 总的来说，将代数与共代数方法结合的双代数方法是共代数方法中最新的研究方向 之一，已经在进程、自动机等的操作语义与指称语义的性质研究得到了应用，具有十分 重要的理论意义和应用价值。 1 1 3共代数方法在进程代数领域的研究 进程代数作为研究并发进程的模型，其思想就是通过一些构造子( 空进程、前缀、 选择、并发等) ，用代数的方法描述并发进程，并用一系列等式给出其性质。 进程代数首先由b e r g s t r a 和k l o p 在1 9 8 2 年提出1 3 2 】，主要的模型有m i l n e r 的c c s ( c a l c u l u so fc o m m u n i c a t i n gs y s t e m s ) m3 4 】，h o w e 的c s p ( c o m m u n i c a t i n gs e q u e n t i a l p r o c e s s e s ) 3 5 ，3 q 和b e r g s t r a ，k l o p 的a c p ( a l g e b r ao fc o m m u n i c a t i n gp r o c e s s e s ) a t ，它们 本质上都是用公理化方法研究进程。 传统研究进程语义的办法是通过借助标号变迁系统、同步树等，利用结构化的归纳 定义方法，给出进程的操作语义( 即结构化操作语义) 。而由于进程本身的特殊性，其指 称语义被认为是难以描述的。 由于标号变迁系统本身就是一个共代数，而进程也属于基于状态的系统，因此可以 利用共代数方法对进程进行研究。计算机科学中利用共代数方法对进程进行研究要追 溯 1 1 j 1 9 8 8 年，a c z e l 在其开创性论文【1 1 1 中利用共代数方法，探讨了进程的语义域( 非良基 集) ，给出了c c s 的指称语义描述。 此后，许多学者都利用共代数方法对进程代数的语义进行了研究，u w o l t e r 利用共 代数描述c s p 中提出的各种概念3 9 】。b k l i n 的论文【4 q 讨论了共代数和共归纳原理在 描述进程等价方面的作用，特别是在迹( t r a c e ) 的等价性方面的作用。 j a c o b s 利用多项式自函子，将传统的标号变迁系统的迹语义推广到一般的共 代数h 1 】，并利用该多项式自函子的弱终结共代数给出了迹语义的合适描述。后 来，j a c o b s ；和i h a s u o 在文章4 2 冲将 4 1 f e 的迹语义限制在有限行为上，并指出，有限的 迹语义是惟一的，并且与某个终结共代数相关，而一般的迹语义的则与某个弱终结共代 数相关，并且不是惟一的。 1 1 4 双代数方法在进程语义中的研究 进程具有代数和共代数的性质，是一个典型的双代数：进程的语法表达式可以看成 某个基调上的项，由空进程和若干操作构造，这是典型的代数结构；进程的运行可以通 4第一章引言 过内部状态的变迁来展示其可观察行为( 可观察到的外部动作) ，这是共代数行为。因 此可以利用初始代数和终结共代数上的双代数结构，研究进程的操作语义和指称语义， 并借助归纳与共归纳原理，对其性质进行证明。 计算机中利用双代数方法研究进程的语义始于r u t t e n 6 ，1 ，在论文f 6 1 中，r u t t e n 使 用a c z e l 研究进程语义域的成果，给出了一种描述进程指称语义的方法。随后，r 1 t t t e n 在 论文7 1 中将之前的工作扩展到双代数结构上，利用有限幂集函子上存在终结共代数和 某个基调上的闭项是初始代数这一事实，给出了初始代数和终结共代数上的双代数结 构，并利用jfg r o o t e 和f v a a n d r a g e r 等人提出变迁规则的t y f t ，t y x t 格式【4 3 】，证明了由 该方法导出的操作语义等于指称语义，进一步，使用该模型对进程代数b p a 进行了初步 应用，给出了扩展的b p a 的操作语义和指称语义。 t u r i 在r u t t e n 的研究基础上，使用m o n a d 研究操作语义与指称语义之问的对偶性 时，也结合了进程代数b p a 作为例子。t u r i 的研究成果，可以作为使用双代数结构研究 进程代数的理论基础2 5 】。 b j a c o b s 在其最新书稿【4 4 】中利用有限幂集函子_ p 上的终结共代数，对一个简单的 进程代数模型给出了一种语义描述，并指出，如果两个待观察对象是观察等价的，则它 们映射到终结共代数上的同一个元素上。 总之，利用初始代数和终结共代数上的双代数结构研究并发进程的语义是可行的， 且具有十分重要的意义。它可以将进程代数本身的研究与使用共代数方法对进程语义 的研究统一起来，给出一个一致的理论框架，并能够结合归纳和共归纳原理的特点，证 明进程的性质。 1 2 本文的主要研究内容 使用双代数方法研究形式语义特别是进程的语义是计算机科学中共代数方法的最 新研究方向，具有十分重要的理论意义和应用价值。j r u t t e n ，d 2 h r i 等人的工作奠定 了其理论基础，证明了该方法是可行的。 同时，我们也看到，虽然j r u t t e n ，d t u r i 和b j a c o b s 等人都提出用双代数结构研 究进程代数的设想，并做了一些初步研究。但是由于他们工作的侧重点不同，并没有深 入研究其在进程代数中的应用。 j r u t t e n 主要致力于共代数应用的理论基础研究，在【7 】中给出的模型只是一个简单 的例子，并没有深入探讨在更复杂的进程代数模型的应用；d t u r i 的论文主要着重操作 语义与指称语义的对偶性研究：而b j a c o b s 侧重于确定型模型的研究，对于具有不确定 性质的进程，他只是简单地利用了j r u t t e n 和d t u r i 的研究成果，直接构造出了终结共 1 3 研究意义 5 代数上的代数操作。 本文以r u t t e n ，t u r i ，j a c o b s 等人的工作为基础，并结合w o l t e r 等人的方法，使用双代 数方法，对进程的语义及应用作更为深入的探讨。论文的主要研究内容包括： 1 双代数结构研究：研究j r u t t e n 和d t u r i 给出的双代数结构及其成立的条件，其 中包括初始代数及其上的共代数操作、终结共代数及其上的代数操作、变迁系统 规范、互模拟与同余关系之间的联系等。 2 双代数在形式语义学中的应用研究：探讨双代数结构在形式语义学的应用，包括 操作语义与指称语义的对偶性，初始语义与指称语义、终结语义与操作语义之间 的关系，以及它们在描述语义上的差异等。 3 建立进程上的双代数结构：在分析几种进程代数模型特点的基础上，给出一个适 合用双代数结构描述的进程代数模型，并在该模型上建立双代数结构，研究进程 的各种操作，进程的代数与共代数性质，进程的变迁规则格式及性质等。 4 进程语义研究：利用双代数在形式语义学中的研究成果，给出上述模型的操作语 义和指称语义描述，并使用归纳与共归纳原理，将研究的结果用于验证进程的性 质。 本论文选题在广东省自然科学基金项耳“基于共代数方法的软件体系结构及其应用 研究”( 项目编号：0 3 1 5 4 2 ，经费6 万元) 及国家自然科学基金项目“共代数方法及其在形 式化描述和验证软件体系结构中的应用”( 项目批准号：6 0 4 0 3 0 1 3 ，经费6 万元) 的支持 下，围绕共代数方法及其应用的这一领域进行研究。 1 3 研究意义 j r u t t e n ，d t u r i ，b j a c o b s 等人的工作证明，利用双代数方法研究进程代数的语义， 特别是指称语义，具有十分重要的意义： 1 菇代数方法是计算机科学中理论研究的一个热门方向，它为研究基于状态的系统 行为提供了一致的数学理论基础。利用共代数方法研究进程，可以提供一种新的 研究思路，与传统的进程代数研究方法互补。 2 双代数方法结合了代数与共代数研究的成果。使用双代数方法研究进程的语义， 可以利用初始代数和终结共代数的性质，把使用最小不动点和标号变迁系统研究 进程语义的方法结合起来，统一到一个理论框架之中。 6第一章引言 3 目前归纳原理已经广泛应用于各种场合，而共归纳原理作为其对偶概念，人们对 它的了解还不够深入，目前还未得到广泛应用。利用双代数方法研究进程的语义， 一方面可以利用终结共代数上的共归纳原理，证明一些进程等式，为共归纳原理 的应用提供一些实例；另一方面还可以利用共归纳原理在某些方面的优势，结合 传统的归纳证明原理，提供一种新的证明思路。 4 进程演算很难有一个合适的形式化模型，研究进程的语义特别是研究其指称语义 是一件比较困难的事情。利用双代数方法研究进程的语义，能够给出一种具有对 偶性质的操作语义和指称语义描述。 此外，使用双代数方法研究进程语义的成果还可为其他研究领域所借鉴，例如对自 动机、流等的研究。 1 4 论文的总体结构 本文共分为六章，各章的主要内容为： 第一章引言：给出本文的研究背景、研究内容、研究意义及论文的总体结构。 第二章预备知识：简单介绍本文所涉及的基础知识。 第三章代数与共代数：介绍代数与共代数的相关知识，包括代数与共代数的定 义、互模拟与同余关系、初始代数与终结共代数、归纳与共归纳原理、初始语义与终结 语义等。 第四章双代数结构：主要研究了j r u t t e n 和d m l r i 给出的双代数结构，包括双代 数的定义、初始代数和终结共代数上的双代数结构、初始语义与终结语义的一致性、变 迁系统规范的格式及其性质等。 第五章进程语义：为本文的核心部分，主要给出一个适合用双代数结构描述的进 程代数模型，并探讨由该模型所定义的进程的代数与共代数特性，然后利用变迁系统规 范将这个模型扩展到双代数结构中，给出了进程的初始语义与终结语义，最后使用归纳 与共归纳原理将研究成果应用到对进程性质的证明中去。 第六章结束语：对全文进行总结，并提出进一步研究的问题和方向。 第二章预备知识 本章介绍论文涉及的一些相关知识，首先对范畴论的历史和思想进行了简单介绍， 然后介绍了良基集与非良基集，并进一步给出了不动点定理，最后讨论了结构化操作语 义及其在进程中的应用。 2 1 范畴理论 范畴理论是上一世纪四十年代中后期，由s e i l e n b e r g 和s m a cl a n e 等为研究同调 代数而创立的一个抽象代数分支，它的主要思想就是用范畴、函子、自然变换、极限等 基本概念，统一研究某些数学结构( 如群、环、代数、共代数、拓扑空间、域等) 及其性 质。 范畴由对象及对象问满足一定性质的射组成，对象和射的基本构造可以通过积、共 积、均等射、共均等射、回拉、外推等来完成，不同的范畴可以用函子相联系，函子与函 子间的映射可以通过自然变换来完成，一个函子还可能存在着对应的伴随函子。 范畴论的研究成果对许多数学和计算机科学中的分支都产生了深远的影响，本文涉 及到的代数与共代数，都可以从范畴论的角度得到清楚的解释。代数与共代数都定义在 某个函子上，任何代数以及它们之间的同态都构成了一个范畴，初始代数就是该范畴的 初始对象，任何共代数以及它们之间的同态也构成了一个范畴，终结共代数是该范畴的 终结对象。此外，代数与共代数之间的对偶性可以根据范畴论得出，共代数的许多性质 可以从代数对偶得到。 有关范畴理论的基础知识，这里就不做详细介绍，可见 4 5 ，4 6 】。 2 2 良基集与非良基集 良基集( w e l l f o u n d e ds e t s ) 是指满足良基公理的集合，目前已经广泛用代数理论中。 根据良基公理，传统意义下的集合就是良基集，初始代数可利用良基集进行描述。非良 7 8 第二章丽备知识 基集n o n w e l l - f o u n d e ds e t s ) 由反良基公理给出，是共代数理论的一个重要概念，同样， 终结共代数也可利用非良基集进行描述。 非良基集的概念主要由p a c z e l 在1 9 8 8 提出，在f 1 1 中，他利用非良基集为m i l n e r 的并 发进程模型c c s 提供了一种语义描述，其工作的一个重要贡献是将进程理论中基于互 模拟的证明原理与共代数中基于共归纳的基本原理联系在一起，导致了人们在程序设计 语言的语义及逻辑等领域对非良基集做进一步的研究。 2 2 1良基集 首先来看良基集的定义，其中为传统集合论中的隶属关系( m e m b e r s h i pr e l a t i o n ) ： 定义2 2 1 一个集合x 被称为良基定义( w e l l f o u n d e dd e f i n e d ) 的当且仅当它是空集 或者在关系下有最小元。 上述定义表明了良基集的元素问不存在无穷的链z 2 z 。z o ( 其 中z 。为x 中的元素) 。 定义2 22 所有良基定义的集合构成的类称为泛良基类( u n i v e r s eo f w e l l - f o u n d e d s e t s ) 。 w = x i x 是良基集 下面给出良基公理( f o u n d a t i o na x i o m ) ，其中泛类定义为所有集合构成的类，这里 讲的集合指传统意义下的集合。 公理2 23 泛类是泛良基类。 上述公理说明了传统意义下的集合都是良基集，即集合的元素间不存在无穷 的链。有趣的是，由所有良基集的真子集构成的类汐( ) 也是泛良基类，因为它也是 由所有良基集构成的类，即： 汐( ) = w 因此，有如下定理： 定理2 2 4 所有良基集构成的泛类是类与函数范畴上的幂集函子的初始代数。 2 2 2 非良基集 每一个集合都可以看成一个n l ( g r a p h ) ，即如果对于集合a o e 的两个元素z ，y ，如果 有y z ( e 3 9 集合论中的隶属关系) ，则在图中存在一条以z 为起点，为终点的边。每 一个图都惟一对应一个集合。 下面给出图的装饰( d e c o r a t i o n ) 的定义： 2 3 不动点定理 9 定义2 2 5 一个图的装饰是一个函数d ，它将图中的每一个节点映射为一个集合， 定义如下： d ( z ) = d ( y ) iy z ) 下面给出反良基公理f a n t i _ f 0 u n d a t i o na x i o m ) ： 公理2 2 6 每一个图都有惟一的装饰。 上述公理说明了非良基集的存在，例如对于只有一个节点和一条源和目的都是该节 点的边的一个图，根据装饰的定义，可以得到： d ( x ) = d ( z ) = d ( z ) ) ) 这就允许存在这样一个集合，满足n = n ) 。 所有非良基集构成的泛类是有限幂集函子上的终结共代数。 定理2 2 7 所有非良基集构成的泛类是类与函数范畴上的幂集函子的终结共代数。 因此，根据上面的定理，可以利用非良基集给出终结共代数描述。 2 3 不动点定理 不动点定理通常用来证明一些递归定义的方程有惟一解，传统研究形式语义的方 法使用不动点定理来证明递归等式存在惟一解。进程代数也借助了最小不动点给出递 归定义的进程表达式的解。m c b h e n n e s s y , j w d eb a k k e r 等人利用度量空间和偏序集 研究并发语言时，也使用了不动点定理证明观察语义( o b s e r v a t i o n a ls e m a n t i c s ) 与复合语 义( c o m p o s i t i o n a ls e m a n t i c s ) 间的一致性【4 7 4 s 。 在后文可以得到，初始代数是其对应函子上的一个最小不动点，终结共代数是其对 应函子上的一个最大不动点。在研究初始语义和终结语义时，通常不必使用不动点定 理，而是利用初始代数导出的惟一映射和到终结共代数的惟一映射给出语义。 下面介绍t a r s k i 的不动点定理【4 9 l ，首先给出完全格的定义： 定义2 3 1 一个偏序集( d ，e ) 是一个完全格( c o m p l e t el a t t i c e ) 当且仅当对所有x d ，其上确界u x 和下确界n x 存在。 可以看到，完全格有最小元j _ = n d 和最大元t = l i d 。 1 0 第二章预备知识 定义2 3 2 令( d ，e ) 为一个偏序集，函数，：d d 是单调( m o n o t o n i c ) 的仅当对所有 的d ，d ， d ed ，爿f ( d ) e f ( d ) 一个元素d d 是，的一个不动点( f i x e dp o i n t ) 当且仅当d = ，( d ) 。 下面定理来1 刍t a r s k i 的不动点理论： 定理2 3 3 ( 不动点定理) 令( d ，e ) 为一个完全格，：d d 是一个单调函数，那 么门亍一个最大不动点。和一个最小不动点 z r n a ：c = u 。d lz e ，( z ) ) 。= 厂 扣d i m ) ez ) 我们可以利用最小元和最大元求得最小不动点和最大不动点 定理2 3 4 令( d ，e ) 为一个有限的完全格，：d d 是一个单调函数，那么，上的 最小不动点可以由根据下列式子求得： 其中，m 为某个自然数，并且，o ( j - ) = 上，广“( j - ) = f ( f ”( 上) ) 。同样地，虽大不动点也可 以通过下式求得： z m 。= 严( t ) 其中，m 为某个自然数，并且，o ( t ) = t ，”1 ( t ) = f ( f “( t ) ) 。 2 4形式语义 在计算机科学中，早在上个世纪六十年代，人们就开始意识到对程序设计语言和规 约描述语言给定精确语义的重要性。而形式语义学就是利用数学工具来精确描述程序 设计语言和计算模型的语义的一个理论计算机科学领域。 最直接的形式语言例子是程序设计语言，当描述一个程序设计语言的时候，我们不 但需要描述它的语法，而且还需要描述它的语义。通常，程序员在学习一个程序设计语 言的时候，会先学习它的语法和一些例子，然后编写出符合语法规则的程序。这些程序 就是由语法构造出来的，其语义可以通过程序在计算机中的执行来表达。 e l 前应用得比较广泛的主要有三种描述语义方法： 2 4 形式语义 操作语义：程序的语义可以通过在一台抽象计算机上逐步执行给出，它 主要关注计算的过程。 指称语义：程序的语义可以通过映射到一个数学模型给出，这个模型表 示了程序执行的结果，因此它主要关心执行的结果，而不是过程。 公理语义：程序的语义可以通过使用逻辑系统，利用一些公理或规则来 对程序性质的推导给出，它能够反映执行过程中一些被忽略的方面。 本文主要关注操作语义和指称语义，在后面可以看到，它们都可在范畴论的抽象层 次上，使用代数与共代数作为工具进行研究，指称语义可以根据初始代数的初始性给 出，也叫初始语义，操作语义可以根据终结共代数的终结性给出，也叫终结语义。更进 一步，利用某个函子上的最大互模拟关系是同余关系，还可以得到操作语义和指称语义 之间的对称性。 下面首先来看操作语义和指称语义是如何对程序的语义进行描述的。 2 4 1 操作语义 在操作语义中，主要关心一个程序的执行过程，而不是其最终的执行结果。也就是 说，关心的是程序语句在执行过程中，机器内部状态的变化。一般的，常用 k h l ，y ”吨，】 来表示机器内部状态，其中z 的值为u ，”的值为忱，等等。 操作语义主要有两种： 自然 五义( n a t u r a ls e m a n t i c s ) ：主要关心的是多步执行的结果。 结构化操作i 五义( s t r u c t u r a lo p e r a t i o n a ls e m a n t i c s ) = 主要关心的是每一 步执行的过程。 下面例子来自【5 0 ，较好地说明了操作语义的思想： 例子2 4 1 考虑下面程序语句： z ：= z ；o ：= ；掣：= z 上述语句是将z 的值与l 的值交换。为了描述程序的运行状态，我们用( n s ) 表示程 序p 在s 状态下的语义。因此，上述语句在初始状态扛一5 ，y 一7 ，z o 】下的运行过程如 1 2 下 z ：= x ；x ：= ；y ：= z ，陋h5 ，y _ 7 ，z ho 】) 扣：= ；：= z ，陋h5 ，y h7 ，z h5 ) ( y ：= z ，陋一7 ，y 一7 ，z 一5 】) 陋一7 ，y 一5 ，= 一5 】 第二章预备知识 2 4 2指称语义 操作语义关心的是程序的执行过程，而指称语义则关心程序的执行结果，即将程序 看成一个从初始状态到终结状态的函数，并且利用一个指称函数将语法构造映射成为一 个数学对象( 通常是一个表示程序执行结果的函数) 。 指称语义的特点是指称函数是复合定义的，即( i ) 每个成分都有对应的指称物；( i i ) 复 合成分的指称只依赖于它的子成分的指称。 指称函数可以通过定义类似下面的函数来实现： 函。：s t m _ ( s t a t eqs t a t e ) 它将一个程序语句映射成为一个偏函数。下面利用【5 0 】给出的例子，说明如何对上一个 例子中的语句给出指称语义： 例子2 4 2 对于上述语句，定义指称语义如下 赋值语句z ：= ”定义如下： ；操作定义如下 根据上面定义，可以得到 。陋：= l sy = s y = v 如果y z 否则 - i s l ；s 2 l = t 鼠4 s 2 io 鼠4 s l l t s z 4 名：= z ；z ：= ；y ：= z l = 5 d 。4 ：= z lo t s z 4 z ：= y l 。函。4 。：= z l 2 5 结构化操作语义与进程 因此有： 函。呤：= $ ；。：= 弘y ：= z i 扛h5 ，y h7 ，z h0 ) = 如：= z i 。t s ：枷z ：= y lo 岛，肛：= z 扛一5 ，y ”7 ，z h0 ) = 函。晒：= ：l 。5 枷。：= 砌扛h5 ，y ”7 ，z 一5 ) = s d s 瞄：= z 扛h7 ，y ”7 ，z h5 ) = ( x h7 ，y ”5 ，z h5 ) 2 5结构化操作语义与进程 1 3 结构化操作语义( s t r u c t u r a lo p e r a t i o n a ls e m a n t i c s ，简称s o s ) 主要是利用与语法构 造类似的归纳定义方法，为描述程序设计语言和规范描述语言的操作语义提供了一个框 架，广泛应用在对并发进程语义的研究中。这种研究方法主要有两个方面的优势： 第一、应用广泛，几乎所有现有的语言都能用这种方式描述语义。 第二、可以利用结构化归纳法对程序进行分析。 在对并发进程的语义的研究过程中，虽然d eb a k k e r ，z u c k e r ，h e n n e s s y 和a b r a m s k y 等 人对并发进程的指称语义做了大量的研究5 2 t4 7 】，但是指称语义还是被认为难以用来 描述并发进程的语义删，而结构化操作语义由于其直观性和灵活性，被认为是研究并发 进程语义的理想模型。 在对并发进程的研究中，结构化操作语义通常利用一个标号变迁系统产生，其中状 态是在某一代数基调上构造的闭项，状态之间的变迁关系可以由一系列的规则给出，例 如规则 煮葺 ， 嚣+ 与o 说明了只要z 7 成立，就有z + y 二z 成立，其中z ，y ，一都是闭项。 在后文中可以看到，由结构化操作语义给出的变迁系统规范如果符合一定的格式， 使得其对应的共代数上的最大互模拟关系是同余关系，我们就可以利用双代数结构，给 出一种具有对偶性质的初始语义和指称语义描述。 第三章代数与共代数 代数( a l g e b r a ) 就是集合以及集合上满足一定性质的操作，例如群、环、域、向量等。 泛代数则在更高的抽象层次上，从不同的代数结构中提取出它们的共同性质进行研究， 它对各种结构进行了统一、简明的表示，并且所得的结果可用于对其它新的代数结构的 研究中，我们通常采用范畴论来对代数进行抽象、简明的定义。 在计算机科学中，常用代数理论来研究抽象数据类型( a b s t r a c td a t at y p e ) ，因为抽 象数据类型实际上也是在一数据集合上给出一组满足某些性质的操作，本质上是一种 代数。代数上的操作通常具有口：t a a 的形式，在抽象数据类型中，a 可看成数据类 型，o - 可以看成构造子。 代数方法对于数据结构的研究起到了非常重要的作用，但是它对于刻划基于状态的 动态系统是比较困难的。对于这类型的系统，以往的方法大多数是用自动机或者变迁系 统来进行描述，通过多年的研究，人们发现，这种基于状态的系统可以利用共代数方法 研究。 共代数( c o a l g e b r a ) 本质上也是集合及其上满足一定性质的操作，但是与代数不同的 是，共代数x 上的操作