小议基于双代数的进程语义研究

《小议基于双代数的进程语义研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中山大学硕士学位论文基于双代数的进程语义研究姓名：陈鹤群申请学位级别：硕士专业：计算机软件与理论指导教师：周晓聪20060501论文题目：专业：硕士生：指导教师：基于双代数的进程语义研究计算机软件与理论陈鹤群周晓聪副教授摘要双代数是同一基集上的代数共代数对，它结合了代数的构造和共代数的观察。计算机科学中的许多概念都是构造与观察的结合体，如程序、进程、自动机等，都可用双代数方法进行研究。目前，双代数方法已经被证明是研究基于状态系统的静态结构与动态行为之间的关系及性质的可行途径。由于程序的语法构造可以通过初始代数给出，程序的行为描述可以通过终结共代数给出，因此可以在初

2、始代数和终结共代数上构造双代数，组成一个双代数对，从而利用初始代数和终结共代数的性质，研究该语言的形式语义。这种使用双代数结构研究形式语义的的方法是共代数研究领域中一个最新的研究方向，已经应用在对进程、自动机等的操作语义和指称语义的性质研究之中。进程具有典型的代数与共代数性质，是一个双代数：它的语法表达式可以看成某个基调上的项，这是代数结构；它的运行可以通过内部状态的变迁来展示其可观察行为，这是共代数行为。因此，进程的语义也可利用双代数结构进行研究。本文利用初始代数与终结共代数上的双代数结构，对进程的语义进行研究。文章首先研究J．Rutten给出的双代数结构，探讨

3、其成立的条件，并结合D．Turi使用双代数研究操作语义与指称语义间对偶性的一些成果，研究双代数结构在进程代数中的应用。文章提出了一个能够用双代数结构描述的进程代数模型，分析了由该模型定义的进程的代数与共代数特性，在研究变迁系统规范和定义出终结共代数上的代数操作的前提下，将这个模型扩展到双代数结构中，并给出进程的操作语义和指称语义描述。文章最后使用初始代数上的归纳原理、终结共代数上的共归纳原理，证明了一些进程性质，展示了双代数语义方法的应用。关键词：双代数、进程代数、进程语义、初始语义、终结语义Title：Major：Name：SupervisorBialgebra

4、icSemanticsforProcessesComputerSoftwareandTheoryChenHequnZhouXiaocongIAssociateProfessorAbstractIIIAbialgebraconsistsofanalgebra-coalgebrapairwithacommoncarrier．Itcombinethenotionofconstructionandthenotionofobservation．Incomputerscience，mostobjectsareconstructiveandhaveobservablebehav

5、iors，suchaspro-gram，process，automaton，etc．Theyca／lbestudiedthroughthemethodsofbialgebra．Bialgebrmcmethodswereprovedtobeaeffectivewaytoinvestigatetherelationshipbetweenstaticstructureanddynamicalbehaviorofstate-basedsystems．Thesyntaxofaprogramminglanguageisainitialalgebralwhiletheseman

6、ticsofthislanguageisafinalcoalgebra．Apairofbialgebracanbeconstructedbygivenacoalgebraoninitialalgebra，andaalgebraonfinalcoalgebra．Ifthebialgebrapairsareconstructedunderthesamefunctor，thepropertiesofinitialalgebraandfinalcoalgebracallbeusedtoinvestigatethesemanticsofprogram．Thiswayisan

7、ewideainthetheoryofcoalgebra，andhasbeenappliedinthestudiesofoperationalsemanticsanddenotationalsemanticsforprocess，automaton，etc．ProcessCanbeconsideredasbialgebra：Asaalgebra，itssyntaxexpressionsaretermsofcertainsignature；Asacoalgebra，itsdynamicalbehaviorcanbeobservedthroughthetransiti

8、onofi