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, 16. dubna 2007 Hana Rudová, Logické programování I, 16. dubna 2007 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, 16. dubna 2007 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) rodic(a,b). rodi c(b,c). predek(X,Y) predek(X,Z) rodic(X,Y). rodic(X,Y), predek(Y,Z). 1\ = {rodíc(a, b),rodíc(b, c), predek(a, b), predek(b, c), predek(a, c)} ?2 = {rodíc(a,b),rodíc(b,c), predek(a, b), predekib, c), predekia, c), predekia, a)} 1\ i ?2 jsou Herbrandovy modely klauzulí Hana Rudová, Logické programování I, 16. dubna 2007 Hana Rudová, Logické programování I, 16. dubna 2007 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). 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) Negace v logickém programování Hana Rudová, Logické programování I, 16. dubna 2007 Negativní znalost 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 Hana Rudová, Logické programování I, 16. dubna 2007 Negace v logickém programování Negace jako neúspěch (negation as failure) slabší verze CWA: definitivně neúspěšný (finitely failed) SLD-strom cíle : -A : -A má definitivně (konečně) neúspěšný SLD-strom ->A (negation as failure, IMF normální cíl: cíl obsahující i negativní literály ■ : -nad(c,a), -inad(b,c). rozdíl mezi CWA a NF ■program nad(X, Y) : -nad(X,Y), cíl :--inad(b,c) ■ neexistuje odvození cíle podle NF, protože SLD-strom : -nad(b, c) je nekonečný ■ existuje odvození cíle podle CWA, protože neexistuje vyvrácení: -nad(b,c) CWA i NF jsou nekorektní: A není logickým důsledkem programu P řešení: definovat programy tak, aby jejich důsledkem byly i negativní literály zúplnění logického programu Hana Rudová, Logické programování I, 16. dubna 2007 Negace v logickém programování 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. „odvozovací pravidlo" (A je (uzavřený) term): P if A ->A (CWA) pro SLD-rezoluci: P ý= nad(a, c), tedy lze podle CWA odvodit - 0): f(X\,.. .,Xm) ± giXi, ■ ■ ■, Yn) 7. pro každý f/m: f(Xu...,Xm) = f(Yu...,Ym) - Xi = Yi A ■ ■ ■ A 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, 16. dubna 2007 Negace v logickém programování na(X1,X2) ■ -3Y(X1 = c,X2 = b,f(Y)) v (X1 = b,X2 = a,g). q/n predikátový symbol programu P na(c,b):-f(Y). na(b,a):-g. Xi,...,Xn jsou „nové" proměnné, které se nevyskytují nikde v P Nechť C je klauzule ve tvaru q(t\,..., tn) : -Li,..., Lm kde m > 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/n) = {Ci,...,C„}. Pak formuli l¥(q,P) získáme následujícím postupem: q(Xi,...,Xn) : -E(Ci) VE(C2) v ■ ■ ■ vE(Q) pro j > 0a q(X\,.. .,Xn) : - □ pro j = 0 [q/n není v programu P Hana Rudová, Logické programování I, 16. dubna 2007 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, 16. dubna 2007 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. a: — ^b,a. a: —^b,a. b. b : --ia. stratifi kovaný není stratifi kovaný ■ 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(...) : - (...), ... e P, p e Sk => q e S0 u ... u Sk-i Hana Rudová, Logické programování I, 16. dubna 2007 1 7 Negace v logickém programování Stratifi kované 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 :-~ úspěšné odvození Hana Rudová, Logické programování I, 16. dubna 2007 1 9 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, 16. dubna 2007 20 Negace v logickém programování SLDNF rezoluce: uvázlé odvození SLD+ 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, 16. dubna 2007 Negace v logickém programování 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ř. - -iA tedy sice platí, ale SLDNF rezoluce ho nedokáže odvodit Hana Rudová, Logické programování I, 16. dubna 2007 25 Negace v logickém programování Hana Rudová, Logické programování I, 16. dubna 2007 26 Negace v logickém programování