邏輯式程序設計語言

1、第六章 邏輯式程序設計語言,邏輯式語言基本形式：用一種符號邏輯作為程序設計語言來進行程序設計，通常稱為邏輯程序設計語言，或聲明性語言,第六章 邏輯式程序設計語言,程序要對數據結構實施某個算法過程,算法實現計算邏輯 算法 = 邏輯 + 控制邏輯程序設計的基本觀點是程序描述的是數據對象之間的關系。關系也是聯系對象和對象、對象和屬性的聯系就是我們所說的事實。事實之間的關系以規(guī)則表述，根據規(guī)則找出合乎邏輯的

2、事實就是推理邏輯程序設計范型是陳述事實、制定規(guī)則，程序設計就是構造證明。程序的執(zhí)行就在推理,6.1謂詞演算,謂詞演算是符號化事實的形式邏輯系統(tǒng)，它也是邏輯程序設計語言的模型表示命題表示命題之間的關系描述如何根據假設為真的命題推斷出新命題 謂詞演算諸元素 用形式方法研究論域上的對象需要一種語言，它能表達該域對象具有什么性質(properti

3、es)， 以及對象間有些什么關系(relations) 描述以公式(Formulas)表達。謂詞公式中各元素按一定邏輯規(guī)則變換，即謂詞演算(predicate calculus),(1)公式 由一組約定的符號組成的序列，它包括常量、變量、邏輯連接、命題函數、謂詞、量詞(2)常量 指明論域上的對象(3)變量 可束定到特定域上某個范圍的對象上(4)函數 表征對象具有的映射關系(5)謂詞 表征對象某種性質的符號(6)量

4、詞 量詞限定的變量名作用域是整個公式(7) 邏輯操作 and， or， not， →(蘊含) (全等)當謂詞應用到的變元是常量或已被束定的變量上時，就叫做句子(sentence)或命題(proposition),謂詞變元的個數稱作目(arity)，有單目、N目謂詞之稱 N-目謂詞的例子。 謂詞 目 含義 od

5、d(X) 1 X是奇數 father(F，S) 2 F是S的父親 divide(N，D，Q，R) 4 N除D得商Q和余數R 謂詞例化 結果值

6、 odd(2) False divide (23， 7， 3，2) Ture father (changshan， changping) True divide (23， 7， 3， N) N未例化， 不知真假,謂詞的

7、量化量化謂詞 結果值 ?Xodd(X) False ?Xodd(X) True ?X(X=2*Y+1→odd (X)) True ?X?Ydivide (X，3，Y，0) Tr

8、ue， 如X =3，Y=1?X?Ydivide (X，3，Y，0) False?X?Ydivide(X，3，Y，0) False， 但很難證明,證明一個全稱謂詞是比較難的，因為最可靠的證明方法是枚舉例證。 于是采取反證的方法，全稱量化的謂詞取反量化謂詞 取反?Xodd(X)

9、 ?Xnot odd(X) [1]?Xodd(X) ?Xnot odd(X) [2]?X(X=2*Y+1→odd(X)) ?Xnot(X+2*Y+1→odd(X)) [3]

10、 ?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 div

11、ide (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) ∨

12、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稱為子句

13、若以';'代'∨'則有: Ci = L1 ∨L2 ∨…Lv = L1;L2;…;Lv 因此，任一公式均可化為'∨'連接的子句的集合,6.2 自動定理證明,證明系統(tǒng) 事實即證明系統(tǒng)中的公理(axioms) 證明系統(tǒng)(proof system)是應用公理演繹出定理

14、 (theorems)的合法演繹規(guī)則的集合 演繹也叫歸約(deduction)，是對證明系統(tǒng)中合法 推理規(guī)則的一次應用 演繹從公理導出結論(conclusion)， 中間可利用以 這些規(guī)則演繹出的定理證明(proof)是個語句序列， 以每個語句得到證明而結束， 即每個句子要么演繹成公理， 要么演繹成前此導出的定理,一個證明若有N個語句(命題)則稱N步

15、證明反駁(refutation)是一個語句的反向證明。 它證明 一個語句是矛盾的， 即不合乎給定的公理一個語句若能從公理出發(fā)推演出來， 則稱合法語句， 任何合法語句也叫做定理(theorem)從某一公理集合導出的所有定理集合稱為理論(theory),模型 從公理集合中導出定理集稱之為理論，有了理論我們要解釋它的語義必須借助某個模型(model)。因為形式系統(tǒng)只是符號抽象，借助

