（应用数学专业论文）lts中的弱不变量与限制乘积.pdf

摘要本文在文献【1 】， 2 】的框架下，首先，对带不可观察迁移的l t s 给出了弱不变量的定义，讨论了其性质及与其它概念( 包括弱互模拟、 弱同态、不变量等) 之间的关系。其次，本文还引入了迁移系统的限制乘 积概念，并以此为工具，研究了弱互模拟和弱不变量之间的相互转化。 最后，本文利用余代数的可观察部分概念，把弱不变量定义推广到一般 余代数上，并且证明了只要选择合适的观察者，余代数中弱不变量定义 和l t s 中弱不变量定义是一致的。 关键字：弱互模拟；弱不变量；抽象；迁移系统的限制乘积 i i a b s t r a c to nt h eb a s eo fr e f e r e n c e 1 】a n d 【2 】，f i r s to fa l l ，t h i sp a p e rg a v et h e d e f i n i t i o no fw e a ki n v a r i a n tf o rl t sw i t hh i d d e nt r a n s i t i o n ，d i s c u s s e di t sc h a r a c - t e ra n dt h er e l a t i o nb e t w e e nw e a ki n v a r i a n ta n do t h e rn o t i o n s s e c o n d l y , t h i sp a p e r i n t r o d u c e dt h ec o n c e p to fr e s t r i c tp r o d u c to ft r a n s i t i o ns y s t e m ，a n dt o o kt h i sa s i m p l e m e n t ，s t u d i e dt h em u t u a l l yt r a n s i t i o nb e t w e e nw e a kb i s i m u l a t i o na n dw e a k i n v a r i a n t f i n a l l y , t h i sp a p e ru s e dt h en o t i o no fo b s e r v a b l ep a r to fc o a l g e b r a st o d e f i n ew e a ki n v a r i a n t a n dp r o v e dt h a tf o rt h er i g h tc h o i c eo fo b s e r v e r ，t h en o t i o n s o fw e a ki n v a r i a n tf o rc o a l g e b r a sa n dw e a ki n v a r i a n tf o rl t sc o i n c i d e k e y w o r d s ：w e a kb i s i m u l a t i o n ；w e a ki n v a r i a n t ；a b s t r a c t i o n ；r e s t r i c tp r o d u c t o ft r a n s i t i o ns y s t e m 首都师范大学位论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究 工作所取得的成果。除文中已经注明引用的内容外，本论文不含任何其他个人或 集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体， 均已在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：i 1 渤像 i 、， 日期：吖年钥日 首都师范大学位论文授权使用声明 本人完全了解首都师范大学有关保留、使用学位论文的规定，学校有权保留 学位论文并向国家主管部门或其指定机构送交论文的电子版和纸质版。有权将学 位论文用于非赢利目的的少量复制并允许论文进入学校图书馆被查阅。有权将学 位论文的内容编入有关数据库进行检索。有权将学位论文的标题和摘要汇编出 版。保密的学位论文在解密后适用本规定。 学譬论文作者签名：，j 弗命 f 日期：司年6 月f 日 1 引言 在编程语义中，传统上都用韧始代数来建模有限数据类型( 比 热有限漉) 瀚，鹣，后寒终络余代数放溪来建模无限效蠡类螯戮余代 数是代数的对偶，它适用予某些类型的自动机【8 】，而且非常适用于迁移 系统和动力系统( 比如确宠性自动机) 泛代数的纛个基本概念；代数， 代数懿嚣态、鬻余对应余代数，余我数瓣霹态，互模羧麓瑟纛者是泛 余代数理论的基本组成部分代数上的些结果在余代数上都有对偶形 式l l o 】，并产生了一系列新的结果，比如，子余代数的格和互模拟，单余 代数程余努缡l l l 1 3 l 等。荧于余我数瓣基本蠢容z z 材。m r u t t e n 等绘了 详细的介绍，觅参考文献【3 1 f 一余代数( a ，o ) 由一状态集a 、一迁移结构口：a ，f ( a ) 组 成f 其孛f ：s e t - - - - 4s e t 必函子。蠡谈迁移系统罴一类特殊懿余健数。 函子f ( a ) = 0 a 的余代数就是标识迁移系统余代数通常被视为迁移 系统的推广，这种推广最火的好处就魑产生出许多标准的概念，比如： 麓模羧【1 4 一l 镶，爨察等稔f l t l 鬟器攘态运算【l 翻簿。燕是毒夔簇念， 比如弱互模拟，弱不变量概念在迁移系统中比较赢观，但在余代数中就 不容易表述文献1 定义了余代数的w 观察部分，并且利用此您义给出 了余健数弱鬟模羧兹定义。褥出灵要选择会透约鼹察者，余代数弱互模 拟概念和标记迁移系统中的弱互模拟概念是一致的本文受此启发，把 驹不变量定义推广到一般余代数上 下甏分缨本文懿续搀褰主要蠹骞。第二郝分是襄各懿谈，黠本 文中将要用到的范畴论、余代数、l t s 的有关概念和结果做一个简要的 介绍第三部分是本文的主要结果本文在文献【2 】的框架下，首先， 砖蒂不可观察迂移豹l t s 定义了弱不变量壤念，礤瓷了弱不变爨关予交 和并、关于像和原像以及荧于乘积封闭等性质及与其它概念( 包括弱互 模拟、弱同态、不变量等) 之间的关系其次，本文借助于抽象概念，通 2 过转化标识迁移系统，得出弱不变量和不变量可以相互表示此外，本 文还引入了迁移系统限制乘积的概念，并以此为工具，研究了弱互模拟 和弱不变量之间的相互转化最后，本文利用文献【1 】1 中给出的余代数的 可观察部分概念，把弱不变量定义推广到一般余代数上，并且证明了， 只要选择合适的观察者，余代数中弱不变量定义和l t s 中弱不变量定义 是一致的 3 2 预备知识 先简单介绍阅读本文时所需要的有关预备知识，包括范畴论、 余代数、l t s 、不变量等方面的有关概念和结论所列结论的详细证明 见参考文献【2 j ，1 3 ， 2 0 1 2 1范畴论及余代数的基本概念和结论 范畴c 由一个对象类和一个态射类构成用s e t 表示集合范畴， 它的对象是集合，态射是集合间的映射，态射的合成是集合间映射的合 成。f 一余代数上的恒等函数也是余代数同态，两个同态的复合还是同 态，则f 一余代数和f 一余代数同态也构成一个范畴c o a i g ( f ) ，也记作 s e t f 本文中还用到了范畴r e l ，它的对象是集合，态射是二元关系， 态射的合成是关系的复合 f ：s e t + s e t 为一函子，f 一余代数( f 一系统) ( a ，a ) 由一 集合a 、一函数a ：a ，f ( a ) 组成集合以叫做该系统的承载者，也 叫作状态集函数。叫f 一迁移结构 ( a ，n ) 和( b ，p ) 是两个f 一余代数，f 为任一函子函数，：a + b 叫做f 一余代数同态( f 一同态) ，如果它满足f ( f ) o a = 卢o ，即下图 交换 j 4 lb r e l 一自函子g ：r e l ，r e l 是s e t 一自函子f ：s e t s e t 的扩 p 一 一n可 la q 以 4 张，如果满足 ( 1 ) 对所有集合s ，g ( 研；f ( s ) ( 2 ) 对所有函数，：x + y g ( 9 r ，( ，) ) = 9 r ，( f ( 川 关系子就是指可以被r e l 一自函子扩张的s e t 一自函子 f , g 为关系子关系族玎= ( o x f ( x ) g ( x ) ) 叫做自然关系当 且仅当对所有的函数，：x + y ，下图在i l e l 中交换 f ( x 卜_ 里以( x ) 附4卜 f c y ) 彳；- g ( y ) 只g 为关系子若存在一自然关系q = ( f i x e ( x ) g 僻) ) 满足 所有的f i x ( x 0 ) 在r e l 中都是满的则g 就叫做f 的自然因子记作 g f 为表示卵的作用，也记成r l ：g f 关系子f 的自然a c c e 啪r 就是指关于所有函数自然的关系族 口= ( 叽) s “，叫做s k i p 如果对每一f 一余代数一4 = ， 啾a a 为一二元关系，且该关系族满足对任意的f 一余代数a b 及 它们之间的同态，：a b ，下列图形在r e l 中交换 a lb “ll 即 a 了一b p 为f 的自然a 删，= 为任意f 一余代数可证得 5 纵= ( 纵o n ) 盯为s k i p 关系其中( 一) 盯表示二元关系的自反传递闭包 纵又叫做p 推出的典范s k i p f 为一关系子，f 的观察者为一三元组o = ，其中矿：岔i d f 即伊是i d f 的因子，且满足所有的d 都是关 系子，p 是f 的自然a c c e d e r 上述定义中就是用来定义f 的可见部分以下用0 来表示乘 积函子i i 科函子f 的观察者d 推出典范s k i p 关系，o a = ( 似o a ) 盯 那么关于观察者0 ，余代数的可观察部分定义为： 对f 一余代数4 和观察者0 = ，关于因子 g 。的a 的可观察部分为n 3 。a g i ( a ) 满足下图在r e l 中交换 g ( a ) 卜 a 矿 a f 言而( 箭f ( a ) 即0 t = o ( u a f ( ) ) 。 o l t a 关于全部观察者，n 的可观察部分就是关系o f a h i j ( 以) 即q 。a o ( a ) 余代数a 的可观察部分就记为 利用余代数的可观察部分的概念，文献【1 】给出了余代数弱同态和 弱互模拟的定义 对于观察者d ，函数，：a + b 是f 一余代数a ，8 间的弱同 态，如果满足下图在r e l 中交换 6 o ( a ) 酉7 i o ( b ) 对于观察者d ，关系0 a b 是f 一余代数a g 间的弱互模 拟，当且仅当存在关系1 0 o ( o ) ，满足下图在r e l 中交换 x 卫l - 0 ky 且有下列结论； 命题2 1 1 4 1 ：( 1 ) 函数。，：a + b 的图9 r f ( f ) 是f 一余代数a b 间的 弱互模拟当且仅当，是4 到b 的弱同态 ( 2 ) 弱互模拟的逆也是弱互模拟 2 2l t s 和不变量的有关概念 7 沿用文献【1 】1 ，【2 】的记号设l 是动作集合，f l 表示隐藏 ( 不可观察) 动作，0 = l r ) 为可观察动作的集合一个标识迁移系统 ( l t s ) 由状态集x 、标识集l 和迁移关系r x l x 组成$ l y 表示由z 到y 的f 一迁移，即 t ，z 号y 表示由。 经过一系列r 一迁移( 包括空迁移) 迁移到y 定义2 2 1 1 ：设x 和x 是同一标识集工上的标识迁移系统 r x x 是两l t s 间的弱互模拟，如果r 满足下列条件： ( 1 ) 若 r ，考哥一，z 0 ，贝03 y x 满足 y 考上考口且 r ( 2 ) 若 冗，y = 串上考暑，则矗x 满足z 爿 号一且 r ( 3 ) 若 r ，$ 昔一，则3 y x 7 满足y 昔y 且 r ( 4 ) 若 r ，y 考y 则9 x x 满足z 昔一且 r 定义2 3 1 j ：隔同态】设 ， 是标识迁移系统， ，：x + y 是弱同态，如果，满足如下条件：对v x x ，z 0 ， ( 1 ) 对“x ，若z 哥上号一，则m ) 每上葺m ) ( 2 ) 对y ，若m ) 弓上辱y ，则j 。ex ，满足z 爿上 爿一且，( ) = y ( 3 ) 对v x x ，若茹哥z ，贝0i ( x ) 考，( 一) ( 4 ) 对y ，若，( z ) 爿玑则矗。x ，满足z 号一且，p ) = f j 设 是一l t s ，谓词p x ，o r x 定义为： o p ( x ) 争( 工，v 一x z z ) = 争p ( z ) 若p o f ，则谓词p 是不变量 8 不变量的充要条件是p 为子余代数，即存在唯一余代数结构p + f ( p ) ，使得包含映射m ：p + x 为余代数同态 p竺x ll c f ( p 卜丽f ( x ) f l 】，【2 】，【4 】 本文中其它未加定义的概念、记号和相关结论可见参考文献 3 主要内容 3 1弱不变量 9 对于带不可观察迁移的l t s ，首先给出它的弱不变量的定义 设 是一个l t 8 ，p x 定义3 1 ：谓词o x 定义如下：对比x ，o 。p ( ) 当且仅 当； ( 1 ) 唧二，“x z 爿上等，) 号p f ) ( 2 ) ( r e x z 考一) = p ( ) 若p 0 。p ，则称p 是x 中的弱不变量。 容易得到： 命题3 2 t 设 是个l t s ，p x 则p 是弱不变量当 且仅当以下两个条件成立， ( 1 ) w p , v o ，( 。号警一) 净p ( 2 ) v 2 ：p ，0 毋z ) = 争一p 由命题3 2 ，我们可以得出l t s 的弱不变量的另一种等价定义 上面给出了l t s 的弱不变量的定义，以下讨论弱不变量的性 质，因为弱不变量是不变量概念的推广，所以它也具有不变量所具有的 性质，如命题3 3 、3 4 和3 6 所示，它关于交和并、关于像和原像以及关 于乘积封闭此外。由弱不变量的定义，可以知道不变量是弱不变量的 一个特例 命题3 3 。设 是一个l t s , v i ，只x 是弱不变量， 则u 斛只和n k ，只也是弱不变量 特别的，x ( i = o 时的并) 和t ( i = 口时的交) 是弱不变量 1 0 证明：只证明u 斛只的情形，i 1 州只的情形类似 设z u 。j 只，且z 爿上爿一则3 i j ，使得ze b ，因 为弓是弱不变量，有e b ，则u 州只 z = 专一的情形是类似的 所以u 科只是弱不变量 命题3 4 。设，： 是弱同态 1 ) 若p x 是弱不变量，则f ( p ) y 也是弱不变量 2 ) 若q y 是弱不变量，则i - 1 ) x 也是弱不变量 证明：1 ) 由命题2 1 知g r f ( f ) 是弱互模拟于是只需证明7 r 2 1 r 1 ( p ) 是弱不变量即对坳l r 2 7 r 1 ( p ) ， ( 1 ) 若y 号上哥y ，则矿丌2 r f l ( p ) ( 2 ) 若y = 令，则y 7 r 2 7 r 1 ( p ) 考虑如下图形，其中7 f 1 ，l r 2 是x y 到x , y 的投影在g r f ( f ) 上的限 制将i l l7 ( 2 视为关系( 即等同于其图) ，则有他o z i l = ，对丌2 ”i 1 ( p ) ， j 9 r f ( i ) 满足砘 = y 班p 满足霄f 1 ( z ) = 即 y = 7 r 2 7 r i - 1 ( 。) x = 兰生= ；9 r ，( ，) 卫l y r1 7l 伊 o ( x ) 气i i 茅万一0 ( g r f ( f ) 而r d ( y ) ( 1 ) ”j 上爿，因为g r f ( f ) 是弱互模拟，于是j z x ，使得 z 爿上昔一且 g r f ( f ) 由p 是弱不变量知一p 又由 r f l ( 。) = ，得出y = l r 2 7 r i - 1 ( z ) 即暑e 现霄f 1 ( p ) 对于( 2 挎= 辛矿因为扩，( ，) 是弱互模拟，则列x 声 ，且 ，( ，) 由p 是弱不变量，则一p 又由! ，= 丌2 i 1 ) ， 得y 霄2 7 r i l ( p ) 所以丌2 ”i 1 ( p ) 是弱不变量 2 ) 由命题2 1 知g r f c f ) - t 是弱互模拟则只需证明丌2 ”i 1 ( q ) 是弱 不变量即对丌2 町1 ( q ) ( 1 ) 若爿弓，则丌2 百1 ( q ) ( 2 ) 若z 毒一，则茹i r 2 1 r i - 1 ( q ) 如下图，其中7 1 - 1 ，7 r 2 是y x 到y , x 的投影在g r f ( f ) - 1 上的限制 将7 r t ，丌2 视为关系( 即等同于其图) ，则有”2 0 7 f 1 1 = f 一对比砸町1 ( q ) ， 丑 o t f ( f ) 一1 满足他 = z | 暑f q 满足口i 1 ( f ) = 即 z = = r 2 ，r f l ( 暑，) y = = 墨= ：g r f ( f ) _ 1 l 暖 卢。r1 7l 酽 o ( y ) 石而严( g r f ( f ) 1 ) 面硒o ( x ) ( 1 k = 辛l = 辛一，因为，( ，) 一1 是弱互模拟，于是影y ，使 得口号上昔f 且 g r f ( f ) 由q 是弱不变量知矿q 又由7 r i l ( f ) = ，得出z = 丌2 7 r i l ( g ) 即z 7 丌2 7 r i l ( q ) 对于( 2 净毋z 因为g r f ( f ) 一1 是弱互模拟，则彰y ，l ，= 号矿，且 ，( ，) 由q 是弱不变量，则矿q 又由一= 丌2 霄i 1 ( ) ， 得一丌2 r f l ( q ) 所以丌2 ”i 1 ( q ) 是弱不变量 下面的命题说明不变量是弱不变量的一个特例 命题3 5 t 设 是标识迁移系统，p x 是不变量，则 p 是弱不变量 证明：因p 是不变量，即对比p ，。l 。，则z 7 p 即满足弱 不变量定义中( i ) w p v f o ，若茸上j 一则z p ( 2 ) w p ， 若z 一则一p r 一迁移为o 的情况所以p 是弱不变量 以下结果证明了弱不变量是关于乘积封闭的 命题3 6 ：如果p 是x 中的弱不变量，p 是x 中的弱不变量， 那么p p xx x 也是弱不变量 证明：由文献【4 】知余代数范畴c o a l g ( f ) 有任意积，则xx x 仍 为余代数，那么由定义很容易验证p 一是x x 的弱不变量 显然有 推论3 7t 如果只是墨中的弱不变量，那么n 只n 五也是弱 不变量 3 2抽象及限制乘积 本节借助于抽象概念，通过转化标识迁移系统，弱不变量可以用 不变量来表示，即原l t s 中的弱不变量是转化后的l t s 的不变量方法 是把一系列r 一迁移变成单一的r 一迁移，用l 来代替= 净0 = 亭 又引入了l t s 中的限制迁移概念，并以此为工具，得到弱不变量和弱 互模拟之间可以互相转化 定义3 8 n ：设s = 是标识迁移系统，定义s 的抽象 君= 是如下的l t s 其中亍满足下列条件； ( 1 ) 亍当且仅当对v f o ，z ：= 争一= = 争一 ( 2 ) 亍当且仅当z 命题3 9 ：标识迁移系统s = ，否是它的抽象，p x 则p 是s 的弱不变量当且仅当p 是君的不变量 证明：。净”假设p 是s 中的弱不变量，下面证明p 是否中的 不变量，即在吾中，( 忱p ，$ 。) = z p 以下分两种情况证明： ( 1 ) z 下 在否中，z 上争在s 中，霉番上哥一 = 一p因为p 是s 中的弱不变量 ( 2 ) i = r 在否中，z - - l , z 营在s 中，茹爿一 辛一p因为p 是s 中的弱不变量 “”p 是否中的不变量下面证明p 是s 中的弱不变量，也 分两种情况讨论：对忱p ， ( 1 ) l r ， 在s 中，卫考上考一营在君中，茹上一 号p因为p 是否中的不 变量 ( 2 ) z = r ， 在s 中z 爿z 营在君中，z z = z p因为p 是可中的不变量 结合上面命题和定义2 4 【4 】容易得到以下结果： 推论3 1 0 ：s 中的弱不变量是它的抽象君的子余代数 下面定义什么n ql t s 的限制乘积 设 ， 是标识迁移系统，x y 上的迁移关系 t ，s 定义如下： 定义3 1 1 l ， x y ， ( 1 ) ( t ，s ) 铮z 茸上考引臣暑，昔上 号矿，记作 爿上j 1 4 ( 2 ) ( t ，s ) 营z 考一且y 弓矿 记作 = ： 带有限制迁移关系的乘积记为x ，y 按照上面定义的限制乘积，有如下定理： 定理3 1 2 t 冗x x 是弱互模拟当且仅当r 是x ，x 中的弱 不变量 证明：。“r 是弱不变量，则( 1 ) 对于v r ，若 = 辛= 亭 ，则 r ( 2 ) 若 = = 争 ， 则 r 现只证明r 满足弱互模拟定义中的( 1 ) ，( 3 ) ( 2 ) ，( 4 ) 同理可证 对于( 1 ) v r ，z = 号上= 辛z ，因为r 是弱不变 量，则 ：= 寺- ：= = ，且 冗即3 x ， y 啼考矿且 一，d r 对于( 3 ) v r ，z 茹，因为r 是弱不变量，若 ，则 r 即为x ，满足y 矿且 r “兮”r 是弱互模拟，那么由定义中( 1 ) ( 2 ) 推出若 音 三呻= = = ，贝4 r 由( 3 ) ( 4 ) 推出若 = 亭 ，则 r 则r 是弱不变量 3 3 一般余代数的弱不变量 本节利用文献 1 1 给出的余代数的可观察部分概念，把弱不变量 定义推广到一般余代数上，给出了一般余代数上弱不变量的定义，并且 证明了，只要选择合适的观察者，余代数中弱不变量定义和l t s 中弱不 变量定义是一致的 定义3 1 3 ：c ：x + f ) 为一余代数，谓词p x ，对于观察者 d ，p 为x 中的弱不变量，如果p 为的子余代数，即存在唯一的关 系，y p d ( p ) ，使得下图在r e l 中交换其中m ：p x 是包含映射 ( 视为关系) 。 p竺x 0l 扩 o ( p 卜预示广o ( x ) 引理3 1 4 1 1 ： 略当且仅当z o 且z 号上耐。 引理3 1 5 1 1 ： o 备当且仅当z o 且z 茸 设 是一个l t s ，选择观察者d = ，其 中g ( x ) = o x ，町：g i d f ；n ( x ) = x 。x ：曰= i d x f p 是f 的自然o 嘲o r 研究余代数中弱不变量定义和l t s 中弱不变量定义的 关系，我们有如下命题。 命题3 1 6 ：对上述l t s 和观察者d ，定义3 1 3 与命题3 2 的两个 条件是等价的 证明：。垮”设p 是对于观察者d 定义3 1 3 定义的弱不变量 则存在关系1 1 ：p ，g ( p ) = ox p 和协：p + h ( p ) = p 满足 1 6 p里x 1l 略 g ( p 卜可丽+ g ) p竺x d卜 卧， p 了x 下面证明p 满足命题3 2 中的两个条件 ( i ) 对任意j o ，设$ p 且z 茸上号一因为 m 是嵌入，则zex 由引理3 1 4 知 略，所以 略o m = g ( m ) o 饥则孔”p 满足 饥且 g ( m ) 因为c ( m ) 也是嵌入，则z = z ”p ( 2 ) 利用引理3 1 5 同理可以证明 。# ”设p 是满足命题3 2 中两个条件的弱不变量先定义关 系协：p c ( p ) ；o p 其中 m 当且仅当z p 且 z 穹哥z 定义关系他：p h ( p ) = p 其中 。，如加当 且仅当z p 且z 号z 只需证明图( 1 ) 在r e l 中交换只证明略o m = g ( m ) o 饥 a 盘o m ；g ( m ) o 讹同理可证 ：设 略。m ，则z p ，因为m 是嵌入，则z x 且 略由引理3 1 4 知z 爿上号一因为p 满足 定义3 2 ，则一p 由饥定义知 1 1 又因为c ( m ) 是嵌 入，得 g ( m ) 即得 g ( m ) 。m ：设 g ( m ) o t , 则j v ( p ) ，满足 g ( m ) 因为g ( m ) 是嵌入，得$ = z ”则 m 由m 定义知z = 串z 由引理3 1 4 知 略又因 为m 是嵌入，得到 略o m 1 7 参考文献 1 1 j a nr o t h e ，d v a g a nm 甜l l l a 、r i t o w a r d sw e a kb i s i m u l a t i o nf o rc o a i g e b r a s e l e c t r o n i cn o t e si nt h e o r e t i c a lc o m p u t e rs c i e n c e6 8n o 1 ( 2 0 0 2 ) ， 2 】j a nr o t h e b e h a v i o u r a le q u i v a l e n c e sf o rc o a l g e b r a s d i s s e r t a t i o n t e c h n i s c h e n u n i v e r s i t i td r e s d e n 2 0 0 4 【3 lj j m m r u t t e n f u n d a m e n t a ls t u d y u n i v e r s a lc o a l g e b r a ：at h e o r yo fs y s - t e m s t h e o r e t i c a lc o m p u t e rs c i e n c e 2 4 9 ( 2 0 0 0 ) 3 - 8 0 1 4 】b a r tj a c o b s i n t r o d u c t i o nt oc o a l g e b r a t o w a r d sm a t h e m a t i c so fs t a t e sa n d o b s e r v a t i o n s d r a f tc o p y 2 0 0 5 【5 1j a g o g u e n ，j w t h a t c h e r ，e g w a g n e r a ni n i t i a la l g e b r aa p p r o a c ht ot h e s p e c i f i c a t i o n ，c o r r e c t n e a sa n di m p l e m e n t a t i o no fa b s t r a c td a t at y p e s ，i nr y e h ( e d ) ，c u r r e n tt r e n d si np r o g r a m m i n gm e t h o d o l o g y ，p r e n t i c e - h a i l ，e n g l e w o o dc l i f f s ， n j ，1 9 7 8 ，p p 8 0 - 1 4 9 【6 1 6d j l e h m a n n ，m b s m y t h a l g e b r a i cs p e c i f i c a t i o no fd a t at y p e s ：as y n t h e t i c a p p r o a c h ，m a t h s y s t e m st h e o r y l 4 ( 1 9 8 1 ) 9 7 - 1 3 9 f 7 lm a a r b i b ，e g m a n e s ，p a m m e t r i z e dd a t at y p e sd on o tn e e dh i g h l yc o n - s t r a i n e dp a r a m e t e r s ，i n f o r ma n dc o n t r o l 5 2 ( 2 ) ( 1 9 8 2 ) 1 3 9 - 1 5 8 8 jm a a r b i b ，e g m a n e s ，m a c h i n e si nac a t e g o r y , j p u r ea p p l a l g e b r a l 9 ( 1 9 8 0 ) 9 - 2 0 9 j j m m r u t t e n ，d t u r i i n i t i a la l g e b r aa n df i n a lc o a l g e b r as e m a n t i c sf o rc o i l - c u r r e n c y , i n ：j w d eb a k k e r ，w 一p d er o e v e r ，g r o z e n b e r g ( e d s ) ，p r o c r e xs c h o o l s y r u p ，( ad e c a d eo fc o n c u r r e n c y ) ，l e c t u r en o t e si nc o m p u t e rs c i e n c e ，v 0 1 8 0 3 ， s p r i n g e r ，b e r l i n ，1 9 9 4 ，p p 5 3 0 - 5 8 2 【1 0 lj a w a dy a b u h l a i l ，j e s dg 6m e z - t o r r e c i l l a s ，r o b e r tw i s b a u e r d u a lc o a l - g e b r n so fa l g e b r a so v e rc o m m u t a t i v er i n g s j o u r n a lo fp u r ea n da p p l i e da l g e b r a ，1 5 3 ( 2 0 0 0 ) 1 0 7 - 1 2 0 嗍e l s e v i e r e o m l o c a t e j p a a f l l 】j j m m r u t t e n a u t o m a t aa n dc o i n d u c t i o n ( a ne x e r c i s e i nc o a l g e b r a ) ， r e p o r ts e n - r 9 8 0 3 ，c w i ，1 9 9 8 【1 2 lj j m m r u t t e n ，d ，t u f f o n t h e f o u n d a t i o n s o f f i n a l s e 口n a n t i c s ：n o n - s t a n d a r d s e t s ，m e t r i cs p a c e s , p a r t i a lo r d e r s ，i n ：j w d eb a k k e r , w 一p d er o e v e r ，g r o z e n - b e r g ( e d s ) ，p r o c r e xw o r k s h o po i ls e m a n t i c s ， f 1 3 1j j m m r u t t e n e l e m e n t so fs t r e a mc a l c u l u s ( a ne x t e n s i v ee x e x c i s ei n c o i n d u c t i o n ) e l e c t r o n i cn o t e si nt h e o r e t i c a lc o m p u t e rs c i e n c e4 5 ( 2 0 0 1 ) 【1 4 】p a c z e l ，n m e n d l e r af i n a lc o a l g e b r at h e o r e m i n ：d h p i t t ，d e r y e h e a r d ，p d y b j e r ，a m p i t t s ，a p o i g n e ( e d s ) ，p r o c c a t e g o r yt h e o r y a n dc o m p u t e r s c i - e n c e ，l e c t u r en o t e si nc o m p u t e rs c i e n c e ，s p r i n g e r ，b e r l i n ，1 9 8 9 ，p p 3 5 7