（计算机软件与理论专业论文）范畴论计算演示工具的设计与实现.pdf

中山大学硕士学位论文范畴论计算演示工具的设计与实现 题目：范畴论计算演示工具的设计与实现 专业：计算机软件与理论 硕士生：闻啸 指导老师：周晓聪副教授 摘要 范畴理论是2 0 世纪4 0 年代中后期，由s e i l e n b e r g 和s m a cl a n e 等为研 究同调代数而创立的一个抽象代数分支。以范畴、函子和自然变换等为基本概念 统一地研究某些数学结构及其性质。随着理论计算机科学的发展，特别是域论理 论、直觉逻辑、类型理论以及计算机科学中的代数与共代数方法的深入研究，范 畴理论在计算机科学领域的应用也日益广泛。 由于范畴理论本身十分抽象，有些构造和计算还具有一定的复杂性，因此我 们希望设计一个范畴论计算演示工具。构造一个平台来辅助我们学习与研究范畴 理论。 简单地说，范畴论计算演示语言的设计目标要提供一个简单的语言，以一种 命令行交互的形式，给出有关范畴论基本构造的一些具体的、离散的例子，使得 范畴论学习者对范畴论这些抽象的构造及其性质有一个初步的感性认识。范畴论 学习者可通过使用该工具举出一些范畴论构造的直观例子，并对这些构造的一些 简单性质进行验证，从而熟悉和理解这些范畴论构造。 本文设计并开发了一个范畴理论计算演示开发工具，该软件实现了对范畴理 论中的许多类型的识别，并且支持类型之间的复合运算，同时具备简单的操作性。 文章详细地介绍了范畴理论计算演示开发工具的开发过程，包括语言部分的l e x 词法分析器和y a c c 语法分析器的设计和开发，同时还详细的分析了范畴论工 具的u m l 建模，设计模式和关键的算法实现。 关键词：范畴，u m l ，设计模式，l e x ，y a c c 中山大学硕士学位论文范畴论计算演示工具的设计与实现 t i t l e ：d e s i g na n di m p l e m e n t a t i o no f c a t e g o r yc o m p u t a t i o na n dd e m o n s t r a t i o nt o o l 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 ：w e nx i a o s u p e r v i s o r ：v i c e - p r o f e s s o rz h o ux i a o c o n g a b s t r a c t c a t e g o r yt h e o r yi sab r a n c ho fa b s t r a c ta l g e b r aw h i c hw a sc r e a t e dt os t u d y h o m o t o p ya l g e b r ai n l a t e1 9 4 0 sb y s e i l e n b e r ga n ds m a cl a n e w i t h t h e d e v e l o p m e n to 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 s p e c i a l l yd o m a i nt h e o r y , i n s t i n c t i v e l o g i c ，t y p et h e o r ya n dt h er e s e a r c ho fa l g e b r aa n dc o a l g e b r am e t h o d si nc o m p u t e r s c i e n c e ，c a t e g o r yt h e o r yi sa p p l i e dm o r ea n dm o r ef r e q u e n t l y i nt h ec o m p u t e r s c i e n c ed o m a i n ， b e c a u s e c a t e g o r yt h e o r y i se x t r e m ea b s t r a c ta n di t sc o n s t r u c t i o n sa n d c o m p u t a t i o n sa r ec o m p a r a t i v e l yc o m p l e x ，t h e r e f o r ew ed e s i g nac a t e g o r yc o m p u t a t i o n d e m o n s t r a t i o nt o o la n dc o n s t r u c tap l a t f o r mt oa s s i s to u rl e a r n i n ga n dr e s e a r c ho n c a t e g o r yt h e o r y t h eg o a lo ft h ec a t e g o r yd e m o n s t r a t i o nt o o li st op r o v i d eas i m p l el a n g u a g e ， w h i c hb a s e do na ni n t e r a c t i v ec o m m a n d ，t od e m o n s t r a t es o m ec o n c r e t ee x a m p l e s ， h e l p i n gb e g i n n e r st og e tab a s i ck n o w l e d g ea b o u tt h ec o n s t r u c t i o n si nc a t e g o r y t h e o r y i nt h i st h e s i s ，w ed e s i g na n dd e v e l o p eac a t e g o r yt h e o r yd e m o n s t r a t i o nt 0 0 1 t h i st o o lr e a l i z e dt h ei d e n t i f i c a t i o no fv a r i o u st y p e so fc a t e g o r yt h e o r ya n ds u p p o r t c o m p o s i t ec a l c u l a t i o no f t y p ev a r i a b l e s b e s i d e s ，i th a sf e a t u r e so fs i m p l eo p e r a t i o n a n dp o w e r f u lp r o c e s sf u n c t i o n i nt h i st h e s i s ，w ep r e s e n tt h es y s t e m sd e s i g na n d i m p l e m e n t a t i o no ft h et o o li nd e t a i l ，s u c ha sd e m o n s t r a t i o nl a n g u a g ed e s i g na n d d e v e l o p m e n tu s e db yl e xa n dy a c c a tt h es a m et i m e , w ea l s od i s c u s s e dt h e c a t e g o r yt h e o r yd e m o n s t r a t i o nt o o l su m lm o d e l i n g ，d e s i g np a t t e r na n dr e a l i z a t i o n o f k e ya l g o r i t h m s k e y w o r d ：c a t e g o r y , u m l ，d e s i g np a t t e r n ，l e x ，y a c c 1 l 中山大学硕士学位论文范畴论计算演示工具的设计与实现 1 1 研究背景及意义 第一章绪论 范畴理论是上一世纪4 0 年代中后期，由s e i l e n b e r g 和s m a cl a n e 等为研 究同调代数而创立的一个抽象代数分支 3 】 4 1 。它以范畴、函子、自然变换等为 基本概念统一地研究某些数学结构及其性质。范畴理论可以说是一种语言，一种 描述数学结构的抽象语言。阻范畴理论为工具，可以将某些数学结构的性质加以 泛化而推广到其他数学结构，也可以将某些数学性质具体从而丰富到某些数学结 构以推广该数学结构的应用范围。进一步，通过范畴理论中的通用概念，可以将 许多不同数学分支联系在起结合起来进行研究。作为一门抽象的数学工具性的 理论，范畴理论已经广泛应用在各个数学分支，如同调代数、代数几何、代数拓 扑、代数k 理论。随着理论计算机科学的发展，特别是域论理论、直觉逻辑、 类型理论等的深入研究，范畴理论在计算机科学领域的应用也日益广泛。 范畴理论中的许多构造，如积、共积、回拉、外推等的构造比较抽象，因此 在使用范畴论为工具的研究中通常需要一些例子来演示这些构造的计算结果，以 便得到直观的影响，但是其中有些构造是比较复杂的，因此我们希望开发一个计 算演示工具计算一些范畴论的构造，以帮助人们使用范畴论进行共代数方法、形 式语义学等方面的研究。 通过开发范畴论计算演示工具，我们可以更加清楚地了解范畴理论中许多对 象是如何构造的，从而为深入的研究函子和共代数的构造打下良好的基础。同时， 我们可以利用范畴论计算演示工具来计算一些比较复杂的构造过程，根据计算的 结果我们可以判断是否和预测的结果一致，这样可以大大减少手工计算的强度， 因此方便了人们对范畴理论的研究。 1 2 当前的研究现状 现在关于范畴理论的辅助工具比较多，比较著名的如p v 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 ) 程序辅助证明系统【5 和m l 函数式程序设计语言【6 】。下面我 山大学硕士学位论文 范畴论计算演示工具的设计与实现 们简单的介绍一下： p v s 是由斯坦福大学开发的基于古典简单类型高阶逻辑和谓词子类型 的交互式定理证明器，广泛用于硬件验证、容错和分布式算法验证和u m l 模型验证。p v s 具有丰富的类型系统，包括基本类型( 如b o o l 、r e a l 等) 和 类型构造符( 如集合( s e t ) ，元组( t u p l e ) ，记录( r e c o r d ) 和函数( f u n c t i o n ) ) 。除 了丰富的类型外，p v s 环境还包括类型检查器、定理证明器和模型检验 工具等工具集。 m l 是为了自动机定理证明而设计的，m l 支持函数式程序设计，其中， 程序是由函数所组成的，这些函数可以操作简单的数据结构。m l 的推 导规则和证明方法通过函数表示，因此它具有高阶函数式程序设计的能 力。 这里我们希望利用l e x 和y a c c 开发工具编写一个简单的检查范畴理论构 造的验证系统，通过这个系统我们可以直观的构造范畴论中各个类型，并且可以 对这些类型进行复合运算，通过这些运算的结果来检测是否和预测的结果一致。 这样可以大大的减少人工计算的强度。l e x 和y a c c 是开发编译器非常重要的 工具 7 】，l e x 是由贝尔实验室的m e l e s k 和e ，s c h m i d t 在u n i x 操作系统上首次 实现的。l e x 词法分析工具将词法分析的重点放在正规表达式的描述和识别正 规表达式之后的处理上，因此更易于维护词法分析器。y a c c 是由贝尔实验室 的s c j o h n s o n 在2 0 世纪7 0 年代编制完成。y a c c 大大的简化了语法分析器设 计的设计难度，将程序设计语言编译器的设计重点放在语法制导翻译上，从而方 便了编译器的设计和对编译器代码的维护。因此，通过l e x & y a c c 来开发范畴 论计算计算演示工具具有良好的可移植性和可扩充性。 1 3 本文的主要工作 这篇文章主要讨论了范畴论计算演示工具的设计和开发，以及如何利用 l e x 和y a c c 开发识别范畴论语法的解释器。 论文的总体设计如下： 1 第一章绪论主要介绍了论文研究的背景、意义与当前的现状。 1 第二章主要介绍了范畴理论的一些基础知识，包括范畴( c a t e g o r y ) 、对象 2 中山大学硕士学位论文 范畴论计算演示工具的设计与实现 ( o b j e c t ) 、射( m o r p h i s m ) 、函子( f u n c t o r ) 、自然变换( n a t u r a lt r a n s f o r m a t i o n ) 的概念 的定义，并讨论了积( p r o d u c t ) 、共积( c o p r o d u c t ) 、均等射( e q u a l i z e r ) 、共均等射 ( c o e q u l i z e r ) 、回拉( p u l l b a c k ) 、外推( p u s h o u t ) 等结构的构造，同时给出了范畴论计 算演示工具计算它们构造的具体例子。 2 第三章主要介绍了范畴论语言的设计 8 】。范畴论语言的设计包括两个部 分：词法分析器和语法分析器。词法分析器和语法分析器采用l e x & y a c c 来 开发。l e x 和y a c c 是开发编译器两种非常重要的、而且功能强大的工具，可 以大大的简化编译器的开发 3 第四章主要介绍了范畴论计算演示工具系统的分析过程，并介绍了如何利 用u m l 建模技术对整个系统进行建模 9 。 4 第五章主要介绍了范畴论计算演示工具系统整个架构的设计，并详细讨论 了每个类的结构，同时对系统所使用的设计模式进行了分析【2 0 】。 5 最后详细的介绍了关键代码的实现过程。其中包括了词法分析器和语法分 析器的设计与实现，以及整个软件架构的实现。 计算演示工具的设计采用采用面向对象的软件开发方法，设计过程中吸收了 软件工程领域有益的概念和有效的方法。整个设计体现了面向对象设计的抽象 性、封装性、继承性和多态性，对开发出模块化、数据抽象程度高的，体现信息 隐蔽、可复用、易修改、易扩充等特性的程序有一定的借鉴作用。 1 4 本文的研究的主要创新点 本文是为了方便初学者快速的掌握范畴论的原理和相关构造，为进一步学习 函子和共代数的原理打下坚实的基础，从而开发了范畴论计算演示工具。 本文设计的范畴论计算演示工具有以下的创新之处： 1 该工具具有操作简单，使用方便的特性，用户通过使用类似d o s 命令的 操作方法，可以轻易的实现对集合、关系、函数的赋值，并且可以调用 系统库中的函数来实现对这些变量的复合运算。 2 该工具实现了范畴论中元素、有序对、集合这些基本的数据类型的无缝 的转换，一个元素可以是一个数字，还可以是一个有序对或者一个集合， 这就为识别任何复杂的集合结构提供了有效的机制。 中山大学硕士学位论文 范畴论计算演示工具的设计与实现 3 该工具内部结构的实现采用了c + + 语言开发，而不是传统的c 语言。通 过面向对象的设计方式我们可以轻易的封装任何数据类型的结构和操 作，这为以后的维护和开发提供了良好的保证。 4 中山大学硕士学位论文范畴论计算演示工具的设计与实现 第二章范畴论基础 在这一章，我们将介绍范畴理论的基础知识【1 【2 】，包括范畴( c a t e g o r y ) 、对 象( o b j e c o 、射( m o r p h i s m ) 、函子( f u n c t o r ) 、自然变换( n a t u r a lt r a n s f o r m a t i o n ) 等基本 概念的定义；也会介绍一些特殊的对象和射。如初始对象( i n i t i a ld b j e c t ) 、终结对 象( f i n a lo b j e c t ) 、单射( m o n o m o r p h i s m ) 、满射( e p i m o r p h i s m ) 和同构射( i s o m o r p h i s m ) 等；并讨论积( p r o d u c o 、共积( c o p r o d u c t ) 、均等射( e q u a l i z e r ) 、共均等射 ( c o e q u a l i z e r ) 、回拉( p u l l b a c k ) 和外推( p u s h o u t ) 等一些基本的极限( 1 i m i c ) 和共极限 ( c o l i m i 0 ，以及幂对象( e x p o n e n to b j e c o ) 和笛卡尔封闭范畴( c a r t e s i a nc l o s e d c a t e g o r y 的构造。 2 1 基本概念 2 1 1 范畴的定义： 范畴( c a t e g o 啪是一个数学系统，其中包括两个数据、一些操作和这些操作所 满足的公理，两个数据是： 对象( o b j e c t ) ：范畴c 中的对象记为a 、b 射铆o r p h i s m 或a r r o w ) ：范畴c 中的射记为f 昏 操作包括： 对于每个射，有两个操作：d o m 和c o d ，其中d o m ( o 是范畴c 中的对象， 称为，的域( d o m a i n ) 或f f i ( s o u r c e ) ，c o d ( 巧也是范畴c 中的对象，称为的共域 ( c o d o m a i n ) 或目标( t a r g e t ) 。通常记：，：a b 为范畴c 中的射，这时a 就是，的 域，而b 是它的共域。 对于每个对象a 有一个射i d a ：a 斗a ，称为对象a 的恒等射( i d e n t i t y m o r p h i s m ) 。 对于两个射，和臣如果c o d ( t ) 和d o m ( g ) 是同一个对象，那么这两个射可 复合( c o m p o s a b l e ) ，记为：矿也可省略中间的而直接写成g f , 且d o m ( g 。毋 中山大学硕士学位论文范畴论计算演示工具的设计与实现 = d o m ( o ，c o d ( g 。毋= c o d ( 曲。射的复合( c o m p o s i t i o n ) j f f l 常记为，设有，：a b ， g ：b 斗c ，则g f ：a c 。 这些操作必须满足以下公理： 恒等射是复合操作的恒等元，即对，：a j b ，有坷，。，= 厂= 产商。 复合操作可结合，即对，：a b ，g ：b 斗c ，h ：c 寸d ，有： 即 妒一伪。，：a j d ，从而可记为伊矿，：a j d 。 范畴的所有对象不一定组成一个集合，而所有的射也不一定组成一个集合。 所以通常称范畴的一类对象( ac l a s s c o l l e c t i o no b j e c to f c a t e g o r y ) 或一类射。如果范 畴的任意两个对象a 、b ，所有a b 的射构成集合，那么称该范畴为局部小范 畴( 1 0 c a us m a l lc a t e g o r y ) ，这时记a 到b 的所有射为h o m ( a ，b ) 或c ( a ，b ) 。如果 范畴的所有射构成一个集合，则称该范畴为小范畴( s m a l lc a t e g o r y ) ，注意这时它 的所有对象电显然构成一个集合。 范畴c 的对偶范畴( 哪妒f f pc a t e g o r y ) ，记为c ”，其对象是c 的对象，而对 于c 的任意射，：a 斗b ，在c o p 都有且仅有一个对应的射严：b 专a ，且c o p 的射 都是通过这种对应得到。对于c 。9 的两个劓：矿9 ：c 斗b ，f 9 ：b j a ，其复合定 义为：严。矿9 2 管印”：c j a 。 对偶的概念在范畴理论中十分重要。范畴理论的很多术语都成对出现，即有 它的对偶术语象初始对象和终止对象、积和共积等。所谓对偶术语的含义是范 畴c 的初始对象就是其对偶范畴c ”的终止对象，而范畴c 的终止对象是其对偶 范畴c ”的初始对象等等。多数术语的对偶术语是在该术语前加“共”米称呼( 某 些中文文献是在前加“余”，在英文中则是前面加”c o 一”) 。 同样，范畴理论的许多定理、命题等都有其对偶定理、命题，只要将该定理 中的某些术语，合适地换成其相应的对偶术语即可。 2 1 2 范畴的图式 范畴理论经常用图式( d i a g r a m ) 表达射之间的关系，范畴c 的图式是一个有向 巾山大学硕士学位论文范畴论计算演示工具的设计与实现 图，其顶点用c 的对象标记，而有向边用c 的射标记，且源顶点是射的域所标 记的顶点，目标顶点是射的共域标记的顶点。换句话说，是图式的顶点对应对象， 边对应射，图式的有向路径则对应该路径上射的复合。 说c 的一个图式是交换的( c o m m u t a t i v e ) 或说一个图式交换( c o m m u t e ) ，是指该 图式中任意有相同源顶点和目标顶点的不同有向路径对应c 中相同的射，等价 地，是指这些不同有向路径所对应的射的复合在c 中相等。例如下述图式交换就 表示：k o h = g o ， 图2 1 范畴的图式交换 在范畴论计算工具中，为了证明k o h = 9 7 ，我们可咀采用下面计算方法： 显然对c 的任意图式d i a g ，只要将其所有的有向边的方向反向，且边上的标 记射，改为尸9 ，则得到c 叩的图式d i a 酽9 。如果d i a g 交换，则d i a g 。p 也交换。 设有以下图式： 图2 2 范畴的图式交换 如果内部两个方框所代表的图式交换，则整个图式交换，也就是说：如果 f 7 = j 。i 且h 。g = 妒z ，则有h 。g 歹= k 。j 。i 。 范畴c 的初始对象( i n i t a i lo b j e c t ) 是范畴c 的一个对象i ，且满足对于范畴c 的任意对象a ，有唯一的射i a ：i 专a 。对偶地，对象t 称为终止对象( t e r m i n a l o b j e c t ) ， 如果满足对任意对象a ，有唯一的射! a ：a 呻t 。后文通常用j 表示终止对象。 瓣攀一攀 一 i y i j 正r卜h卜0_口一 中山大学硕士学位论文范畴论计算演示工具的设计与实现 设有范畴c 的射，：a 斗b ，说它- 是l r q 构射( i s o m o r p h i s m ) ，如果存在范畴c 的 射g ：b 斗a ，使得9 0 f = f d a ，且户9 = i d b 。这时9 称为，的逆( i n v e r s e ) ，对称地， ，也是9 的逆。如果对象a 和b 之间存在同构射，则称对象a 和对象b 同构， 记为a 兰b 。 如果对象i - 和对象l s 都是范畴c 的初始对象，则对象i 一利对象1 2 同构。同 样，如果对象t 1 和t 2 都是终止对象，则t i 和t 2 同构。 说范畴c 的射n 1 ：a _ b 是单射( m o n i c ) 如果满足，对任意的射，c a 和射 g ：c a ，若m 7 = m 。g ，则，= 9 。说范畴c 的射e ：a 斗b 是满射( e p i c ) ，如果满 足，对任意的射f b 。c 和射g ：b - - - c ，若r e = 9 。e ，贝j j f = g 。 2 1 3 范畴积的构造 范畴c 的对象a 和b 的积( p r o d u c t ) 是对象p ，以及射p a ：p j a 和p b ：p 啼a ， 满足对任意的对象c ，如果有射f ：c 专a 和9 ：c j b ，则可找到唯一的射m ： c - - - p 使得p a l t i = ，和p bm = g 同时成立。这时射m 称为，和9 的积媒介射 ( p r o d u c t m a t e ) 。通常就称p 为对象a 和b 的积，射p a 和p b 为投影射( p r o j e c t i o n m o r p h i s m ) 。用图表示如下： a ，墅二p 一竺竺丑 图2 3 范畴积的构造i 若对象p - 和对象p 2 都是对象a 和b 的积，则p 和p z 同构。 若范畴c 的任意两个对象都有积，则称该范畴有二元积。这时对于对象a 和 b 可选定一个积，记为a x b ，对应地投影射记为a 和e ，射，和9 的积媒介射 记为领旷。可将两个对象的积推广到有限个对象a ，a 2 ，a 。的积，记为 a i x a 2 x x a 。，定义为：( ( ( a i a 2 ) x ) x a 。) ，对应地积媒介射 ， 中山大学硕士学位论文 范畴论计算演示工具的设计与实现 记为 。若范畴c 的任意有限个对象都有积，则称该范畴有有限 积。 由于积在同构的意义下惟，因此我们可以用a x b 表示对象a 和b 的积( 定 义中的那个对象p 】，而通常用a ：a b 寸a ，“b ：a x b - - b 表示其中的射，并称它 们为( 积的) 投影射( p r o j e c t i o n ) 。当然，有时我们也使用其他的下标，或者根本不 使用下标，这时读者需要从上下文判断所给出的投影射的源和目标。对于任意的 对象c 和，c 寸a ，g ：c 呻b ，我们用领9 ：c - - + a x b 表示交换图2 3 中所惟一存在 的丌1 ，并称其为，和夕的积伴随射( p r o d u c t m a t e ) ，从而我们有如下交换图： 采! 苎出b 要曼二：i 拶 图2 4 范畴积的构造2 在集合范畴s e t 中，两个集合a 和b 的积的最自然代表就是这两个集合的笛 卡尔积( c a r t e s i a np r o d u c t ) ： a x b = l a e a 八b b 所需要的射a ：a b 斗a 和兀b ：a x b - - b 就是坐标投影函数，两个函数 ，c 寸a 和g ：c - - b 的积伴随射领g ：c - a x b 的定义为镬9 ( c ) = 领c ) ，9 ( c ) 。 范畴论计算演示工具中积的构造过程： 9 中山大学硕士学位论文范畴论计算演示工具的设计与实现 假定范畴c 有积，它的两个射，a _ b 和g ：c - - d 的积，记为产9 ：a x c - - - b x d ， 定义为：弘g = 妒n ，g 。c ，用交换图表示为 f g 图2 5 两个射的积的构造 范畴论计算演示工具中两个射的积的构造过程： 中山大学硕士学位论文 范畴论计算演示工具的设计与实现 积的媒介射具有以下性质： 1 对于兀a ：a b 斗a 和n a ：a x b - - a b ，有 = i d a 。b 。 2 。h = c x d 则有： a ) ( 厂。9 ) 。( hx k ) = ( 厂。 ) x ( g 。的 b ) 伊。g ) 。 = 2 1 4 范畴共积的构造 给定范畴c ，两个对象a 和b 的( 二元) 共积( b i n a r yc o p r o d u c t ) 是三元组但p a ， p b ) ，其中p 是c 的对象，p a ：a - - p , p b ：b - - - p 是c 的射，且满足：对任意c 对象c 和射，a 专c ，g ：b - - - c ，都存在惟一的射m ：p - - - c 使得m 。玖= ，且m 。p b = 夕，这 些条件用交换图表示如下： t p 山大学硕上学位论文 范畴论计算演示工具的设计与实现 4 p 套i 一盥一b 图2 6 范畴共积的构造l 我们用a + b 表示对象a 和b 的共积，并通常用奴：a j a + b ，k s ：b - - - a + b 表 示其中的射，并称它们为( 共积的) 注入射( 啦加c f 泐) 。对于任意的对象c 和j a 寸c ， g ：b 斗c ，我们听鲥：a + b 斗c 表示图1 , 6 所惟一存在的m ，并称其为，和g 的共 积伴随射( c o p r o d u c t m a t e ) ，这样我们有如下交换图： 图2 7 范畴共积的构造2 范畴论计算演示工具中共积的构造过程： 在集合范畴s e t 中，两个集合a 和b 的共积( 的最自然代表) 就是这两个集 合的笛卡尔积( d i s j o i n tu n i o n ) ： a + b = l a e a u b e b 这里0 ，1 只是两个标志而已，可任取两个不相同的值。所需要的射“：a j a + b 定义为对任意a e a ，“( a ) = ，蚝：b - - a + b 定义为对任意的b e b ，b ( b ) = ， 那么两个函数，a 斗c 和g ：b - - - c 的共积伴随射阢9 】：a + b 寸c 的定义为 中山大学硕士学位论文范畴论计算演示工具的设计与实现 暖g 】( a ，o ) = a ，i f , g c o ，1 ) = b 。 假定范畴c 有共积，它的两个射，a 斗b 和g ：c - d 的积，记为 f + g ：a + c - - b + d ，定义为： 内：【岛誓幻匆】，用交换图表示为 图2 8 两个射的共积的构造 范畴论计算演示工具中两个射的共积的构造过程： d 假定范畴c 有共积。共积的伴随射以及射的共积运算有如下性质 1 陬，b 】- f d a + b i d a + i d b = f d a + b ； 2 对任意的射，a c ，g ：b - - - c 以及h ：c - - d ，有【_ l o f , 矗o g 卜h 。t t ；g ：a + b - - d ； 3 对任意的射，a 畸c ，g ：b - - c 以及_ t ：d a ，k ：e - - - b 有【产h ，g 。柚= 斫g 】。砷+ 。： d + e - - c ； 4 对任意的射，a c ，g ：b - - - d 以及，l ：c 寸e ，k ：d - - - f 有( + 幻。( 产g ) = ( h b o + ( k 勺) a + b - - e + f ； 中山大学硕士学位论文 范畴论计算演示工具的设计与实现 2 1 与均等射和共均等射的构造 在范畴c 中，说射e ：e a 是两个射f ，9 ：a 寸b 的均等射( e q u a l i s e r ) ，如果 它满足下面两个条件： 1 户e = 9 。e 2 对任意的射h ：c 斗a ，如果也有广 = 9 。h ，则存在唯一的射m ：c 斗e ， 使得h = e o m 。用图表示如下： ej 图2 9 均等射的构造 集合范畴s e t 有均等射，任意两个函数z 9 ：a 斗b 的均等射e q ( f , , f f ) ：e q ( f , 9 ) 斗a 定义为： e q 伍9 ) = a a ，( a ) = 9 ( a ) )对任意的a e q 旺9 ) ，e q 伍9 ) ( a ) = a 对任意的 ：c 专a ，若f 。h = 9 。h ，即对任意c c 有奠7 t ( c ) ) = 9 ( ( c ) ) ，从而有 h ( c ) e q 伉g ) 。从而可定义r e ：c - - e q 伍9 ) 为对任意的c c ，r e ( c ) = h ( c ) 。 范畴论计算演示工具中均等射的构造过程： 在范畴c 中，说射e ：b 斗e 是两个射，9 ：a 专b 的共均等射( c o e q u a l i s e r ) ， 如果它满足下面两个条件： 1 e o ，= e 。g 2 对任意的射h ：b 斗c ，如果也有 o ，= h 。9 ，则存在唯一的射1 7 l ：e _ c ， 使得h = 丌l o e 。用图表示如下： 岔，“-c _ _ 巾山大学硕士学位论文 范畴论计算演示工具的设计与实现 。i t 蠹! _ 夏- 了曩曰 图2 1 0 共均等射的构造 范畴论计算演示工具中共均等射的构造过程： 2 1 6 回拉与外推的构造 在范畴c 中，射，：a 斗c 和g ：b 斗c 的回拉( p u l l b a c k ) 是三元组 p a ，p b ) ： 1 p 是范畴c 中一个对象，记为a x c b ，以及 2 两个射p a ：p 呻a 和p b ：p 寸b ，使得f o p a = 夕o p b 。 它们满足，任给对象。d ，若有射h ：d 呻a 和七：d 斗b 也使得户h - - g 。j ：，则 存在唯一的射m ：d 斗p ，使得p 。m = h 和p e 。m = 七同时成立。用图表示如下： 图2 1 1 回拉的构造 在上图中，在对象p 所在的角作了标记表示该交换图代表的是回拉。回拉的对 +，*_一一露，。譬，一 一。2话摄棼 e 孓一 巾山大学硕士学位论文范畴论计算演示工具的设计与实现 偶概念是外推0 u l l o u t ) 。 我们通常使用a x c b 来表示两个射，a 斗c 和9 ：b 呻c 的回拉对象p ，如果集 合范畴s e t 有回拉。任意两个函数，a 呻c 和9 ：b 寸c 的回拉定义为： a c b = ( a e a a b b a f ( a ) = g ( b ) ) p a ，p n 是相应的坐标投影射 对于任意的函数 ：d 斗a 和k ：d - b ，若f 。h = 9 。k ，则对任意的d e d 有 贝 ( d ) ) 穹( _ 】：( d ) ) ，从而 ea x c b ，从而可定义m ：d 斗a c b 为 m ( d ) = 。显然有7 l o p a - - - - h 且m o p n = k ，且同时使得这两个等式成立的 m 是惟一的。 范畴论计算演示工具中回拉的构造过程： 设有下面的图式 、 8 g 9 ( ，) p 百一e t d 图2 1 2 回拉的复合 如果内部两个方框所代表的图式是回拉，则整个图式也是回拉。 在范畴c 中，射厂：c 斗a 和9 ：c 斗b 的外推是三元组( p ，p p b ) ： 1 p 是范畴c 中一个对象，记为a x 。b ，以及 2 两个射p a ：a 哼p 和p b ：b - - p ，使得p a 。，印。9 。 它们满足，任给对象d ，若有射h ：a d 和k ：b j d 也使得ho f = k 。g ，则 口奠 ?r， 一媾黎。 中山大学硕士学位论文范畴论计算演示工具的设计与实现 存在唯一的射脚：p _ d ，使得m 。p a = 由和巾。| 口b = 丘同时成立。用图表示如下： e la 9 一- 誉惑卜 图2 1 3 外推的构造 范畴论计算演示工具中外推的构造过程： 中山大学硕上学位论文 范畴论计算演示工具的设计与实现 第三章范畴论计算演示语言设计 范畴论计算演示语言提供一个简单的语言，以一种命令行交互的形式，给出 有关范畴论基本构造的一些具体的、离散的例子，使得范畴论学习者对范畴论这 些抽象的构造及其性质有一个初步的感性认识。范畴论学习者可通过使用该丁具 举出一些范畴论构造的直观例子，并对这些构造的一些简单性质进行验证，从而 熟悉和理解这些范畴论构造。 范畴论计算演示语言的实现采用了l e x 和y a c c 米实现，使用l e x 和y a c c 我们可 以非常方便的对一条语句进行词法和语法分析。词法分析生成器l e x 是一个u n i x 下的实用工具，它将一个词法分析规则转换为c 函数的实现。语法分析器y a c c 能够 识别的语法是b n f 范式，用户定义一个b n f 类型的语法规则，y a c c 将该规则转换为 语法分析器，通过在b n f 语法规则中嵌入语法动作，可以建立某种形式的语法树。 3 1 b n f 表示说明 巴克斯诺尔范式( b n f ：b a e k u s n a u r f o r m ) 是由j o h n b a e k u s 和p e t e r n a u r 首先引入的用来描述计算机语言语法的符号集。它以递归方式描述语言中的各种 成分，凡遵守其规则的程序就可保证语法上的正确性。b n f f l 3 于其简洁、明了、 科学而被广泛接受，成为描述各种程序设计语言的最常用的工具。巴克斯范式主 要由终结符、非终结符、元符号组成，终结符一般用粗体表示，非终结符一般用 标准字体表示。巴克颠范式的左部是一个非终结符，右部是由非终结符和终结符 中山大学硕士学位沦文范畴论计算演示工具的设计与实现 组成的一个任意符号串。具有相同左部的产生规则可以共用一个左部，右部之间 以竖直线叩分开。下面简单的介绍巴克斯范式符号的定义。 表3 1b n f 符号的说明 符号解释 左边的元素由右边的元素构造 该符号前面的元素可以出现0 或多次 f 花括号里的元素是同种语义效果 【】 方括号里的元素是可选的 左右两个表达式任选其一( 或的意思) 3 2 演示语言的语法 范畴论计算演示工具主要实现了两种操作：一个是赋值语句的操作，例如对 集合、关系和函数的赋值，使它们获得一个正确的结构：另一个是命令语句的操 作，例如对集合进行并、交、差运算，函数的复合、逆运算，及积、共积、回拉 和外推的操作。 范畴论计算演示语言语法包含了命令序列的语法、值声明的语法、动作命令 的语法，它们采用b n f 范式表示。命令序列是由许多的命令构成，一个命令可以 是赋值命令，也可以是一个计算动作命令。 3 r 2 1 命令序列的语法 c o m m a n d l i s t：2c o m m a n dc o m m a n dc o m m a n d l i s t c o m m a n d ：= v a l u e d e c l a r a t i o na c t i o n c o t m n a n d 命令序列是一些命令的集合，比如说我们要计算两个函数的复合，那么首先 我们要对两个函数进行赋值，然后才能对它们进行复合运算，这些命令的组合就 是一个命令序列。一个命令有两种类别，一个是赋值语句的语法，另一个是动作 命令的语法。 中山大学硕士学位论文 范畴论计算演示工具的设计与实现 3 2 2 值声明的语法 v a l u e d e c l a r a t i o n ：= t y p e l d n a m e e x p r e s s i o n = v a l u e e x p r e s s i o n n a m e e x p r e s s i o n ：2i d e n t i f y ( n a m e e x p r e s s i o n ) 】i ( n a m e e x p r e s s i o n ) i n a m e e x p r e s s i o n + n a m e e x p r e s s i o n n a m e e x p r e s s i o n + n a m e e x p r e s s i o n n a m e e x p r e s s i o n 一 n a m e e x p r e s s i o n t y p e l d：= s e t r e l a t i o n i f u n c t i o n变量的类型 i d e n t i f y ：= a z a z 】+ 0 - 9 + 一般的标识符 值声明的语法包括集合赋值的语法、关系赋值的语法和函数赋值的语法，其 巾n a m e e x p r e s s i o n 表示变量的名字，集合只有一个变量名，而没有扩展名，关系 和函数都有扩展名。例如 s e ta = 1 ，2 , 3 ，4 ，5 表示给集合a 赋值 r e l a t i o nr ( a - b ) = ， ) 表示给关系r 贼值，其中a - b 是关系的扩展 名，表示一个集合a 到b 的映射。 n a m e e x p r e s s i o n + n a m e e x p r e s s i o n 表示扩展名中的积，例如 f u n c t i o n 瑾( a + b ) 一 c ) 表示函数f 是集合a 和b 的的积到c 的映射。 n a m e e x p r e s s i o n + n a m e e x p r e s s i o n 表示扩展名的共积，例如 f u n c t i o n g “a 4 b ) c ) 表示函数g 是集合a 和b 的的共积到c 的映射。 v a l u e e x p r e s s i o n 表示一个由多个元素的集合构成的表达式，它的语法在后面有详 细的说明。 通过以上的分析，该值声明表达式可以支持任何复杂的函数的识别，例如 f u n c t i o n h ( ( ( a - b ) 一 c ) 一 d ) = 。 f u n c t i o n i ( ( ( a + b ) 一 c ) 一 d ) = ) 。 v a