理論計算機科學

關於計算和計算機械的數學理論，也稱為計算理論或計算機科學的數學基礎。理論計算機科學主要包括：①自動機論與形式語言理論②程式理論③形式語義學④算法分析和計算複雜性理論。

基本介紹

• 書名：計算和計算機械的數學理論

學科的產生

在幾千年的數學發展史中，人們研究了各種各樣的計算，創立了許許多多的算法，但以計算或算法本身的性質為研究對象的數學理論卻是到20世紀30年代才發展起來的。當時為了要解決數學基礎的某些理論問題，即是否有的問題不是算法可解的，數理邏輯學家提出了幾種不同的（後來證明是彼此等價的）算法定義，從而建立了算法理論（即可計算性理論）。30年代前期，K.哥德爾和S.C.克林尼等人創立了遞歸函式論，將數論函式的算法可計算性刻劃為遞歸性。30年代中期，A.M.圖靈和E.L.波斯特彼此獨立地提出了理想計算機的概念，將問題的算法可解性刻劃為在具有嚴格定義的理想計算機上的可解性。30年代發展起來的算法理論，對在40年代後期出現的存儲程式型計算機的設計思想是有影響的。圖靈提出的理想計算機（稱為圖靈機）中的一種通用機就是存儲程式型的。

學科內容

在這些領域中，自動機理論和形式語言理論是50年代發展起來的。前者的歷史還可以上溯到30年代，因為圖靈機就是一類自動機(無限自動機)。50年代以來一些學者開始考慮與現實的計算機更相似的理想計算機，J.諾伊曼在50年代初提出了有自繁殖功能的計算機的概念。王浩在50年代中期提出了一種圖靈機的變種，這是一種比原來的圖靈機更接近現實機器的機器。他還提出一種存儲帶上的內容不能清除的機器，並證明這種機器是與圖靈機等價的。60年代前期，又有人提出具有隨機存取存儲器的計算機（簡稱RAM）以及多帶圖靈機等。

形式語言理論

導源於數理語言學中的喬姆斯基理論。在這種理論中，形式語言分為四種:①0型語言；②1型語言;③2型語言;④3型語言。相應地存在著0型、1型、2 型、3型四種形式文法。1型語言又名上下文有關語言，2型語言又名上下文無關語言，3型語言又名正則語言。其中2型語言最受人注意。60年代中期，還發現了這四類語言與四類自動機之間的對應關係（見表）

在上表中，左邊所列的語言恰好是右邊與之對應的自動機所能識別的語言（見形式語言理論）。

程式設計理論

包括程式正確性證明和程式驗證，它的一些基本概念和方法是40年代後期諾伊曼和圖靈等人提出的。諾伊曼等在一篇論文中提出藉助於證明來驗證程式正確性的方法。後來圖靈又證明了一個子程式的正確性。他的方法是：設有一給定的程式，且有變數X1，X2，…，Xn以及輸入謂詞P(X1，…，Xn)與輸出謂詞Q(X1，…，Xn)。如果能證明下列事實：若在程式執行前謂詞P（X1，…，Xn）成立，則在程式執行後，謂詞Q(X1，…，Xn)成立，程式的正確性得證。

圖靈的這一結果長期未引起注意，一直到P.瑙爾在1963年和E.F.費洛伊德在1966年重新提出這一方法後，才引起計算機科學界的重視。此後，有不少理論工作者在從事這方面的研究。但正如E.W.戴克斯特拉在70年代中期曾指出的，實際有效的方法是邊設計邊驗證，在設計完畢時證明或驗證的過程也同時結束。J.T.施瓦茲和M.戴維斯70年代後期提出了一種他們稱之為“正確程式技術”的軟體技術。這種方法是先選定成千種基本程式模組，並藉助已知的各種驗證方法（包括程式正確性證明）來保證這些基本程式的正確性。然後再提出一組能保持正確性的程式組合規則。這樣，就可以通過不斷的組合，生成各種各樣的程式。

