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

《从数理逻辑观点看计算机专业的理论基础探讨.docx》由会员分享，可在线阅读，更多相关《从数理逻辑观点看计算机专业的理论基础探讨.docx（11页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。

1、从数理逻辑观点看计算机专业的理论基础探讨 计算机科学与技术学科包括计算机系统结构、计算机软件与理论、计算机应用技术。一般地说，探讨型计算机学院将按一级学科设置专业。离散数学是计算机专业的基础理论，包括数理逻辑、集合论、图论、代数系统、形式语言与自动机等，对于计算机体系结构、计算机软件与理论和计算机应用技术等核心课程的起着重要作用。 本文将从数理逻辑观点看计算机系统结构、计算机软件与理论和计算机应用技术的核心课程，以此探讨数理逻辑的理论基础作用。 1 公理系统及数理逻辑简介 亚里土多德在逻辑史上第一次应用了形式化、公理化的演绎系统，类似自然演绎系统，为逻辑的形式化开了先河。亚里士多德关于演绎证明

2、的逻辑结构给出基本概念，通过定义派生概念；给出公理或公设，通过逻辑证明定理。这种由初始概念、定义、公理、推理规则、定理等所构成的演绎体系，称为公理系统。 欧几里德整理、总结和发展了希腊古典时期的大量数学学问，形成了几何原本。实质公理系统，给出点、线、面、角等23个原始定义概念，给出5条公设、5条公理，由公理公设动身加以证明白467定理。这也标记着公理学的产生，是实质公理学的典范。 俄国数学家罗巴切夫斯基提出从直线外一点，至少可以做两条直线和这条直线平行公理，从而发觉了锐角非欧几何；1854年黎曼提出在同一平面内任何两条直线都有交点公理，从而发觉了钝角非欧几何。非欧几何从直观的空间上升到抽象空间

3、，使得人们相识到区分感性直观与科学抽象的重要性。 弗雷格第一个严格的关于逻辑规律的公理系统。在1879年出版了著作概念文字：一种仿照算术语言构造的纯思维的形式语言，他完备地发展了命题演算和谓词演算，第一次把谓词演算形式化，标记着数理逻辑的发展由创建时期进入奠基时期。 皮亚诺提出了自然数算术的一个公理系统用逻辑演算表述数学、推导数学。关于自然数论的五个公理始终沿用到现在，成为自然数论的动身点。 罗素(B.Russell)继承皮亚诺的探讨，完备了命题演算和谓词演算的成果，以集合论为基础，对自然数作出定义，证明自然数满意皮亚诺的五个公理。罗素总结了数理逻辑的成果，和怀特海合著了数学原理，他的成果汇合

4、成为一本巨著，奠定了数学的基础。 希尔伯特18101年的几何基础，第一个逻辑理论问题是公理的无冲突性，在实数的算术理论中为欧氏几何构造一个模型，这事实上就是笛卡儿几何，在此模型中欧几里德何五组公理都真；其次个逻辑理论问题是公理的相互几独立性，利用模型方法作出了证明。几何基础已经发展成为一个形式公理系统。几何原本里，点线面都有定义。在几何基础里，这三个概念没有定义，也没有直观的说明，这是形式公理方法的特征。由于几何基础的基本概念没有直观的详细内容，这个系统可以有各种不同的说明即模型。 1931年，关于数学原理一书证明白数理逻辑的不完全定理。在数理逻辑发展史上具有划时代意义。哥德尔完全性定理，哥德

5、尔不完全性定理，给出包括自然数公理的系统肯定时不完备的，即肯定存在逻辑真的公式，是不行证明的。 欧内斯特内格尔在科学的结构中提出四种科学说明的模式：演绎模型、或然性说明、功能性说明以及发生学说明。在科学说明中，演绎模型是最重要的方法之一。鲁道夫卡尔纳普世界的逻辑构造中，提出构造系统的任务要把一切概念都从某些基本概念中逐步地引导出来，形成概念系谱。一种理论的公理化就在于：这个理论的全部命题都被支配在以公理为其基础的演绎系统中，这个理论的全部概念都被支配在以基本概念为其基础的构造系统中。 在人类发展过程中，数理逻辑是最重要的系统的学问表示和科学说明方法，从而形成概念系谱，获得牢靠定理。数理逻辑是计

6、算机专业的基础理论，本文将探讨它也是计算机专业的理论基础。 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是公式，则(&Oslas

7、h;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) 推导

8、规则 分别规则(简称MP规则)：从P和P®Q推出Q。 概括规则(简称UG规则)：从P推出(xP)。 2.2 证明与定理 定义设是公式集。假如公式序列A1,A2,An中的每个公式Ai满意以下条件之一，则称它为An的从的一个推演(演绎)。其中称为推演的前提集，称An为结论，记为 An。 (1) Ai是公理； (2) AiÎ； (3) 有j, k，其中，V是顶点集合，E是边的集合。因此，图论的理论都可以用集合方法探讨。 (3) 代数系统 代数系统主要包括群、环、域。如群可以用公理方法表示，其定理可以用公理化方法证明。 定义 设G是一个非空集合，是它的个代数运算，假如满意以下条件：

9、 结合律： xyz (x∢y)∢z = x∢(y∢z) 左单位元：x (e∢x= x) 左逆元： x$y (y∢x = e) 则称G对代数运算。作成一个群。 (4) 形式语言与自动机理论 1956年，美国语言学家乔姆斯基从产生语言的角度探讨语言，将语言形式地定义为由一个字母表中的字母组成的一些串的集合。对任何语言L，使得LÍ*。19511956年间，克林从识别的角度探讨语言，在探讨神经细胞中建立了自动机，他用这种自动机来识别语言。对于根据肯定的规则构造的任一个自动机，该自动机就定义了一个语言，这个语言由该自动

