基本信息

書名：計算係統的形式語義(套裝上下冊)

定價：398.00元

作者：陸汝鈐

齣版社：清華大學齣版社

齣版日期：2017-01-01

ISBN：9787302414940

字數：

頁碼：1856

版次：1

裝幀：精裝

開本：16

商品重量：0.4kg

編輯推薦

都說計算機科學如參天大樹直達天際；
是誰在關注深達萬丈它的理論根係？
都說計算機科學如乘龍駒一日韆裏；
又有多少人能一探它的地下王國日新月異？
誰說計算機理論隻認得工程科技？
微如量子秘如生命竟也服從形式語義；
數學和邏輯能助你捋清韆絲萬縷；
《計算係統的形式語義》帶你明察奧秘！

內容提要

計算係統的形式語義是目前計算機科學理論研究的兩大方嚮之一，其研究成果對程序設計語言、編譯技術、應用軟件、分布式係統等分支領域有重大的實際意義。本書大體上分為三個部分。部分是數學基礎，為章。第二部分包括第二到第五章，概述瞭形式語義中的操作語義、指稱語義、公理語義和代數語義四大經典流派。第三部分包括第六到第九章，概述瞭形式語義學的現代應用， 分彆介紹分布式係統、移動計算和移動通信係統、非規範進程代數和微觀生命係統，以及量子程序設計語言的形式語義。
全書內容豐富，結構嚴謹，集形式語義學理論及其應用的有關分支之大成，係統地反映瞭這個領域各方麵的研究成果，特彆是它的近代發展潮流和趨勢，並對不同流派的理論和方法給予瞭分析和評論。
本書可作為計算機科學專業研究生、本科生有關課程的教材或教學參考書，也可供有關專業或交叉學科的科研人員進修或作為工具書。

目錄

作者介紹

文摘

序言

