苗德成

（韶關(guān)學(xué)院 信息科學(xué)與工程學(xué)院,廣東 韶關(guān)512005）

基于范疇論的共享系統(tǒng)數(shù)據(jù)模型研究綜述

苗德成

（韶關(guān)學(xué)院 信息科學(xué)與工程學(xué)院,廣東 韶關(guān)512005）

摘要：數(shù)據(jù)模型是共享系統(tǒng)設(shè)計(jì)與開發(fā)的核心與基礎(chǔ),范疇論對研究共享系統(tǒng)數(shù)據(jù)模型的建模方法具有獨(dú)特的優(yōu)勢,為語義計(jì)算與程序邏輯的精確描述提供堅(jiān)實(shí)數(shù)學(xué)基礎(chǔ),同時(shí)也具有廣闊的應(yīng)用前景.對共享系統(tǒng)數(shù)據(jù)模型的范疇論基礎(chǔ)、基于范疇論的共享系統(tǒng)數(shù)據(jù)模型的研究現(xiàn)狀及當(dāng)前面臨的主要問題等方面的主要和最新研究成果進(jìn)行簡要地介紹,以引起國內(nèi)相關(guān)研究領(lǐng)域?qū)W者對基于范疇論的共享系統(tǒng)數(shù)據(jù)模型的關(guān)注.

關(guān)鍵詞：數(shù)據(jù)模型；范疇論；共享系統(tǒng)；語義計(jì)算；fibration

共享系統(tǒng)以計(jì)算機(jī)和通信技術(shù)為支撐,以共享為基本運(yùn)作方式,在廣泛應(yīng)用的背景下形成和發(fā)展起來的一種企業(yè)級信息系統(tǒng),其研究范圍涉及眾多領(lǐng)域.數(shù)據(jù)模型精確描述共享系統(tǒng)的數(shù)據(jù)結(jié)構(gòu)、數(shù)據(jù)操作和語義約束,在抽象層面上描述共享系統(tǒng)的靜態(tài)特征、動態(tài)行為和依存規(guī)則,是共享系統(tǒng)的核心和基礎(chǔ),同時(shí)也是共享系統(tǒng)開發(fā)與應(yīng)用的主線.在眾多學(xué)者的共同努力下,共享系統(tǒng)數(shù)據(jù)模型作為軟件理論與程序設(shè)計(jì)方法學(xué)一個(gè)重要的應(yīng)用領(lǐng)域取得了巨大成功,在系統(tǒng)建模與形式語義分析中具有突出的作用.隨著應(yīng)用需求與軟件系統(tǒng)復(fù)雜度的不斷提升,可靠性與完備性等非功能性因素導(dǎo)致的技術(shù)難題在共享系統(tǒng)數(shù)據(jù)模型研究過程中日益突出,完善和提升已有數(shù)據(jù)模型解決問題的能力,研發(fā)通用、便利、高效的新方法和新技術(shù),成為共享系統(tǒng)數(shù)據(jù)模型新一輪的研究重點(diǎn).

范疇論是計(jì)算機(jī)科學(xué)基礎(chǔ)理論研究領(lǐng)域的一個(gè)重要方向,在數(shù)據(jù)庫系統(tǒng)建模［1］、軟件規(guī)范［2］和程序設(shè)計(jì)方法［3］等領(lǐng)域有廣泛的應(yīng)用.應(yīng)用范疇論對共享系統(tǒng)數(shù)據(jù)模型進(jìn)行研究,可有效融合共享系統(tǒng)數(shù)據(jù)模型傳統(tǒng)的研究方法,為高效處理共享系統(tǒng)數(shù)據(jù)模型的語義計(jì)算及精確描述其程序邏輯提供一種基于范疇論的統(tǒng)一的數(shù)學(xué)框架,用以研究對象的普適性與相似性,適于建立較高抽象層次的數(shù)據(jù)模型.基于范疇論的共享系統(tǒng)數(shù)據(jù)模型,以下簡稱范疇數(shù)據(jù)模型,是傳統(tǒng)數(shù)據(jù)模型研究方法在范疇論層面上的拓展與深化,特別是共代數(shù)方法（Coa1gebraic Methods）出現(xiàn)后,Monads與Comonads、Fibrations與OPfibrations等對偶范疇概念的有機(jī)結(jié)合,使得范疇數(shù)據(jù)模型在計(jì)算機(jī)科學(xué)的理論研究和工程實(shí)踐中具有廣闊的應(yīng)用前景.