16、模型我們可為每個常量、函數、謂詞符號找到真理性的解釋。即定義每個論域，并表明域上成員和常量公理之間的關系。 公理的謂詞符號必須派定為域中對象的性質， 函數派定為對域中對象的操作。 公理集合一般情況下只是定義的部分(偏)函數和謂詞， 是問題域的一個側面。 所以能滿足該理論的模型往往不止一個。,例 一個最簡單的理論 公理集: ?Xin

17、terval(X)→not interval (X+1) (a1)?Xnot interval (X+1)→interval(X) (a2)2=1+1 (a3) 從間隔數公理可導出定理:

18、 ?Xinterval (X)→interval (X+2) (t1)?Xinterval (X+2) → interval(X) (t2),謂詞interval(間隔數)在整數域上有兩個子域odd、even都能夠滿足間隔數理論不能證明interval(3)，也不能證明not interval(3)為真命題。這就是Hi

19、lbert討論過的可判定(decidability)問題。1936年Church和Turing證實謂詞演算可判定性問題是沒有解的一旦我們斷言interval(3)或interval(2)是真命題,我們立刻可通過演繹證明按這個理論寫出的每一個謂詞為真。這就是Godel和Herbrand1930年證實的謂詞演算具備的完整性(completeness),證明技術

20、 從謂詞演算具有完整性， 理論上可證明按公理集合建立的任何理論。關鍵是效率。 如果我們從公理出發(fā)做出每一個步驟， 在新的步驟上仍然要查找每一個公理，找出可能的推理。如此下去就形成一個龐大的樹行公理集， 每層的結點表示一個公理的語句， 其深度和寬度隨問題和最初給出的公理而定， 一層一步驟， N層的樹就是N步推理。 對于自動定理證明程序， 只有窮舉每條可能的證明步驟才能說它是完全的。 窮舉完所有路徑馬上遇到

21、組合爆炸問題，無論是深度優(yōu)先還是廣度優(yōu)先，百步演繹可能的路徑數都是天文數字。,歸結定理證明 J.A.Robinson1965年提出的歸結法(resolution) ，是命題演算中對合適公式的一種證明方法。 為了證明合適公式F為真， 歸結法證明?F恒假來代替F永真。 把兩子句合一(unification)并消去一對正逆命題，故歸結也譯作消解。 歸結證明的過程并稱之歸結演繹， 其步驟如下:,[1]

22、把前題中所有命題換成子句形式。[2]取結論的反,并轉換成子句形式,加入[1]中的子句集.[3]在子句集中選擇含有互逆命題的命題歸結。用合一算法得出新子句(歸結式)，再加入到子句集。[4]重復[3]，若歸結式為空則表示此次證明的邏輯結論是矛盾，原待證結論若不取反則恒真。命題得證。 否則繼續(xù)重復[3]。,例：歸結證明 若有前題 待證命題 取反得新子句 p1 Q∨?P

23、 ?P∨?U p5 P p2 R∨?Q p6 U p3 S∨?R p4 ?U∨?S 取待證命題的反， 得P∧U， 它是∧連接的兩個子句P、U，把它們加到前題子句集， 為p5，p6。,歸

24、結演繹如下圖: Q∨?P P p1-p5歸結 Q R∨?Q 再與p2歸結 S∨?R R 再與p3歸結 S ?U∨?S

25、 再與p4歸結 U ?U 再與p6歸結 矛盾,,,,,,,,,,,,由本例可以看出兩個問題：第一，歸結法是由合一算法實現的。所謂合一是找出型式匹配的兩子句， 將它們合一為歸結式， 相當于代數中的化簡。第二，如果得不出矛盾，那么歸結法要無休止地做

26、下去，中間歸結式出得越多， 匹配查找次數越多， 每一步都做長時間計算。 Solution：利用切斷(cut)操作， 并利用對子句形式進一步限制的超級歸結法(Hyperresolution)。,Horn子句實現超歸結 Horn子句是至多只有一個非負謂詞符號的子句 Horn子句形式示例如下: ?P∨?Q∨S∨?R∨?T 其中只有一個非負謂詞S,可作以下演算： 先將S移向右方

27、 ┠ S∨?P∨?Q∨?R∨?T 按德·摩根定律 ┠ S∨? (P∧Q∧R∧T) '∨?'即’→’， 則 ┠ S →(P ∧ Q ∧ R ∧ T) 此條件Horn子句的意義是 if S then (P∧Q∧R∧T) 。 若S為空， 則為無條件Horn子句， 是一個斷言(事實),6.3 邏輯程序

