从数理逻辑观点看计算机专业的理论基础探讨

计算机科学与技术学科包括计算机系统结构、计算机软件与理论、计算机应用技术。一般地说，研究型计算机学院将按一级学科设置专业。离散数学是计算机专业的基础理论，包括数理逻辑、集合论、图论、代数系统、形式语言与自动机等，对于计算机体系结构、计算机软件与理论和计算机应用技术等核心课程的起着重要作用。

本文将从数理逻辑观点看计算机系统结构、计算机软件与理论和计算机应用技术的核心课程，以此探讨数理逻辑的理论基础作用。

1 公理系统及数理逻辑简介

亚里土多德在逻辑史上第一次应用了形式化、公理化的演绎系统，类似自然演绎系统，为逻辑的形式化开了先河。亚里士多德关于演绎证明的逻辑结构给出基本概念，通过定义派生概念；给出公理或公设，通过逻辑证明定理。这种由初始概念、定义、公理、推理规则、定理等所构成的演绎体系，称为公理系统。

欧几里德整理、总结和发展了希腊古典时期的大量数学知识，形成了《几何原本》。实质公理系统，给出点、线、面、角等23个原始定义概念，给出5条公设、5条公理，由公理公设出发加以证明了467定理。这也标志着公理学的产生，是实质公理学的典范。

俄国数学家罗巴切夫斯基提出从直线外一点，至少可以做两条直线和这条直线平行公理，从而发现了锐角非欧几何；1854年黎曼提出在同一平面内任何两条直线都有交点公理，从而发现了钝角非欧几何。非欧几何从直观的空间上升到抽象空间，使得人们认识到区分感性直观与科学抽象的重要性。

弗雷格第一个严格的关于逻辑规律的公理系统。在1879年出版了著作《概念文字：一种模仿算术语言构造的纯思维的形式语言》，他完备地发展了命题演算和谓词演算，第一次把谓词演算形式化，标志着数理逻辑的发展由创建时期进入奠基时期。

皮亚诺提出了自然数算术的一个公理系统用逻辑演算表述数学、推导数学。关于自然数论的五个公理一直沿用到现在，成为自然数论的出发点。

罗素(B.Russell)继承皮亚诺的研究，完备了命题演算和谓词演算的成果，以集合论为基础，对自然数作出定义，证明自然数满足皮亚诺的五个公理。罗素总结了数理逻辑的成果，和怀特海合著了《数学原理》，他的成果汇集成为一本巨著，奠定了数学的基础。

希尔伯特1899年的《几何基础》，第一个逻辑理论问题是公理的无矛盾性，在实数的算术理论中为欧氏几何构造一个模型，这实际上就是笛卡儿几何，在此模型中欧几里德何五组公理都真；第二个逻辑理论问题是公理的相互几独立性，利用模型方法作出了证明。《几何基础》已经发展成为一个形式公理系统。《几何原本》里，点线面都有定义。在《几何基础》里，这三个概念没有定义，也没有直观的解释，这是形式公理方法的特征。由于《几何基础》的基本概念没有直观的具体内容，这个系统可以有各种不同的解释即模型。

1931年，《关于数学原理》一书证明了数理逻辑的不完全定理。在数理逻辑发展史上具有划时代意义。哥德尔完全性定理，哥德尔不完全性定理，给出包括自然数公理的系统一定时不完备的，即一定存在逻辑真的公式，是不可证明的。

欧内斯特・内格尔在《科学的结构》中提出四种科学说明的模式：演绎模型、或然性说明、功能性说明以及发生学说明。在科学说明中，演绎模型是最重要的方法之一。鲁道夫・卡尔纳普《世界的逻辑构造》中，提出构造系统的任务要把一切概念都从某些基本概念中逐步地引导出来，形成概念系谱。一种理论的公理化就在于：这个理论的全部命题都被安排在以公理为其基础的演绎系统中，这个理论的全部概念都被安排在以基本概念为其基础的构造系统中。

在人类发展过程中，数理逻辑是最重要的系统的知识表示和科学说明方法，从而形成概念系谱，获得可靠定理。数理逻辑是计算机专业的基础理论，本文将讨论它也是计算机专业的理论基础。