研究發(fā)現(xiàn),范疇數(shù)據(jù)模型主要集中在范疇論基礎(chǔ)、現(xiàn)狀及當(dāng)前面臨的主要問題3個(gè)方面,本文從這3方面進(jìn)行綜述.受篇幅限制,本文內(nèi)容不可能涵蓋范疇數(shù)據(jù)模型這一領(lǐng)域的所有研究成果,只能概述其主要研究工作及成果.希望文本的研究能引起相關(guān)研究領(lǐng)域,特別是在形式語言理論和程序設(shè)計(jì)方法學(xué)等計(jì)算機(jī)科學(xué)基礎(chǔ)理論研究領(lǐng)域的學(xué)者的興趣與關(guān)注,進(jìn)而共同推動范疇論及其在計(jì)算機(jī)科學(xué)中的應(yīng)用與發(fā)展.

1　共享系統(tǒng)數(shù)據(jù)模型的范疇論基礎(chǔ)

范疇是范疇論最基本的概念,其基本構(gòu)成要素是對象和態(tài)射.雖然范疇的應(yīng)用較為廣泛,但目前尚未形成一個(gè)統(tǒng)一的范疇定義,本文從共享系統(tǒng)數(shù)據(jù)模型的研究角度,給出范疇的一種形式化定義.

范疇C滿足下面3條基本性質(zhì)∶

（1）匹配性質(zhì).若f o g有定義,則dom（f o g）＝dom（g）且cod（f o g）＝cod（f）；

（2）結(jié)合律性質(zhì).若 f o g與h o g有定義,則h o（f o g）＝（h o f）o g；

（3）等式射存在性質(zhì).?A∈O bj C,存在唯一的單位態(tài)射1A∈M or C,使得下式成立∶dom（1A）＝cod（1A）＝A；如果dom（f）＝A,則f o 1A＝f；如果cod（f）＝A,則1Ao f＝f.

例1以形式語言中的數(shù)據(jù)類型Ti為對象,以函數(shù)（f∶Ti→Tj）為態(tài)射,構(gòu)成形式語言范疇L.讀者很容易驗(yàn)證形式語言范疇L滿足定義1的3條基本性質(zhì).

在例1中,確定自然數(shù)、字符和布爾等一些基本的數(shù)據(jù)類型和函數(shù),可將形式語言范疇L具體化一個(gè)面向特定應(yīng)用領(lǐng)域的程序設(shè)計(jì)語言,解決一些簡單的應(yīng)用問題.同時(shí),應(yīng)用文獻(xiàn)［3］提出的簡單重用、擴(kuò)張重用和選擇重用方法可得到具有不同層次的形式語言,進(jìn)而構(gòu)成一個(gè)形式語言族范疇{Li}解決復(fù)雜應(yīng)用領(lǐng)域的實(shí)際問題,便于工程設(shè)計(jì)人員開發(fā)出結(jié)構(gòu)清晰、層次分明、正確可靠、易于維護(hù)的軟件系統(tǒng).同時(shí),{Li}中的圖表交換（Diagram Commuting）［4］性質(zhì)也為系統(tǒng)開發(fā)人員提供極大的便利,根據(jù)個(gè)人偏好和系統(tǒng)需求選擇適合軟件系統(tǒng)開發(fā)特定階段具有恰當(dāng)抽象表達(dá)能力的語言以解決特定問題.

范疇論在計(jì)算機(jī)科學(xué)中的研究思路是將研究目標(biāo)抽象為對象,將目標(biāo)間的關(guān)系抽象為態(tài)射,在高度統(tǒng)一的范疇論框架內(nèi)深入研究各種性質(zhì),如形式語言的語法構(gòu)造,語義性質(zhì)分析和語義行為描述等.當(dāng)前部分基礎(chǔ)數(shù)學(xué)文獻(xiàn)的研究基于數(shù)理邏輯不預(yù)設(shè)集合論模型的考慮,所定義的范疇不要求態(tài)射構(gòu)成一個(gè)集合,但從計(jì)算機(jī)處理離散對象的實(shí)際應(yīng)用角度分析,將態(tài)射限定在集合內(nèi)是合理的.若范疇全體對象與態(tài)射均構(gòu)成集合,則該范疇是小范疇（Sma11Category）［4］,本文的研究對象均基于小范疇.

定義2令C、D為兩個(gè)小范疇,函子F∶C →D由一對映射

例2任意范疇C都存在一個(gè)到自身的自函子F∶C → C.

函子是范疇間一種保持結(jié)構(gòu)的映射,如定義1中的單位態(tài)射和復(fù)合操作等.單位函子是自函子的一種特例,如操作語義中的空命令skiP,并發(fā)進(jìn)程的掛起操作等,而自函子的I/O返回類型相同.

定義3設(shè)P∶C→D是兩個(gè)小范疇C，D間的一個(gè)函子,f∶C→D∈M or D,P（Y）＝D.對C中一個(gè)態(tài)射u∶X→Y∈M or C,如果P（u）＝f且對?v∶Z→Y∈M or C與?h∶P（Z）→C∈M or D,有f o h＝P（v）,并存在唯一的w∶Z→X∈M or C,使u o w＝v與P（w）＝h,則稱態(tài)射u是f與Y的卡式射.