有人指出，程式正確性證明技術所發展出來的“循環不變式”，即一個程式中的某一循環的入口或出口點上所附的謂詞，有些文獻中稱作“歸納斷言”，可以用來供程式研究用。也就是說，不像過去那樣，對一個給定的程式找出其若干個循環不變式，然後藉助這些不變式來證明這個程式的正確性；而是在編制這個程式之前，根據對這一程式的要求，找出若干個循環不變式，然後根據這些不變式來生成這個程式。

自動程式設計的概念也是從40年代提出的。圖靈在1947年的一篇論文中，提出藉助定理證明的方法來設計程式。他的想法大致如下:設要求設計一個程式，使成為計算一個給定的遞歸函式F(X)的程式，並令F(n)=m（這裡n是任一自然數，m是自然數），需要找到一個證明F(n)=m的構造性證明。在有了這樣一個構造性證明以後，就可以從這個證明中提取出F(X)的求值算法，然後生成所需要的程式。圖靈的這一思想長時間不為人所知。1969年又有人獨立地提出了這一想法。

程式語言的形式語法的研究，從50年代中期起有了較大的發展。而形式語義的研究自60年代以來雖有不少研究工作者從事這方面的工作，提出幾種不同的語義理論，主要是操作語義學、指稱語義學或稱數學語義學、公理語義學和代數語義學，但仍沒有一種公認在軟體技術中夠用的形式語義學，因而需要提出一種更適於用到實際計算中的新的語義學。

在程式正確性證明和形式語義學中套用的程式邏輯，是60年代末發展起來的。這是謂詞邏輯的一種擴充。原來的謂詞邏輯中是沒有時間概念的，所考慮的推理關係是在同一時間裡的關係。程式是一種過程，一個程式的輸入謂詞與輸出謂詞之間的邏輯關係就不是同一時間裡的關係。因此，在有關程式性質的推理中，原來的謂詞邏輯不夠用，需要有一種新的邏輯。

60年代末，E.恩格勒等人創立了算法邏輯。C.A.R.霍爾也創立了一種程式邏輯。這種邏輯是在原來的邏輯上增加一個程式運算元而得到的。例如，可以將程式作為一種新的運算元置於一個謂詞公式的前面，如表達式

{S}P(X1，…，Xn)表示在程式S執行完畢時，謂詞P(X1，…，Xn)成立（這裡的）X1，…，Xn是程式S 中的變數）。

算法分析和計算複雜性理論

關於算法的複雜性的研究。關於這一領域的名稱曾有爭論。一般認為，各類具體算法的複雜性的研究稱作算法分析，而一般算法複雜性的研究稱作計算複雜性理論。計算複雜性理論原是可計算理論的一支，是以各種可計算函式(即遞歸函式)的計算複雜性（在早期稱作“計算難度”）為其研究對象的。可計算性分為理論可計算性和實際可計算性兩種。作為可計算性理論一支的計算複雜性理論，是以前者的複雜程度為其研究對象的；而作為計算機科學一個領域的複雜性理論，則是以後者的複雜程度為其研究對象的。

這一分支的基本問題是要弄清楚實際可計算函式類的結構和一些性質。實際可計算性是一個直觀的概念。如何對這一概念進行精確的描述，是一個並不容易的問題。60年代中期以來，有關的研究工作者一般是以計算時間多項式有界的函式作為實際可計算的函式。這實際上是一個論題，而不是一個可以在數學中加以證明或否證的命題。有人指出，在有關的多項式次數較高時（如n的情形），很難說是實際可計算的。

另一個帶根本性的問題是：確定性機器與非確定性機器的解題能力的比較問題。人們早已知道，確定性圖靈機與非確定性圖靈機的解題能力是相等的。因為非確定性機器雖比確定性機器效率高，而如果計算時間沒有限制，則確定性機器總可以用窮舉的方法來模擬非確定性機器。因此，二者的解題能力是一樣的。但在計算時間多項式有界時，二者的解題能力是否相等，這就是有名的P=? NP問題。

關於計算和算法（包括程式）的研究，對串列計算的性質研究較多，而對並行計算性質的研究則還很不夠（特別是對異步的並行計算更是如此）。因此，關於並行計算的研究很可能將成為計算機理論的研究重點。