计算系统的形式语义

计算系统的形式语义前言本书是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等教授都曾向作者提供他们的著作，使作者获得了宝贵的知识来源。为撰写本书，作者参考的文献数量较大，无法一一致谢。其中包括许多不署名的维基百科类资料，非常感谢这些未曾谋面的知识传播者。我们在书中尽可能地对引用的资料给出了出处，包括插图。为了减少本书可能给读者带来的枯燥感，我们在每一章的前面加配了一首唐诗，每首诗的意境和它所在章的内容（之某些重要部分）存在一些本质的联想。我想读者会同意：在文化艺术和科学技术这两个差别巨大的领域之间不可能有真正的科学对应关系或推理关系，必须强调这仅仅是一种联想关系。它肯定不，也肯定因人而异。学习和研究都是艰苦的劳动，但同时也应该是快乐的。作者赞成博拉·米卢蒂诺维奇的快乐足球理念，从事科学工作也要有快乐感。在此感谢马冬洁应邀为封面作图，并为每章的唐诗配图作画，使本书增色不少。作者真诚地感谢清华大学出版社的大度宽容和坚定支持，使得这本撰写时间宽度达十年以上的书稿能够终完成。