逻辑式程序设计语言.pptx

,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,#,6.1,谓词演算,谓词演算是符号化事实的形式逻辑系统，它也是逻辑程序设计语言的模型,谓词演算诸元素,用形式方法研究论域上的对象需要一种语言，它能表达该域对象具有什么性质(,properties)，,以及对象间有些什么关系(,relations),描述以公式(,Formulas),表达。谓词公式中各元素按一定逻辑规则变换，即谓词演算(,predicate calculus),(1),公式,由一组约定的符号组成的序列，它包括常量、变量、逻辑连接、命题函数、谓词、量词,(2),常量,指明论域上的对象,(3),变量,可束定到特定域上某个范围的对象上,(4),函数,表征对象具有的映射关系,(5),谓词,表征对象某种性质的符号,(6),量词,量词限定的变量名作用域是整个公式,(7),逻辑操作,and，or，not，(,蕴含)(全等),当谓词应用到的变元是常量或已被束定的变量上时，就叫做句子(,sentence),或命题(,proposition),谓词变元的个数称作目(,arity)，,有单目、,N,目谓词之称,N-,目谓词的例子。,谓词 目 含义,odd(X)1 X,是奇数,father(F，S)2 F,是,S,的父亲,divide(N，D，Q，R)4 N,除,D,得商,Q,和余数,R,谓词例化 结果值,odd(2)False,divide(23，7，3，2)Ture,father(changshan，changping)True,divide(23，7，3，N)N,未例化，不知真假,谓词的量化,量化谓词 结果值,Xodd(X)False,Xodd(X)True,X(X=2*Y+1odd(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),Xnot odd(X),1,Xodd(X),Xnot odd(X),2,X(X=2*Y+1odd(X),Xnot(X+2*Y+1odd(X),3,Xnot(X=2*Y+1)or odd(X),4,X(X=2*Y+1)and not add(X),5,X,Y divide(X，3，Y，0),X,Y not divide(X，3，Y，0),6,X,Y divide(X，3，Y，0),X,Y not divide(X，3，Y，0),7,X,Y divide(X，3，Y，0),X,Y not divide(X，3，Y，0),8,谓词演算的等价变换,1以，,消除、符号,2化为前束范式,消除最外的,符号,否定符号内移,(,XP(X),X(,p(X),3,用斯柯林变换消去存在量词,X(a(X)b(X),Y c(X，Y),X(a(X)b(X)c(X，g(X),4,消除前束范式的全称量词,a(X)b(X)c(X，g(X),一般谓词公式变换为子句的实例。,号为“可推出”,5用分配率,P(QR)=(PQ)(PR),化成合取范式,(,a(X)c(X，g(X)(b(X)c(X，g(X),经过以上变换,任何一复合公式均可成为如下形式:,F=C1C2 Cn,且其中,Ci,称为子句,若以,;,代,则有:,Ci=L1 L2 Lv=L1;L2;Lv,因此，任一公式均可化为连接的子句的集合,6.2,自动定理证明,证明系统,事实即证明系统中的公理(,axioms),证明系统(,proof system),是应用公理演绎出定理,(,theorems),的合法演绎规则的集合,演绎也叫归约(,deduction)，,是对证明系统中合法,推理规则的一次应用,演绎从公理导出结论(,conclusion)，,中间可利用以,这些规则演绎出的定理,证明,(,proof),是个语句序列，以每个语句得到证明而结束，即每个句子要么演绎成公理，要么演绎成前此导出的定理,一个证明若有,N,个语句(命题)则称,N,步证明,反驳,(,refutation),是一个语句的反向证明。它证明,一个语句是矛盾的，即不合乎给定的公理,一个语句若能从公理出发推演出来，则称,合法语句,，任何合法语句也叫做,定理,(,theorem),从某一公理集合导出的所有定理集合称为,理论,(,theory),模型,从公理集合中导出定理集称之为,理论,，有了理论我们要解释它的语义必须借助某个,模型,(,model)。,因为形式系统只是符号抽象，借助模型我们可为每个常量、函数、谓词符号找到真理性的解释。即定义每个论域，并表明域上成员和常量公理之间的关系。公理的谓词符号必须派定为域中对象的性质，函数派定为对域中对象的操作。,公理集合一般情况下只是定义的部分(偏)函数和谓词，是问题域的一个侧面。所以能满足该理论的模型往往不止一个。,例 一个最简单的理论,公理集:,Xinterval(X)not interval(X+1)(a1),Xnot interval(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),也不能证明,not interval(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。,例：归结证明,若有前题 待证命题 取反得新子句,p1 Q,P,P,U p5 P,p2 R,Q p6 U,p3 S,R,p4,U,S,取待证命题的反，得,PU，,它是连接的两个子句,P、U，,把它们加到前题子句集，为,p5，p6。,归结演绎如下图:,Q,P P p1-p5,归结,Q R,Q,再与,p2,归结,S,R R,再与,p3,归结,S,U,S,再与,p4,归结,U,U,再与,p6,归结,矛盾,由本例可以看出两个问题：,第一，归结法是由合一算法实现的。所谓,合一,是找出型式匹配的两子句，将它们合一为归结式，相当于代数中的化简。,第二，如果得不出矛盾，那么归结法要无休止地做下去，中间归结式出得越多，匹配查找次数越多，每一步都做长时间计算，,Solution,：,利用切断(,cut),操作，并利用对子句形式进一步限制的,超级归结法,(,Hyperresolution)。,Horn,子句实现超归结,Horn,子句是至多只有一个非负谓词符号的子句,Horn,子句形式示例如下:,P,QS,R,T,其中只有一个非负谓词,S,可作以下演算：,先将,S,移向右方,S,P,Q,R,T,按德摩根定律,S,(PQRT),即，则,S(P Q R T),此条件,Horn,子句的意义是,if(PQRT)then S。,若,S,为空，则为无条件,Horn,子句，是一个断言(事实),6.3,逻辑程序的风格,第一,个特点是它不描述计算过程而是描述证明过程,第二个特点是描述性,第三个特点是大量用表和递归实现重复操作,例 求平均成绩的逻辑程序，打开一分数文件,scores，,读入分数求和并用的数,N,除之得平均成绩,average:-see(scores)，,getinput(Sum，N)，,seen(scores)，,Av is Sum/N，,print(Average=，Av),getinput(Sum，N):-ratom(X)，,not(eof)，,getinput(Sum1，N1)，,Sum is Sum1+X，,N is N11.,getinput(0，0):-eof.,6.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=rose Z=stem,no,例:最大公约数的欧基里得算法,最大公约数欧基里得算法可用三条规则描述:,gcd(A，0，A).,gcd(A，B，D):-(AB)，(B0)，R is A mod B，,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),故它不是谓词，仅仅是一特殊的结构：,(，),函数求值的的结果一般通过谓词,is(，)束定到变元上,gcd(A，B，D);-(AB)，(B0)，R is A mod B，gcd(B，R，D).,把,函数改写为约束，很容易写出,prolog,程序,例 求斐波那契数的,Prolog,程序,斐波那契函数以下述公式生成以下数列:,1，1，2，3，5，8，13，21，,Fib(0)=1,Fib(1)=1,Fib(n)=Fib(n-1)+Fib(n-2),第一、二式是事实也是公理，把结果值作为变元照写。第三式说明，若,n,为斐波那契数，,n-1,和,n-2,的斐波那契必须成立，且这两个数之和是,n,的斐波那契数，,n1，,于是有,Prolog,程序,Fib(0，1).,Fib(1，1).,Fib(n，f):-Fib(m，g)，Fib(k，h)，m is n-1，k is m-1，,f is g+h，n1.,当有查询?-,Fib(5，f),时，,f,返回8,(2)逻辑程序的算法表达,算法怎样用公理表达呢？拿一个最典型的,Quicksort,分类程序讨论。,quicksort(,未分类表，分类完的表):-,(从未分类表拿出第一元素,以它为基准,分成两个表),1,quicksort(,小表，分类完小表)，2,quicksort(,大表，分类完大表)，3,append(,分类完小表，,基准元素和分类完大表，分类完总表)4,这样把快速分类的总目标变成了四个子目标,例 快速分类的,Prolog,代码,r1 split(_，).,r2 split(Pivot，Head|Tail，Head|Sm，Lg):-,Head Pivot，split(Pivot，Tail，Sm，Lg).,r3 split(Pivot，Head|Tail，Sm Head|Lg):-,Pivot Head，split(Pivot，Tail，Sm，Lg).,r4 quicksort(，).,r5 quicksort(Head ，Head).,r6 quicksort(Pivot|Unsorted AllSorted):-,split(Pivot，Unsorted，Small，Large),quicksort(Small，SmSorted)，,quicksort(Large，Lgsorted),append(SmSorted，Pivot|LgSorted，AllSorted).,(3)逻辑和控制分离,Prolog,无通常意义的控制结构，也就是该程序动作次序（显然也有）和计算的子句逻辑没有必然的关系。例如:把上例中,r4,r5,r6,写在,r1,r2,r3,前面并不影响本程序的执行结果。,cut,和,not,谓词,因为,Prolog,的归结模型只能完整地证明正命题，是否有解无法判定,如果明知再作没有意义，可人为截断,cut,(1)安全,cut,非形式解释,cut，,它如同一篱笆，由程序员任意置放在规则之中，以停止无意义的回溯。,例 安全,cut,示例：,求1到,N,的整数之和,r1 sum_to(N，1):-N=1，！.,r2 sum_to(N，R):-N1 is N-1，sum_to(N1，R1)，,R is R1+N.,当有查询:,?-,sum_to(1，X)/,匹配,r1,X=1;/,打;号由于有！不致无限查,找第2个,no,?-sum-to(6，X)/,匹配,r1,失败，匹配,r2,连续,r2,X=21;/,直至成功，打;号也不再找,no,r1,可用,sum_to(1,1).,事实代,(2),cut,实现,not,操作,r1 not(X):-X，！，fail.,r2 not(_).,其推理过程是:,若,X,为假，匹配,r1，,在未达到！时已失败，则匹配规则,r2，,由于,r2,什么变元都可以且总为成功，所以，,not(X),是成功的。,若,X,为真，匹配,r1,后，,X,为真，控制通过！传到,fail,则,r1,失败。于是回溯到！过不去，只好失败。由于用了!就地失败，它不再匹配,r2，,故,not(X),为失败。,正是由于这个原因，谓词,p,和,not(not(p),求值结果不能保证一样，有时,not(p),和,not(not(p),求值结果倒是一样的，以下是,not,谓词出毛病的例子:,例 不可靠的,not,谓词,假定一规则,test,有以下定义:,test(S，T):-S=T.,运行以下查询时有:,?-,test(3，5).,no,?-test(5，5),yes,?-not(test(5，5),no,?-test(X，3)，R is X+2.,X=3,R=5,?-not(not test(X，3)，R is X+2.,！error in arithmetic expression:not a number,由于第二次,not(,外部的)求值时用到上例规则,r1，,其中,X,是,not(test(X，3),的结果值，故,X+2,不是数加2,。,这个问题原因在于子句逻辑的不可判定性,(3)不安全的,cut,cut,使我们处于两难的境地，它的高效是以风险为代价得到的，如同60年代,goto,技巧对非结构化程序的影响。只要模型是超级归结，,cut,的两面性是不可以解决的。,6.5 Prolog,评价,Prolog,提供一种证明风格的声明式程序设计，推理清晰，概括能力强，程序和数据没有明显分离。,Prolog,程序具有自文档性,由于非过程性，它也成为潜在的并行程序设计语言的候选者,它的效率仍不及传统过程语言。由于它的声明性质，程序员在优化算法时作用有限,复杂的大型系统一开始很难按照证明系统开发，程序不大运算量惊人，而,Prolog,本身也只有局部量，天生来也不是大型软件开发的工具。因此，,Prolog,只能作为逻辑程序设计的独枝存在，解决大型应用多范型语言是个出路,