Operační sémantika Operační a deklarativní sémantika Operační sémantikou logického programu P rozumíme množinu O(P) všech atomických formulí bez proměnných, které lze pro nějaký cíl g1 odvodit nějakým rezolučním důkazem ze vstupní množiny P u {g}. ^ímto výrazem jsou míněny všechny cíle, pro něž zmíněný rezoluční důkaz existuje. Deklarativní sémantika logického programu P ??? Opakování: interpretace Interpretace 1 jazyka £ je dána univerzem T> a zobrazením, které přiřadí konstantě c prvek T>, funkčnímu symbolu f In n-ární operaci v D a predikátovému symbolu pln n-ární relaci. ■ příklad: F = {{f (a, b) = f (b,a)}, {f (f (a, a), b) = a}} interpretace 'h: D = Z, a := 1, b := -1,/ := " + " Interpretace se nazývá modelem formule, je-li v ní tato formule pravdivá ■ interpretace množiny N s obvyklými operacemi je modelem formule ( 0 + s(0) = s(0)) Hana Rudová, Logické programování I, 9. dubna 201 3 Hana Rudová, Logické programování I, 9. dubna 2013 Sémantiky Herbrandovy interpretace Omezení na obor skládající se ze symbolických výrazů tvořených z predikátových a funkčních symbolů daného jazyka ■ při zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi Herbrandovo univerzum: množina všech termů bez proměnných, které mohou být tvořeny funkčními symboly a konstantami daného jazyka Herbrandova interpretace: libovolná interpretace, která přiřazuje ■ proměnným prvky Herbrandova univerza ■ konstantám sebe samé ■ funkčním symbolům funkce, které symbolu f pro argumenty ti, ■ ■ ■ , tn přiřadí term f(ti, ■■■ ,tn) ■ predikátovým symbolům libovolnou funkci z Herbrand. univerza do pravdivostních hodnot Herbrandův model množiny uzavřených formulí T: Herbrandova interpretace taková, že každá formule z P je v ní pravdivá. Hana Rudová, Logické programování I, 9. dubna 2013 Specifikace Herbrandova modelu Příklad: Herbrandovy interpretace Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant Pro specifikaci Herbrandovy interpretace tedy stačí zadat relace pro každý predikátový symbol Příklad: Herbrandova interpretace a Herbrandův model množiny formulí lichy(s(0)). % (1) lichyCs(sCX))) :- "lichy(X). % (2) 2i = 0 12 = {líchy(5(0))} % = {líchy (5(0)), líchy (5(5(5(0))))} 24 = {líchy(sn(0))\n e {1,3,5,7,...}} 25 = {líchy(sn(0))\n e N}} není model (1) není model (2) není model (2) Herbrandův model (1) i (2) Herbrandův model (1) i (2) Hana Rudová, Logické programování I, 9. dubna 201 3 5 Sémantiky Deklarativní a operační sémantika Je-li S množina programových klauzulí a M libovolná množina Herbrandových modelů S, pak průnik těchto modelů je opět Herbrandův model množiny S. Důsledek: Existuje nejmenší Herbrandův model množiny S, který značíme M(S). Deklarativní sémantikou logického programu P rozumíme jeho minimální Herbrandův model M(P). Připomenutí: Operační sémantikou logického programu P rozumíme množinu O(P) všech atomických formulí bez proměnných, které lze pro nějaký cíl g1 odvodit nějakým rezolučním důkazem ze vstupní množiny P u {Cj}. ^ímto výrazem jsou míněny všechny cíle, pro něž zmíněný rezoluční důkaz existuje. Pro libovolný logický program P platí M(P) = O(P) Hana Rudová, Logické programování I, 9. dubna 201 3 rodic(a,b). rodi c(b,c). predek(X,Y) :- rodic(X,Y). predek(X,Z) :- rodic(X,Y), predek(Y,Z). 1\ = {rodičia, b),rodíc(b, c), predekia, h), predek(b, c), predek(a, c)} 1z = {rodíc(a,b),rodíc(b,c), predekia, b), predekib, c), predekia, c), predekia, a)} 1\ i ?2 jsou Herbrandovy modely klauzulí Cvičení: Napište minimální Herbrandův model pro následující logický program. muz(petr). muz(pavel). zena(olga). zena(jitka). pary(X,Y) :- zena(X), muz(Y). Uveďte další model tohoto programu, který není minimální. Hana Rudová, Logické programování I, 9. dubna 2013 6 Séma SLD rezoluce v Prologu (pokračování) Výpočetní strategie SLD-rezoluce v Prologu: úplnost Korektní výpočetní strategie prohledávání stromu výpočtu musí zaručit, že se každý (konečný) výsledek nalézt v konečném čase Korektní výpočetní strategie = prohledávání stromu do šířky ■ exponenciální paměťová náročnost ■ složité řídící struktury Použitelná výpočetní strategie = prohledávání stromu do hloubky ■ jednoduché řídící struktury (zásobník) ■ lineární paměťová náročnost ■ není ale úplná: nenalezne vyvrácení i když existuje ■ procházení nekonečné větve stromu výpočtu => na nekonečných stromech dojde k zacyklení ■ nedostaneme se tak najiné existující úspěšné uzly Hana Rudová, Logické programování I, 9. dubna 201 3 SLD rezoluce v Prologu Test výskytu Kontrola, zda se proměnná vyskytuje v termu, kterým ji substituujeme ■ dotaz : -a(B,B). ■ logický program: a(X,f(X)). ■ by vedl k: [B/X], [X/f(X)] Unifikátorpro0(*i,...,*n) ag(f(X0,X0),f(X1,X1),...,f(Xn-1,Xn-1)) Xi=f(Xo,Xo), Xz = f(Xi,X\),..., Xn = f(Xn-i,Xn-i) X2=f(f(X0,Xo),f(X0,Xo)),... délka termu pro Xt exponenciálně narůstá => exponenciální složitost na ověření kontroly výskytu Test výskytu se při unifikaci v Prologu neprovádí Důsledek: ? - X = f(X) uspěje s X = /(/(/(/(/(/(/(/(/(/(...)))))))))) Hana Rudová, Logické programování I, 9. dubna 201 3 SLD rezoluce v Prologu Prolog: prohledávání stromu do hloubky => neúplnost použité výpočetní strategie Implementace SLD-rezoluce v Prologu ■ není úplná logický program: q : -r. (1) r:-q. (2) q. (3) dotaz: : -q. q. (3) □ Hana Rudová, Logické programování I, 9. dubna 201 3 SLD rezoluce v Prologu SLD-rezoluce v Prologu: korektnost Implementace SLD-rezoluce v Prologu nepoužívá při unifikaci test výskytu => není korektní (1) t(X) : -p(X,X). P(XJ(X)). (2) t:-p(X,X). P(XJ(X)). :-t(X). X = /(/(/(/(...)))))))))) problém se projeví yes dokazovací systém nehledá unifikátor pro X a f(X) Řešení: problém typu (2) převést na problém typu (1) ? ■ každá proměnná v hlavě klauzule se objeví i v těle, aby se vynutilo hledání unifikátoru (přidáme X = X pro každou X, která se vyskytuje pouze v hlavě) ř : -p(X,X). P(XJ(X)):-X = X. ■ optimalizace v kompilátoru mohou způsobit opět odpověď „yes" Hana Rudová, Logické programování I, 9. dubna 2013 SLD rezoluce v Prologu Řízení implementace: řez Příklad: řez orezaní ■ nemá ale žádnou deklarativní sémantiku ■ místo toho mění implementaci programu ■ p : -q,!, v. S ře^le^ňfeKríÚV^hová jako kterýkoliv jiný literál ■ pokud uspěji => přeskočím řez a pokračuji jako by tam řez nebyl ■ pokud ale neuspěji (a tedy i při backtrackingu) a vracím se přes řez => vracím se až na rodiče : -p. a zkouším další větev => nezkouším tedy další možnosti, jak splnit p upnutí => a nezkouším ani další možnosti, jak splnit q v SLD-stromu ořezání Hana Rudová, Logické programování I, 9. dubna 2013 SLD rezoluce v Prologu Příklad: řez II a(X):-b(X,Y),\,c(Y). (1) a(X) : -c(X). (2) fc(2,3). (3) b(l,2). (4) c(2). (5) s(X) : -a(X). (6) s(X):-p(X). (7) p(B) :-q(A,B),r(B). (8) p(A) :-q(A,A). (9) q(a,a). (10) q(a,b). (11) r(b). (12) Hana Rudová, Logické programování I, 9. dubna 201 3 [X/2.Y/3] (3). (1) b(X,Y),!,c(Y). V >,c(3). (rez) c(3). fail SLD rezoluce v Prologu ř : -p, r. t: -s. p : -q(X),\,v. p : -u, w. q(a). q(b). s. u. (D (2) (3) (4) (5) (6) (7) (8) [X/a] (i)/\^) :-p,r. :-s. Y X X' q(X),!,r,r. D (5) "\ !,v,r. (!) v, r. fail Hana Rudova, Logické programování I, 9. dubna 2013 SLD rezoluce v Prologu Příklad: řez a(X) : -b(X,Y),c(Y),\. a(X) : -c(X). fo(2,3). b(l,2). c(2). s(X) : -a(X). s(X) : -p(X). p(B) : -q(A,B),r(B). p (A) : -q(A,A). q(a, a). q(a, b). r(b). (1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11) (12) ' s(X). (1) b(X,Y),c(Y),!. [X/2.Y/3] (3) Hana Rudová, Logické programování I, 9. dubna 201 3 SLD rezoluce v Prologu Negativní znalost Negace v logickém programování logické programy vyjadřují pozitivní znalost negativní literály: pozice určena definicí Hornových klauzulí => nelze vyvodit negativní informaci z logického programu ■ každý predikát definuje úplnou relaci ■ negativní literál není logickým důsledkem programu relace vyjádřeny explicitně v nejmenším Herbrandově modelu ■ nad(X,Y) : -na(X,Y). na(c,b). nad(X, Y) : -na(X, Z),nad(Z, Y). na(b, a). ■ nej menší Herbrandúv model: {na(b, a),na(c, b),nad(b, a),nad(c,b),nad(c, a)} ani program ani model nezahrnují negativní informaci ■ a není nad c, a není na c ■ i v realitě je negativní informace vyjádřena explicitně zřídka, např. jízdní řád Předpoklad uzavřeného světa neexistence informace chápána jako opak: předpoklad uzavřeného světa (dosed world assumption, CWA) převzato z databází určitý vztah platí pouze když je vyvoditelný z programu. P if A „odvozovací pravidlo" (A je (uzavřený) term): ->A (CWA) pro SLD-rezoluci: P ý= nad(a, c), tedy lze podle CWA odvodit - 0, t\,..., tn jsou termy a Li,... ,Lm jsou literály. Pak označme E(C) výraz 3Yi,Yu(X\ = t\,... ,Xn = tn,L\,... ,Lm) kde Y\,..., ľk jsou všechny proměnné v C. Nechť de f (q In) = {Ci,..., C,}. Pak formuli l¥(q,P) získáme následujícím postupem: q(X1,...,Xn) : -E(Ci) VE(C2) v ■ ■ ■ v E(C,) pro j > 0a q(X\,... ,Xn) '■ - □ pro j = 0 [q/n není v programu P Hana Rudová, Logické programování I, 9. dubna 201 3 23 Negace v logickém programování Clarkova Teorie Rovnosti (CET) všechny formule jsou univerzálně kvantifikovány: 1. X = X 2. X=Y^Y = X 3. X=YaY = Z^X = Z 4. pro každý f/m: Xi = Yx A ■ ■ ■ A Xm = Ym - f(Xu ..., Xm) = f(Ylt..., Ym) 5. pro každý p/m: Xx = Yx A ■ ■ ■ A Xm = Ym - (p(Xlt...,Xm) - p(Ylt..., Ym)) 6. pro všechny různé f/m. a g/n, (m, n > 0): f(X\,... ,Xm) ± g(Y\,..., Yn) 7. pro každý f/m: f(X1,...,Xm) = f(Y1,...,Ym) —► X\ = Y\ /\ ■ ■ ■ /\ Xm = Ym 8. pro každý term ř obsahující X jako vlastní podterm: ř ^ X X ± Y je zkrácený zápis -<(X = Y) Hana Rudová, Logické programování I, 9. dubna 201 3 24 Negace v logickém programován Korektnost a úplnost NF pravidla Korektnost NF pravidla: Nechť P logický program a : -A cíl. Jestliže : -A má definitivně neúspěšný SLD-strom, pak V(-iA) je logickým důsledkem comp(P) (nebo-li comp(P) i= V(-iA)) Úplnost NF pravidla: Nechť P je logický program. Jestliže comp(P) i= V(-iA), pak existuje definitivně neúspěšný SLD-strom : -A. ■ zůstává problém: není rozhodnutelné, zda daná atomická formule je logickým důsledkem daného logického programu. ■ teorém mluví pouze o existenci definitivně neúspěšného SLD-stromu ■ definitivně (konečně) neúspěšný SLD-strom sice existuje, ale nemusíme ho nalézt ■ např. v Prologu: může existovat konečné odvození, ale program přesto cyklí (Prolog nenajde definitivně neúspěšný strom) Odvození pomocí NF pouze test, nelze konstruovat výslednou substituci ■ v (comp(P) i= V(-vl)) je A všeob. kvantifikováno, v V(-vl) nejsou volné proměnné Hana Rudová, Logické programování I, 9. dubna 201 3 Negace v logickém programování Normální a stratifikované programy normální program: obsahuje negativní literály v pravidlech problém: existence zúplnění, která nemají žádný model ■ p : -->p. zúplnění: p «- -ip rozdělení programu na vrstvy ■ vynucují použití negace relace pouze tehdy pokud je relace úplně definovaná a. a: --li?, a. b. a. a: --ifc, a. b : --ifl. stratifikovaný není stratifikovaný normální program P je stratifikovaný: množina predikátových symbolů programu lze rozdělit do disjunktních množin So,...,Sm (Si = stratům) ■ p(...):-..., q(...),... e P, p e Sk => q e S0 u ... u Sk ■ p(...):-..., -. q e S0 u ... u Sk-i Hana Rudová, Logické programování I, 9. dubna 201 3 Negace v logickém programován Stratifikované programy II program je m-stratifikovaný m je nejmenší index takový, že So u ... u Sm je množina všech predikátových symbolů z P Věta: Zúplnění každého stratifikovaného programu má Herbrandův model. ■ p :--ip. nemá Herbrandův model ■ p : --ip. ale není stratifikovaný stratifikované programy nemusí mít jedinečný minimální Herbrandův model ■ cyklí: -^zastaví. ■ dva minimální Herbrandovy modely: {cyklí}, {zastaví} ■ důsledek toho, že cyklí: -^zastaví, je ekvivalentní cyklí v zastaví Hana Rudová, Logické programování I, 9. dubna 201 3 27 Negace v logickém programování SLDNF rezoluce: úspěšné odvození ■ NF pravidlo: : - C. má konečně neúspěšný SLD-strom ■ Pokud máme negativní podcíl - úspěšné odvození Hana Rudová, Logické programování I, 9. dubna 201 3 28 Negace v logickém programován SLDNF rezoluce: neúspěšné odvození ■ NF pravidlo: :-C. má konečně neúspěšný SLD-strom ■ Pokud máme negativní podcíl - neúspěšné odvození Hana Rudová, Logické programování I, 9. dubna 201 3 29 Negace v logickém programování Cvičení: SLDNF odvození Napište množinu SLDNF odvození pro uvedený dotaz. :- a(B). a(X) :- b(X), \+ c(X). a(X) :- d(X), Y is X+l, \+ c(Y), b(X). b(l). c(A) :- d(A). d(l). Hana Rudová, Logické programování I, 9. dubna 201 3 31 Negace v logickém programování SLDNF rezoluce: uvázlé odvození ■ NF pravidlo: : - C. má konečně neúspěšný SLD-strom ■ Pokud máme negativní podcíl - uvázlé odvození Hana Rudová, Logické programování I, 9. dubna 201 3 30 Negace v logickém programování SLD+ odvození ■ P je normální program, Go normální cíl, R selekční pravidlo: SLD+-odvození Go je buď konečná posloupnost (Go; Co),..., (Gj-i; Cí-i), Gi nebo nekonečná posloupnost ,,,... kde v každém kroku m + l(m > 0), R vybírá pozitivní literál v Gm a dospívá k Gm+\ obvyklým způsobem. ■ konečné SLD+-odvození může být: 1. úspěšné: Gi = □ 2. neúspěšné 3. blokované: Gi je negativní (např. -^A) Hana Rudová, Logické programování I, 9. dubna 201 3 32 Negace v logickém programování SLDNF rezoluce: pojmy ■ Úroveň cíle ■ P normální program, Go normální cíl, R selekční pravidlo: úroveň cíle Go se rovná ■ 0 žádné SLD+-odvození s pravidlem R není blokováno ■ k + 1 maximální úroveň cílů : -A, které ve tvaru -,..., (Gi, e), (: - L\,... ,Lm-i,Lm+i, ...,Ln) je (úspěšné) SLDNF odvození cíle Go ■ e označuje prázdnou cílovou substituci Hana Rudová, Logické programování I, 9. dubna 201 3 34 Negace v logickém programování Korektnost a úplnost SLDNF odvození ■ korektnost SLDNF-odvození: P normální program, : -G normální cíl a R je selekční pravidlo: je-li 9 cílová substituce SLDNF-odvození cíle : -G, pak G9 je logickým důsledkem comp(P) ■ implementace SLDNF v Prologu není korektní ■ Prolog neřeší uvázlé SLDNF-odvození (neprázdná substituce) ■ použití bezpečných cílů (negace neobsahuje proměnné) ■ úplnost SLDNF-odvození: SLDNF-odvození není úplné ■ pokud existuje konečný neúspěšný strom : -A, pak -iA platí ale místo toho se odvozování: -A může zacyklit, tj. SLDNF rezoluce -iA neodvodí => -iA tedy sice platí, ale SLDNF rezoluce ho nedokáže odvodit Hana Rudová, Logické programování I, 9. dubna 2013 35 Negace v logickém programování Hana Rudová, Logické programování I, 9. dubna 2013 36 Negace v logickém programování