形式语义教材-Ch3 逻辑式语言

––72第三章逻辑式语言§3.1概述1972年,Kowalski和Colmerauer第一次提出了逻辑程序设计概念,Colmerauer和他的研究小组在法国Marseille大学第一个实现了逻辑程序设计语言PROLOG语言的解释器。在此之后，在1983年，D.H.D.Warren第一个实现了Prolog的编译器。自从编译器诞生开始,Prolog语言成了世界公认的著名语言。Prolog是一个顺序的具体逻辑式语言,而并行的逻辑语言有Parlog,ConcurrentProlog,GHP等。逻辑式语言的理论基础是Horn逻辑。逻辑式语言的应用领域有:关系数据库,问题求解,自然语言的理解,方程式的符号解法,生物化学中的分子结构分析,数理逻辑,人工智能等等。逻辑式语言的特点有:■具有良好的逻辑性■具有良好的并行性■具有良好的不确定性■可求多个解■有不完全值概念■无类型概念。§3.2有趣的Prolog语言在正式介绍逻辑式语言的理论、语法、语义等内容以前,首先粗略地领会一下Prolog程序的风格和趣味性。Prolog程序和我们所见到的过程式以及函数式语言有着很大的不同。在Prolog语言里,变量用大写字母打头的标识符来表示,凡是小写字母打头的都是常量(整常数或原子)。Prolog程序由一组子句组成,其中子句有两类,其一叫做事实,其二叫做规则。事实说明––73一个断言,比如like(mary,candy)表示这样一个事实：mary喜欢candy。规则部分,则用来表示推理,如下面是一个规则的例子:likes(mary,X)←likes(john,X),likes(stoy,X).它表示如果john喜欢X,并且stoy也喜欢X,则mary喜欢X。当然程序中的子句究竟代表什么内容,这是程序员自己才知道的。一个Prolog程序也可以是全部由事实部分组成。我们知道程序必须有个输入部分。那么,Prolog程序的输入是什么?这一点也和通常的程序不同,即输入的不是数据,而是一个提问。Prolog系统将回答yes或no。如果是yes情况,则具体还指出提问中的变量取什么样的值时,能够使提问成为真。例如,假设有图Prolog程序则这是仅由4个事实(公理)组成的程序。事实部分主要说的是谁喜欢什么。对于这个程序可以提出以下种种问题。比如:□?-like(mary,candy).回答yes（mary喜欢candy吗?）□?-like(mary,mary).回答no（mary喜欢mary吗?）□?-like(mary,X).回答yes:X=candy,X=wine（mary都喜欢什么?）□?-like(mary,X),like(john,X).回答yes:X=wine（什么东西(X)被mary和john所喜欢?）□?-like(mary,candy),like(john,candy).回答no（mary和john都喜欢candy吗?）□?-like(X,candy).回答yes:X=mary（都谁喜欢candy?）图3.2.1likes(mary,candy).mary喜欢糖果likes(mary,wine).mary喜欢水果likes(john,wine).john喜欢水果likes(john,meat).john喜欢肉类––74□?-like(X,wine).回答yes:X=mary,X=john（都谁喜欢wine?）□?-like(X,Y).回答yes:（谁都喜欢什么?）(1)X=mary,Y=food(2)X=mary,Y=wine(3)X=john,Y=wine(4)X=john,Y=mary从本例可以看出,对于同一程序可提出很多很多的问题。在这些提问里可包含一些变量X1,X2,....,Xn。如果回答是yes,则将指出当提问中的这些变量取什么样的值时使提问成为真。在提问时,只要把已知的内容写成常量,而把想知道的部分写成变量,那么即可达到了解未知部分的目的,因此是很有趣的。提问的语法结构是,由?-符号打头,并其后是一串原子式(用逗号隔开)。开始的提问部分称为初始总目标(或称目标子句),而其中的每个原子式称为子目标。总目标中的最前一个子目标称为当前子目标。如果所有子目标都成功,则总目标也就成功,这时系统将发出yes,并给出一个具体解。前面考虑了只有事实的Prolog程序。但只有事实部分远不能描述很多实际问题，比如“mary喜欢的john都喜欢”等问题。下面再考虑带规则（推理）部分的Prolog程序例，具体如下:male(john).john是男的male(stoy).stoy是男的male(david).david是男的female(mary).mary是女的female(rose).rose是女的female(mira).mira是女的parents_of(john,mary,davis).john的母父是mary和davisparents_of(stoy,mary,davis).stoy的母父是mary和davisparents_of(rose,mary,davis).rose的母父是mary和davisparents_of(mira,mary,davis).mira的母父是mary和davissister_of(X,Y):-female(X),female(Y),––75parents(X,M,F),parents(Y,M,F).Y是X的姐妹,当X是女的,且Y是女的,且X和Y的母父是一样的brother_of(X,Y):-male(X),male(Y),parents(X,M,F),parents(Y,M,F).Y是X的兄弟,若X是男的,且Y是男的,且X和Y的母父是一样的child_of(X,Y):-parents_of(Y,_,X).若X是Y的父亲,则Y是X的儿子child_of(X,Y):-parents_of(Y,X,_).若X是Y的母亲,则Y是X的儿子inherit_of(X,Y):-child_of(X,Y).若Y是X的儿子,则Y是X的后辈inherit_of(X,Y):-chile_of(Z,Y),inherit_of(X,Z).若Y是Z的儿子,Z是X的后辈,则Y是X的后辈程序由10个事实和6个规则组成。可以提问如下种种问题:■?-female(X).谁是女的?..........回答:X=mary;X=rose;X=mira■?-female(john).john是女的吗?....回答:no■?-child_of(mary,X).谁是mary的孩子?...........回答:X=john;X=rose;X=mira■?-child_of(X,stoy).stoy是谁的孩子?..回答:X=mary;X=davis■?-sister_of(mira,X).mary的姐妹都是谁?...回答:X=rose■?-brother_of(stoy,X).stoy的兄弟都是谁?■?-inherit_of(john,X).john的后辈都是谁?■?-inherit_of(X,davis).davis的前辈都是谁?■?-inherit_of(john,mary).john是mary的前辈吗?■?-parents_of(john,M,F).john的母亲和父亲是谁?■?-male(X),child_of(mary,X).都有谁是mary的男孩?§3.3逻辑式语言逻辑式程序设计的主要思想是把一阶谓词逻辑的公式作为––76程序设计的工具,而Prolog语言是顺序化了的特定逻辑式语言。逻辑式语言的理论基础是一阶理论与归结理论。■定义3.3.1.一阶理论(firstordertheory):由四部分组成:(∑,L,A,R)[1]字母表(alphabet):∑[2]一阶语言(firstorderlanguage):L[3]公理集(setofaxioms):A[4]推理规则集(setofinferencerules):R其中字母表∑包括以下几类符号:□Constant:a,b,c,..........□Variable:x,y,z,...........□Function:f,g,h,...........□Predicate:p,q,r,..........□Connective:~,∧,∨,→□Quantifier:,□Punctuation::(,)■定义3.3.2.项原子(1)任何常量a∈Constant是项,任何变量x∈Variable是项;若f∈Function是n元函数符号,ti是项,则f(t1,t2,...,tn)是项。(2)设p∈Predicate是任一n元谓词符号(0≤n),并且ti是项,则p(t1,t2,...,tn)是原子公式。以后有时也简称为原子。■定义3.3.3.一阶语言一阶语言L是合适公式的集合。其中合适公式的定义如下:(1)原子公式是合适公式。(2)若F,F1,F2是合适公式,则下面公式都是合适公式:F1∧F2,F1∨F2,~F1,(F),F1→F2,F1←F2,x.F,x.F■定义3.3.4.自由变量设F是一个公式,并且变量X出现于公式F中。如果X∈––77FreeF(F),则称变量X为公式F的一个自由变量。其中FreeF(F)的定义如下:FreeF(A)=FreeA(A)FreeF(F1∧F2)=FreeF(F1)∪FreeF(F2)FreeF(F1∨F2)=FreeF(F1)∪FreeF(F2)FreeF(~F)=FreeF(F)FreeF(x.F)=FreeF(F)-{x}FreeF(x.F)=FfreeF(F)-{x}FreeT(const)={}FreeT(X)={var}FreeT(f(t1,..,tn))=∪iFreeT(ti)FreeA(p(t1,..,tn))=∪iFreeT(ti)■定义3.3.5.全称闭包设F为公式,且Free(F)={x1,...,xn}则称下面式子x1x2...xn(F)为F的全称闭包(universalclosureofformula)。■定义3.3.6.文字原子或原子的非统称为文字(Literal)。其中原子被称为正文字,而原子的非则被称为负文字。例3.3.1.□文字的正确例:p(f(X),Y),~p(a,f(X))□文字的错误例:p(f(X),Y)∧~p(a,f(X))■定义3.3.7.子句设Li(1≤i≤n)是文字,{x1,...,xk}=FreeF(L1∨...∨Lm},则称下面形式的式子为子句:x1x2...xn(L1∨L2∨.....∨Lm)换言之,子句(Clause)是文字的析取式的全程闭包。例3.3.2.□正确子句例:xy(p(x,y)∨~p(f(a),y)∨~q(a,b))––78□错误子句例:xy(p(x,y)∧q(x,y)∨~p(f(a),x))假设x1..xn.(A1∨...∨Ak∨~B1∨...∨~Bm)是子句,则可简写成下面形式之一:□A1∨...∨Ak∨~B1∨...∨~Bm□A1∨...∨Ak←B1∧...∧Bm■定理3.3.8.Skolem定理设F是一阶公式,则F可转换成子句的合取式S:S=C1∧C2∧....∧Cn并使得F与S的不可满足性一致。其中每个Ci是子句。证明:略。例3.3.3.下面是公式到子句的合取式的转换例。□要转换的公式:wx[p(x)[~y[q(x,y)p(f(w))]∧z[q(x,z)p(x)]]]□消除:wx[~p(x)∨[~y[~q(x,y)∨p(f(w))]∧z[~q(x,z)∨p(x)]]]□~移入内部:wx[~p(x)∨[y[q(x,y)∧~p(f(w))]∧z[~q(x,z)∨p(x)]]]□移右:wx[~p(x)∨[y.q(x,y)∧~p(f(w))]∧[z.~q(x,z)∨p(x)]]]□消除:x[~p(x)∨[q(x,g(x))∧~p(f(a))]∧[z.~q(x,z)∨p(x)]]]□移外:xz[~p(x)∨[q(x,