猜你喜欢
计算系统的形式语义

计算系统的形式语义

书籍作者：陆汝钤 ISBN：9787302414940
书籍语言：简体中文 连载状态：全集
电子书格式：pdf,txt,epub,mobi,azw3 下载次数：4460
创建日期：2021-02-14 发布日期：2021-02-14
运行环境：PC/Windows/Linux/Mac/IOS/iPhone/iPad/Kindle/Android/安卓/平板
内容简介
计算系统的形式语义是目前计算机科学理论研究的两大方向之一，其研究成果对程序设计语言、编译技术、应用软件、分布式系统等分支领域有重大的实际意义。本书大体上分为三个部分。第一部分是数学基础，为第一章。第二部分包括第二到第五章，概述了形式语义中的操作语义、指称语义、公理语义和代数语义四大经典流派。第三部分包括第六到第九章，概述了形式语义学的现代应用， 分别介绍分布式系统、移动计算和移动通信系统、非规范进程代数和微观生命系统，以及量子程序设计语言的形式语义。
　　全书内容丰富，结构严谨，集形式语义学理论及其应用的有关分支之大成，系统地反映了这个领域各方面的研究成果，特别是它的近代发展潮流和趋势，并对不同流派的理论和方法给予了分析和评论。
　　本书可作为计算机科学专业研究生、本科生有关课程的教材或教学参考书，也可供有关专业或交叉学科的科研人员进修或作为工具书。
前言
前言计算系统的形式语义前言
　　本书是1992年出版的《计算机语言的形式语义》一书（简称1992版）的更新版。在1992版中我们分别介绍了形式语义形式语义的四个主要流派：操作语义、指称语义、公理语义和代数语义，并在此基础上综合阐述了并发和分布式程序分布式程序的形式语义。从该书出版以来，已经二十余年过去了，在此期间，国内外形式语义学的研究有了许多重大的突破。
　　首先，应该提到的是移动通信的发展促进了一类新的进程代数——π演算的出现和发展，使得用进程代数编写的程序不仅可以在固定网络上运行，而且可以改变通信网络的拓扑结构，并在可变的网络结构上实行通信。围绕π演算出现了许多变种，开展了深入的研究。除了可变的网络结构之外，π演算还创造了其他的手段来改进通信技术。例如，利用π演算，有可能建立专用的私密信道。随着π演算而兴起的环境演算环境演算Ambient甚至可以提供建立网上防火墙的手段。服务于保密通信的Spi演算Spi演算把编码和解码引进了语言之中。带有噪音信道的含噪进程代数有希望把香农的信息论引进进程代数中，从而在两类通信理论之间架起一座桥梁。所有这些使得服务于移动通信的进程代数成了一门单独的学问。
　　其次，分子生物学是近年来发展最快的研究方向之一。人类基因图谱的测序完成大大推动了基因组学、蛋白质组学，以及系统生物学的研究。恩格斯曾经说过，数学在生物学中的应用为零，但是这样的时代早就过去了。以数学为基础的形式化方法已经深入到生物领域，成为描述微观生命现象的有力手段。特别值得称道的是概率论和随机过程作为重要的数学手段在面向微观生命现象的进程代数理论中发挥了重要作用。除了概率进程代数、随机进程代数和性能评估进程代数这些比较通用的工具之外，一大批特意针对微观生命现象的描述工具已经被设计出来并投入应用。诸如Bioambient、因果π演算、化学抽象机、生化抽象机等工具提供了许多颇有启发的思路。描述微观生命现象的数学工具早已经不纯粹是微积分和微分方程等连续数学的天下，而成了连续工具和离散工具八仙过海的多极世界。
　　再次，实用化量子计算机出现和推广应用的前景正在吸引越来越多的科学家关注量子计算领域。近年来出现了一批面向量子计算的程序设计语言，其中也包括量子进程代数，科学家们已经开始讨论量子软件和量子软件工程。量子程序设计和经典程序设计有许多本质不同。例如，量子不可克隆原理的存在使得量子程序设计语言不可能有简单的赋值语句。同时，由于对一个量子系统的测量会引起该系统所处状态的坍缩，这使得系统状态的可观察性和程序运行流程的可控制性受到影响。另一方面，量子力学的特殊性质并非只对量子程序设计起限制作用，它的某些性质有可能对量子程序设计是“有用”的。例如，量子离物传态量子离物传态、量子密集编码、量子密码通信等方面的研究成果有可能对量子网络和分布式量子软件工程产生较大影响，宜于我们去关注和开发利用。在一定意义上，量子程序的运行可以用经典程序来模拟。因此，尽管量子计算机还没有完全实现，但是量子程序设计和量子软件的研究并不一定要等到量子计算机实现以后再做，而是可以先行一步。而量子密码通信先于量子计算机的实现又提供了研究量子软件的必要性和现实性。更进一步说，量子软件的研究成果可以为未来量子计算机的设计提供新思路，比起先有经典计算机，后有经典程序设计的历史来说，这样做更合理。同样，在实际设计和使用量子程序设计语言之前先把它们的数学基础，即形式语义研究清楚，然后再去设计和使用，这比起传统的程序设计语言先设计、先使用，后论证其理论基础、后补其漏洞来说，未尝不是一件好事。
　　近十余年来形式语义学的研究成果极其丰富，本书把以上三个方面作为补写和更新的重点，是充分考虑到实践需求的一种选择。这三个方面都具有强烈的应用背景，同时又有深刻的理论问题，构成了三个新的章。同时本书也对原有的六章内容做了必要的补充。其中主要的四部分是：指称语义一章原书以（反映程序不确定性的）幂域理论结尾，本书添加了概率幂域理论和概率加不确定性幂域理论，同时还介绍了基于单体的计算理论和指称语义的完全抽象性完全抽象性研究。在公理语义一章添加了Hoare逻辑的概率推广和Dijkstra最弱前置条件语义最弱前置条件语义（简称最弱前置语义）的概率推广。同时还介绍了基于一种实时模态逻辑的时段演算。并发和分布式语义一章原来重点介绍了CSP和CCS两个进程代数理论，本书补充介绍了另一个重要的进程代数ACP， 从而比较完备地展示了进程代数家族的三剑客架构。另外还分别给出了以扩充Petri网形式出现的CCS真并发语义和以抽象数据类型形式出现的CCS代数语义。这两种方法原则上可以推广到其他进程代数。这一章最后以Glabbeek的进程代数并发语义的比较研究结尾。最后，由于本书增添了以上各项内容，对第一章数学基础也要做必要的（最低限度的）增补。其中完整增加的有三节：一些基本的代数、拓扑和泛函知识，概率和随机过程随机过程知识，以及线性逻辑和Gentzen演算知识。另外对范畴论和格论两节做了必要的增补。
　　自然界有大量的信息交换并不采取人类语言或计算机语言的形式。一个明显的例子是生命系统。例如，DNA序列就可以看成是一种文字，它构成了生命的“天书”。基因对蛋白质的表达，细胞间和细胞内部的通信，这里都有信息交换和信息处理在起作用。另一个明显的例子是量子系统。凡涉及量子计算、量子纠缠、量子通信、量子密钥等问题，无不归于信息表示和信息处理的范畴。尽管现在的生命过程描述语言和量子程序设计语言都以计算机语言的形式出现，用于生命现象的模拟、预测和量子计算机的编程，我们仍然可以把微观生命系统和量子系统看成自然界的“天造”计算系统。俗话说人算不如天算，它们不仅应该和人造的计算系统平起平坐，而且还为人造计算系统提供了启示和展望。为此也需要形式化的数学工具，以严格和正确地刻画生命信息和量子信息的表示和处理。为此，我们统称本书的内容为计算系统的形式语义。
　　本书的内容通过每章的概述、除概述以外的各节，以及文献和中、英名词索引四部分组成，它们互不包含。概述是各章涉及内容的一个鸟瞰。章中各节是对其中某些内容有选择地展开讲解。文献是前两部分内容的出处和延伸阅读信息，其中早期文献可以提供有关研究的发展渊源信息，而近期文献则可以提供相关领域的发展前景和专家们的视角。由于形式语义的文献数量极多，肯定有一些重要的有关文献在写作本书时被遗漏掉。即使是已经列入本书介绍范围的一些文献，也肯定有一些因为作者理解不深，甚至理解有误而未能在本书中正确介绍其思想。我想提请读者注意的是，本书不能作为开展研究工作的直接依据。有兴趣在形式语义领域开展研究的读者，可以参照本书提供的线索，进一步阅读原著文献，可以在阅读时对照本书的解释、分析和某些进一步的发展，但是不能忽视阅读原著，以免出现可能的误导。
　　本书在撰写过程中得到了很多专家的帮助。从开始有写这本书的计划起，作者经常和应明生教授就此交流看法并得到他的很多宝贵建议。应明生、周巢尘、林惠民、夏培肃、陈仪香、袁崇义、林闯、李未、李克正、Bauer、Petri、Broy、KriegBrückner、Reisig等教授都曾向作者提供他们的著作，使作者获得了宝贵的知识来源。为撰写本书，作者参考的文献数量较大，无法一一致谢。其中包括许多不署名的维基百科类资料，非常感谢这些未曾谋面的知识传播者。我们在书中尽可能地对引用的资料给出了出处，包括插图。
　　为了减少本书可能给读者带来的枯燥感，我们在每一章的前面加配了一首唐诗，每首诗的意境和它所在章的内容（之某些重要部分）存在一些本质的联想。我想读者会同意：在文化艺术和科学技术这两个差别巨大的领域之间不可能有真正的科学对应关系或推理关系，必须强调这仅仅是一种联想关系。它肯定不唯一，也肯定因人而异。学习和研究都是艰苦的劳动，但同时也应该是快乐的。作者赞成博拉·米卢蒂诺维奇的快乐足球理念，从事科学工作也要有快乐感。在此感谢马冬洁应邀为封面作图，并为每章的唐诗配图作画，使本书增色不少。
　　作者真诚地感谢清华大学出版社的大度宽容和坚定支持，使得这本撰写时间宽度达十年以上的书稿能够最终完成。
目录
第1章数学基础
1.1λ演算
1.2格论
1.3范畴论
1.4不动点理论
1.5Petri网论
1.6Hilbert空间和相关拓扑、代数结构
1.7概率和随机过程
1.8矢列演算、线性逻辑、线性类型系统和线性带类型λ演算
1.8.1从矢列演算讲起
1.8.2线性逻辑
1.8.3线性类型系统

