摘 要：本文闡述了邏輯與計算、計算機的起源、程序設(shè)計之間的相互關(guān)系，并在一階邏輯的基礎(chǔ)上，以LISP、PROLOG等為例，給出了邏輯在程序設(shè)計語言和邏輯程序設(shè)計中的應(yīng)用，以此說明計算機科學(xué)是邏輯的超大規(guī)模應(yīng)用。

關(guān)鍵詞：邏輯；計算；計算機

中圖分類號：TP3 文獻標(biāo)識碼：A

1 引言（Introduction）

20世紀(jì)30年代，Godel、Church、Turing等邏輯學(xué)家給出了“可計算”概念的嚴(yán)格定義。Turing于1936年發(fā)明了一種抽象機器——第一臺通用數(shù)字計算機。該機器可用來輔助求解數(shù)學(xué)基礎(chǔ)問題。1940年，Turing的邏輯抽象機付諸實踐。Turing設(shè)計了ACE計算機。von Neumann主持研制了EDVAC和IAS計算機。50年代，計算機科學(xué)成為一門獨立的學(xué)科。從那時起，邏輯與計算機科學(xué)間的聯(lián)系越來越緊密，主要表現(xiàn)在計算機理論、復(fù)雜性理論、類型論、程序設(shè)計語言的形式語法和語義、編譯技術(shù)、程序規(guī)范和驗證、并發(fā)理論、知識工程、歸納學(xué)習(xí)[1]、數(shù)據(jù)庫理論、專家系統(tǒng)、定理證明、邏輯程序設(shè)計和函數(shù)程序設(shè)計等方面。

2 邏輯與計算（Logic and computing）

計算機是邏輯和技術(shù)的共同產(chǎn)物20世紀(jì)30年代，邏輯學(xué)家Godel、Church、Turing提出了計算的抽象概念。40年代中期，Turing和von Neumann主持設(shè)計、制造了第一臺計算機。此外，他們的工作為理解計算過程和計算形式化的發(fā)展打下了廣泛的邏輯基礎(chǔ)。

如今邏輯仍是新穎計算機體系結(jié)構(gòu)抽象思想的重要來源，這些新結(jié)構(gòu)包括推理機、數(shù)據(jù)流機、數(shù)據(jù)庫機、重寫機。邏輯為程序設(shè)計提供了一整套的思想，同時為程序的推理提供了系統(tǒng)的框架。邏輯在程序設(shè)計語言的理論和設(shè)計方面發(fā)揮著重要作用，數(shù)理邏輯可視為兩類主要邏輯程序設(shè)計語言的直接模型。一類是基于Church的λ一演算[2]的函數(shù)程序設(shè)計語言，如LISP、ML、LUCID、MIRANDA。另一類是基于Horn子句歸結(jié)的關(guān)系程序設(shè)計語言，如PROLOG、PARLOG、GHC。Peter Landin早在20世紀(jì)70年代就指出，像ALGOL這樣的語言也不過是對Church的λ一演算稍加擴充后的“語法變形”。后來，Martin-Lof直覺主義類型論被用來研究更高層的程序設(shè)計語言。其突出特征是程序正確性證明自動伴隨著程序書寫過程。

為設(shè)計、理解、講解計算機及程序設(shè)計語言，為編寫、分析程序以及進行有關(guān)性質(zhì)的正確推導(dǎo)，邏輯在發(fā)揮著重要作用。邏輯學(xué)家本身亦可稱為抽象工程師。

為分析知識表達和推理的過程以及綜合用于表達和推理的機器，邏輯為我們提供了語言及技術(shù)。

在人工智能研究中，邏輯在下述諸方面得到成功應(yīng)用。

（1）知識表示的模型。

（2）機器歸納推理和學(xué)習(xí)的組織。

（3）自動演繹系統(tǒng)的理論基礎(chǔ)。

然而，與邏輯在計算的理論和實踐中的作用相比，邏輯在人工智能中的作用更多的是引發(fā)人們的爭論。要結(jié)束這種爭論，必須更好地理解自然智能與人工智能的差別。與此同時，邏輯的倡導(dǎo)者和批評者均應(yīng)做出更多的工作來闡述各自的觀點。

3 邏輯與計算機的起源（The origin of logic and

computing）

在現(xiàn)代計算機的發(fā)明過程中，邏輯起決定性的作用。這一點并未被人們廣為接受。抽象計算機發(fā)明于1936年，該發(fā)明由1930年Godel的重要邏輯發(fā)現(xiàn)所引發(fā)。1936年Godel有關(guān)計算的理論鼓舞Turing來尋求一種既嚴(yán)格又抽象的邏輯模型。這種模型不僅是關(guān)于計算過程的，而且是關(guān)于計算機本身的。以此為輔助的理論概念。Turing證明數(shù)學(xué)的形式系統(tǒng)是不可判定的，從而解決了Hilbert第三問題。盡管Turing的最初計算機僅是抽象邏輯概念，但在這之后的10年（1937—1946）中，Turing成為了實用計算機的設(shè)計、制造、使用的領(lǐng)頭人。

