計算系統的形式語義

《計算系統的形式語義》是一本於2017年2月1日清華大學出版社出版的圖書，作者是陸汝鈐。 ^[1] 

計算系統的形式語義是計算機科學理論研究的兩大方向之一，其研究成果對程序設計語言、編譯技術、應用軟件、分佈式系統等分支領域有重大的實際意義。本書大體上分為三個部分。第一部分是數學基礎，為第一章。第二部分包括第二到第五章，概述了形式語義中的操作語義、指稱語義、公理語義和代數語義四大經典流派。第三部分包括第六到第九章，概述了形式語義學的現代應用，分別介紹分佈式系統、移動計算和移動通信系統、非規範進程代數和微觀生命系統，以及量子程序設計語言的形式語義。

全書內容豐富，結構嚴謹，集形式語義學理論及其應用的有關分支之大成，系統地反映了這個領域各方面的研究成果，特別是它的近代發展潮流和趨勢，並對不同流派的理論和方法給予了分析和評論。

本書可作為計算機科學專業研究生、本科生有關課程的教材或教學參考書，也可供有關專業或交叉學科的科研人員進修或作為工具書。 ^[2] 

第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章移動通信和移動計算系統的形式語義 ^[3] 

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的概率分支雙模擬 ^[3]