淺談邏輯在計算機科學中的應用

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

關鍵詞：邏輯；計算；計算機

中圖分類號：TP3 文獻標識碼：A

1 引言（Introduction）

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

2 邏輯與計算（Logic and computing）

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

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

為設計、理解、講解計算機及程序設計語言，為編寫、分析程序以及進行有關性質的正確推導，邏輯在發揮著重要作用。邏輯學家本身亦可稱為抽象工程師。

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

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

（1）知識表示的模型。

（2）機器歸納推理和學習的組織。

（3）自動演繹系統的理論基礎。

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

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

computing）

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

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

Turing的工作有一明顯的技術解釋，不需要對每個計算任務都建造一個獨立的機器，而只需建造一臺機器——通用機器。人們可以通過編寫適當的程序來做所需的計算，事實上，Turing本人動手建造了一臺通用機。

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

4 邏輯與程序設計（（Logic and programming）

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

4.1 自動程序設計

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

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

4.2 邏輯與程序設計語言

4.2.l 抽象邏輯程序設計

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

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

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

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

證明論方法可追溯到1959年Tarski.A.“關于元數學的基本概念”中的“推導關系”及 Hertz和Gentzen提出的衍推關系S。

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

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

（2）單調性，即如果г├φ，г′г，則г′┝φ。

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

可將自反性視為一公理模式，單調性視為弱化規則，傳遞性視為切割規則。

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

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

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

在邏輯程序設計文獻中，標準模型指程序描述的“封閉世界”。標準模型通常被刻劃為初始模型。

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

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

4.2.2 邏輯程序設計語言

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

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

5 結論（Conclusion）

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

參考文獻（References）

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

社，1989.

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

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

社，1993.

作者簡介：

張 強（1962-），男，碩士，教授，碩士生導師.研究領域：計

算機科學理論，軟件技術，現代教育技術.