Turing機似乎是真正計算機的抽象。然而，它卻創(chuàng)立于20世紀(jì)30年代。抽象Turing機是人們可以執(zhí)行的可能計算模式的理想模型。Turing本人的最大成就是證明了一些Turing機是“通用的”——它們可模仿任何Turing機的行為，他所給出的通用機是如今的存儲程序通用計算機的抽象原型。每個特殊機器的編碼描述是一程序，它可使通用機當(dāng)專用機使用。

Turing的工作有一明顯的技術(shù)解釋，不需要對每個計算任務(wù)都建造一個獨立的機器，而只需建造一臺機器——通用機器。人們可以通過編寫適當(dāng)?shù)某绦騺碜鏊璧挠嬎悖聦嵣?，Turing本人動手建造了一臺通用機。

von Neumann在闡述EDVAC、IAS機的設(shè)計和操作時，側(cè)重用抽象的邏輯描述語言來說明，很少涉及詳細的工程細節(jié)。關(guān)于機器的系統(tǒng)結(jié)構(gòu)和程序設(shè)計原則，全都用抽象概念來闡述，今天可以看出，von Neumann和Turing在計算機設(shè)計和程序設(shè)計方法學(xué)等主要問題上所依照的正是邏輯原則。相反，精確的工程細節(jié)相對說來是次要的。從那時起，重視邏輯抽象（相對具體實現(xiàn)）就成為計算機科學(xué)的指導(dǎo)原則。

4 邏輯與程序設(shè)計（（Logic and programming）

Turing和von Neumann在有關(guān)程序設(shè)計的討論中多次強調(diào)“流程圖”的重要地位。此后，“流程圖”很快成為早期程序設(shè)計的一種標(biāo)準(zhǔn)邏輯工具。直到目前，“流程圖”仍應(yīng)用于有關(guān)計算的形式推理中。Hoare、Dijkstra、Floyd等有關(guān)程序推理邏輯原則的思想盡在Turing和von Neumann的料想之中。Turing和von Neumann曾強調(diào)指出，程序設(shè)計有靜態(tài)、動態(tài)兩個方面，程序本身的靜態(tài)文本主要是指邏輯表達式：性質(zhì)僅用邏輯方法分析的語法結(jié)構(gòu)。運行程序的動態(tài)過程是上述靜態(tài)文本語義的一部分。

4.1 自動程序設(shè)計

1950年，Turing的朋友Strachey使用計算機將高層“數(shù)學(xué)”描述轉(zhuǎn)換成低層“機器語言”指令。他希望程序員能以更自然和符臺人們習(xí)慣的方式思考和編寫程序?？墒?，Turing本人對此想法井無興趣，他早在1947年就指出，這不過是一件簡單的事情。事實上，Turing非常精于機器語言，他能用機器碼和32進位、低位在前的非正常表達直接并且方便地進行思考。

50年代后期，隨著解釋器、編譯器技術(shù)的發(fā)展及FORTRAN、LISP、ALGOL的推出，程序員被從瑣碎的工作中解放出來。

4.2 邏輯與程序設(shè)計語言

4.2.l 抽象邏輯程序設(shè)計

邏輯程序設(shè)計語言是邏輯學(xué)與計算機科學(xué)結(jié)合的典型代表。在回答“邏輯程序設(shè)計是什么”之前，先給出“邏輯是什么”的回答。因為邏輯程序設(shè)計的公理化概念依賴于邏輯自身的公理化概念。邏輯的研究通常有兩條主要途徑：

（1）模型論方法——在模型和句子之間建立滿足關(guān)系。

（2）證明論方法——句子集之間的衍推關(guān)系。

這兩種方法本身均不足以對邏輯程序設(shè)計進行公理化。

證明論方法可追溯到1959年Tarski.A.“關(guān)于元數(shù)學(xué)的基本概念”中的“推導(dǎo)關(guān)系”及 Hertz和Gentzen提出的衍推關(guān)系S。

以一階邏輯[3]為例，存在許多不同的證明演算（如Hilbert系統(tǒng)、Gentzen系統(tǒng)、自然演繹系統(tǒng)等）。其中，起關(guān)鍵作用的是衍推關(guān)系S，因為，它在許多不同系統(tǒng)中保持不變。一階衍推關(guān)系├ 滿足三條性質(zhì)：

（1）自反性，即φ├φ。

（2）單調(diào)性，即如果г├φ，г′г，則г′┝φ。

（3）傳遞性，即若г├φ，г∪{φ}┝ψ， 則г┝ψ。

可將自反性視為一公理模式，單調(diào)性視為弱化規(guī)則，傳遞性視為切割規(guī)則。

（弱邏輯程序設(shè)計）邏輯程序設(shè)計語言中，程序P是邏輯L中的一理論。當(dāng)程序被執(zhí)行時，用戶可做詢問（詢問屬于P語言中一特別句子類）。當(dāng)用戶提出一詢問φ時，如φ是P中公理的可證推論，則機器將返回證明φ為真的一集回答?？梢曔@些回答為對φ的不同證明。如果由P得不到詢問φ的證明，則或者機器在有窮時間之后停止并提示“失敗”，或者機器永不停止。因此，機器中的計算與邏輯中的演繹等價。

