浅谈逻辑在计算机科学中的应用

摘 要：本文阐述了逻辑与计算、计算机的起源、程序设计之间的相互关系，并在一阶逻辑的基础上，以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-），男，硕士，教授，硕士生导师.研究领域：计

算机科学理论，软件技术，现代教育技术.