對f與Y的卡式射u,稱u位于f上；類似地,稱Y位于D上.若u是范疇C中的一個(gè)錐［4］,則由錐態(tài)射w的唯一性可知,定義3中的卡式射u是C中的泛錐（Universa1Cone）,即極限錐.相應(yīng)地,泛錐u的頂點(diǎn)X為u的終對象［5］,而由泛錐的泛性質(zhì)知卡式射u是一個(gè)同構(gòu).為簡化問題陳述而又不失一般性,記定義3中f與Y卡式射u為.

定義4設(shè)P∶C→D是兩個(gè)小范疇C，D間的一個(gè)函子,如果對?Y∈O bj C與?f∶C→P（Y）∈M or D,都存在一個(gè)f與Y的卡式射,則稱P是一個(gè)fibration.

由定義4知,fibration本質(zhì)上是一種確保大量卡式射存在的函子,對于一個(gè)fibration P∶C→D,稱D為基范疇,C為全范疇.對基范疇D中的一個(gè)對象C,?X∈O bj C,k∈M or C,若有P（X）＝C與P（k）＝1c, 則X與k構(gòu)成的子范疇CC稱為對象C上的纖維［4］,并稱k為垂直態(tài)射.實(shí)際上,纖維CC是全范疇C的一個(gè)全子范疇.

例3設(shè)S et為集合范疇,?X∈O bj S et,X上的一個(gè)謂詞是一個(gè)二元組

取例3的謂詞fibration Pre基范疇S et中態(tài)射g∶X→Y,對

例4以定義4中fibration P的基范疇的對象集O bj D構(gòu)造共享系統(tǒng)數(shù)據(jù)模型的數(shù)據(jù)結(jié)構(gòu),基范疇?wèi)B(tài)射集M or D描述共享系統(tǒng)數(shù)據(jù)模型的數(shù)據(jù)操作,而對共享系統(tǒng)數(shù)據(jù)模型中較為復(fù)雜的第三個(gè)元素語義約束,以全范疇對象集O bj C描述共享系統(tǒng)數(shù)據(jù)模型的語義性質(zhì)和語義行為,全范疇?wèi)B(tài)射集M or T對應(yīng)O bj T間存在的語義關(guān)聯(lián),并以fibration P∶C→D及其各類函子,如真值函子與等式函子等,處理共享系統(tǒng)數(shù)據(jù)模型的語義約束.在范疇論的形式化理論框架內(nèi)建立共享系統(tǒng)數(shù)據(jù)模型SD,SD＝（O bj B，Mor B，∑P）,O bj B為反映共享系統(tǒng)靜態(tài)特征的各類數(shù)據(jù)結(jié)構(gòu),M or B描述共享系統(tǒng)狀態(tài)變遷的動態(tài)行為,∑P為fibration P∶T→B及其各類函子構(gòu)成的集合,建立SD中各類數(shù)據(jù)結(jié)構(gòu)及其語義性質(zhì)和語義行為間的密切聯(lián)系,對應(yīng)共享系統(tǒng)語義約束的依存規(guī)則.

例4中的數(shù)據(jù)結(jié)構(gòu)O bj B與數(shù)據(jù)操作M or B是共享系統(tǒng)數(shù)據(jù)模型SD的基本要素,抽象描述共享系統(tǒng)的靜態(tài)特征與動態(tài)行為,而SD的語義性質(zhì)和語義行為則提供了一種從范疇論的角度深入探討數(shù)據(jù)結(jié)構(gòu)與數(shù)據(jù)操作關(guān)系及其性質(zhì)的可行途徑.

2　范疇數(shù)據(jù)模型的研究現(xiàn)狀

為支持共享系統(tǒng)的用戶以群體協(xié)作的方式高效完成任務(wù),數(shù)據(jù)模型不僅要解決空間的分布問題,處理特殊領(lǐng)域的應(yīng)用,而且要支持用戶級的共享,其研究工作異常復(fù)雜,設(shè)計(jì)與研發(fā)也相當(dāng)困難和艱巨.幾十年來,學(xué)術(shù)界和工業(yè)界根據(jù)共享系統(tǒng)應(yīng)用領(lǐng)域的業(yè)務(wù)需求、共享模式和企業(yè)信息系統(tǒng)結(jié)構(gòu)特征,從不同角度提出了大量共享系統(tǒng)數(shù)據(jù)模型,代表性工作如以Hayes和Robert等人的黑板模型［6-7］、以DePao1i和Tisato等人的計(jì)算機(jī)支持的協(xié)同工作模型［8］、以郝忠孝和湯庸等人的時(shí)態(tài)數(shù)據(jù)模型［9-10］等.相對于傳統(tǒng)共享系統(tǒng)數(shù)據(jù)模型,范疇數(shù)據(jù)模型的研究歷程相對年輕.本文僅分析范疇數(shù)據(jù)模型的研究現(xiàn)狀,傳統(tǒng)共享系統(tǒng)數(shù)據(jù)模型讀者可參見文獻(xiàn)［11］.

