（计算机软件与理论专业论文）基于共代数的流演算研究.pdf

论文题目： 专业： 硕士生： 指导教师： 基于共代数的流演算研究 计算机软件与理论 崔振 周晓聪副教授 摘要 代数方法从“构造”的角度研究抽象数据类型的语义，并且已经在抽象 数据类型、计算机语言的形式语义等领域有了广泛的应用。而代数的对偶概 念共代数，从上世纪9 0 年代以来，才得到计算机学者的广泛关注，并逐步 成为理论计算机科学的研究热点之一。共代数从“观察”的角度考察系统及 其性质，并已经在自动机理论、并发程序的形式语义、面向对象程序的规范 等领域有了广泛的应用。 共代数理论作为新兴的理论，正在发展之中，许多方面还不成熟，要对 共代数理论作全面研究目前仍有不小的困难，流共代数作为一种特殊的共代 数，其性质相对简单，但通过对它的研究有助于认识并探讨一般的共代数理 论。 流共代数存在唯一到终结共代数的同态射，而终结共代数的状态集可以 看作一系列流的集合。本文正是基于终结共代数研究了流演算，包括实数域 上流演算和比特流演算，并用程序实现流的一些操作，例如卷积、混合积等， 特别地，在j r u t t e n 等人工作的基础上进一步探讨了实数域上流演算在差分 与微分方程中的应用和比特流在电路分析与设计中的应用。在流演算的基础 上介绍了加权流自动机以及其在计数难题方面的应用，进一步，介绍了有理 流与加权流自动机之间的相互转换，并设计、实现有理流到加权流自动机的 转换。 关键词：共代数，流演算，有理流，比特流，加权自动机 t i t l e ： m a j o r ： n a m e ： s u p e r v i s o r ： r e s e a r c ho ns t r e a mc a l c u l u sb a s e do nc o a l g e b r a c o m p u t e rs o f t w a r ea n dt h e o r y z h e n c u i v i c ep r o f e s s o rx i a o c h o n gz h o u a b s tr a c t a l g e b r m cm e t h o d si n v e s t i g a t es e m a n t i c so fd a t at y p e sf r o mt h ec o n s t r u c - t i v ep o i n t s ，a n dh a v eb e e na p p l i e di nm a n yr e s e a r c hf i e l d s ，f o re x a m p l e ，d a t a t y p e s ，s e m a n t i c so fc o m p u t e rl a n g u a g ee t c a st h ed u a lc o n c e p t so fa l g e b r a s ， c o a l g e b r a i cm e t h o d s ，w e r en o tn o t i c e db yc o m p u t e rs c i e n t i s t su n t i lt h e1 9 9 0 s ， a n dg r a d u a l l yb e c a m ea na c t i v ea r e ao ft h e o r e t i c a lc o m p u t e rs c i e n c e e r o mt h e o b s e r v a b l ep o i n t s ，c o a l g e b r a mm e t h o d si n v e s t i g a t es y s t e m s ，a n dh a v eb e e n a p p l i e di nm a n yr e s e a r c hf i e l d s s u c ha sa u t o m a t at h e o r y ls e m a n t i c so fc o n - c u r r e n c y , s p e c i f i c a t i o n so fo b j e c t o r i e n t e ds o f t w a r ea n d s oo n a san e wt h e o r y , c o a l g e b r a i cm e t h o d sa r ed e v e l o p i n g ，a n ds t i l ln o tm a - t u r e i fo n ew a n t st oh a v eac o m p r e h e n s i v er e s e a r c hi nt h e m ，t h e r ee x i s tm a n y d i f f i c u l t i e s a sas p e c i f i cc o a l g e b r a ，s t r e a mc o a l g e b r ai sr e l a t i v e l ys i m p l e ，a n d c a nh e l pu n d e r s t a n da n ds t u d yg e n e r a lc o a l g e b r a i cm e t h o d s t h e r ei so n l yo n em o r p h i s mf r o ms t r e a mc l a l g e b r at of i n a lc o a l g e b r a ， i nw h i c hs t a t e sa r ev i e w e da sac o l l e c t i o no fs t r e a m s o nt h eb a s i so fc o a l - g e b r a ，w en o to n l ys t u d ys t r e a mc a l c u l u si nt h i sp a p e r ，i n c l u d i n gs t r e a m so f r e a ln u m b e r sa n db i t s t r e a m s ，b u ta l s oi m p l e m e n ts o m eo p e r a t i o no fs t e a r n s ， f o re x a m p l e ，c o i n v o l u t i o np r o d u c t ，s h u f f l ep r o d u c te t c ，p a r t i c u l a r l y , b a s e do n j r u t t e n sw o r k ，w ef u r t h e re x p l o r et h ea p p l i c a t i o u so fs t r e a m s ，f o re x a i n - p l e ，s t r e a m so fr e a ln u m b e r sa r ea p p l i e di nd i f f e r e n c ee q u a t i o n s ；b i t s t r e a m si n d i 百t a lc i r c u i t s t h e nw e i n t r o d u c ew e i g h t e ds t r e a ma u t o m a t aa n di t sa p p l i c a - t i o n si nc o i n d u c t i v ec o u n t i n g f h r t h e rm o r e ，w ei n t r o d u c et h et r a n s f o r m a t i o n b e t w e e nr a t i o n a ls t r e a m sa n dw e i g h t e da u t o m a t a ，a n df u r t h e rd e s i g na n d i m p l e m e n tt h et r a n s f o r m a t i o nf r o mr a t i o n a ls t r e a m st ow e i g h t e da u t o m a t a 中山大学硕士学位论文基于共代数的流演算研究 k e y w o r d s ：e o a l g e b r a ，s t r e a mc a l c u l u s ，r a t i o n a ls t r e a m ，b i t s t r e a m s ，w e i g h t e d a u t o m a t a i v 第一章绪论 1 1 研究背景及意义 在计算机科学中，代数方法( a l g e b r a i cm e t h o d s ) 从构造( c o n s t r u c t i v e ) 的角 度研究抽象数据类型的语义，并且已经在抽象数据类型、计算机语言的形式语 义等领域有了广泛的应用。作为代数的对偶概念，共代数( c o a l g e b r a ) 也是集合 及其上满足一定性质的操作，其操作具有n ：x x 】x xj 如的形式。在 计算机科学研究中，通常将共代数看成具有内部状态的系统，x 是系统所有可 能状态构成的集合，操作n 看成是对系统的观察( o b s e r v e ) 。在这种意义下，共代 数方法从观察的角度描述诸如对象、自动机、进程、软件构件等基于状态的系 统【1 。正因为对象、自动机可以看成具有内部状态的系统，j r u t t e n 将共代数理 论称为系统的一种通用理论【2 卜 上世纪9 0 年代以来，共代数方法才得到学者的关注，并逐步成为理 论计算机科学的研究热点之一。1 9 8 8 年，p a c z e t 等人第一次使用共代数 方法给出了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 l 中进程的终结语义( f i n a l s e m a n t i c s ) 3 l 。9 0 年代初，j r u t t e n 等将共代数方法用于自动机理论和并发程 序语义等的研究阻，5 1 ，而h r e i c h e l ，b j a c o b s 等人则将共代数方法用于面 向对象程序的规范与语义的研究【6 ，7 ，并进一步开发了对面向对象规范进 行描述与验证的【8 ，9 l o o p ( l o g i co fo b j e c t o r i e n t e dp r o g r a m m i n g ) t 具。此 外，j r u t t e n 等人还对共代数的基本和数学基础进行了深入探讨，从而奠定了 泛共代数理论( u n i v e r s a lc o a l g e b r at h e o r y ) 的基础【2 1 。 2 0 世纪9 0 年代中后期以来，共代数方法得到了计算机科学工作者的广泛关 注与研究。从1 9 9 8 年开始，国际上每年都召开有关计算机科学中的共代数方法 的学术会议c m c s ( i n t e r n a t i o n a lw o r k s h o po nc o a l g e b r a i cm e t h o d 8i nc o m p u t e r s c i e n c e ) ，从2 0 0 5 年开始，该会议与w a d t ( w o r k s h o po na l g e b r a i cd e v e l o p m e n t t e c h n i q u e s ) 在单数年合并为c a l c o ( i n t e r n a t i o n a lc o n f e r e n c eo na l g e b r aa n d c o a l g e b r ai nc o m p u t e rs c i e n c e ) ，这些会议展示了计算机科学中的代数及共代 数方法研究的最新进展。 共代数理论作为新兴的理论，正在发展之中，许多方面还不成熟，要对共 中山大学硕士学位论文基于共代数的流演算研究 代数理论作全面研究目前仍有不小的困难，流共代数作为一种特殊的共代数， 其性质相对简单，但通过对它的研究有助于认识并探讨一般的共代数理论。近 年来，j r u t t e n 等人致力于研究流共代数上的流演算( c a l c u l u so f s t r e a m s ) 及其 在求解差分与微分方程 1 0 ，1 1 、计数难题【1 2 、信号流图与电路设计 1 3 ，1 4 】以 及软件构件和连接件性质研究【1 5 1 等方面的应用。 流共代数存在惟一的到终结共代数的共代数同态，这个性质使得我们可以 使用共归纳( c o i n d u c t i v e ) 原理定义以终结共代数为目标的一些函数，通过这样 的方法可以进一步研究流共代数所描述的系统的性质。共归纳原理是将共代数 方法应用于系统的规范描述等领域的重要理论基础，它应用于流共代数，促进 对流共代数的研究，同时，从侧面演示出了共归纳原理的优势。共归纳原理的 基础是流共代数到终结共代数存在惟一的同态射，这也体现了终结共代数的重 要性。流共代数的终结共代数的状态集可以看作一系列流的集合，本论文是在 流演算的基础上做了更加深入的探讨，从而让我们更加深入的理解流共代数， 并帮助我们认识和探讨一般的共代数理论。 1 2 国内外研究现状 共代数理论已经在自动机理论【1 6 、并发程序的形式语义 17 】、面向对象程 序的规范【1 8 ，7 】等领域有了广泛的应用。流共代数这种特殊的共代数，很多理论 都可以由共代数衍生而来，但流共代数又有着特殊的性质，这需要我们进一步 的研究。而最重要的是考虑流共代数的终结共代数，j r u t t e n 基于终结共代数 研究了流演算( s t r e a mc a c u l u s ) 1 0 ，1 1 1 ，提出了基于形式变量x = ( 0 ，1 ，0 ，) 的 一系列流演算，例如卷积( c o i n v o l u t i o np r o d u c t ) 、混合积( s h u f f l ep r o d u c t ) 等，而 其中最具有共代数特点的是运用了共归纳原理定义了它们。j r u t t e n 给出了许 多运算规则，并提出用流演算来求解行为差分方程与微分方程，这是一种新颖 的方法。另外，在流演算的基础上给出了流自动机的相关理论，特别地给出了 有理流( r a t i o n a ls t r e a m ) 转化为自动机的重要定理，并提出了解决关于组合数方 面的问题，尤其是共归纳计数( c o i n d u c t i v ec o u n t i n g ) 【1 2 ，1 9 。 流演算的一个重要应用是分析与设计数字电路( d i g i t a lc i r c u i t ) 。j r u t t e n 提出基于流演算的流电路( s t r e a mc i r c u i t s ) ，定义了乘法器( m u l t i p l i e r ) 电路、加 法器( a d d e r ) 电路、拷贝( c o p i e r ) 电路、寄存器( r e g i s t e r ) 电路四种基本流电路， 并在此基础上介绍了流电路的复合以及带有反馈环的流电路，研究了电路 2 中山大学硕士学位论文 第一章绪论 与流( 尤其是有理流) 的关系，通过例子给出了如何运用流演算来分析流电 路【2 0 ，1 3 】。j r u t t e n 在早期给出了类似数字电路的流电路，但这些流电路表示 的流是基于实数域上的流，也就是说电路不是描述布尔值上的运算，并且加法 器电路也不产生进位，只是两( 多) 个流简单的相加，但这些为后来的研究做好 了准备。 j r u t t e n 在文章 2 0 ，1 3 1 中给出了一些基本的流电路，但对于描述现实 中各种复杂的数字电路还远远不够，需要进一步的工作。早在上世纪9 0 年 代， w e g e n e r 就研究了基于布尔代数上带有反馈与存储的电路。后来，j v u i l l e n m i n 对数字电路中基于比特流( b i t s t r e a m ) 代数结构进行了系统性的研究f 2 1 ，2 2 ， 2 3 1 ，提出了电路的三种代数结构：布尔代数、模一2 代数( m o d u l o - 2a l g e b r a ) 与2 一原子代数( 2 一a d i ca l g e b r a ) ，并基于这些代数结构对组合电路进行了研 究。j r u t t e n 在v u i l l e n m i n 等人研究的基础上，定义了基于流的克林代数( k l e e n e a l g e b r a ) 结构，给出了这四种代数结构问关于流演算的一些混合法则 14 ，并 通过互模拟( b i s i m i l a t i o n ) 关系和共归纳原理证明了这些演算法则。j r u t t e n 在 文章【2 4 1 中把电路每个输入端输入一系列的高低电平看作是时间上的一个流， 对应于输出也是一个流，两个流之间对应于一个函数，称为流函数( s t r e a m f u n c t i o n ) ，在数字电路中称为逻辑函数。j r u t t e n 定义了基于比特流的基本 门电路：连接c o n n e c t ) 和断开( d i s c o n n e c t ) 电路、拷贝( c o p y ) 门、或o r ，s u m ) 门、 与a n d ) 门、非( i n v e r t e r ，n e g a t i o n ) 门、寄存门( r e 幽t e r ) ，并介绍了带有反馈环 与有寄存功能的电路，另外提出了线性电路( f i n e a rc i r c u i t ) ，着重研究了线性电 路与有理流的关系。 流演算的另一个重要应用是研究软件构件与连接器性质。f a r b a b 等提出 了时间数据流( t i m e sd a t a s t r e a m ) ，把时间与数据一起看作一个流，并进一步定 义了各种连接器( c o n n e c t o r ) ，又称为信道( c h a n n e l ) ，而其中运用了共归纳做为 连接器的推导方法，证明了一些连接器之间的等价性。时间数据流由时间流与 数据流这两对流构成，而通常最能体现此特征的是数据流网络，f a r b a b 就把时 间数据流应用于数据流网络中协议的证明 1 5 】。 另外，还有一些流的研究，比如u h e n s e l 、b j a c o b s 用原型证明系统( p r o t o t y p e v e r i f i c a t i o ns y s t e m ) 2 5 验证流的操作的性质等。 3 中山大学硕士学位论文基于共代数的流演算研究 1 3 论文主要内容与组织 本文是在范畴论和共代数的基础上，用共代数方法，特别是运用共归纳方 法，对流演算进行探讨，并在流演算的基础上讨论它的应用。特别地，本论文讨 论了流与加权自动机之间的相互转化，并实现了有理流到加权自动机的转化。 论文的组织结构如下： 第一章绪论，介绍论文研究的背景，意义与当前现状。 第二章流共代数基础知识，介绍范畴、函子等范畴论基本概念，共代数、共 代数同态、终结共代数、互模拟等共代数理论的核心概念，然后在共代数基础 上介绍流共代数的相关概念。 第三章实数域上流演算及其应用，主要是介绍实数域上流的一些操作，并 进一步探讨在差分方程与微分方程中的应用，特别地，用程序实现了流演算。 第四章比特流流演算及其应用，介绍了基于比特流上四种不同的代数结构 及比特流在分析与设计电路中的应用，特别地，给出了许多关于比特流应用的 例子。 第五章流与加权自动机之间的转换，介绍了单元流和多元流加权自动机及 其应用，然后探讨了流与加权自动机之间的转化，特别地，用程序实现了有理 流到加权自动机的转换。 最后是结束语。首先总结了本论文所做的工作，然后指出一些值得继续探 讨的问题与需要完善的工作等。 4 第二章流共代数基础 2 1概述 共代数是代数的对偶概念。代数方法从构造的角度研究抽象数据类型的语 义，而共代数则是从观察的角度来描述基于状态的系统。例如，有穷链表是通 过给出空链表与向链表添加元素这两个操作构造得到的，可以用归纳原理定义 链表的操作以及证明相关的性质；无穷链表可以通过观察得到，一种观察是查 看链表的头元素，另一种观察是查看其余元素组成的链表，可以用共归纳原理 定义链表的操作以及证明相关的性质。 共代数理论作为新兴的理论，正在发展之中，要对共代数理论作全面的研 究有很大的困难，而流共代数作为一种特殊的共代数，其相关的性质比较简单， 通过对流共代数研究有助于我们认识并探讨一般的共代数理论，并且现有的共 代数理论也可以适当地衍生到流共代数中，以帮助我们理解流共代数。 流共代数的转换结构具有这样的形式：x d x ，表示从一个状态 可以观察到的值以及到达的下一个状态。前面所举的无穷链表可以看作是一个 流共代数，x 表示所有链表所组成的集合，d 是表示链表中的元素值( 观察值) ， 那么链表有两种观察，一种是得到头元素，另一种是去掉头元素后所形成的链 表。 流共代数作为共代数一种特殊的形式，因此我们在介绍流共代数理论前介 绍相关共代数理论，例如共代数定义、共代数同态、互模拟、终结共代数等一些 基本概念，同时所介绍的共代数是基于某个范畴上的共代数，所以我们也介绍 与范畴相关的理论，比如范畴定义、函子等一些概念。 在这一章，我们将要着重研究流共代数的一些理论，为后面章节作准备， 比如流共代数定义、流共代数同态、流共代数互模拟、流的终结共代数等一些 核心概念。另外还可以研究流共代数的( 共) 积、( 共) 均等射、回拉、外推，流共 代数与同态，流共代数与观察等价，简单共代数，扩张共代数，共自由共代数， 共等式规范等方面的内容，这些都可以从共代数相关理论衍生而来，请参考文 章 2 6 ，2 7 ，2 8 ，2 9 ，3 0 1 但所得的结论中真正针对流共代数特性的结果并不多，还 有待进一步挖掘。 中山大学硕士学位论文基于共代数的流演算研究 2 2 流共代数定义 流有两个操作，一个操作得到流当前状态所能显示的值，另一个操作则 让流转入下一个状态。因此流系统是三元组( x ，v a l u e ：x d ，n e x t ：x x 1 ，这里x 是流所有可能状态的集合，操作v a l u e ：x d 返回流当前状 态所能显示的值，这些值具有类型d ( 属于集合d ) ，操作n e x t ：x x 使 得流转入下一状态。外界只能通过操作n e x t 使得流转入下一状态，但是 无法看到状态本身的值。因此从某一内部状态z 开始，外界能够看到的就 是v a l u e ( x ) ，v a l u e ( n e x t ( x ) ) ， o f 牡e ( 几e 耐( n e 戚( z ) ) ) ，这样一个集合d 上元素的无 穷序列。在数学上，函数v a l u e 和n e x t 可合成一个函数，记为= ( v a l u e ，n e x t ) ： x - + d x x ，它定义为v x e x ，( v a l u e ，n e x t ) ( x ) = h e a d ( x ) ，n e x t ( x ) ) 。由集合x 和x 上 的观察组成的流系统，就是流共代数。在给出流共代数的具体定义之前，我们 先介绍有关范畴( c a t e g o r y ) 与共代数的理论。 2 2 1范畴与函子的基本概念 范畴理论是上一世纪4 0 年代中后期，由s e i l e n b e r g 和s m a cl a n e 等为研究 同调代数而创立的一个抽象代数分支，它以范畴、函子、自然变换等为基本概 念统一地研究某些数学结构及其性质2 6 1 。范畴理论可以说是一种语言，一种描 述数学结构的抽象语言。以范畴理论为工具，可以将某些数学结构的性质加以 泛化而推广到其它数学结构，也可以将某些数学性质具体从而丰富到某些数学 结构以推广该数学结构的应用范围。进一步，通过范畴理论中的通用概念，可 以将许多不同数学分支联系在一起结合起来进行研究。作为- - f 7 抽象的数学工 具性的理论，范畴理论已经广泛应用在各个数学分支，如同调代数、代数几何、 代数拓扑、代数k 理论。随着理论计算机科学的发展，特别是域论理论、直觉逻 辑、类型理论等的深入研究，范畴理论在计算机科学领域的应用也日益广泛。 具体地说，范畴是一个数学系统，包括对象( o b j e c t ) 和射( m o r p h i s m ) 两个数 据、一些操作以及这些操作所满足的公理。范畴上的操作包括： 1 ，每个射，有两个操作：d o m 和c o d ，d o m ( f ) 是范畴c 的对象，称为，的域 ( d o m a i n ) 或源( s o u r c e ) ，c o d ( f ) 也是范畴c 的对象，称为，的共域( c o d o m a i n ) 或目 标( t a r g e t ) 。通常用：f ：a b 表示射，这时a 就是，的域，而b 是它的共域； 2 每个对象a 有一个恒等射( i d e n t i t ym o r p h i s m ) i d a ：a a ； 6 中山大学硕士学位论文 第二章流共代数基础 3 对于两个射，和g ，如果c o d ( f ) = d d m ( 9 ) ，则它们有复合( c o m p o s i t i o n ) 记 为g 。，或g f 。 范畴的操作必须满足下面的公理： 1 恒等射是复合操作的恒等元，即对任意的f ：a 一口，有i d b 。f = f = f0 i d a ； 2 复合操作是可结合的，即对任意的f ：a b ，g ：b g ，h ：g d ， 有h ( g f ) = ( h g ) f ：a d ( 从而可记为h g f ：a d ) 。 最常见的范畴是集合范畴丘f ，它的对象是集合，射是集合之间的函数，复 合是通常的函数复合，很容易验证它确实是一个范畴。两个范畴间的关系可以 通过函子来描述，函子是保持范畴结构的映射。 定义2 1 说f 是从范畴c 到范畴口的函子( f u n c t o r ) ，记为f ：c 一口如果满 足： ( i ) 对范畴c 的每个对象a ，指派了范畴d 的一个对象与之对应，将这个对象 记为f ( a ) ： ( i i ) 对范畴c 中的每个的射f ：a b ，指派了范畴口中的一个射：f ，： f a _ f b ： ( i i i ) f ( i d a ) = i d f ( a ) ，即函子保持恒等射； ( i v ) f ( go f ) = f ( g ) o f ( ，) ，即函子保持复合。 a l， b f a lf， f b 图2 1 ：函子的定义 2 2 2 共代数与共代数同态 共代数是代数的对偶概念，是集合及其上满足一定性质的操作。但与代数 不同，共代数x 上的操作具有q ：x x 1 x 2 五。的形式，x 是系统所 有可能状态的集合，而“可以看作系统的一个观察，也就是说共代数是从观察的 角度探讨系统的性质。尽管共代数是代数的对偶概念，但并不能将代数中的定 7 中山大学硕士学位论文基于共代数的流演算研究 理转化为对偶定理直接为共代数所运用，其中重要的一个原因是，目前还有许 多代数性质依赖于集合范畴的性质，而这些性质在集合范畴的对偶性质中并不 成立【3 1 1 。下面给出共代数的范畴论定义： 定义2 2 给定任意范畴c 。范畴c 上的自函子n ：c c 的共代数，简 称n 一共代数，是二元组( x ，) ，其中x 是范畴c 的对象，称为该n 一共代数的载 体( c a r r i e r ) ，：x _ n x 是范畴c 的射，称为该q 一代数的变迁射( t r a n s i t i o n m a p ) 。 从q 一代数( x ，f ) 到q 一代数( y i ( ) 的q 一共代数同态是范畴c 的射，：x y ，且满 足( o ，= n ，o f ，如交换图2 2 所示： l 上 图2 2 ：共代数同态 对于共代数( x ，) ，若m ：y x 是在基范畴c 的单射，且存在变迁射( ： y q y ，使得m 成为同态，则称( y ) ) 是( x ，) 的子共代数，这时射m 不一定是 唯一的。但如果给定自函子q ：c c 保持单射，那么对任意单射m ：y x = u ( x ，) ，至多存在一个结构射( ：y q y 使得m 成为同态m ：( ) 一( x ，f ) 。 2 2 3 流共代数定义 基于共代数的定义，我们可以看到流共代数是基于某个集合d 上的流 共代数，它是一个二元组( x ，f ：x d x x ) ，其中x 是集合，称为该流共代数 的基集，而：x d 烙是函数，称为该流共代数的转换结构。两个流共代 数( x ，：x - * d x ) n ( y ，( ：y d y ) 之间的同态是函数，：x y ，且满足交 换图2 3 ，也就是说有eo ，= ( i d d f ) o ，其中j d d 是d 上的恒等函数。 事实上，流共代数( x ，f ：x - - * d x ) d p 的转换结构：x - + d x x 可看作两 个函数v a l u e x ：x _ d 和n e x t x ：x - x ，其中v a l u e x 返回流共代数在当前 状态下的值，而n e x t x 给出流的下一状态。例如我们设d = 1 ，2 ，3 ，x = o ，b ，e ，d ) ，v a l u e ( a ) = v a l u e ( b ) = 1 ，v a l u e ( c ) = v a l u e ( d ) = 2 ，n e x t ( a ) = n e x t ( b ) = c ，n e x t ( c ) = a ，n e x t ( d ) = d ，这就定义了一个流共代数。我们再 8 中山大学硕士学位论文第二章流共代数基础 x 一 叫 d x - y j( d y 图2 3 ：流共代数同态 给一个流共代数，设d = ( 1 ，2 ，3 ，4 ，y = u ， ，叫 ，图2 4 也给出了一个流共代 数( ) 。 图2 4 ：流共代数示例 z 现在可以定义函数，：x y 为f ( a ) = i ( b ) = u ，f ( c ) = v ，f ( d ) = ”，则，是同 态，：( x ，) 一( y i e ) 。 2 3 流共代数互模拟 互模拟是共代数理论的核心概念之一，最早是在进程代数中定义和研 究3 2 1 ，也是进程代数以及各种并发模型的核心概念。但是目前对于互模拟这个 概念，人们仍然没有能够很好地推广到一般范畴。互模拟，表面上来看是指两 个系统之间的互相模拟，以致于从外部来看，在某种程度上，它们是行为等价 的( b e h a v i o r a le q u i v a l e n c e ) 。行为等价是一个直观的描述，是指两个系统( 诸如对 象、进程等) 从观察者的角度看可以互相模拟对方的行为。 2 3 1 共代数互模拟 给定集合范畴上的自函子q ：且t 一t ，两个共代数( x ，) 和( y ，( ) 之间 的互模拟( 关系) ，是关系t x x y ，且存在变迁射x ：t n t 使得坐标投 影函数奴：t x ，虹：t y 都是同态( 图2 5 ) 。自然，当( x ，f ) = ( y 】( ) 时， 称t 为( x ，) 上的互模拟( 关系) 。 9 中山大学硕士学位论文基于共代数的流演算研究 0le q x 气i f 凹面一q y 图2 5 ：互模拟关系 下面来看一个互模拟关系的例子 3 3 】： 例子2 1 标号变迁系统。一标号变迁系统：标号集l = a ，6 ) ，状态集x = x o ，x l ，z 2 ) ，变迁关系兄由图2 6 左图给出。另一系统的状态集y = y o ，鲈1 ，y 2 ， 变迁关系s 由图2 6 右图给出。 图2 6 ：标号变迁系统示例 令关系t = ( z o ，y o ，( o ，抛) ，( x l ，y i ) ，( x 2 ，可1 ) ) ，可验证t 是互模拟。实际 上，从。o 开始，第一个系统所能执行的动作是a ( a b ) ，即执行一次a ，再可执行多 次n 6 ( 即执行多次a ，然后执行b ，然后再循环) ，这也可看作是第一系统以z o 为 起始状态能接受的语言，不难发现第二个系统若以珈为起始状态可接受相同的 语言。 2 3 2 流共代数互模拟 基于共代数互模拟，两个流共代数( x ，f = ( v a l u e x ，n 8 z 坟) ) 和( ( = ( v a l u e r ，n e x t y ) ) 的互模拟，是一个关系_ r 彤，并且要满足：对任意的( z ，f ) r 有：( i ) v a l u e x ( x ) = v a l u e r ( y ) ；( i i ) ( n e x t x ( x ) ，n e x t r ( y ) ) e r 。 现在我们给出一些例子。设d = 0 ，1 ) ，下面给出了d 上三个流共代数： 1 0 中山大学硕士学位论文 第二章流共代数基础 不 x = ( x = 忙l ，z 2 ，x 3 ，z 4 ) ，& = ( v a l u e x ，礼e 茁奴) ) 的状态转换图如图2 7 所 0 型1 型0 - 。 图2 7 ：流共代数( x ，) y = ( y = 1 ，抛，y 3 ，y a ，y 5 ，y o ，知= ( v a l u e y ，礼e 茁如) ) 的状态转换图如 图2 8 所示： 芝逻兰兰! 箩 图2 8 ：流共代数( y ) 矗) z = ( z = z l ，砘) ，z = ( v a l u e z ，n e x t z ) ) 的状态转换图如图2 9 所示 图2 9 ：流共代数( z ，翻) 对于上面三个流共代数，不难得到： r 1 = ( z 1 ，z 1 ) ，( x 2 ，z 2 ) ，( x 3 ，z 1 ) ，( x 4 ，z 2 ) ) 是x 和z 之间的互模拟 r 2 = ( 掣l ，z 1 ) ，( y 2 ，z 2 ) ，( y 3 ，z 1 ) ，y 4 ，z 2 ，z 1 ) ，( y o ，。2 ) ) 是y 和z 之间的互 模拟； r 3 = 忙l ，x 3 ) ，( x 2 ，茁4 ) ，( x 3 ，z 1 ) ，( x 4 ，z 2 ) ) 是x 上( 即x 与x 之间) 的互模 拟； 吼= ( l ，y 3 ) ，( y 2 ，y 4 ) ，( y 3 ，蜘) ，( y 4 ，舶) ，( y 5 ，y 1 ) ，( y o ，驰) 是y 上的互模拟。 进一步地，可以看到上述兄l 是x 和z 之间的惟一互模拟，而r 2 是y 和z 之 间的惟一互模拟。凰和r 4 说明某个共代数上的互模拟关系不一定是等价关 系，凰甚至不是对称关系。 中山大学硕士学位论文 基于共代数的流演算研究 我们知道互模拟是一个关系，那么对于关系上的运算是怎样的呢? 可以证 明下面的结论： 1 如果r 是互模拟，那么兄_ 1 也是一个互模拟关系。 2 如果尼黾互模拟，那么对称闭包s ( r ) 也是一个互模拟关系。 3 如果r _ 黾互模拟，那么传递闭包t ( r ) 也是一个互模拟关系。 4 两个互模拟关系的复合也是互模拟关系。 2 4 流的终结共代数 任意共代数( 墨) 到终结共代数都存在惟一的同态射，并且同态射给出了 共代数的所有可观察的行为，这使得对任意x e x ，终结共代数都存在一个观察 者与x 有相同的可观察行为，所以我们可以将终结共代数看一个标准的观察者， 它能观察到所有共代数的行为，从而我们可以其它共代数的行为定义为终结共 代数所观察到的行为，这对我们研究一般的共代数有非常重要的意义。 2 4 1 终结共代数定义 终结共代数是一个共代数，并且每一个共代数到它都有且仅有一个同态射。 具体地说，给定函子t ：j e 一& t ，t 上的终结共代数是z = ( z ，o l z ：z t z ) ，它 满足对任意t 上的共代数x = ( x ，a x ：x z x ) 都存在惟一的同态i x ：x z 。 2 4 2 流的终结共代数 集合d 上的流共代数的终结共代数是( d “，( h e a d ，t a i l ) ) ，其中： d n = ，：n d ) = 印盯1 l v i e n ，a i e d 协= c r 0 盯1 盯。e d n ，h e a d ( a ) = 印，t a i l ( a ) = 口l - 即任意d 上的流共代数( x ，f = ( v a l u e x ，n e x t x ) ) ，( x ， ) 到( d “，( h e a d ，t a i l ) ) 的 惟一同态是b e h x ：x d ”，v x e x ，h e n ，b e h x ( x ) ( n ) = v a l u e x ( n e x 发( z ) ) 。而 流也可以看作共代数，换句话说，流的终结共代数也是( d n ，( h e a d ，n 引) ) 。 直观地，可认为共代数同态f ：( x ，f ) 一( y ，( ) 保持可观察的行为，即，( z ) 与x 有着相同的可观察行为，从而不妨将，( 。) 认为是对。的观察，( x ) 的行为就 是z 可观察到的行为。因此，b e h x ( z ) 与z 具有相同的可观察行为，且对z 的任意 1 2 中山大学硕士学位论文 第二章流共代数基础 观察，或者说任意同态，：( x ，) 一( r ( ) ，( z ) 的行为也能被b e h z ( x ) j 观察到，因 为b e h x ( x ) = b e h y ( f ( x ) ) ，从这个意义我们说，6 e h ( 茁) 是状态z 的所有可观察行 为。 实际上，终结共代数( d n ，( h e a d ，t a i l ) ) 是具有这种性质的惟一共代数，即： 1 共代数( x ，f ) 存在到终结共代数同态b e h x ：( x ，) 一( d “，( h e a d ，t a i l ) ) ， 这使得对任意x c x ，终结共代数都存在一个观察者6 e 奴( z ) 与z 有相同的可观察 行为； 2 对( x ，f ) 的任意其他观察者g ：( x ，f ) 一( ) ，b e h x ( x ) 能通过b e h y 观察 n g ( x ) 所观察到的。的所有行为，目v b e h x ( x 1 = b e h y ( g ( x ) ) 。 2 4 3 共归纳与终结共代数 归纳原理和归纳证明是将代数理论应用到计算机科学，而共归纳定义和共 归纳证明是将共代数方法用于系统的规范描述等领域的重要理论基础【1 。共归 纳的基础是终结共代数的性质：任意共代数到终结共代数都存在惟一的同态射， 这使得终结共代数的最大互模拟关系是等价关系，从而要证明终结共代数中的 两个元素相等，只需证明两个元素是互模拟关系即可。 集合d 上的流共代数存在终结共代数( d “，( h e a d ，t a i l ) ) 。终结共代数上的任 意一个元素f 流) o 有： h e a d ( o ) = 口( o ) ，t a i l ( a ) = ( 口( 1 ) ，口( 2 ) ，) 一( o ) ( 或h e a d ( a ) ) 称为盯的初值，( 盯( 1 ) ，盯( 2 ) ，) ( 或t a i l ( o ) ) 称为盯的导数 ( d e r i v a t i v e ) ，也可记为口7 或口( 1 ) 。那么流口表示为：口= ( 口( o ) ，口( 1 ) ，口( 2 ) ，) = ( s o ，8 l ，8 2 ，) ，o - = ( s l ，s 2 ，) 。进一步，可以定义盯( 。) p 的南阶导数) 为： 盯( o ) = 盯 盯( + 1 ) = f 盯( 七) 1 7 现在考虑怎么证明两个盯和下相等。一种办法是利用数学归纳法，即证 n o ( o ) = 7 - ( o ) ，且当口( 凫) = r ( ) 是有口( + 1 ) = r ( + 1 ) ，但是在很多情况 下，我们并不能为流。写出一个通项，因此使用数学归纳法在由盯( ) = 丁( ) 推 出口( + 1 ) = t ( k + 1 ) 时可能很难成功。而共代数方法提供了另外一种方法， 即共归纳证明原理，即要证明a = r ，只要证明数列盯和7 - 是互模拟的。说关 系r d n d n 是互模拟关系，如果协，r d n ， r - 盏含：( i ) o ( o ) = 1 3 中山大学硕士学位论文基于麸代数的流演算研究 r ( 0 ) ；( i i ) r 。说盯和r 是互模拟的，记为盯一r ，如果存在互模拟关 系尉睫得 r 。由于d “是终结共代数，因此它上面的最大互模拟关系是 恒等关系，即盯一丁意味着盯= r ，即下面的共归纳定理： 定理2 1 如果两个流盯和7 - 互模拟：盯一下，那么对任意的n 0 ，口( n ) 1 - ( n ) 进一步，盯= 丁，即盯1 - = 盯= 丁。 上述共归纳原理利用互模拟来定义终结共代数中的元素相等，我们在后面 流演算中演示了这种共归纳原理的应用。一般地，用共归纳方法证明问题有下 面两个步骤： ( i ) 适当构造一个