第2章操作语义
2.1概述
2.2SECD抽象机
2.3维也纳定义语言
2.4赫斯利方法和PL／Ⅰ标准
2.5W文法及其抽象机
2.6变换语义学
2.7结构化的操作语义

第3章指称语义
3.1概述
3.2指称语义的描述方法
3.3函数式语言的指称语义
3.4命令式语言： 直接语义和继续语义
3.5变量、说明和作用域
3.6过程和函数
3.7元语言META Ⅳ
3.8域的递归理论
3.9递归域的两个模型
3.10幂域理论
3.11不确定程序的指称语义
3.12概率幂域和概率指称语义
3.13基于概率不确定幂域的指称语义
3.14计算理论的范畴论语义

第4章公理语义
4.1概述
4.2Hoare公理系统
4.3分程序的公理语义
4.4过程的公理语义
4.5联立子程序的公理语义
4.6类程的公理语义
4.7Pascal的公理语义
4.8完备性和可表达性
4.9过程公理的健康性和完备性
4.10完全正确性
4.11最弱前置条件和不确定性公理语义
4.12最弱概率前置语义
4.12.1概率程序的最弱前置语义
4.12.2概率不确定程序的最弱前置语义
4.13类型理论和程序逻辑
4.14模态逻辑和时序逻辑
4.15分支时序逻辑和线性时序逻辑
4.16区间逻辑和时段演算
4.16.1区间逻辑IL
4.16.2时段演算DC
4.16.3一个实例
4.17动态逻辑

