Technika a styl programování v Prologu Technika a styl programování v Prologu M Styl programování v Prologu 3 některá pravidla správného stylu 3 správný vs. špatný styl komentáře Ladění Efektivita Hana Rudová, Logické programování 1,21. března 201 2 2 Technika a styl programování v Prologu Styl programování v Prologu I. Cílem stylistických konvencí je m redukce nebezpečí programovacích chyb 3 psaní čitelných a srozumitelných programů, které se dobře ladí a modifikují Hana Rudová, Logické programování 1,21. března 201 2 3 Technika a styl programování v Prologu Styl programování v Prologu I. Cílem stylistických konvencí je m redukce nebezpečí programovacích chyb m psaní čitelných a srozumitelných programů, které se dobře ladí a modifikují M Některá pravidla správného stylu m krátké klauzule 3 krátké procedury; dlouhé procedury pouze s uniformní strukturou (tabulka) Hana Rudová, Logické programování 1,21. března 201 2 3 Technika a styl programování v Prologu Styl programování v Prologu I. Cílem stylistických konvencí je m redukce nebezpečí programovacích chyb 3 psaní čitelných a srozumitelných programů, které se dobře ladí a modifikují M Některá pravidla správného stylu 3 krátké klauzule 3 krátké procedury; dlouhé procedury pouze s uniformní strukturou (tabulka) 3 klauzule se základními (hraničními) případy psát před rekurzivními klauzulemi 3 vhodná jména procedur a proměnných St nepoužívat seznamy ([. . .]) nebo závorky ({...}, (...)) pro termy pevné arity 3 vstupní argumenty psát před výstupními Hana Rudová, Logické programování 1,21. března 201 2 3 Technika a styl programování v Prologu Styl programování v Prologu I. Cílem stylistických konvencí je m redukce nebezpečí programovacích chyb m psaní čitelných a srozumitelných programů, které se dobře ladí a modifikují M Některá pravidla správného stylu m krátké klauzule 3 krátké procedury; dlouhé procedury pouze s uniformní strukturou (tabulka) m klauzule se základními (hraničními) případy psát před rekurzivními klauzulemi 3 vhodná jména procedur a proměnných St nepoužívat seznamy ([. . .]) nebo závorky ({...}, (...)) pro termy pevné arity 3 vstupní argumenty psát před výstupními m struktura programu - jednotné konvence v rámci celého programu, např. & mezery, prázdné řádky, odsazení S klauzule stejné procedury na jednom místě; prázdné řádky mezi klauzulemi; každý cíl na zvláštním řádku Hana Rudová, Logické programování I, 21. března 201 2 3 Technika a styl programování v Prologu Správný styl programování konstrukce setříděného seznamu Seznam3 ze setříděných seznamů Seznámí, Seznam2: merge( Seznámí, Seznam2, Seznam3 ) mergeC [2,4,7], [1,3,4,8], [1,2,3,4,4,7,8] ) Hana Rudová, Logické programování 1,21. března 201 2 4 Technika a styl programování v Prologu Správný styl programování konstrukce setříděného seznamu Seznam3 ze setříděných seznamů Seznámí, Seznam2: merge( Seznámí, Seznam2, Seznam3 ) 3 mergeC [2,4,7], [1,3,4,8], [1,2,3,4,4,7,8] ) merge( [], Seznam, Seznam ) :- Hana Rudová, Logické programování 1,21. března 201 2 4 Technika a styl programování v Prologu Správný styl programování M konstrukce setříděného seznamu Seznam3 ze setříděných seznamů Seznámí, Seznam2: merge( Seznámí, Seznam2, Seznam3 ) 3 mergeC [2,4,7], [1,3,4,8], [1,2,3,4,4,7,8] ) M merge( [], Seznam, Seznam ) :- ! . % prevence redundantních řešení Hana Rudová, Logické programování 1,21. března 201 2 4 Technika a styl programování v Prologu Správný styl programování M konstrukce setříděného seznamu Seznam3 ze setříděných seznamů Seznámí, Seznam2: merge( Seznámí, Seznam2, Seznam3 ) 3 mergeC [2,4,7], [1,3,4,8], [1,2,3,4,4,7,8] ) M merge( [], Seznam, Seznam ) :- ! . % prevence redundantních řešení merge( Seznam, [], Seznam ). Hana Rudová, Logické programování 1,21. března 201 2 4 Technika a styl programování v Prologu Správný styl programování M konstrukce setříděného seznamu Seznam3 ze setříděných seznamů Seznámí, Seznam2: merge( Seznámí, Seznam2, Seznam3 ) 3 mergeC [2,4,7], [1,3,4,8], [1,2,3,4,4,7,8] ) merge( [], Seznam, Seznam ) :- ! . % prevence redundantních řešení merge( Seznam, [], Seznam ). merge( [X|Telol], [Y|Telo2], [X|Telo3] ) :- Hana Rudová, Logické programování 1,21. března 201 2 4 Technika a styl programování v Prologu Správný styl programování konstrukce setříděného seznamu Seznam3 ze setříděných seznamů Seznámí, Seznam2: merge( Seznámí, Seznam2, Seznam3 ) 3 mergeC [2,4,7], [1,3,4,8], [1,2,3,4,4,7,8] ) merge( [], Seznam, Seznam ) :- ! . % prevence redundantních řešení merge( Seznam, [], Seznam ). merge( [X|Telol], [Y|Telo2], [X|Telo3] ) :-X < Y, !, Hana Rudová, Logické programování 1,21. března 201 2 4 Technika a styl programování v Prologu Správný styl programování konstrukce setříděného seznamu Seznam3 ze setříděných seznamů Seznámí, Seznam2: merge( Seznámí, Seznam2, Seznam3 ) 3 mergeC [2,4,7], [1,3,4,8], [1,2,3,4,4,7,8] ) M merge( [], Seznam, Seznam ) :- ! . % prevence redundantních řešení merge( Seznam, [], Seznam ). merge( [X|Telol], [Y|Telo2], [X|Telo3] ) :-X < Y, !, merge( Telol, [Y|Telo2], Telo3 ). Hana Rudová, Logické programování 1,21. března 201 2 4 Technika a styl programování v Prologu Správný styl programování konstrukce setříděného seznamu Seznam3 ze setříděných seznamů Seznámí, Seznam2: merge( Seznámí, Seznam2, Seznam3 ) merge( [2,4,7], [1,3,4,8], [1,2,3,4,4,7,8] ) merge( [], Seznam, Seznam ) :- ! . % prevence redundantních řešení merge( Seznam, [], Seznam ). merge( [X|Telol], [Y|Telo2], [X|Telo3] ) :-X < Y, !, merge( Telol, [Y|Telo2], Telo3 ). merge( Seznámí, [Y|Telo2], [Y|Telo3] ) :- Hana Rudová, Logické programování 1,21. března 201 2 4 Technika a styl programování v Prologu Správný styl programování konstrukce setříděného seznamu Seznam3 ze setříděných seznamů Seznámí, Seznam2: merge( Seznámí, Seznam2, Seznam3 ) 3 merge( [2,4,7], [1,3,4,8], [1,2,3,4,4,7,8] ) merge( □ , Seznam, Seznam ) :- ! . % prevence redundantních řešení merge( Seznam, [], Seznam ). merge( [X|Telol], [Y|Telo2], [X|Telo3] ) :-X < Y, !, merge( Telol, [Y|Telo2], Telo3 ). merge( Seznámí, [Y|Telo2], [Y|Telo3] ) :-merge( Seznámí, Telo2, Telo3 ). Hana Rudová, Logické programování 1,21. března 201 2 4 Technika a styl programování v Prologu Špatný styl programování merge( SI, S2, S3 ) :- 51 =[],!, S3 = S2; % první seznam je prázdný 52 = [] , ! , S3 = SI; % druhý seznam je prázdný 51 = [X|TI], 52 = [Y|T2], C X < Y, ! , Z = X, % Z je hlava seznamu S3 merge( TI, S2, T3 ) ; Z = Y, merge( SI, T2, T3) ), 53 = [ Z | T3 ]. Hana Rudová, Logické programování 1,21. března 201 2 5 Technika a styl programování v Prologu Styl programování v Prologu II. M Středník „;" může způsobit nesrozumitelnost klauzule m nedávat středník na konec řádku, používat závorky 3 v některých případech: rozdělení klauzle se středníkem do více klauzulí Hana Rudová, Logické programování 1,21. března 201 2 6 Technika a styl programování v Prologu Styl programování v Prologu II M Středník „;" může způsobit nesrozumitelnost klauzule 3 nedávat středník na konec řádku, používat závorky 3 v některých případech: rozdělení klauzle se středníkem do více klauzulí M Opatrné používání operátoru řezu 3 preferovat použití zeleného řezu (nemění deklarativní sémantiku) 3 červený řez používat v jasně definovaných konstruktech negace: P, !, fail; true alternativy: Podminka, !, Cill ; Ci 12 Podminka -> Cill Cil 2 \+ P Hana Rudová, Logické programování 1,21. března 201 2 6 Technika a styl programování v Prologu Styl programování v Prologu II M Středník „;" může způsobit nesrozumitelnost klauzule m nedávat středník na konec řádku, používat závorky 3 v některých případech: rozdělení klauzle se středníkem do více klauzulí M Opatrné používání operátoru řezu 3 preferovat použití zeleného řezu (nemění deklarativní sémantiku) m červený řez používat v jasně definovaných konstruktech M Opatrné používání negace „\+" m negace jako neúspěch: negace není ekvivalentní negaci v matematické logice negace: P, !, fail; true alternativy: Podminka, !, Cill ; Ci 12 Podminka -> Cill Cil 2 \+ P Hana Rudová, Logické programování 1,21. března 201 2 6 Technika a styl programování v Prologu Styl programování v Prologu II M Středník „;" může způsobit nesrozumitelnost klauzule m nedávat středník na konec řádku, používat závorky 3 v některých případech: rozdělení klauzle se středníkem do více klauzulí M Opatrné používání operátoru řezu 3 preferovat použití zeleného řezu (nemění deklarativní sémantiku) m červený řez používat v jasně definovaných konstruktech M Opatrné používání negace „\+" m negace jako neúspěch: negace není ekvivalentní negaci v matematické logice Pozor na assert a retract: snižuji transparentnost chování programu negace: P, !, fail; true alternativy: Podminka, !, Cill ; Ci 12 Podminka -> Cill Cil 2 \+ P Hana Rudová, Logické programování 1,21. března 201 2 6 Technika a styl programování v Prologu Dokumentace a komentáře M co program dělá, jak ho používat (jaký cíl spustit a jaké jsou očekávané výsledky), příklad použití Hana Rudová, Logické programování 1,21. března 201 2 7 Technika a styl programování v Prologu Dokumentace a komentáře co program dělá, jak ho používat (jaký cíl spustit a jaké jsou očekávané výsledky), příklad použití které predikáty jsou hlavní (top-level) Hana Rudová, Logické programování 1,21. března 201 2 7 Technika a styl programování v Prologu Dokumentace a komentáře co program dělá, jak ho používat (jaký cíl spustit a jaké jsou očekávané výsledky), příklad použití 3 které predikáty jsou hlavní (top-level) 3 jak jsou hlavní koncepty (objekty) reprezentovány Hana Rudová, Logické programování 1,21. března 201 2 7 Technika a styl programování v Prologu Dokumentace a komentáře 3 co program dělá, jak ho používat (jaký cíl spustit a jaké jsou očekávané výsledky), příklad použití které predikáty jsou hlavní (top-level) 3 jak jsou hlavní koncepty (objekty) reprezentovány doba výpočtu a paměťové nároky Hana Rudová, Logické programování 1,21. března 201 2 7 Technika a styl programování v Prologu Dokumentace a komentáře M co program dělá, jak ho používat (jaký cíl spustit a jaké jsou očekávané výsledky), příklad použití M které predikáty jsou hlavní (top-level) M jak jsou hlavní koncepty (objekty) reprezentovány M doba výpočtu a paměťové nároky jaké jsou limitace programu Hana Rudová, Logické programování 1,21. března 201 2 7 Technika a styl programování v Prologu Dokumentace a komentáře M co program dělá, jak ho používat (jaký cíl spustit a jaké jsou očekávané výsledky), příklad použití M které predikáty jsou hlavní (top-level) 3 jak jsou hlavní koncepty (objekty) reprezentovány M doba výpočtu a paměťové nároky jaké jsou limitace programu 3 zda jsou použity nějaké speciální rysy závislé na systému Hana Rudová, Logické programování 1,21. března 201 2 7 Technika a styl programování v Prologu Dokumentace a komentáře M co program dělá, jak ho používat (jaký cíl spustit a jaké jsou očekávané výsledky), příklad použití M které predikáty jsou hlavní (top-level) M jak jsou hlavní koncepty (objekty) reprezentovány M doba výpočtu a paměťové nároky jaké jsou limitace programu M zda jsou použity nějaké speciální rysy závislé na systému jaký je význam predikátů v programu, jaké jsou jejich argumenty, které jsou vstupní a které výstupní (pokud víme) 3 vstupní argumenty „+", výstupní „-" merge( +Seznaml, +Seznam2 , -Seznam3 ) 3 JmenoPredikatu/Arita merge/3 Hana Rudová, Logické programování 1,21. března 201 2 7 Technika a styl programování v Prologu Dokumentace a komentáře co program dělá, jak ho používat (jaký cíl spustit a jaké jsou očekávané výsledky), příklad použití 3 které predikáty jsou hlavní (top-level) M jak jsou hlavní koncepty (objekty) reprezentovány M doba výpočtu a paměťové nároky 3 jaké jsou limitace programu zda jsou použity nějaké speciální rysy závislé na systému jaký je význam predikátů v programu, jaké jsou jejich argumenty, které jsou vstupní a které výstupní (pokud víme) 3 vstupní argumenty „+", výstupní „-" merge( +Seznaml, +Seznam2 , -Seznam3 ) m JmenoPredikatu/Arita merge/3 M algoritmické a implementační podrobnosti Hana Rudová, Logické programování I, 21. března 201 2 7 Technika a styl programování v Prologu Ladění Přepínače na trasování: trace/0, notrace/0 Trasování specifického predikátu: spy/1, nospy/1 3 spy( merge/3 ) 3 debug/0, nodebug/0: pro trasování pouze predikátů zadaných spy/1 Hana Rudová, Logické programování 1,21. března 201 2 8 Technika a styl programování v Prologu Ladění M Přepínače na trasování: trace/0, notrace/0 Trasování specifického predikátu: spy/1, nospy/1 3 spy( merge/3 ) debug/0, nodebug/0: pro trasování pouze predikátů zadaných spy/1 M Libovolná část programu může být spuštěna zadáním vhodného dotazu: trasování cíle 3 vstupní informace: jméno predikátu, hodnoty argumentů při volání 3 výstupní informace 3 při úspěchu hodnoty argumentů splňující cíl 3 při neúspěchu indikace chyby 3 nové vyvolání přes stejný cíl je volán při backtrackingu Hana Rudová, Logické programování 1,21. března 201 2 8 Technika a styl programování v Prologu Krabičkový (4-branový) model 3 Vizualizace řídícího toku (backtrackingu) na úrovni predikátu 3 Cal 1: volání cíle 3 Exit: úspěšné ukončení volání cíle 3 Fai 1: volání cíle neuspělo 3 Redo: jeden z následujících cílů neuspěl a systém backtrackuje, aby nalezl alternativy k předchozímu řešení Call Exit > + predek( X, Z ) :- rodic( X, Z ). + > < I predekC X, Z ) :- rodic( X, Y ), + predek( Y, Z ). + < Fail Redo Hana Rudová, Logické programování 1,21. března 201 2 9 Technika a styl programování v Prologu Příklad: trasování a(X) :- nonvar(X). a(X) :- c(X). a(X) :- d(X). cd). d(2). Call I ------> + a(X) I a(X) <------+ a(X) Fail I Exi t nonvar(X).| ------> c(X). I d(X). + <------ Redo Hana Rudová, Logické programování 1,21. března 201 2 10 Technika a styl programování v Prologu Příklad: trasování a(X) :- nonvar(X). 1 ?- a(X). a(X) :- c(X). 1 1 Call : a(_463) ? a(X) :- d(X). 2 2 Call : nonvar(_463) cd). 2 2 Fai 1 : nonvar(_463) d(2). Call I ------> + a(X) I a(X) <------+ a(X) Fail I Exi t nonvar(X).| ------> c(X). I d(X). + <------ Redo Hana Rudová, Logické programování 1,21. března 201 2 10 Technika a styl programování v Prologu Příklad: trasování a(X) a(X) a(X) c(l). d(2). - nonvar(X) - c(X). - d(X). Call I ------> + a(X) I a(X) <------+ a(X) Fai 1 I I Exi t nonvar(X).| ------> c(X). I d(X). + <------ I Redo a(X) ? X 1 1 Call a(_463) ? 2 2 Call nonvar (_ _463) ? 2 2 Fail nonvarC _463) ? 3 2 Call c(_463) ? 3 2 Exit c(l) ? 1 1 Exit a(l) ? = 1 ? Hana Rudová, Logické programování 1,21. března 201 2 10 Technika a styl programování v Prologu Příklad: trasování a(X) a(X) a(X) c(l). d(2). - nonvar(X) - c(X). - d(X). Call I ------> + a(X) I a(X) <------+ a(X) Fai 1 I I Exi t nonvar(X).| ------> c(X). I d(X). + <------ I Redo a(X) ? X = 1 ? 1 1 Call a(_463) 7 2 2 Call nonvarC _463) ? 2 2 Fail nonvarC _463) ? 3 2 Call c(_463) ? 3 2 Exit : c(l) ? 1 1 Exit : a(l) ? 1 1 Redo : a(l) ? 4 2 Call : d(_463) 7 Hana Rudová, Logické programování 1,21. března 201 2 10 Technika a styl programování v Prologu Příklad: trasování a(X) :- nonvar(X). a(X) :- c(X). a(X) :- d(X). c(l). d(2). Cal1 I I ------> + a(x) :- nonvar(X).| I a(X) :- c(X). I <------+ a(X) :- d(X). + Fail I I 1 ?- a(X). 1 1 Call : 2 2 Call : 2 2 Fail : 3 2 Call : 3 2 Exi t: ? 1 1 Exi t: Exit X = 1 ? ; ------> 1 1 Redo: 4 2 Call : <------ 4 2 Exi t: Redo 1 1 Exi t: X = 2 ? ; no % trace a(_463) ? nonvar(_463) ? nonvar(_463) ? c(_463) ? c(D ? a(l) ? a(l) ? d(_463) ? d(2) ? a(2) ? Hana Rudová, Logické programování 1,21. března 201 2 10 Technika a styl programování v Prologu Efektivita Čas výpočtu, paměťové nároky, a také časové nároky na vývoj programu m u Prologu můžeme častěji narazit na problémy s časem výpočtu a pamětí m Prologovské aplikace redukují čas na vývoj 3 vhodnost pro symbolické, nenumerické výpočty se strukturovanými objekty a relacemi mezi nimi Hana Rudová, Logické programování 1,21. března 201 2 Technika a styl programování v Prologu Efektivita Čas výpočtu, paměťové nároky, a také časové nároky na vývoj programu m u Prologu můžeme častěji narazit na problémy s časem výpočtu a pamětí m Prologovské aplikace redukují čas na vývoj 3 vhodnost pro symbolické, nenumerické výpočty se strukturovanými objekty a relacemi mezi nimi Pro zvýšení efektivity je nutno se zabývat procedurálními aspekty m zlepšení efektivity při prohledávání odstranění zbytečného backtrackingu i- zrušení provádění zbytečných alternativ co nejdříve návrh vhodnějších datových struktur, které umožní efektivnější operace s objekty Hana Rudová, Logické programování 1,21. března 201 2 Technika a styl programování v Prologu Zlepšení efektivity: základní techniky -0 Optimalizace posledního volání (LCO) a akumulátory Rozdílové seznamy při spojování seznamů M Caching: uložení vypočítaných výsledků do programové databáze Hana Rudová, Logické programování 1,21. března 201 2 12 Technika a styl programování v Prologu Zlepšení efektivity: základní techniky M Optimalizace posledního volání (LCO) a akumulátory Rozdílové seznamy při spojování seznamů M Caching: uložení vypočítaných výsledků do programové databáze M Indexace podle prvního argumentu 3 např. v SICStus Prologu m při volání predikátu s prvním nainstaniovaným argumentem se používá hašovací tabulka zpřístupňující pouze odpovídající klauzule 3 zamestnanec( Prijmem', KrestniJméno, Odděleni, ...) & seznamy( [], ...) :- ... . seznamy( [H|T], ...) :- ... . Hana Rudová, Logické programování 1,21. března 201 2 12 Technika a styl programování v Prologu Zlepšení efektivity: základní techniky M Optimalizace posledního volání (LCO) a akumulátory Rozdílové seznamy při spojování seznamů M Caching: uložení vypočítaných výsledků do programové databáze M Indexace podle prvního argumentu 3 např. v SICStus Prologu m při volání predikátu s prvním nainstaniovaným argumentem se používá hašovací tabulka zpřístupňující pouze odpovídající klauzule 3 zamestnanec( Prijmem', KrestniJméno, Odděleni, ...) & seznamy( [], ...) :- ... . seznamy( [H|T], ...) :- ... . -0 Determinismus: 3 rozhodnout, které klauzule mají uspět vícekrát, ověřit požadovaný determinismus Hana Rudová, Logické programování I, 21. března 201 2 12 Technika a styl programování v Prologu Predikátová logika l.řádu Teorie logického programování PROLOG: PROgramming in LOGic, část predikátové logiky 1 .řádu fakta: rodi c(petr, petri k), VXa(X) m klauzule: VXVY rodic(X,Y) => predek(X,Y) Hana Rudová, Logické programování 1,21. března 201 2 14 Teorie logického programování Teorie logického programování M PROLOG: PROgramming in LOGic, část predikátové logiky 1 .řádu 3 fakta: rodi c(petr, petri k), VXa(X) m klauzule: VXVY rodic(X,Y) => predek(X,Y) M Predikátová logika I. řádu (PLI) 3 soubory objektů: lidé, čísla, body prostoru, ... 3 syntaxe PL1, sémantika PL1, pravdivost a dokazatelnost Hana Rudová, Logické programování 1,21. března 201 2 14 Teorie logického programování Teorie logického programování M PROLOG: PROgramming in LOGic, část predikátové logiky 1 .řádu m fakta: rodi c(petr, petri k), VXa(X) * klauzule: VXVY rodic(X,Y) => predek(X,Y) M Predikátová logika I. řádu (PL1) 3 soubory objektů: lidé, čísla, body prostoru, ... m syntaxe PL1, sémantika PL1, pravdivost a dokazatelnost M Rezoluce ve výrokové logice, v PL1 m dokazovací metoda M Rezoluce v logickém programování M Backtracking, řez, negace vs. rezoluce Hana Rudová, Logické programování 1,21. března 201 2 14 Teorie logického programování Predikátová logika I. řádu (PLI) Abeceda J4. jazyka L PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru Hana Rudová, Logické programování 1,21. března 201 2 Predikátová logika Predikátová logika I. řádu (PLI) Abeceda JA jazyka £ PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru funkční symboly f, g, ... označují operace (příklad: +, x ) 3 arita = počet argumentů, n-ární symbol, značíme f/n 3 nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0, 1, ...) Hana Rudová, Logické programování 1,21. března 201 2 Predikátová logika Predikátová logika I. řádu (PLI) Abeceda JA jazyka £ PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru funkční symboly f, g, ... označují operace (příklad: +, x ) m arita = počet argumentů, n-ární symbol, značíme f/n 3 nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0, 1, ...) M predikátové symboly p,q, ... pro vyjádření vlastností a vztahů mezi objekty m arita = počet argumentů, n-ární symbol, značíme p/n příklad: <, e Hana Rudová, Logické programování 1,21. března 201 2 Predikátová logika Predikátová logika I. řádu (PLI) Abeceda JA jazyka £ PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru funkční symboly f, g, ... označují operace (příklad: +, x ) 3 arita = počet argumentů, n-ární symbol, značíme f/n 3 nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0, 1, ...) M predikátové symboly p,q, ... pro vyjádření vlastností a vztahů mezi objekty 3 arita = počet argumentů, n-ární symbol, značíme p/n příklad: <, e logické spojky a, v, -i, =>, = Hana Rudová, Logické programování 1,21. března 201 2 Predikátová logika Predikátová logika I. řádu (PLI) Abeceda JA jazyka £ PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru funkční symboly f, g, ... označují operace (příklad: +, x ) m arita = počet argumentů, n-ární symbol, značíme f/n 3 nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0, 1, ...) M predikátové symboly p,q, ... pro vyjádření vlastností a vztahů mezi objekty m arita = počet argumentů, n-ární symbol, značíme p/n příklad: <, e logické spojky a, v, -i, =>, = kvantifikátory V, 3 3 logika I. řádu používá kvantifikaci pouze pro individua (odlišnost od logik vyššího řádu) 3 v logice 1. řádu nelze: v R : VA <= R, V/ : R - R Hana Rudová, Logické programování 1,21. března 201 2 Predikátová logika Predikátová logika I. řádu (PLI) Abeceda JA jazyka £ PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru funkční symboly f, g, ... označují operace (příklad: +, x ) m arita = počet argumentů, n-ární symbol, značíme f/n 3 nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0, 1, ...) M predikátové symboly p,q, ... pro vyjádření vlastností a vztahů mezi objekty m arita = počet argumentů, n-ární symbol, značíme p/n příklad: <, e logické spojky a, v, -i, =>, = kvantifikátory V, 3 3 logika I. řádu používá kvantifikaci pouze pro individua (odlišnost od logik vyššího řádu) ^ v logice 1. řádu nelze: v R : VA <= R, V/ : R - R závorky: ),( Hana Rudová, Logické programování 1,21. března 2012 15 Predikátová logika Jazyky PL1 M Specifikace jazyka L je definována funkčními a predikátovými symboly symboly tedy určují oblast, kterou jazyk popisuje M Jazyky s rovností: obsahují predikátový symbol pro rovnost „=" Hana Rudová, Logické programování 1,21. března 201 2 16 Predikátová logika Jazyky PLI M Specifikace jazyka L je definována funkčními a predikátovými symboly symboly tedy určují oblast, kterou jazyk popisuje Jazyky s rovností: obsahují predikátový symbol pro rovnost „=" Příklady M jazyk teorie uspořádání 3 jazyk s =, binární prediátový symbol < Hana Rudová, Logické programování 1,21. března 201 2 16 Predikátová logika Jazyky PLI Specifikace jazyka L je definována funkčními a predikátovými symboly symboly tedy určují oblast, kterou jazyk popisuje 3 Jazyky s rovností: obsahují predikátový symbol pro rovnost „=" Příklady 3 jazyk teorie uspořádání 3 jazyk s =, binární prediátový symbol < jazyk teorie množin m jazyk s =, binární predikátový symbol e Hana Rudová, Logické programování 1,21. března 201 2 16 Predikátová logika Jazyky PLI Specifikace jazyka £ je definována funkčními a predikátovými symboly symboly tedy určují oblast, kterou jazyk popisuje Jazyky s rovností: obsahují predikátový symbol pro rovnost „=" Příklady M jazyk teorie uspořádání 3 jazyk s =, binární prediátový symbol < jazyk teorie množin m jazyk s =, binární predikátový symbol e M jazyk elementární aritmetiky 3 jazyk s =, nulární funkční symbol 0 pro nulu, unární funkční symbol s pro operaci následníka, binární funkční symboly pro sčítání + a násobení x Hana Rudová, Logické programování 1,21. března 2012 16 Predikátová logika Term, atomická formule, formule M Term nad abecedou JA 3 každá proměnná z JA je term 3 je-li f In z JA a t\,..., tn jsou termy, pak f(t\,..., tn) je také term ^ každý term vznikne konečným počtem užití přechozích kroků f( X, g(X,0)) Hana Rudová, Logické programování 1,21. března 201 2 Predikátová logika Term, atomická formule, formule M Term nad abecedou J4. 3 každá proměnná z JA je term m je-li f In z JA a ři,..., tn jsou termy, pak f(t\,..., tn) je také term ^ každý term vznikne konečným počtem užití přechozích kroků f( X, g(X,0)) M Atomická formule (atom) nad abecedou JA m je-li p/n z JA a t\,..., tn jsou termy, pak p(t\,..., tn) je atomická formule f(X) < g(X,0) Hana Rudová, Logické programování 1,21. března 201 2 Predikátová logika Term, atomická formule, formule M Term nad abecedou JA 3 každá proměnná z JA je term 3 je-li f In z JA a t\,..., tn jsou termy, pak f(t\,..., tn) je také term 3 každý term vznikne konečným počtem užití přechozích kroků f( X, g(X,0)) M Atomická formule (atom) nad abecedou JA 3 je-li p/n z JA a t\,..., tn jsou termy, pak p(t\,..., tn) je atomická formule f(X) < g(X,0) Formule nad abecedou J4. 3 každá atomická formule je formule 3 jsou-li F a G formule, pak také (->F), (F A G), (F v G), (F ^> G), (F = G) jsou formule ^ je-li X proměnná a F formule, pak také (VX F) a (3X F) jsou formule 3 každá formule vznikne konečným počtem užití přechozích kroků (3X ((f(X) = 0) A p(0))) Hana Rudová, Logické programování 1,21. března 201 2 Predikátová logika Interpretace Interpretace 1 jazyka L nad abecedou SA je dána 3 neprázdnou množinou V (také značíme nazývá se univerzum) a m zobrazením, které každé konstantě c g SA přiřadí nějaký prvek T> s* každému funkčnímu symbolu f In g SA přiřadí n-ární operaci nad T> každému predikátovému symbolu p/n g SA přiřadí n-ární relaci nad V Rudová, Logické programování 1,21. března 201 2 18 Predikátová logika Interpretace M Interpretace 1 jazyka L nad abecedou SA je dána neprázdnou množinou T> (také značíme nazývá se univerzum) a 3 zobrazením, které * každé konstantě c g SA přiřadí nějaký prvek T> každému funkčnímu symbolu f In g JA přiřadí n-ární operaci nad T> 3 každému predikátovému symbolu p In g JA přiřadí n-ární relaci nad T> M Příklad: uspořádání na M m jazyk: predikátový symbol mensí/2 3 interpretace: univerzum R; zobrazení: mensí(x,y) := x < y Hana Rudová, Logické programování 1,21. března 201 2 18 Predikátová logika Interpretace M Interpretace 1 jazyka L nad abecedou JA je dána 3 neprázdnou množinou T> (také značíme nazývá se univerzum) a 3 zobrazením, které St každé konstantě c g JA přiřadí nějaký prvek T> > každému funkčnímu symbolu f In g JA přiřadí n-ární operaci nad T> každému predikátovému symbolu pln g JA přiřadí n-ární relaci nad T> M Příklad: uspořádání na M 3 jazyk: predikátový symbol mensí/2 m interpretace: univerzum R; zobrazení: mensi(x,y) := x < y M Příklad: elementární aritmetika nad množinou N (včetně 0) jazyk: konstanta zero, funční symboly 5/1, plus 12 interpretace: St univerzum N; zobrazení: zero := 0, s(x)\=l+x, plus(x,y) := x + y Hana Rudová, Logické programování 1,21. března 2012 18 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1 Hodnota termu qp(t): každému termu je přiřazen prvek univerza m příklad: nechť q?(X) := 0 qp(plus(s(zero),X)) = Hana Rudová, Logické programování 1,21. března 201 2 19 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1 Hodnota termu qp(t): každému termu je přiřazen prvek univerza m příklad: nechť , <3>, <5>,...} 1 \= p(zero) a p(s(zero)) Hana Rudová, Logické programování 1,21. března 201 2 19 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ Hodnota termu qp(t): každému termu je přiřazen prvek univerza 3 příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = qp(s(zero)) + qp(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 Každá dobře utvořená formule označuje pravdivostní hodnotu (pravda, nepravda) v závislosti na své struktuře a interpretaci Pravdivá formule 1 q: formule q označena pravda Nepravdivá formule 1 ^ q: formule q označena nepravda 3 příklad: p II predikátový symbol, tj. p c \1\ p := {(1>, (3>, (5>,...} 1 \= p(zero) a p(s(zero)) iff 1 \= p(zero) a 1 \= p(s(zero)) Hana Rudová, Logické programování 1,21. března 201 2 19 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ Hodnota termu qp(t): každému termu je přiřazen prvek univerza 3 příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = qp(s(zero)) + qp(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 Každá dobře utvořená formule označuje pravdivostní hodnotu (pravda, nepravda) v závislosti na své struktuře a interpretaci Pravdivá formule 1 q: formule q označena pravda Nepravdivá formule 1 ^ q: formule q označena nepravda 3 příklad: pII predikátový symbol, tj. p c \1\ p := {<1>, <3>, <5>,...} 1 \= p(zero) a p(s(zero)) iff 1 \= p(zero) a 1 \= p(s(zero)) iff (qp(zero)) e p a (qp(s(zero))) e p Hana Rudová, Logické programování 1,21. března 201 2 19 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ Hodnota termu qp(t): každému termu je přiřazen prvek univerza 3 příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = qp(s(zero)) + qp(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 Každá dobře utvořená formule označuje pravdivostní hodnotu (pravda, nepravda) v závislosti na své struktuře a interpretaci Pravdivá formule 1 q: formule q označena pravda Nepravdivá formule 1 ^ q: formule q označena nepravda 3 příklad: p II predikátový symbol, tj. p c= \1\ p := {(1), <3>, <5>,...} 1 \= p(zero) a p(s(zero)) iff 1 \= p(zero) a 1 \= p(s(zero)) iff (qp(zero)) e p a (qp(s(zero))) e p iff (qp(zero)) e p a <(1 + qp(zero)) e p Hana Rudová, Logické programování 1,21. března 201 2 19 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ Hodnota termu qp(t): každému termu je přiřazen prvek univerza 3 příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = qp(s(zero)) + q?(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 Každá dobře utvořená formule označuje pravdivostní hodnotu (pravda, nepravda) v závislosti na své struktuře a interpretaci Pravdivá formule 1 h

, (3>, (5>,...} 1 \= p(zero) a p(s(zero)) iff 1 \= p(zero) a 1 \= p(s(zero)) iff (qp(zero)) e p a (qp(s(zero))) e p iff (qp(zero)) e p a ((1 + qp(zero)) e p iff <0>epaep (1) g p ale (0) é p, tedy formule je nepravdivá v 1 Hana Rudová, Logické programování 1,21. března 2012 19 Predikátová logika Model Interpretace se nazývá modelem formule, je-li v ní tato formule pravdivá 3 interpretace množiny N s obvyklými operacemi je modelem formule ( 1 + s(0) = s(s(0))) 3 interpretace, která se liší přiřazením s/l: s(x):=x není modelem této formule Rudová, Logické programování 1,21. března 201 2 20 Predikátová logika Model Interpretace se nazývá modelem formule, je-li v ní tato formule pravdivá 3 interpretace množiny N s obvyklými operacemi je modelem formule ( 1 + s(0) = s(s(0))) 3 interpretace, která se liší přiřazením s/l: s(x):=x není modelem této formule Teorie Ť jazyka X je množina formulí jazyka X, tzv. axiomů m -i s(X) = Oje jeden z axiomů teorie elementární aritmetiky Hana Rudová, Logické programování 1,21. března 201 2 20 Predikátová logika Model Interpretace se nazývá modelem formule, je-li v ní tato formule pravdivá 3 interpretace množiny N s obvyklými operacemi je modelem formule ( 1 + s(0) = s(s(0))) 3 interpretace, která se liší přiřazením s/l: s(x):=x není modelem této formule Teorie Ť jazyka X je množina formulí jazyka X, tzv. axiomů m -i s(X) = Oje jeden z axiomů teorie elementární aritmetiky M Model teorie: libovolná interpretace, která je modelem všech jejích axiomů 3 všechny axiomy teorie musí být v této interpretaci pravdivé Hana Rudová, Logické programování 1,21. března 201 2 20 Predikátová logika Model Interpretace se nazývá modelem formule, je-li v ní tato formule pravdivá 3 interpretace množiny N s obvyklými operacemi je modelem formule ( 1 + s(0) = s(s(0))) 3 interpretace, která se liší přiřazením s/l: s(x):=x není modelem této formule Teorie Ť jazyka X je množina formulí jazyka X, tzv. axiomů m -i s(X) = Oje jeden z axiomů teorie elementární aritmetiky M Model teorie: libovolná interpretace, která je modelem všech jejích axiomů 3 všechny axiomy teorie musí být v této interpretaci pravdivé M Pravdivá formule v teorii Ť \= F: pravdivá v každém z modelů teorie Ý m říkáme také formule platí v teorii nebo je splněna v teorii 3 formule 1 + s(0) = s(s(0)) je pravdivá v teorii elementárních čísel Hana Rudová, Logické programování 1,21. března 201 2 20 Predikátová logika Model Interpretace se nazývá modelem formule, je-li v ní tato formule pravdivá G je logicky pravdivá, formule 1 + s(0) = s(s(0)) není logicky pravdivá Hana Rudová, Logické programování 1,21. března 2012 20 Predikátová logika Zkoumání pravdivosti formulí M Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost Fi,..., Fn formulí jazyka X, v níž každé Fi je buď axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) použitím určitých odvozovacích pravidel Hana Rudová, Logické programování 1,21. března 201 2 21 Predikátová logika Zkoumání pravdivosti formulí M Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost Fi,..., Fn formulí jazyka X, v níž každé Fi je buď axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) použitím určitých odvozovacích pravidel M Odvozovací pravidla - příklady m pravidlo modus ponens: z formulí F a F => G lze odvodit G Hana Rudová, Logické programování 1,21. března 201 2 21 Predikátová logika Zkoumání pravdivosti formulí M Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost Fi,..., Fn formulí jazyka X, v níž každé Fi je buď axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) použitím určitých odvozovacích pravidel M Odvozovací pravidla - příklady m pravidlo modus ponens: z formulí F a F => G lze odvodit G m rezoluční princip: z formulí F v A, G v ->A odvodit F v G Hana Rudová, Logické programování 1,21. března 201 2 21 Predikátová logika Zkoumání pravdivosti formulí M Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost Fi,..., Fn formulí jazyka X, v níž každé Fi je buď axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) použitím určitých odvozovacích pravidel M Odvozovací pravidla - příklady m pravidlo modus ponens: z formulí F a F => G lze odvodit G m rezoluční princip: z formulí F v A, G v ->A odvodit F v G G lze odvodit G m rezoluční princip: z formulí F v A, G v ->A odvodit F v G M F je dokazatelná z formulí Ai, ■ ■ ■ , An Ai, ■ ■ ■ ,An\- F existuje-li důkaz F z Ai, ■ ■ ■ , An M Dokazatelné formule v teorii Ť nazýváme teorémy teorie Ť Hana Rudová, Logické programování 1,21. března 201 2 21 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) 3 VY ((0 < Y) A ( EIX (X < Y))) je uzavřená formule 3 ( 3X (X < Y)) není uzavřená formule Hana Rudová, Logické programování 1,21. března 201 2 22 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) 3 VY ((0 < Y) A ( EIX (X < Y))) je uzavřená formule 3 ( 3X (X < Y)) není uzavřená formule M Množina odvozovacích pravidel se nazývá korektní, jestliže pro každou množinu uzavřených formulí T a každou uzavřenou formuli F platí: jestliže T \- F pak ľNF (jestliže je něco dokazatelné, pak to platí) Hana Rudová, Logické programování 1,21. března 201 2 22 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) 3 VY ((0 < Y) A ( EIX (X < Y))) je uzavřená formule 3 ( 3X (X < Y)) není uzavřená formule M Množina odvozovacích pravidel se nazývá korektní, jestliže pro každou množinu uzavřených formulí T a každou uzavřenou formuli F platí: jestliže T \- F pak ľNF (jestliže je něco dokazatelné, pak to platí) Odvozovací pravidla jsou úplná, jestliže jestliže ľNF pak T \- F (jestliže něco platí, pak je to dokazatelné) Hana Rudová, Logické programování 1,21. března 201 2 22 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) * VY ((0 < Y) A ( EIX (X < Y))) je uzavřená formule 3 ( 3X (X < Y)) není uzavřená formule M Množina odvozovacích pravidel se nazývá korektní, jestliže pro každou množinu uzavřených formulí T a každou uzavřenou formuli F platí: jestliže T \- F pak ľNF (jestliže je něco dokazatelné, pak to platí) Odvozovací pravidla jsou úplná, jestliže jestliže ľNF pak T \- F (jestliže něco platí, pak je to dokazatelné) M PLI: úplná a korektní dokazatelnost, tj. pro teorii Ť s množinou axiomů SA platí: Ť \= F právě když JA \- F Hana Rudová, Logické programování 1,21. března 201 2 22 Predikátová logika