前言計算係統的形式語義前言
本書是1992年齣版的《計算機語言的形式語義》一書（簡稱1992版）的更新版。在1992版中我們分彆介紹瞭形式語義形式語義的四個主要流派：操作語義、指稱語義、公理語義和代數語義，並在此基礎上綜閤闡述瞭並發和分布式程序分布式程序的形式語義。從該書齣版以來，已經二十餘年過去瞭，在此期間，外形式語義學的研究有瞭許多重大的突破。
首先，應該提到的是移動通信的發展促進瞭一類新的進程代數——π演算的齣現和發展，使得用進程代數編寫的程序不僅可以在固定網絡上運行，而且可以改變通信網絡的拓撲結構，並在可變的網絡結構上實行通信。圍繞π演算齣現瞭許多變種，開展瞭深入的研究。除瞭可變的網絡結構之外，π演算還創造瞭其他的手段來改進通信技術。例如，利用π演算，有可能建立專用的私密信道。隨著π演算而興起的環境演算環境演算Ambient甚至可以提供建立網上防火牆的手段。服務於保密通信的Spi演算Spi演算把編碼和解碼引進瞭語言之中。帶有噪音信道的含噪進程代數有希望把香農的信息論引進進程代數中，從而在兩類通信理論之間架起一座橋梁。所有這些使得服務於移動通信的進程代數成瞭一門單獨的學問。
其次，分子生物學是近年來發展快的研究方嚮之一。人類基因圖譜的測序完成大大推動瞭基因組學、蛋白質組學，以及係統生物學的研究。恩格斯曾經說過，數學在生物學中的應用為零，但是這樣的時代早就過去瞭。以數學為基礎的形式化方法已經深入到生物領域，成為描述微觀生命現象的有力手段。特彆值得稱道的是概率論和過程作為重要的數學手段在麵嚮微觀生命現象的進程代數理論中發揮瞭重要作用。除瞭概率進程代數、進程代數和性能評估進程代數這些比較通用的工具之外，一大批特意針對微觀生命現象的描述工具已經被設計齣來並投入應用。諸如Bioambient、因果π演算、化學抽象機、生化抽象機等工具提供瞭許多頗有啓發的思路。描述微觀生命現象的數學工具早已經不純粹是微積分和微分方程等連續數學的天下，而成瞭連續工具和離散工具八仙過海的多極世界。
再次，實用化量子計算機齣現和推廣應用的前景正在吸引越來越多的科學傢關注量子計算領域。近年來齣現瞭一批麵嚮量子計算的程序設計語言，其中也包括量子進程代數，科學傢們已經開始討論量子軟件和量子軟件工程。量子程序設計和經典程序設計有許多本質不同。例如，量子不可剋隆原理的存在使得量子程序設計語言不可能有簡單的賦值語句。同時，由於對一個量子係統的測量會引起該係統所處狀態的坍縮，這使得係統狀態的可觀察性和程序運行流程的可控製性受到影響。另一方麵，量子力學的特殊性質並非隻對量子程序設計起限製作用，它的某些性質有可能對量子程序設計是“有用”的。例如，量子離物傳態量子離物傳態、量子密集編碼、量子密碼通信等方麵的研究成果有可能對量子網絡和分布式量子軟件工程産生較大影響，宜於我們去關注和開發利用。在意義上，量子程序的運行可以用經典程序來模擬。因此，盡管量子計算機還沒有完全實現，但是量子程序設計和量子軟件的研究並不要等到量子計算機實現以後再做，而是可以先行一步。而量子密碼通信先於量子計算機的實現又提供瞭研究量子軟件的必要性和現實性。更進一步說，量子軟件的研究成果可以為未來量子計算機的設計提供新思路，比起先有經典計算機，後有經典程序設計的曆史來說，這樣做更閤理。同樣，在實際設計和使用量子程序設計語言之前先把它們的數學基礎，即形式語義研究清楚，然後再去設計和使用，這比起傳統的程序設計語言先設計、先使用，後論證其理論基礎、後補其漏洞來說，未嘗不是一件好事。
近十餘年來形式語義學的研究成果極其豐富，本書把以上三個方麵作為補寫和更新的重點，是充分考慮到實踐需求的一種選擇。這三個方麵都具有強烈的應用背景，同時又有深刻的理論問題，構成瞭三個新的章。同時本書也對原有的六章內容做瞭必要的補充。其中主要的四部分是：指稱語義一章原書以（反映程序不確定性的）冪域理論結尾，本書添加瞭概率冪域理論和概率加不確定性冪域理論，同時還介紹瞭基於單體的計算理論和指稱語義的完全抽象性完全抽象性研究。在公理語義一章添加瞭Hoare邏輯的概率推廣和Dijkstra弱前置條件語義弱前置條件語義（簡稱弱前置語義）的概率推廣。同時還介紹瞭基於一種實時模態邏輯的時段演算。並發和分布式語義一章原來重點介紹瞭CSP和CCS兩個進程代數理論，本書補充介紹瞭另一個重要的進程代數ACP， 從而比較完備地展示瞭進程代數傢族的三劍客架構。另外還分彆給齣瞭以擴充Petri網形式齣現的CCS真並發語義和以抽象數據類型形式齣現的CCS代數語義。這兩種方法原則上可以推廣到其他進程代數。這一章後以Glabbeek的進程代數並發語義的比較研究結尾。後，由於本書增添瞭以上各項內容，對章數學基礎也要做必要的（低限度的）增補。其中完整增加的有三節：一些基本的代數、拓撲和泛函知識，概率和過程過程知識，以及綫性邏輯和Gentzen演算知識。另外對範疇論和格論兩節做瞭必要的增補。
自然界有大量的信息交換並不采取人類語言或計算機語言的形式。一個明顯的例子是生命係統。例如，DNA序列就可以看成是一種文字，它構成瞭生命的“天書”。基因對蛋白質的錶達，細胞間和細胞內部的通信，這裏都有信息交換和信息處理在起作用。另一個明顯的例子是量子係統。凡涉及量子計算、量子糾纏、量子通信、量子密鑰等問題，無不歸於信息錶示和信息處理的範疇。盡管現在的生命過程描述語言和量子程序設計語言都以計算機語言的形式齣現，用於生命現象的模擬、預測和量子計算機的編程，我們仍然可以把微觀生命係統和量子係統看成自然界的“天造”計算係統。俗話說人算不如天算，它們不僅應該和人造的計算係統平起平坐，而且還為人造計算係統提供瞭啓示和展望。為此也需要形式化的數學工具，以嚴格和正確地刻畫生命信息和量子信息的錶示和處理。為此，我們統稱本書的內容為計算係統的形式語義。
本書的內容通過每章的概述、除概述以外的各節，以及文獻和中、英名詞索引四部分組成，它們互不包含。概述是各章涉及內容的一個鳥瞰。章中各節是對其中某些內容有選擇地展開講解。文獻是前兩部分內容的齣處和延伸閱讀信息，其中早期文獻可以提供有關研究的發展淵源信息，而近期文獻則可以提供相關領域的發展前景和專傢們的視角。由於形式語義的文獻數量極多，肯定有一些重要的有關文獻在寫作本書時被遺漏掉。即使是已經列入本書介紹範圍的一些文獻，也肯定有一些因為作者理解不深，甚至理解有誤而未能在本書中正確介紹其思想。我想提請讀者注意的是，本書不能作為開展研究工作的直接依據。有興趣在形式語義領域開展研究的讀者，可以參照本書提供的綫索，進一步閱讀原著文獻，可以在閱讀時對照本書的解釋、分析和某些進一步的發展，但是不能忽視閱讀原著，以免齣現可能的誤導。
本書在撰寫過程中得到瞭很多專傢的幫助。從開始有寫這本書的計劃起，作者經常和應明生教授就此交流看法並得到他的很多寶貴建議。應明生、周巢塵、林惠民、夏培肅、陳儀香、袁崇義、林闖、李未、李剋正、Bauer、Petri、Broy、Krieg�睟rückner、Reisig等教授都曾嚮作者提供他們的著作，使作者獲得瞭寶貴的知識來源。為撰寫本書，作者參考的文獻數量較大，無法一一緻謝。其中包括許多不署名的維基百科類資料，非常感謝這些未曾謀麵的知識傳播者。我們在書中盡可能地對引用的資料給齣瞭齣處，包括插圖。
為瞭減少本書可能給讀者帶來的枯燥感，我們在每一章的前麵加配瞭一首唐詩，每首詩的意境和它所在章的內容（之某些重要部分）存在一些本質的聯想。我想讀者會同意：在文化藝術和科學技術這兩個差彆巨大的領域之間不可能有真正的科學對應關係或推理關係，必須強調這僅僅是一種聯想關係。它肯定不...，也肯定因人而異。學習和研究都是艱苦的勞動，但同時也應該是快樂的。作者贊成博拉·米盧蒂諾維奇的快樂足球理念，從事科學工作也要有快樂感。在此感謝馬鼕潔應邀為封麵作圖，並為每章的唐詩配圖作畫，使本書增色不少。
作者真誠地感謝清華大學齣版社的大度寬容和堅定支持，使得這本撰寫時間寬度達十年以上的書稿能夠終完成。