28、的風格,第一個特點是它不描述計算過程而是描述證明過程第二個特點是描述性第三個特點是大量用表和遞歸實現重復操作sort（old_list,new_list） ┠ permute(old_list,new_list) ∧ sorted(new_list) sorted(list) ∧ ?j 使得 1≤ j < n, list(j) ≤ list(j+1)*permute是一個謂詞，如果第二個參數組是第一個參數組的一個

29、排列，就返回真,Prolog語言,Prolog是一種基于一階謂詞的邏輯式語言Prolog是基于Horn子句的，使用歸結推理，具有很強的邏輯描述能力和推理能力Prolog語言特點：一階邏輯的語言形式是形式化地嚴格定義的一階邏輯的語法簡易易懂邏輯公式不需要重復表達，與不同應用無關事實、假設、推理、查詢、視圖和完整性規(guī)約條件都能以基于一階邏輯的prolog語言表達邏輯語言Prolog可作為定義和比較其它知識表示模型的共同模型,例

30、 求平均成績的邏輯程序，打開一分數文件scores， 讀入分數求和并用的數N除之得平均成績 average :- see(scores)， getinput (Sum，N)， seen (scores)， Av is Sum /N， print ('Average

31、= '， Av) getinput (Sum，N) :- ratom (X)， not (eof)， getinput (Sum1，N1)， Sum is Sum1 + X，

32、 N is N1＋1. getinput (0，0) :- eof.,6.4 典型邏輯程序設計語言Prolog,Prolog要環(huán)境支持 ，即管理事實和規(guī)則的數據庫 Prolog的基本成分是對象(常量、變量、結構、表)、謂詞、運算符、函數、規(guī)則從純語法意義上Prolog的項什么都可以表示: ::=|||()|

33、 ||,從語義角度， 以下語法描述提供了處理時的語義概念: → → ( | | ) → → : - → → ， → /*形如p或q(T， …，)的字面量*/,與Prolog交互,？- （在每輪交互開始時系統(tǒng)都會給出“提示符號”）表示希望得到一個查詢？- consult（links）.Consult結構讀入包含事實和規(guī)則的文

34、件，并將這些內容添加到當前規(guī)則數據庫末尾。？- link（algol60，L），link（L，M）.L = cplM = bcpl表示：是否存在L和M，使link（algol60，L）and link（L，M）？輸入“；”并回車，Prolog將用另一個解作為響應，或者用“no”說明已經無法在找到解。規(guī)則的表示規(guī)則就是horn子句 :- 1, 2, ……, k.:- 左邊的項稱為頭部，在:- 右邊的那些項稱為條件。事實

35、是規(guī)則的特殊形式，只有頭部而沒有條件。Path(L, L).Path(L, M) :- link(L, X), path(X, M).其中變量X，出現在條件里面，而不在頭部，表示某個滿足條件的對象,與Prolog交互,合一 ？- f（X, b） = f（a，Y）.X = aY = b得到項T的實例方法：用一些項去替換T中的一個或幾個變量。同一個變量的所有出現必須用同一個項去替換。f（a，b）是f（X，b）的實例

36、，同理f（a，b）是f（a，Y）的實例。共同的實例是f（a，b）。g（a，b）不是g（X，X）的實例合一是在規(guī)則應用時隱含發(fā)生的。算術：“=”運算符表示合一？- X = 2+3 X = 2+3中綴運算符“is”對表達式求值：？- X is 2+3 X = 5,Prolog程序結構 Prolog程序由子句組成， 子句模型是Horn子句。(1) 事實與規(guī)則

37、 Prolog程序先定義公理集例：Prolog的規(guī)則和事實 條件子句(規(guī)則) pretty (X):-artwork(X) pretty (X):-color(X，red)，flower(X). watchout (X):-sharp(X

38、，_). 無條件子句(事實) color (rose，red). sharp (rose，stem). sharp (holly，leaf). flower(rose).

39、 flower(violet) artwork (painting (Monet， haystack_at_Giverny)).,(2)查詢

40、 Prolog中查詢(query)是要求Prolog證明定理。 因為提出的問題就是證明過程的目標,所以查詢也叫目標(goal)。例: Prolog的查詢 ?- pretty (rose). yes

41、 ?- pretty (Y). Y=painting (Monet，haystack_at_Giverny). Y=rose. no ?-prett

42、y(W)， sharp(W，Z) W=rose Z=stem no,例: 最大公約數的歐基里得算法 最大公約數歐基里得算法可用三條規(guī)則描述: gcd (A，0，A). gcd (A，B，D):-(A>B)，(B>0)，R is A mod B，

43、 gcd(B，R，D). gcd (A，B，D):-(A<B)， gcd (B，A，D).,封閉世界內的假設 如果有某個子目標查遍數據庫也找不到能滿足的事實， 該子目標失敗， 但不等于整個目標的失敗。 即使是整個目標最后失敗， 也不等于這個目標追求的命題是否定的， 因為限于數據庫存放的規(guī)則和事實有限， 它是“封閉

44、世界假說”之下的失敗。,函數和計算(1) 函子完成邏輯設計中的計算 函子以結構形式出現， 如: 中綴表示 前綴表示 X+Y*Z +(X，*(Y，Z)) A-B/C -(A，/(B，C)) 故它不是謂詞

45、，僅僅是一特殊的結構： (， …， )函數求值的的結果一般通過謂詞is(，)束定到變元上gcd (A，B，D);-(A>B)，(B>0)，R is A mod B，gcd(B，R，D).把函數改寫為約束，很容易寫出prolog程序,例 求斐波那契數的Prolog程序 斐波那契函數以下述公式生成以下數列: 1， 1， 2， 3， 5

46、， 8， 13， 21， … Fib(0) = 1 Fib(1) = 1 Fib(n) = Fib(n-1) + Fib(n-2)第一、二式是事實也是公理，把結果值作為變元照寫。 第三式說明，若n為斐波那契數，n-1和n-2的斐波那契必須成立，且這兩個數之和是

47、n的斐波那契數， n>1， 于是有Prolog程序 Fib (0，1). Fib (1，1). Fib (n，f):-Fib(m，g)，Fib(k，h)，m is n-1，k is m-1，

48、 f is g+h， n>1. 當有查詢 ?-Fib(5，f)時， f返回8,(2) 邏輯程序的算法表達 算法怎樣用公理表達呢？拿一個最典型的Quicksort分類程序討論。 quicksort(未分類表，分類完的表):- (從未分類表拿出第一元素,以它為基準,分成兩個表), [1] quicksort(小表，分類完小

49、表)， [2] quicksort(大表，分類完大表)， [3] append (分類完小表， 基準元素和分類完大表，分類完總表) [4]這樣把快速分類的總目標變成了四個子目標,例 快速分類的Prolog代碼 r1

50、 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 &l

51、t; Head，split (Pivot，Tail，Sm，Lg). r4 quicksort ([ ]，[ ]). r5 quicksort ([Head [ ] ]，Head). r6 quicksort ([Pivot | Unsorted] AllSorted):- split (Pivot，Unsorted，Small，Large), quic

52、ksort (Small，SmSorted)， quicksort (Large，Lgsorted), append (SmSorted，[Pivot | LgSorted]，AllSorted).,(3)邏輯和控制分離 Prolog無通常意義的控制結構，也就是該程序動作次序（顯然也有）和計算的子句邏輯沒有必然的關系。例如:把上例中r4,r5,r6寫在r1,r2,r3前面并不影

53、響本程序的執(zhí)行結果。,cut和not謂詞 因為Prolog的歸結模型只能完整地證明正命題， 是否有解無法判定 如果明知再作沒有意義，可人為截斷cut(1) 安全cut 非形式解釋cut， 它如同一籬笆， 由程序員任意置放在規(guī)則

54、之中， 以停止無意義的回溯。,例 安全cut示例：求1到N的整數之和 r1 sum_to(N，1):-N=1，！. r2 sum_to (N，R):-N1 is N-1，sum_to(N1，R1)，

55、 R is R1 + N.當有查詢: ?-sum_to(1，X) //匹配r1 X=1; //打‘;’號由于有！不致無限 查找第2個

56、 no ?-sum_to(6，X) //匹配r1失敗， 匹配r2連續(xù)r2 X=21; //直至成功， 打';'號也不再找 no r1 可用sum_to(1,1).事實代,(2) cut 實現n

57、ot操作 r1 not(X):-X，！，fail. r2 not(_).其推理過程是: ·若X為假，匹配r1，在未達到！時已失敗，則匹配規(guī)則r2，由于r2什么變元都可以且總為成功，所以， not(X)是成功的。 · 若X為真，匹配r1后，X為真，控制通過！傳到fail,則r

58、1失敗。 于是回溯到！過不去，只好失敗。由于用了!就地失敗，它不再匹配r2， 故not(X)為失敗。 正是由于這個原因， 謂詞p和not(not (p))求值結果不能保證一樣， 有時not(p)和not(not (p))求值結果倒是一樣的， 以下是not謂詞出毛病的例子:,例 不可靠的not謂詞 假定一規(guī)則test有以下定義: test (S，T):-S=T. 運行以下查詢時有:

59、 ?-test(3，5). no ?-test(5，5) yes ?-not( test(5，5) )

60、 no ?-test(X，3)，R is X+2. X=3 R=5 ?- not (not test (X，3))， R is X+2. ！ error in arithmetic exp

61、ression : not a number,r1 not(X):-X，！，fail.r2 not(_).由于第二次not(外部的)求值時用到上例規(guī)則r1， 其中X是not(test(X，3))的結果值，故X+2不是數加2。這個問題原因在于子句邏輯的不可判定性,(3)不安全的cut cut使我們處于兩難的境地， 它的高效是以風險為代價得到

62、的，如同60年代goto技巧對非結構化程序的影響。只要模型是超級歸結， cut的兩面性是不可以解決的。,6.5 Prolog評價,Prolog提供一種證明風格的聲明式程序設計， 推理清晰， 概括能力強， 程序和數據沒有明顯分離。Prolog程序具有自文檔性由于非過程性，它也成為潛在的并行程序設計語言的候選者它的效率仍不及傳統(tǒng)過程語言。由于它的聲明性質， 程序員在優(yōu)化算法時作用有限復雜的大型系統(tǒng)一開始很難按照證明系統(tǒng)開發(fā)， 程序不

63、大運算量驚人 ， 而Prolog本身也只有局部量， 天生來也不是大型軟件開發(fā)的工具。 因此， Prolog只能作為邏輯程序設計的獨枝存在， 解決大型應用多范型語言是個出路,歸結練習,已知：某些病人喜歡所有的醫(yī)生(A1) 沒有一個病人喜歡任意一個騙子(A2)欲證明：任意一個醫(yī)生都不是騙子(B)證明：事實表示：令P（x）：x是病人D（x）：x是醫(yī)生Q（x）：x是騙子L（x，y）：x喜歡yA1： ? x(

64、P(x)∧ ? y(D(y)→ L(x,y)))A2：？ B：？,歸結練習,P（x）：x是病人D（x）：x是醫(yī)生Q（x）：x是騙子L（x，y）：x喜歡yA1： ? x(P(x)∧ ? y(D(y)→ L(x,y)))A2：? x(P(x)→ ? y(Q(y)→ ?L(x,y)))B： ? x(D(x)→?Q(x))要證明B是A1和A2的邏輯結果，即公式A1 ∧A2 ∧?B是不可滿足的,歸結練習,A1= ? x(P(

65、x)∧ ? y(?D(y)→ L(x,y)))A2： ? x(P(x)→ ? y(Q(y)→ ?L(x,y)))B： ? x(D(x)→?Q(x))A1= ? x(P(x)∧ ? y(?D(y)→ L(x,y))) = ? x ? y(P(x)∧(?D(y)→ L(x,y)))---→ ? y(P(a)∧(?D(y)→ L(a,y)))A2=?B=A1 ∧A2 ∧?B的子句集是什么S=,歸結練習,A1= ?

66、x(P(x)∧ ? y(?D(y)∨L(x,y))) = ? x ? y(P(x)∧(?D(y)∨L(x,y))) ---→ ? y(P(a)∧(?D(y)∨L(a,y)))A2= ? ? x(P(x)→ ? y(?Q(y)∨?L(x,y))) = ? x(?P(x)∨ ? y(?Q(y)∨?L(x,y))) = ? x ? y (?P(x)∨?Q(y)∨?L(x,y))?B= ? (? x(D(x)

67、→?Q(x))) = ? x(?(?D(x)∨?Q(x))) ---→(D(b)∧Q(b))S={P(a), ? D(y)→ L(a,y), ?P(x)∨?Q(y)∨?L(x,y), D(b), Q(b)},歸結練習,S不可滿足的歸結演繹序列為：(1)P(a),(2) ?D(y)∨L(a,y),(3) ?P(x)∨?Q(y)∨?L(x,y),(4)D(b)(5)Q(b)(6) ?Q(y)∨?