范疇數(shù)據(jù)模型的發(fā)展與范疇論自身的基礎(chǔ)理論研究密切相關(guān),1985年Barr與We11s［12］系統(tǒng)分析了Monads與Comonads、Fibrations與OPfibrations等重要范疇論概念的對偶性質(zhì)及其在拓?fù)渌梗═oPos）中的應(yīng)用,奠定了范疇共享系統(tǒng)數(shù)據(jù)模型的理論基礎(chǔ).20世紀(jì)90年代中后期共代數(shù)方法出現(xiàn)以后,范疇論許多對偶概念的數(shù)學(xué)性質(zhì)得到系統(tǒng)化研究.Power對Monads與Comonads間的分配律運(yùn)算進(jìn)行了較為徹底地研究［12-14］,分析了Lawvere理論生成Comonads的數(shù)學(xué)性質(zhì)［15］.Lenisa將Monads與Comonads間的分配律推廣到其他弱化結(jié)構(gòu),并分析了Ei1enberg-Moore范疇和K1eis1i范疇的數(shù)學(xué)性質(zhì)［16］.Hughes分析了Monads與代數(shù)、Comonads與共代數(shù)及其對偶性質(zhì)［17］.Street應(yīng)用2-范疇方法對Monads與Comonads間的混合分配律運(yùn)算和弱分配律運(yùn)算進(jìn)行了研究［18］.以上的范疇論基礎(chǔ)性工作為后期范疇共享系統(tǒng)數(shù)據(jù)模型的研究奠定了良好的理論基礎(chǔ),特別是對數(shù)據(jù)模型語義約束的研究產(chǎn)生了積極的推動作用,擴(kuò)展了共享系統(tǒng)數(shù)據(jù)模型語義約束分析與處理的研究思路.

當(dāng)前,范疇數(shù)據(jù)模型是共享系統(tǒng)數(shù)據(jù)模型在語義性質(zhì)與語義行為等語義計(jì)算研究方面最活躍的一個(gè)領(lǐng)域,在程序語言的類型檢查、多態(tài)計(jì)算、自動驗(yàn)證及面向?qū)ο笳Z義處理等領(lǐng)域有廣泛的應(yīng)用.Lewis首先將Comonads工具引入環(huán)境傳遞語義計(jì)算研究中［19］,隨后Uusta1u和Hasuo基于Comonads研究流計(jì)算、信號計(jì)算［20］和樹結(jié)構(gòu)轉(zhuǎn)換［21］等問題,并建立上下文依賴范疇數(shù)據(jù)模型.

存儲、I/O、異常與控制等計(jì)算效果通常與命令式程序語言相關(guān),而函數(shù)式程序語言處理這類語義行為則被認(rèn)為是臟計(jì)算（ImPure ComPutation）,但計(jì)算效果也可以通過Monads封裝在一個(gè)純函數(shù)式程序語言內(nèi)［22］.基于這一思路,M?ge1berg等學(xué)者應(yīng)用范疇論方法構(gòu)造了一個(gè)基于標(biāo)稱集Pitts范疇的元語言模型EEC（Enriched Effect Ca1cu1us）［23］,在P1otkin與Power冪域范疇內(nèi)可將EEC應(yīng)用到任何可表達(dá)的計(jì)算效果上.EEC是一種與Moggi的Monadic元語言［22］及Levy的ca11-by-Push-va1ue［24］相關(guān)的元語言模型,但在線性邏輯的構(gòu)造上對它們進(jìn)行了擴(kuò)展,EEC的通用概念為范疇數(shù)據(jù)模型的語義約束提供了一個(gè)靈活的語義計(jì)算框架.

近期,Johnson等學(xué)者將OPfibrations應(yīng)用到數(shù)據(jù)庫視圖函數(shù)式更新過程的即時(shí)語義研究中,特別是應(yīng)用Grothendieck OPfibrations提出數(shù)據(jù)庫范疇模型的c-1ens概念,研究數(shù)據(jù)庫視圖函數(shù)式更新過程的即時(shí)語義,為數(shù)據(jù)庫視圖更新問題提供了一種泛解決方法［1］.Ghani與Reve11等學(xué)者在Kennedy對計(jì)量單位的研究工作［25］基礎(chǔ)上,提出λ1-fibration的概念,以其限定于卡式閉范疇的基范疇描述單位消除語義（Unit Erasure Semantics）,以全范疇描述關(guān)系語義,并由λ1-fibration歸納地構(gòu)造參數(shù)化計(jì)量單位fibration,證明了UoM的一些基本定理,給出一些實(shí)例,在范疇論的層面對Kennedy A J的工作進(jìn)行了擴(kuò)展［26］.