2 逻辑公理系统

2.1 逻辑公理系统

逻辑公理系统有初始符号、公式规则、公理以及推导规则四部分。

(1) 初始符号

个体变元x1, x2, …

个体常元c1, c2 , …

函数符号：f11, f21,......；f12, f22,......；

谓词符号：P11,P 21,......； P 12, P 22,....;

逻辑常项：", Ø, ®；

逗号：, ;

括号：(, )

(2) 项和公式

个体常元是项；

个体变元是项；

若是t1,…,tn项，则是f i (t1,…,tn)项。

若是t1,…,tn项，则Pi(t1,…,tn)是公式。

若A是公式，则(ØA)是公式；

若A和B是公式，则(A®B)是公式；

若A是公式，则("xA)是公式。

(3) 公理

公理模式A 1：P® (Q®P) 肯定后件律

公理模式A 2：(P® (Q®R)) ® ((P®Q) ® (P®R))蕴含词分配律

公理模式A 3：(ØP®ØQ) ® (Q®P)换位律

公理模式A 4："xP®Ptx其中，项t对于P中的x是自由的。

公理模式A 5："x( P®Q) ® (P®"xQ)其中x不是P中自由变元。

(4) 推导规则

分离规则(简称MP规则)：从P和P®Q推出Q。

概括规则(简称UG规则)：从P推出("xP)。

2.2 证明与定理

定义设Γ是公式集。如果公式序列A1,A2,…An中的每个公式Ai满足以下条件之一，则称它为An的从Γ的一个推演(演绎)。其中Γ称为推演的前提集，称An为结论，记为Γ├ An。

(1) Ai是公理；

(2) AiÎΓ；

(3) 有j, k

(4) 有j

定义 如果├A，则A是定理。

希尔伯特给出的证明论告诉我们，一个证明是一个有穷序列，它的每一步或者是公理、或者是前提或者是推导规则产生的公式。歌德尔不完全性定理证明表明，不存在一个通用算法，判定任意公式是否是定理的证明。因此，定理的证明一定依靠人的洞察力、创新性和运气。一旦一个定理用逻辑公理方法给出证明，那么，人们理解证明过程就仅是逻辑定义和逻辑关系的变换，且证明的每一步或者是公理、或者是前提或者是推导规则产生的公式。因此，如果计算机基础理论建立在数理逻辑基础上，给出逻辑的证明，对于理解概念、性质和定理将变得精确而简单。

2.3 完备的基础理论

一个具有等词公理的理论是完全的，等词公理如下：

(1) tt

(2) t11t21Ù…... Ùt1nt2n®f(t11,…,1n)f(t21,…,t2n)

(3) t11t21Ù…... Ùt1mt2m®R(t11,…,1n)R(t21,…,t2n)

Peano给出了自然数公理，其语言L ={+，∘, s, 0}，其中+，是二元运算符，s是一元函数符(后继运算符)，0为常元。公理如下：

(1) "x (s(x) ¹ x)

(2) "x"y (x¹y®s(x) ¹ s(y))

(3) "x (x+0 = x)

(4) "x"y (x+ s(y) = s(x+y))

(5) "x (x∘0 = 0)

(6) "x"y (x∘s(y) = x∘y+x)

(7) (p(0) Ù"x (p(x) ®p(s(x)))) ®"x p(x) 其中p(x)是任意公式。

Peano给出的自然数，有一个常元0，三个运算s、+和∘。(1)-(2)是有关运算s的公理；(3)-(4)是有关运算+的公理；(5)-(6)是有关运算∘的公理；(7)是数学归纳法。

歌德尔不完全性定理表明包含Peano自然数公理的系统是不完全的。人们证明自然数仅包含公理(1)-(4)和(7)，这样的理论是完全的。

因此，我们给出的证明系统的基础理论，包括逻辑公理、等词公理和Peano的完全性公理，以增强证明能力。

3 数理逻辑是理论基础

3.1 计算机理论基础

计算机专业主要理论包括数理逻辑、集合论、图论、代数系统、形式语言与自动机理论等，数理逻辑是它们的基础，因为它们的基本概念、导出概念都可以采用数理逻辑方法定义，定理的证明都可以采用数理逻辑的公理化方法证明。

(1) 策梅罗一弗兰克尔公理集合系统

集合论可以用公理化的方法定义一个无悖论的集合系统，策梅罗一弗兰克尔公理集合系统是重要的稽核公理系统，也记为ZF系统，它包括外延性公理、无序对公理、空集公理、替换公理模式、分离公理模式、幂集公理、并集公理、无穷公理、正则公理。

(2) 图论

图是集合的有序偶G=，其中，V是顶点集合，E是边的集合。因此，图论的理论都可以用集合方法讨论。

(3) 代数系统

代数系统主要包括群、环、域。如群可以用公理方法表示，其定理可以用公理化方法证明。

定义 设G是一个非空集合，是它的―个代数运算，如果满足以下条件：

结合律： "x"y"z ((x∘y)∘z = x∘(y∘z))

左单位元："x (e∘x= x)

左逆元： "x$y (y∘x = e)

则称G对代数运算。作成一个群。

(4) 形式语言与自动机理论

1956年，美国语言学家乔姆斯基从产生语言的角度研究语言，将语言形式地定义为由一个字母表Σ中的字母组成的一些串的集合。对任何语言L，使得LÍΣ*。1951~1956年间，克林从识别的角度研究语言，在研究神经细胞中建立了自动机，他用这种自动机来识别语言。对于按照一定的规则构造的任一个自动机，该自动机就定义了一个语言，这个语言由该自动机所能识别的所有句子组成。乔姆斯基将语言分为四类，即正则文法、上下文无关文法、上下文有关文法和短语结构文法。文法产生的所有句子组成的集合就是该文法产生的语言。1959年，乔姆斯基通过深入研究将研究成果与克林的研究成果结合了起来，不仅确定了文法和自动机分别从生成和识别的角度去表达语言，而且证明了文法与自动机的等价性。

形式语言与自动机主要的基本概念是语言、语法和自动机。这些基本概念以及定理可以用数理逻辑的方法定义和证明。

定义：若Σ是字母表，且LÍΣ*，则称L是Σ上的语言，L={α|αÎΣ*}。

定义：设文法G=。如果"a®bÎP， a®b均具有如下形式：

A®ω，A®ωB 其中，A，BÎV，ωÎT*，则称G为右线性文法，L(G)称为右线性语言。

定义：如果G=是正则文法，则文法G产生的语言L(G)称为正则语言，记为RL。

L(G)={ω| SÞ*ωÙωÎ T*}

定义：文法G=称为上下文无关的(context-free)，如果P中的产生式具有形式：

A®ω其中AÎV，ωÎ(V∪T)*

定义：如果G=是正则文法，则文法G产生的子句。

定义：确定有穷自动机，记为DFA。字母表Σ上的有穷自动机M是一个系统，M=，其中，Q是状态的一个非空有穷集合，Σ是一个输入有穷字母表，δ是Q×Σ®Q的一种映射，q0是初始状态集，q0ÎQ，F是终止状态集，FÍQ，δ映射表示为qi=δ(qj, a)。

定义：δ*是Q×Σ*®Q的一种映射，q'=δ* (q, ω)，q ÎQ，q'ÎQ，ωÎΣ*，有

δ* (q, ε)=q，δ* (q,ωa)= δ(δ* (q, ω), a)，δ* (q, aω)=δ* (δ(q, a), ω)

定义：设M=，MÎDFA，L(M)是M接受的语言，则L(M)={ω|δ* (q, ω) ÎF}。

3.2 硬件基础

数字逻辑与数字部件设计主要包括组合逻辑与时序逻辑原理，数理逻辑的命题演算是其基础。基于MIPS指令集，设计寄存器、加法器、移位器、控制器、多路选择器、计数器、比较器等数字部件的逻辑功能。数理逻辑的命题演算将这些逻辑部件的功能表示为真值表，根据真值表表达的逻辑功能，变换为“与、或、非”逻辑运算的逻辑范式。这些逻辑范式的“与、或、非”表达为相应的逻辑部件即实现数字逻辑部件。借助于硬件描述语言和EDA软件工具，完成包括寄存器、加法器、状态机等在内的一系列计算机基础硬件组件的设计和开发。

在计算机组成原理，基于MIPS指令集，设计数据通路(如下图)，而后根据每条指令的指令周期的动作，设计指令控制逻辑，从而实现计算机组成原理的CPU设计。

数理逻辑的命题演算作为组合逻辑、时序逻辑以及控制逻辑的基础，使学生能够从逻辑的角度完成对数字逻辑部件的设计；通过数据通路的设计，控制逻辑的设计完成功能计算机的设计工作。以此为基础利用HDL实现指令系统的子集及部分相应的计算机功能部件，完成一个功能型计算机硬件的核心部分，并能在其上运行简单的汇编程序。

4 软件基础

在1966年G.Jaccopini和C.Bohm证明的"任何程序逻辑可用顺序\选择和循环等三种结构来表示"的定理基础之上，即(1)序列结构；(2)选择结构，if-then，if-then-else；(3) 循环结构，while-do。

一个程序规范可表示为由两个谓词构成的二元组(φ, ψ)。其中φ描述了所欲求解问题必须满足的初始条件，这个条件限定了输入参数的性质，称为初始断言或前置断言。断言ψ描述了问题最终解必须具备的性质，称为结果断言，或后置断言。程序断言是对程序性质的陈述。最重要的一个程序断言形如：

{φ}S{ψ}

其中φ和ψ是两个谓词，它们联合起来构成一个规范(φ, ψ)。S是一个程序。φ称S的前置断言，ψ称S的后置断言。断言{φ}S{ψ}称为S关于(φ, ψ)的正确性断言。它的意义为：“若S开始执行时φ为真，则S的执行必终止且终止时ψ为真。”

Hoare定义了一条赋值公理和四条推理规则，它们是：

赋值公理：{P(x, g(x,y))}yg(x,y){P(x,y)}

条件规则：{PÙR}F1{Q},{PÙØR}F2{Q}Þ{P}if R then F1 else F2 {Q}或{PÙR}F1{Q},{PÙØR}F2{Q}Þ{P}if R do F1

while规：P®I,{IÙR}F1{Q}, (PÙØR) ®QÞ{P}while R do F {Q}

并置规则：{P}F1{R}, {R}F2{Q}Þ{P}F1; F2{Q}

结论规则：P®R, {R}F{Q}Þ{P}F{Q}，{P}F{R}, R®QÞ{P}F{Q}

证明程序部分正确性的公理化方法就是依据以上的几条公理和规则进行的。推理过程一股有两种形式：(1)根据给出的不变式断言，建立一些引理，根据这些引理和赋值公理，对程序F中的每一个赋值语旬Fi导出相应的不变式语句{Ri}Fi{Qi}；(2)再根据这些不变式语句和上述的四条规则逐步地组成越来越长的程序段，一直到推演出{φ(x)}P{ψ(x, y)为止。这样，就证明了程序F的部分正确性。

5 小结

本文基于数理逻辑的公理、等词公理以及Peano的后继、加运算和数学归纳法给出一个完全的公理集。通过对集合论、图论、代数系统以及形式语言与自动机等计算机理论课程的讨论，说明了数理逻辑是计算机专业理论课的基础；通过讨论命题演算、真值表与逻辑范式、数字逻辑部件设计以及计算机组成原理中CPU部件设计，说明命题演算是将数字逻辑部件功能描述变换为逻辑范式，进而实现为数字逻辑部件的设计；通过讨论基于数字逻辑部件，设计数据通路、设计基于MIPS指令集的指令周期逻辑，从而设计指令控制逻辑，实现CPU部件；通过讨论软件规范和Hoare软件逻辑公理，说明数理逻辑在软件方面的基础作用。

“本文中所涉及到的图表、注解、公式等内容请以PDF格式阅读原文”