北航研究生课程_程序语言设计原理教程_第12章

第12章逻辑式程序设计语言程序要对数据结构实施某个算法过程,算法实现计算逻辑算法=逻辑+控制逻辑程序设计的基本观点是程序描述的是数据对象之间的关系。关系也是联系对象和对象、对象和属性的联系就是我们所说的事实。事实之间的关系以规则表述，根据规则找出合乎逻辑的事实就是推理逻辑程序设计范型是陈述事实、制定规则，程序设计就是构造证明。程序的执行就在推理12.1谓词演算谓词演算是符号化事实的形式逻辑系统，它也是逻辑程序设计语言的模型•谓词演算诸元素用形式方法研究论域上的对象需要一种语言，它能表达该域对象具有什么性质(properties)，以及对象间有些什么关系(relations)描述以公式(Formulas)表达。谓词公式中各元素按一定逻辑规则变换，即谓词演算(predicatecalculus)(1)公式由一组约定的符号组成的序列，它包括常量、变量、逻辑连接、命题函数、谓词、量词(2)常量指明论域上的对象(3)变量可束定到特定域上某个范围的对象上(4)函数表征对象具有的映射关系(5)谓词表征对象某种性质的符号(6)量词量词限定的变量名作用域是整个公式(7)逻辑操作and，or，not，→(蕴含)＝(全等)当谓词应用到的变元是常量或已被束定的变量上时，就叫做句子(sentence)或命题(proposition)谓词变元的个数称作目(arity)，有单目、N目谓词之称N-目谓词的例子。谓词目含义odd(X)1X是奇数father(F，S)2F是S的父亲divide(N，D，Q，R)4N除D得商Q和余数R谓词例化结果值odd(2)Falsedivide(23，7，3，2)Turefather(changshan，changping)Truedivide(23，7，3，N)N未例化，不知真假谓词的量化量化谓词结果值Xodd(X)FalseXodd(X)TrueX(X=2*Y+1→odd(X))TrueXYdivide(X，3，Y，0)FalseXYdivide(X，3，Y，0)True，如X=3，Y=1XYdivide(X，3，Y，0)False，但很难证明证明一个全称谓词是比较难的，因为最可靠的证明方法是枚举例证。于是采取反证的方法，全称量化的谓词取反量化谓词取反Xodd(X)Xnotodd(X)[1]Xodd(X)Xnotodd(X)[2]X(X=2*Y+1→odd(X))Xnot(X+2*Y+1→odd(X))[3]Xnot(X=2*Y+1)orodd(X))[4]X((X=2*Y+1)andnotadd(X))[5]XYdivide(X，3，Y，0)XYnotdivide(X，3，Y，0)[6]XYdivide(X，3，Y，0)XYnotdivide(X，3，Y，0)[7]XYdivide(X，3，Y，0)XYnotdivide(X，3，Y，0)[8]•谓词演算的等价变换[1]以∧，∨，消除→、=符号[2]化为前束范式,消除最外的符号,否定符号内移(XP(X)┠X(p(X))[3]用斯柯林变换消去存在量词X(a(X)∧b(X)∨Yc(X，Y))┠X(a(X)∧b(X)∨c(X，g(X)))[4]消除前束范式的全称量词┠a(X)∧b(X)∨c(X，g(X))一般谓词公式变换为子句的实例。‘┠’号为“可推出”[5]用分配率P∨(Q∧R)=(P∨Q)∧(P∨R)化成合取范式┠(a(X)∨c(X，g(X)))∧(b(X)∨c(X，g(X)))经过以上变换,任何一复合公式均可成为如下形式:F=C1∧C2∧…Cn且其中Ci称为子句若以';'代'∨'则有:Ci=L1∨L2∨…Lv=L1;L2;…;Lv因此，任一公式均可化为'∨'连接的子句的集合12.2自动定理证明•证明系统事实即证明系统中的公理(axioms)证明系统(proofsystem)是应用公理演绎出定理(theorems)的合法演绎规则的集合演绎也叫归约(deduction)，是对证明系统中合法推理规则的一次应用演绎从公理导出结论(conclusion)，中间可利用以这些规则演绎出的定理证明(proof)是个语句序列，以每个语句得到证明而结束，即每个句子要么演绎成公理，要么演绎成前此导出的定理一个证明若有N个语句(命题)则称N步证明反驳(refutation)是一个语句的反向证明。它证明一个语句是矛盾的，即不合乎给定的公理一个语句若能从公理出发推演出来，则称合法语句，任何合法语句也叫做定理(theorem)从某一公理集合导出的所有定理集合称为理论(theory)•模型从公理集合中导出定理集称之为理论，有了理论我们要解释它的语义必须借助某个模型(model)。因为形式系统只是符号抽象，借助模型我们可为每个常量、函数、谓词符号找到真理性的解释。即定义每个论域，并表明域上成员和常量公理之间的关系。公理的谓词符号必须派定为域中对象的性质，函数派定为对域中对象的操作。公理集合一般情况下只是定义的部分(偏)函数和谓词，是问题域的一个侧面。所以能满足该理论的模型往往不止一个。例一个最简单的理论公理集:Xinterval(X)→notinterval(X+1)(a1)Xnotinterval(X+1)→interval(X)(a2)2=1+1(a3)从间隔数公理可导出定理:Xinterval(X)→interval(X+2)(t1)Xinterval(X+2)→interval(X)(t2)谓词interval(间隔数)在整数域上有两个子域odd、even都能够满足间隔数理论不能证明interval(3),也不能证明notinterval(3)为真命题这就是Milbert讨论过的可判定(decidability)问题.1936年Church和Turing证实谓词演算可判定性问题是没有解的一旦我们断言interval(3)或interval(2)是真命题,我们立刻可通过演绎证明按这个理论写出的每一个谓词为真.这就是Godel和Herbrand1930年证实的谓词演算具备的完整性(completeness)•证明技术从谓词演算具有完整性，理论上可证明按公理集合建立的任何理论。关键是效率。如果我们从公理出发做出每一个步骤，在新的步骤上仍然要查找每一个公理，找出可能的推理。如此下去就形成一个庞大的树行公理集，每层的结点表示一个公理的语句，其深度和宽度随问题和最初给出的公理而定，一层一步骤，N层的树就是N步推理。对于自动定理证明程序，只有穷举每条可能的证明步骤才能说它是完全的。穷举完所有路径马上遇到组合爆炸问题，无论是深度优先还是广度优先，百步演绎可能的路径数都是天文数字。•归结定理证明J.A.Robinson1965年提出的归结法(resolution)，是命题演算中对合适公式的一种证明方法。为了证明合适公式F为真，归结法证明F恒假来代替F永真。把两子句合一(unification)并消去一对正逆命题，故归结也译作消解。归结证明的过程并称之归结演绎，其步骤如下:[1]把前题中所有命题换成子句形式。[2]取结论的反,并转换成子句形式,加入[1]中的子句集.[3]在子句集中选择含有互逆命题的命题归结。用合一算法得出新子句(归结式)，再加入到子句集。[4]重复[3]，若归结式为空则表示此次证明的逻辑结论是矛盾，原待证结论若不取反则恒真。命题得证。否则继续重复[3]。例：归结证明若有前题待证命题取反得新子句p1Q∨PP∨Up5Pp2R∨Qp6Up3S∨Rp4U∨S取待证命题的反，得P∧U，它是∧连接的两个子句P、U，把它们加到前题子句集，为p5，p6。归结演绎如下图:Q∨PPp1-p5归结QR∨Q再与p2归结S∨RR再与p3归结SU∨S再与p4归结UU再与p6归结矛盾由本例可以看出两个问题：第一，归结法是由合一算法实现的。所谓合一是找出型式匹配的两子句，将它们合一为归结式，相当于代数中的化简。第二，如果得不出矛盾，那么归结法要无休止地做下去，中间归结式出得越多，匹配查找次数越多，每一步都做长时间计算，Solution：利用切断(cut)操作，并利用对子句形式进一步限制的超级归结法(Hyperresolution)。•Horn子句实现超归结Horn子句是至多只有一个非负谓词符号的子句Horn子句形式示例如下:P∨Q∨S∨R∨T其中只有一个非负谓词S,可作以下演算：先将S移向右方┠S∨P∨Q∨R∨T按德·摩根定律┠S∨(P∧Q∧R∧T)'∨'即’→’，则┠S←(P∧Q∧R∧T)此条件Horn子句的意义是if(P∧Q∧R∧T)thenS。若S为空，则为无条件Horn子句，是一个断言(事实)12.3逻辑程序的风格第一个特点是它不描述计算过程而是描述证明过程第二个特点是描述性第三个特点是大量用表和递归实现重复操作例求平均成绩的逻辑程序，打开一分数文件scores，读入分数求和并用的数N除之得平均成绩average:-see(scores)，getinput(Sum，N)，seen(scores)，AvisSum/N，print('Average='，Av)getinput(Sum，N):-ratom(X)，not(eof)，getinput(Sum1，N1)，SumisSum1+X，NisN1＋1.getinput(0，0):-eof.12.4典型逻辑程序设计语言Prolog•Prolog要环境支持，即管理事实和规则的数据库•Prolog的基本成分是对象(常量、变量、结构、表)、谓词、运算符、函数、规则•从纯语法意义上Prolog的项什么都可以表示:•项::=常量|变量|结构|(项)|表后缀算符•|项中缀算符项|，项前缀算符•从语义角度，以下语法描述提供了处理时的语义概念:程序→子句子句→(事实|规则|查询)事实→结构规则→头:-体头→结构体→目标，目标目标→/*形如p或q(T，…，)的字面量*/•Prolog程序结构Prolog程序由子句组成，子句模型是Horn子句。(1)事实与规则Prolog程序先定义公理集例：Prolog的规则和事实条件子句(规则)pretty(X):-artwork(X)pretty(X):-color(X，red)，flower(X).watchout(X):-sharp(X，_).无条件子句(事实)color(rose，red).sharp(rose，stem).sharp(holly，leaf).flower(rose).flower(violet)artwork(painting(Monet，haystack_at_Giverny)).(2)查询Prolog中查询(query)是要求Prolog证明定理。因为提出的问题就是证明过程的目标,所以查询也叫目标(goal)。例:Prolog的查询?-pretty(rose).yes?-pretty(Y).Y=painting(Monet，haystack_at_Giverny).Y=rose.no?-pretty(W)，sharp(W，Z)W=roseZ=stemno例:最大公约数的欧基里得算法最大公约数欧基里得算法可用三条规则描述:gcd(A，0，A).gcd(A，B，D):-(AB)，(B0)，RisAmodB，gcd(B，R，D).gcd(A，B，D):-(AB)，gcd(B，A，D).•封闭世界内的假设如果有某个子目标查遍数据库也找不到能满足的事实，该子目标失败，但不等于整个目标的失败。即使是整个目标最后失败，也不等于这个目标追求的命题是否定的，因为限于数据库存放的规则和事实有限，它是“封闭世界假说”之下的失败。•函数和计算(1)函子完成逻辑设计中的计算函子以结构形式出现，如:中缀表示前缀表示X+Y*Z+(X，*(Y，Z))A-B/C-(A，/(B，C))故它不是