范疇數(shù)據(jù)模型賦予傳統(tǒng)共享系統(tǒng)數(shù)據(jù)模型一種新的思路,對數(shù)據(jù)模型的語義約束和行為語義研究產(chǎn)生了積極的推動作用.同時(shí),由于范疇數(shù)據(jù)模型在解決抽象問題描述方面的獨(dú)特優(yōu)勢及其在理論計(jì)算機(jī)科學(xué),特別是在形式語言理論與程序設(shè)計(jì)方法學(xué)領(lǐng)域的廣闊應(yīng)用前景,已經(jīng)引起科研工作者的濃厚興趣.將范疇論方法引入共享系統(tǒng)數(shù)據(jù)模型研究中的重要意義不僅在于這一建模方法的獨(dú)特優(yōu)勢和深厚的數(shù)學(xué)理論基礎(chǔ),更主要的原因在于范疇論融入傳統(tǒng)共享系統(tǒng)數(shù)據(jù)模型的語義計(jì)算,這種獨(dú)特思路的高度抽象性、靈活擴(kuò)展性及簡潔描述性,為形式語言理論和程序設(shè)計(jì)方法的研究產(chǎn)生極為深遠(yuǎn)的影響.

3　范疇數(shù)據(jù)模型研究當(dāng)前面臨的主要問題

范疇數(shù)據(jù)模型是共享系統(tǒng)數(shù)據(jù)模型研究中相對年輕的一個(gè)領(lǐng)域,盡管范疇數(shù)據(jù)模型及其應(yīng)用已經(jīng)引起一些學(xué)者的關(guān)注,也取得一定的研究成果,但目前仍存在以下主要問題.

3.1反映共享計(jì)算本質(zhì)的內(nèi)在規(guī)律仍需要進(jìn)一步研究和完善

當(dāng)前,工業(yè)界廣泛應(yīng)用的共享系統(tǒng)數(shù)據(jù)模型使用圖形語言或文本語言工具直觀上定義用戶群體共享行為和業(yè)務(wù)共享過程,缺乏統(tǒng)一的概念和精確的形式化描述,在系統(tǒng)狀態(tài)的一致性轉(zhuǎn)換、模型轉(zhuǎn)換的語義完整性等方面缺乏堅(jiān)實(shí)的理論基礎(chǔ),導(dǎo)致數(shù)據(jù)模型的理論研究與實(shí)際應(yīng)用脫節(jié).究其主要原因,在于現(xiàn)有數(shù)據(jù)模型缺乏對共享機(jī)制內(nèi)在規(guī)律的精確描述和準(zhǔn)確表達(dá),而這種內(nèi)在規(guī)律系統(tǒng)、全面、充分地反映共享計(jì)算的本質(zhì),是深入分析用戶群體共享行為和業(yè)務(wù)共享過程的基礎(chǔ).

反映共享計(jì)算本質(zhì)的內(nèi)在規(guī)律不拘泥于任何特定的共享計(jì)算環(huán)境,在較高的抽象層面上描述用戶群體共享行為和業(yè)務(wù)共享過程,有效解決用戶群體組織自適應(yīng)問題,增強(qiáng)用戶群體共享行為的協(xié)調(diào)性和靈活性,共享規(guī)則的普適性也為共享系統(tǒng)的應(yīng)用集成提供有力支持.現(xiàn)有共享規(guī)律均側(cè)重于不同應(yīng)用領(lǐng)域設(shè)計(jì),具有較強(qiáng)的傾向性與局限性.全面、系統(tǒng)地研究共享計(jì)算的本質(zhì),提出與設(shè)計(jì)具有高度抽象性、靈活擴(kuò)展性與普適性的共享規(guī)則,建立一個(gè)便利、高效的基礎(chǔ)性理論框架仍需要進(jìn)一步研究與完善.

3.2范疇數(shù)據(jù)模型與傳統(tǒng)數(shù)據(jù)模型的有機(jī)融合還需更多的研究工作和努力

目前,范疇共享系統(tǒng)數(shù)據(jù)模型只是初步應(yīng)用于數(shù)據(jù)模型數(shù)據(jù)結(jié)構(gòu)、數(shù)據(jù)操作和語義約束的分析與處理中,它與多類代數(shù)、等式理論和泛代數(shù)等傳統(tǒng)數(shù)據(jù)模型建模方法的有機(jī)融合,特別是充分利用共代數(shù)方法在面向?qū)ο笳Z言、代數(shù)規(guī)范及語義計(jì)算中的研究成果對其進(jìn)行深入分析,還需要更多的研究工作和努力.