從實用上考慮，機器中的實現(xiàn)必須能行，使得該語言實際適合一大類應(yīng)用。否則，最好將這樣的系統(tǒng)描述成一定理證明器。

將計算等同于演繹時沒有涉及模型概念，一個理論原則上有許多模型。然而，在解決一特定問題時如計算一數(shù)值函數(shù)，心中通常有一模型（如整數(shù)、實數(shù)），這樣的模型是給定理論的指定模型或標(biāo)準(zhǔn)模型。

在邏輯程序設(shè)計文獻中，標(biāo)準(zhǔn)模型指程序描述的“封閉世界”。標(biāo)準(zhǔn)模型通常被刻劃為初始模型。

用IP表示程序P的指定模型。在這樣的模型中，我們主要的興趣不是（在所有模型下均成立的）有效性，而是在模型IP下的可滿足性。

（強邏輯程序設(shè)計）邏輯程序設(shè)計語言中程序P是一邏輯L中的一理論，程序P的數(shù)學(xué)語義是P的模型IP。程序P進入機器后，用戶可提出關(guān)于什么性質(zhì)在其模型中滿足的問題。這種被稱為詢問的問題，是P語言中的特定句子，并滿足性質(zhì)：模型IP滿足φiffφ從P的公理可證。當(dāng)用戶提出詢問φ時，若φ是P公理的可證推論，則機器給出φ真的回答。這樣的回答可視為φ的證明。換言之，語言的操作語義是通過證明論給出的。如果φ從P不可證，則或者機器回答“失敗”，或者機器永不停止，因此，下面三者等價：機器中的計算、邏輯中的演繹和標(biāo)準(zhǔn)模型中的可滿足。

4.2.2 邏輯程序設(shè)計語言

20世紀(jì)50年代后期，John McCarthy等人直接使用符號邏輯作為IBM704機的程序。他們的系統(tǒng)LISP是實用邏輯程序設(shè)計語言的第一個重要例子。LISP本質(zhì)上是Church的λ一演算。λ一演算討論簡單遞歸數(shù)據(jù)類型（有序偶對）、條件表達式以及用于列舉一系列連續(xù)行為的強制“序列構(gòu)造”。在70年代初，Robert Rowalski和Alain Colmerauer給出了PROLOG。PROLOG基于謂詞演算的Horn子句歸結(jié)。Horn子句歸結(jié)涉及目標(biāo)、子句、控制流、深度優(yōu)先、回溯等概念以及幾個強制式命令（如“cut”）。David.H.D.Warren采用巧妙的技術(shù)，漂亮而且有效地實現(xiàn)了PROLOG。邏輯程序設(shè)計語言LISP和PROLOG的主要優(yōu)點為：靈活、易書寫、易修改，LISP和PROLOG通常被視為兩種邏輯程序設(shè)計（函數(shù)程序設(shè)計和關(guān)系程序設(shè)計）的典范。抽象描述演繹程序設(shè)計的一般思想是將計算視為從表達式到一范式的歸約，在抽象LISP中，主要指對適用于過程函數(shù)調(diào)用、條件表達式、序偶數(shù)據(jù)結(jié)構(gòu)操作等歸約規(guī)則的持續(xù)應(yīng)用.在抽象PROLOG中，主要指β歸約規(guī)則的持續(xù)應(yīng)用。這些規(guī)則包括：分配“合取”、刪除存在量詞，化簡表達式。將這兩種形式合并可得統(tǒng)一的邏輯系統(tǒng)，其中含有兩種程序設(shè)計的特點。目前，J. A. Robinson等人基于此思想給出了一新語言SUPER，它可用來解釋歸約邏輯如何在超大規(guī)模并行計算機上自然地實現(xiàn)。

LISP、PROLOG等語言表明了邏輯系統(tǒng)對計算機的應(yīng)用，邏輯程序設(shè)計近乎于一種適當(dāng)形式的知識闡述，在其中，從公理可導(dǎo)出用戶詢問的答案。在這種意義下，此類程序設(shè)計是連接一般計算到特殊AI系統(tǒng)的橋梁。Robert Kowalski等式“算法=邏輯十控制”概述了同時注重程序的描述、強制兩方面的重要性。

5 結(jié)論（Conclusion）

綜上所述，通過對邏輯與計算、計算機的起源、程序設(shè)計之間的相互關(guān)系的基本梳理和研究，可以充分說明計算機科學(xué)是邏輯的超大規(guī)模應(yīng)用。

參考文獻（References）

[1] 陸鐘萬.面向計算機科學(xué)的數(shù)理邏輯[M].北京：北京大學(xué)出版

社，1989.

[2] 王元元.計算機科學(xué)中的邏輯學(xué)[M].北京：科學(xué)出版社，1989.

[3] 王兵山，張強，李舟軍.數(shù)理邏輯[M].北京：國防科技大學(xué)出版

社，1993.

作者簡介：

張 強（1962-），男，碩士，教授，碩士生導(dǎo)師.研究領(lǐng)域：計

算機科學(xué)理論，軟件技術(shù)，現(xiàn)代教育技術(shù).