第5章代数语义
5.1概述
5.2Σ代数和初始语义
5.3扩充的公理形式
5.4健康性、完备性和可判定性
5.5充分完备性和层次一致性
5.6理论描述语言Clear
5.7代数语义的范畴论基础
5.8终结语义
5.9格语义
5.10可观察性和观察等价性
5.11偏Σ代数
5.12模型描述语言ASL
5.13程序设计语言的代数语义
5.14带动态结构的程序的语义

第6章并发和分布式程序的形式语义
6.1概述
6.2分布式程序设计语言CSP
6.3CSP的结构化操作语义
6.4CSP的流语义
6.5TCSP和失败语义
6.6并行程序的公理语义
6.7CSP的公理语义
6.8通信系统演算(CCS)
6.9CCS的操作语义
6.10同步树和通信树
6.11双模拟和行为等价性
6.12SCCS和集合推导语义
6.13CCS的偏序推导语义
6.14CCS的Petri网语义
6.15分布式变迁系统和CCS
6.16CCS的真并发语义
6.17HennessyMilner 逻辑
6.17.1基本HM逻辑
6.17.2带递归HM逻辑
6.18通信进程代数 ACP家族及其静态语义
6.18.1基本进程代数BPA
6.18.2进程代数PA
6.18.3通信进程代数ACP
6.18.4ACP的扩充
6.18.5ACP的最大扩充ACPc
6.19动态ACP及其操作语义
6.20ACP的指称语义和双模拟语义
6.21抽象数据类型作为进程代数的代数语义
6.22进程代数并发语义的比较研究