利用范疇論方法建立數(shù)據(jù)模型上形式語言模型,并進(jìn)一步建立復(fù)雜共享系統(tǒng)的形式語言族模型,也是一個(gè)需要更多研究工作和努力的方向.例如現(xiàn)有文獻(xiàn)只是應(yīng)用范疇定義對形式語言族模型的范疇建模過程進(jìn)行了簡單證明,但是形式語言族模型構(gòu)成復(fù)雜共享系統(tǒng)的許多元性質(zhì),如可靠性、完備性、可判定性與一致性等重要理論問題尚未解決,這也是當(dāng)前將基于范疇論的數(shù)據(jù)模型應(yīng)用于復(fù)雜共享系統(tǒng)語義分析和軟件規(guī)范描述研究中所面臨的最大挑戰(zhàn)和難題之一.同時(shí),應(yīng)用函子的保持性質(zhì)、反射性質(zhì)和生成性質(zhì)及自然轉(zhuǎn)換復(fù)合定理深入分析數(shù)據(jù)模型構(gòu)成高階范疇的數(shù)學(xué)性質(zhì)和語義解釋也需要大量的研究工作.

3.3范疇論及其在共享系統(tǒng)數(shù)據(jù)模型中的應(yīng)用研究仍需要進(jìn)一步深化和完善

現(xiàn)代科學(xué)研究中,范疇論為各學(xué)科間多樣化的聯(lián)系提供了抽象、統(tǒng)一和簡潔的數(shù)學(xué)語言.但范疇論自身也處于不斷發(fā)展過程中,如Monads與Comonads、Fibrations與OPfibrations等對偶范疇概念分配律運(yùn)算性質(zhì)的深入研究、范疇C上小范疇的切片范疇C at/C中基于分裂OPfibrations的KZ-monads代數(shù)結(jié)構(gòu)、C at/C中基于分裂Fibrations的CoKZ-monads代數(shù)結(jié)構(gòu)、伴隨函子的復(fù)雜性質(zhì)與Monads結(jié)構(gòu)、2-范疇理論的深入分析和數(shù)學(xué)解釋、Comonadic函子存在的前提條件及其數(shù)學(xué)性質(zhì)、基于范疇角度對拓?fù)湎到y(tǒng)的研究等許多方面還需繼續(xù)深化和完善,而且需要將上述研究成果進(jìn)一步從基本范疇,如集合范疇與偏序集范疇等,推廣到群、環(huán)、拓?fù)淇臻g和拓?fù)渌沟绕渌麖?fù)雜范疇,拓寬范疇論自身的數(shù)學(xué)寬度和深度.

在形式語言理論與程序設(shè)計(jì)方法學(xué)研究中,范疇論在程序語言設(shè)計(jì)、形式語義分析和程序正確性驗(yàn)證等理論計(jì)算機(jī)科學(xué)領(lǐng)域有著廣泛的應(yīng)用.數(shù)據(jù)模型可嚴(yán)格地建立在范疇論的數(shù)學(xué)基礎(chǔ)上,雖然目前范疇數(shù)據(jù)模型研究已取得一定進(jìn)展,但仍有許多問題并未引起足夠關(guān)注和有效解決,如基于素描（Sketch）的范疇論方法對形式語言模型的復(fù)雜語義統(tǒng)一建模、模型范疇（Mode1Category）形式化框架內(nèi)模型轉(zhuǎn)換的正確性、對數(shù)據(jù)模型復(fù)雜語義約束的形式化描述、基于拉回（Pu11back）、等值子和極限等范疇論工具對數(shù)據(jù)模型語義約束中各類異構(gòu)對象的集成、K1eis1i范疇與Cok1eis1i范疇在共享系統(tǒng)中的研究與應(yīng)用、應(yīng)用拓?fù)淅碚撋钊?、系統(tǒng)地研究數(shù)據(jù)模型等也是范疇數(shù)據(jù)模型研究中需要解決的問題.

4　總結(jié)與展望