10、机所能识别的全部句子组成。乔姆斯基将语言分为四类，即正则文法、上下文无关文法、上下文有关文法和短语结构文法。文法产生的全部句子组成的集合就是该文法产生的语言。1959年，乔姆斯基通过深化探讨将探讨成果与克林的探讨成果结合了起来，不仅确定了文法和自动机分别从生成和识别的角度去表达语言，而且证明白文法与自动机的等价性。 形式语言与自动机主要的基本概念是语言、语法和自动机。这些基本概念以及定理可以用数理逻辑的方法定义和证明。 定义：若是字母表，且LÍ*，则称L是上的语言，L=|Î*。 定义：设文法G=。假如a®bÎP， a®b均具有如下形式： A

11、®，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，Î(VT)* 定义：假如G=是正则文法，则文法G产生的子句。 定义：确定有穷自动机，记为DFA。字母表上的有穷自动机M是一个系统，M=，其中，Q是状态的一个非空有穷集合，是一个输入有穷字母表，

12、是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指令集，

13、设计寄存器、加法器、移位器、限制器、多路选择器、计数器、比较器等数字部件的逻辑功能。数理逻辑的命题演算将这些逻辑部件的功能表示为真值表，依据真值表表达的逻辑功能，变换为“与、或、非”逻辑运算的逻辑范式。这些逻辑范式的“与、或、非”表达为相应的逻辑部件即实现数字逻辑部件。借助于硬件描述语言和EDA软件工具，完成包括寄存器、加法器、状态机等在内的一系列计算机基础硬件组件的设计和开发。 在计算机组成原理，基于MIPS指令集，设计数据通路(如下图)，而后依据每条指令的指令周期的动作，设计指令限制逻辑，从而实现计算机组成原理的CPU设计。 数理逻辑的命题演算作为组合逻辑、时序逻辑以及限制逻辑的基础，使学

14、生能够从逻辑的角度完成对数字逻辑部件的设计；通过数据通路的设计，限制逻辑的设计完胜利能计算机的设计工作。以此为基础利用HDL实现指令系统的子集及部分相应的计算机功能部件，完成一个功能型计算机硬件的核心部分，并能在其上运行简洁的汇编程序。 4 软件基础 在1966年G.Jaccopini和C.Bohm证明的任何程序逻辑可用依次选择和循环等三种结构来表示的定理基础之上，即(1)序列结构；(2)选择结构，if-then，if-then-else；(3) 循环结构，while-do。 一个程序规范可表示为由两个谓词构成的二元组(, )。其中描述了所欲求解问题必需满意的初始条件，这个条件限定了输入参数的

15、性质，称为初始断言或前置断言。断言描述了问题最终解必需具备的性质，称为结坚决言，或后置断言。程序断言是对程序性质的陈述。最重要的一个程序断言形如： S 其中和是两个谓词，它们联合起来构成一个规范(, )。S是一个程序。称S的前置断言，称S的后置断言。断言S称为S关于(, )的正确性断言。它的意义为：“若S起先执行时为真，则S的执行必终止且终止时为真。” Hoare定义了一条赋值公理和四条推理规则，它们是： 赋值公理：P(x, g(x,y)yg(x,y)P(x,y) 条件规则：PÙRF1Q,PÙØRF2QÞPif R then F1 else

16、 F2 Q或PÙRF1Q,PÙØRF2QÞPif R do F1 while规：P®I,IÙRF1Q, (PÙØR) ®QÞPwhile R do F Q 并置规则：PF1R, RF2QÞPF1; F2Q 结论规则：P®R, RFQÞPFQ，PFR, R®QÞPFQ 证明程序部分正确性的公理化方法就是依据以上的几条公理和规则进行的。推理过程一股有两种形式：(1)依据给出的不变式断言，建立一些引理，依据这些引理和赋值公理，

17、对程序F中的每一个赋值语旬Fi导出相应的不变式语句RiFiQi；(2)再依据这些不变式语句和上述的四条规则逐步地组成越来越长的程序段，始终到推演出(x)P(x, y)为止。这样，就证明白程序F的部分正确性。 5 小结 本文基于数理逻辑的公理、等词公理以及Peano的后继、加运算和数学归纳法给出一个完全的公理集。通过对集合论、图论、代数系统以及形式语言与自动机等计算机理论课程的探讨，说明白数理逻辑是计算机专业理论课的基础；通过探讨命题演算、真值表与逻辑范式、数字逻辑部件设计以及计算机组成原理中CPU部件设计，说明命题演算是将数字逻辑部件功能描述变换为逻辑范式，进而实现为数字逻辑部件的设计；通过探讨基于数字逻辑部件，设计数据通路、设计基于MIPS指令集的指令周期逻辑，从而设计指令限制逻辑，实现CPU部件；通过探讨软件规范和Hoare软件逻辑公理，说明数理逻辑在软件方面的基础作用。 “本文中所涉及到的图表、注解、公式等内容请以PDF格式阅读原文” 第11页 共11页第 11 页 共 11 页第 11 页 共 11 页第 11 页 共 11 页第 11 页 共 11 页第 11 页 共 11 页第 11 页 共 11 页第 11 页 共 11 页第 11 页 共 11 页第 11 页 共 11 页第 11 页 共 11 页