第7章移动通信和移动计算系统的形式语义
7.1概述
7.2π演算及其操作语义
7.3π演算的双模拟语义
7.4进程代数的符号变迁语义
7.4.1CCS型的进程代数的符号语义
7.4.2π演算的（强）符号语义
7.4.3π演算的（弱）符号语义
7.5多维π演算和异步π演算
7.5.1多维π演算
7.5.2异步π演算
7.6安全π演算SPI
7.7SPI演算的环境敏感双模拟语义
7.8Applied π演算
7.9Applied π演算的符号语义
7.9.1Delaune，Kremer和Ryan的DApplied π演算及其
符号语义
7.9.2DolevYao模型、可达性模型和约束系统
7.9.3刘佳和林惠民的符号LApplied π演算语义
7.10对称π演算： χ演算和Fusion演算
7.10.1χ演算
7.10.2Fusion演算
7.11移动Ambient演算
7.11.1基本Ambient演算——移动Ambient演算
7.11.2完整Ambient演算——通信Ambient演算
7.12Ambeint演算的类型系统
7.13分布式Ambient演算的双模拟语义
7.14安全Ambient演算及其双模拟语义
7.14.1安全Ambient演算SA
7.14.2带口令的安全Ambient演算SAP
7.15封装Ambient演算
7.15.1封装Ambient演算BA
7.15.2新封装Ambient演算NBA
7.15.3密封Ambient演算SBA

第8章非规范进程代数和微观生命系统的形式语义
8.1概述
8.2从强化操作语义到因果π演算
8.3概率进程代数
8.3.1部分概率进程代数PCCS
8.3.2全概率进程代数APPA
8.4性能评估进程代数PEPA
8.5随机π演算
8.6含噪π演算
8.7进程演算的拓扑理论
8.8进程序列演算CPS
8.8.1CPS的语法和操作语义
8.8.2CPS的序列双模拟语义
8.8.3CPS的特征序列双模拟语义
8.9CPS的序列极限双模拟
8.9.1动程的贴近双模拟语义
8.9.2CPS的极限序列双模拟语义
8.10Gillespie算法
8.11π通路演算——分子水平的生物进程代数
8.11.1关于通路
8.11.2π通路演算编程信号传导通路
8.11.3随机π通路演算编程基因调控通路
8.12κ演算——基于规则的蛋白质相互作用语言
8.12.1蛋白质相互作用和κ演算
8.12.2κ演算的操作语义和带钩语义
8.12.3κ演算的指称语义
8.13从Gamma模型到化学抽象机
8.13.1Gamma计算模型
8.13.2化学抽象机
8.13.3概率化学抽象机
8.13.4模糊化学抽象机
8.14生化抽象机和计算树逻辑
8.15溶液级建模语言BioPEPA
8.16固定生物膜计算和P系统
8.16.1基本P系统及其变型
8.16.2基于通信的P系统
8.16.3面向DNA计算的H系统和拼接P系统
8.16.4神经型P系统和尖峰放电型P系统
8.17基于移动生物膜的BioAmbients演算
8.17.1BioAmbients演算的基本内容
8.17.2随机BioAmbients演算
8.18膜演算语言Brane
8.18.1膜演算
8.18.2射影膜演算

第9章量子语言的形式语义
9.1概述
9.2一些基本概念
9.2.1基于波动力学的量子力学公设
9.2.2量子力学公设的Hilbert空间表示
9.2.3量子力学公设的Dirac表示形式
9.3量子随机存取机、量子伪码及其操作语义
9.3.1Knill的量子随机存取机QRAM
9.3.2Nagarajan等的顺序量子随机存取机SQRAM
9.3.3Ado和Mateus的基于复杂性分析的QRAM设计及其
操作语义
9.4命令式量子语言及其操作语义
9.4.1命令式量子程序设计语言QCL
9.4.2命令式量子程序设计语言LanQ的抽象机语义
9.4.3不确定性命令式量子语言qGCL
9.5量子λ演算及其类型系统
9.6函数式量子语言的框图操作语义
9.7量子程序语义的范畴论诠释
9.8量子可逆计算和不可逆计算
9.8.1刻画可逆计算的严格广群语义
9.8.2刻画不可逆计算的幺半群范畴语义
9.8.3函数式量子语言QML及其可逆化操作语义
9.8.4从不可逆计算到可逆计算： pGCL语言的可逆化改造

9.9函数式量子语言的范畴论指称语义
9.10量子程序的最弱前置条件语义和公理语义
9.10.1Hermitian算子作为量子谓词
9.10.2最弱前置条件语义及其证明规则
9.10.3量子程序的Hoare公理系统
9.11量子进程代数的操作语义
9.11.1量子进程代数QPALg
9.11.2通信量子进程CQP
9.11.3量子多项式机器QPM
9.12量子进程代数的双模拟语义
9.12.1qCCS1及其量子概率双模拟语义
9.12.2qCCS2及其渐近双模拟
9.12.3QPALg的概率分支双模拟