通過近幾年對數(shù)據(jù)模型、范疇論及程序設(shè)計(jì)方法的研究和總結(jié),本文認(rèn)為目前范疇數(shù)據(jù)模型的研究領(lǐng)域呈現(xiàn)出以下新的特點(diǎn)和發(fā)展趨勢∶（1）范疇數(shù)據(jù)模型為類型理論與程序設(shè)計(jì)方法等領(lǐng)域的研究提供了一個(gè)基于范疇論的形式化框架,將計(jì)算機(jī)科學(xué)中許多重要的基礎(chǔ)理論有機(jī)融合起來,提供新的研究思路進(jìn)而促進(jìn)各相關(guān)理論的深入發(fā)展.如以Monads結(jié)構(gòu)確定的K1eis1i范疇解釋數(shù)據(jù)模型語義約束的外延語義,而Cok1eis1i范疇則可以解釋內(nèi)涵語義,更為重要的是,通過分配律確定的Bik1eis1i范疇可有機(jī)融合外延語義描述的各種計(jì)算副作用與內(nèi)涵語義描述的內(nèi)部計(jì)算細(xì)節(jié),提高數(shù)據(jù)模型對語義約束抽象描述的擴(kuò)展性、統(tǒng)一性與便捷性.（2）范疇數(shù)據(jù)模型的研究歷程相對年輕,與傳統(tǒng)數(shù)據(jù)模型的融合還存在許多問題有待解決.尤其是形式語言族模型構(gòu)成復(fù)雜共享系統(tǒng)的可靠性與完備性等重要元性質(zhì)的形式證明還未得到有效解決,使其在短期內(nèi)無法得到廣泛應(yīng)用,這也是當(dāng)前基于范疇論的共享系統(tǒng)數(shù)據(jù)模型在行為語義和規(guī)范描述研究中面臨的最大難題之一.（3）范疇論自身的高度抽象性和理論復(fù)雜性,使其在計(jì)算機(jī)科學(xué)各研究領(lǐng)域中得到廣泛應(yīng)用,并建立起一套完整的基于范疇論的共享系統(tǒng)數(shù)據(jù)模型建模方法存在一定困難.但是應(yīng)用范疇論工具深入研究共享系統(tǒng)數(shù)據(jù)模型已經(jīng)引起學(xué)術(shù)界的關(guān)注與重視,在范疇論的數(shù)學(xué)框架內(nèi)對數(shù)據(jù)模型復(fù)雜語義進(jìn)行形式化建模,將對形式語言理論的研究、共享系統(tǒng)設(shè)計(jì)與實(shí)現(xiàn)的工程實(shí)踐活動產(chǎn)生積極且深遠(yuǎn)的影響.

由于范疇論還在不斷發(fā)展的過程中,將來會有越來越多的對偶關(guān)系和分配律被發(fā)現(xiàn).展望范疇數(shù)據(jù)模型的進(jìn)一步研究內(nèi)容,本文認(rèn)為至少有以下兩個(gè)方面∶一方面,范疇論高度的抽象性、靈活的擴(kuò)展性和簡潔的描述性使其為類型理論、泛代數(shù)、共代數(shù)與程序設(shè)計(jì)方法等領(lǐng)域的研究提供了更為便捷的研究手段,并形成獨(dú)特的研究思路,進(jìn)而促進(jìn)范疇論在計(jì)算機(jī)科學(xué)各相關(guān)研究領(lǐng)域的廣泛應(yīng)用和深入發(fā)展；另一方面,范疇論在共享系統(tǒng)數(shù)據(jù)模型語義約束中的研究與應(yīng)用,特別是充分利用共代數(shù)方法在面向?qū)ο笳Z言、代數(shù)規(guī)范及語義計(jì)算中的研究成果,形成范疇數(shù)據(jù)模型的研究成果,同時(shí)也促進(jìn)了范疇論自身的發(fā)展,并為其在計(jì)算機(jī)科學(xué)領(lǐng)域中的進(jìn)一步應(yīng)用起到積極的推動作用.

范疇數(shù)據(jù)模型目前尚處于理論深化和完善階段,具體的應(yīng)用研究相對較少.作為多類代數(shù)、等式理論、泛代數(shù)等傳統(tǒng)數(shù)據(jù)模型研究方法的繼承與發(fā)展,范疇數(shù)據(jù)模型將為計(jì)算機(jī)科學(xué)中許多領(lǐng)域的研究及范疇論自身的發(fā)展帶來積極和深遠(yuǎn)的影響,對其及時(shí)地展開研究具有重要的理論研究價(jià)值和廣闊的應(yīng)用前景.

參考文獻(xiàn)：

［1］Johnson M,Rosebrugh R,Wood R J.Lenses,fibrations and universa1 trans1ations［J］.Mathematics Structure in ComPuter Science,2012（22）∶25-42.

［2］Tews H.Coa1gebra method for object-oriented sPecification［D］.Dresden∶Institute Theoretic Information,Technica1University Dresden,2002∶13-53.

［3］苗德成,奚建清,劉勇,等.一種形式語言代數(shù)模型［J］.華南理工大學(xué)學(xué)報(bào)∶自然科學(xué)版,2011,39（10）∶74-78.

［4］Barr M,We11s C.Category theory for comPuting science［M］.New York∶Prentice-Ha11,1990∶252-270.

［5］賀偉.范疇論［M］.北京∶科學(xué)出版社,2006∶1-41.

［6］Hayes R B.A b1ackboard architecture for contro1［J］.Artificia1 Inte11igence,1985,26（3）∶251-321.

［7］Robert TC,Efraim T.Distributed inte11igentexecutive information systems［J］.Decision SuPPort Systems,1995,14（2）∶117-130.

［8］DePao1i F,Tisato F.A mode1 for rea1-time co-oPeration［C］//Proceedings of the secondconference on EuroPean Conference on ComPuter-SuPPorted CooPerative Work.MA,USA.ACM Press,1991∶203-217.

［9］郝忠孝.時(shí)態(tài)數(shù)據(jù)庫設(shè)計(jì)理論［M］.北京∶科學(xué)出版社,2009∶3-80.

［10］湯庸,葉小平,湯娜.時(shí)態(tài)信息處理技術(shù)及應(yīng)用［M］.北京∶清華大學(xué)出版社,2010∶92-214.

［11］苗德成.共享系統(tǒng)數(shù)據(jù)模型研究與應(yīng)用［D］.廣州∶華南理工大學(xué),2012∶5-12.

［12］Barr M,We11s C.ToPoses,triP1es and theories［M］.New York：SPringer,1985∶35-78.

［13］Power J,Watanabe H.Combining amonad and a comonad［J］.Theoretica1ComPuter Science,2002（280）∶137-162.

［14］Power J,Watanabe H.Distributivity foramonad and a comonad［C］//Proceedings SecondWorkshoPofCMCS＇99,1999∶1-14.

［15］Power J,Shkaravska O.From comode1s to coa1gebras∶state and arrays［J］.E1ectronic Notes in Theoretica1ComPuter Science, 2004,7（5）∶453-468.

［16］Lenisa M,Power J,Watanabe H.Distributivity for endofunctors,Pointed and co-Pointed endofunctors,monads and Comonads［C］//Coa1gebraic Methods in ComPuter Science（CMCS＇00）,E1ectronic Notes in Theoretica1 ComPuter Science,2000 （33）∶233-263.

［17］Hughes J.A study of categories of a1gebras and coa1gebras［D］.P：ttsburgh：DePartment of Phi1osoPhy,Carnegie Me11on University,2001.

［18］Street R.Weak distributive 1aws［J］.Theory and APP1ications of Categories,2009,22（12）∶313-320.

［19］Lewis J R,Shie1ds M B,Meijer E,et a1.ImP1icit Parameters∶dynam ic scoPing with static tyPes［C］//Proceedings of 27th ACM SIGPLAN-SIGACT SymPosiums on PrinciP1es of Programming Languages.New York∶ACM Press,2000∶108-118.

［20］Uusta1u T,Vene V.Signa1s and Comonads［J］.Journa1of Universa1ComPuter Science,2005,22（7）∶1310-1326.

［21］Hasuo I,Jacobs B,Uusta1u T.Categorica1viewson comPutationson trees［J］.Lecture Notes in ComPuterScience,2007（4596）∶619-630.

［22］Moggi E.Notions of comPutation and Monads［J］.Information and ComPutation,1991（93）∶55-92.

［23］Mθge1berg R E,Staton S.Fu11 abstraction in a meta1anguage for state［J］.InWorkshoPon Syntax and Semantics of Low Leve1 Languages,2010（18）∶126-145.

［24］Levy P B.Ca11 by Push va1ue,a functiona1/imPerative synthesis［J］.Semantic Structures in ComPutation,2004（2）∶1-47.

［25］Kennedy A J.Re1ationa1Parametricityand unitsofmeasure［C］//POPL,97∶In Proceedings of the 24th ACM SIGPLAN-SIGACT SymPosium on PrinciP1es of Programming Languages.New York∶ACM Press,1997∶442-455.

［26］Ghani N,Reve11T,Atkey R,et.a1.Fibrationa1units of measure［EB/OL］.［2015-03-21］.httPs∶//Persona1.cis.strath.ac.uk/ nei1.ghani/Pub.htm1.

（責(zé)任編輯∶邵曉軍）

中圖分類號：TP301.2

文獻(xiàn)標(biāo)識碼：A

文章編號：1007-5348（2015）10-0015-06

［收稿日期］2015-06-27

［基金項(xiàng)目］廣東省自然科學(xué)基金項(xiàng)目（S2013010015944）；廣東省高等學(xué)校優(yōu)秀青年教師培養(yǎng)計(jì)劃項(xiàng)目（YQ2014155）；韶關(guān)市科技計(jì)劃項(xiàng)目（2013CX/K61）.

［作者簡介］苗德成（1979-）,男,黑龍江伊春人,韶關(guān)學(xué)院信息科學(xué)與工程學(xué)院副教授,博士；研究方向∶形式語言理論與范疇論方法.

A Survey on Sharlng System Data M odel Based on Category Theory

MIAO De-cheng
（Schoo1 of Information Science and Engineering,Shaoguan University,Shaoguan 512005,Guangdong,China）

Abstract∶Data mode1 is core and basis of design and deve1oPment for sharing system,and category theory has Particu1ar advantages on mode11ing sharing system data mode1,which Provides so1id math foundation for describing semantic comPutation and Program 1ogic accurate1y,meanwhi1e,it has wide aPP1ication ProsPect. This PaPer brief1y introduced some Primary and 1atest research fruits inc1uding categorica1 basis of sharing system data mode1,the status quo of sharing system data mode1 based on category theory and Present Prime Prob1ems.It is hoPed that it can raise the awareness of domestic researchers in re1ated fie1ds for sharing system data mode1based on category theory.

Key words∶data mode1；category theory；sharing system；semantic comPutation；fibration