Technika a styl programování v Prologu Technika a styl programování v Prologu Styl programování v Prologu ■ některá pravidla správného stylu ■ správný vs. špatný styl ■ komentáře Ladění Efektivita Styl programování v Prologu I. Cílem stylistických konvencí je ■ redukce nebezpečí programovacích chyb ■ psaní čitelných a srozumitelných programů, které se dobře ladí a modifikují Některá pravidla správného stylu ■ krátké klauzule ■ krátké procedury; dlouhé procedury pouze s uniformní strukturou (tabulka) ■ klauzule se základními (hraničními) případy psát před rekurzivními klauzulemi ■ vhodnájmena procedur a proměnných ■ nepoužívat seznamy ([. . . ]) nebo závorky ({...}, (...)) pro termy pevné arity ■ vstupní argumenty psát před výstupními ■ struktura programu - jednotné konvence v rámci celého programu, např. ■ mezery, prázdné řádky, odsazení ■ 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 2012 Technika a styl programování v Prologu Hana Rudová, Logické programování 1,21. března 201 2 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 ) merge( Seznam, [], Seznam ). % prevence redundantních řešení merge( [X|Te"lol], [Y|Telo2], [X|Te"lo3] ) :■ X < Y, !, merge( Telol, [Y|Telo2], Te"lo3 ). merge( Seznámí, [Y|Telo2], [Y|Te"lo3] ) :-merge( Seznámí, Te"lo2, Te"lo3 ). Hana Rudová, Logické programování 1,21. března 201 2 Technika a styl programování v Prologu Špatný styl programování Styl programování v Prologu II. merge( SI, S2, S3 ) 51 = [], ! , S3 = S2; 52 =[],!, S3 = SI 51 = [XI TI], 52 = [Y|T2], ( X < Y, !, Z = X, merge( TI, S2, T3 ); Z = Y, merge( SI, T2, T3) ), 53 = [ Z I T3 ]. % první seznam je prázdný % druhý seznam je prázdný % Z je hlava seznamu S3 Středník „;" může způsobit nesrozumitelnost klauzule ■ nedávat středník na konec řádku, používat závorky ■ v některých případech: rozdělení klauzle se středníkem do více klauzulí Opatrné používání operátoru řezu ■ preferovat použití zeleného řezu (nemění deklarativní sémantiku) ■ červený řez používat vjasně definovaných konstruktech negace: P, !, fail; true alternativy: Podmínka, !, Cill ; Cil2 Podmínka Opatrné používání negace „\+" ■ negace jako neúspěch: negace není ekvivalentní negaci v matematické logice Pozor na assert a retract: snižuji transparentnost chování programu \+ P ď U ; Cil 2 Hana Rudová, Logické programování 1,21. března 201 2 5 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) ■ jak jsou hlavní koncepty (objekty) reprezentovány ■ doba výpočtu a paměťové nároky ■ 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) ■ vstupní argumenty „+", výstupní „-" mergeC +Seznaml, +Seznam2, -Seznam3 ) ■ ]menoPredikatu/Arita merge/3 ■ algoritmické a implementační podrobnosti Hana Rudová, Logické programování 1,21. března 201 2 7 Technika a styl programování v Prologu Hana Rudová, Logické programování 1,21. března 201 2 6 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 ■ spy( merge/3 ) ■ debug/0, nodebug/0: pro trasování pouze predikátů zadaných spy/1 ■ Libovolná část programu může být spuštěna zadáním vhodného dotazu: trasování cíle ■ vstupní informace: jméno predikátu, hodnoty argumentů při volání ■ výstupní informace ■ při úspěchu hodnoty argumentů splňující cíl ■ při neúspěchu indikace chyby ■ 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 Vizualizace řídícího toku (backtrackingu) na úrovni predikátu ■ Call: volání cíle ■ Exit: úspěšné ukončení volání cíle ■ Fail: volání cíle neuspělo ■ 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 1 -----> + predekC X, i Z ) :- rodicC X, Z ). 1 1 predekC X, Z ) :- rodicC X, Y ), <----------- ------+ predekC Y, Z ). Fail 1 + <- I Exit Redo Hana Rudová, Logické programování I, 21. března 2012 Technika a styl programování v Prologu a(X) a(X) a(X) c(l). d(2). nonvar(X). c(X). d(X). Příklad: trasování I ?- a(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 1 ? 1 1 Call : a(_463) ? 2 2 Call : nonvarC _463) ? 2 2 Fai 1 : 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) ? 4 2 Exit: d(2) ? 1 1 Exit: a(2) ? X = 2 ? no % trace I ?- Hana Rudová, Logické programování I, 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 ■ u Prologu můžeme častěji narazit na problémy s časem výpočtu a pamětí ■ Prologovské aplikace redukují čas na vývoj ■ 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 ■ zlepšení efektivity při prohledávání ■ odstranění zbytečného backtrackingu ■ 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 Zlepšení efektivity: základní techniky ■ Optimalizace posledního volání (LCO) a akumulátory ■ Rozdílové seznamy při spojování seznamů ■ Caching: uložení vypočítaných výsledků do programové databáze ■ Indexace podle prvního argumentu ■ např. v SICStus Prologu ■ 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 ■ zamestnanecC Prijmeni, Krestni]meno, Odděleni, ...) ■ seznamyC [], ...) :- ... . seznamyC [H|t], ...) :- ... . ■ Determinismus: ■ rozhodnout, které klauzule mají uspět vícekrát, ověřit požadovaný determinismus Hana Rudová, Logické programování 1,21. března 201 2 11 Technika a styl programování v Prologu Hana Rudová, Logické programování 1,21. března 201 2 1 2 Technika a styl programování v Prologu Teorie logického programování Predikátová logika l.řádu PROLOG: PROgramming in LOCic, část predikátové logiky l.řádu ■ fakta: rodic(petr, petri k), VXa(X) ■ klauzule: VX VY rodic(X,Y) => predek(X.Y) Predikátová logika I. řádu (PL1) ■ soubory objektů: lidé, čísla, body prostoru, ... ■ syntaxe PL1, sémantika PL1, pravdivost a dokazatelnost Rezoluce ve výrokové logice, v PL1 ■ dokazovací metoda Rezoluce v logickém programování Backtracking, řez, negace vs. rezoluce Predikátová logika I. řádu (PL1) Abeceda JA jazyka L PLI se skládá ze symbolů: ■ proměnné X, Y, ... označují libovolný objekt z daného oboru ■ funkční symboly f, g, ... označují operace (příklad: +, x ) ■ arita = počet argumentů, n-ární symbol, značíme f/n ■ nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0,1,...) ■ predikátové symboly p,q, ... pro vyjádření vlastností a vztahů mezi objekty ■ arita = počet argumentů, n-ární symbol, značíme p/n příklad: <, e ■ logické spojky a, v, =>, = ■ kvantifikátory V, 3 ■ logika I. řádu používá kvantifikaci pouze pro individua (odlišnost od logik vyššího řádu) ■ v logice 1. řádu nelze: v1:¥AeI,¥/:I-I ■ závorky: ),( Hana Rudová, Logické programování 1,21. března 2012 15 Predikátová logika Hana Rudová, Logické programování 1,21. března 2012 14 Teorie logického programování Jazyky PL1 ■ 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 ■ jazyk teorie uspořádání ■ jazyk s =, binární prediátový symbol < ■ jazyk teorie množin ■ jazyk s =, binární predikátový symbol e ■ jazyk elementární aritmetiky ■ 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 Term nad abecedou JA ■ každá proměnná z JI je term ■ je-li f/n z JI 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)) Atomická formule (atom) nad abecedou JA ■ je-li pln z a ti.....tn jsou termy, pak p(t\.....tn) je atomická formule f(X) < g(X,0) Formule nad abecedou JA ■ každá atomická formule je formule ■ 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 ■ 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í I, 21. března 2012 17 Predikátová logika Interpretace ■ Interpretace 1 jazyka L nad abecedou JA je dána ■ neprázdnou množinou T> (také značíme \1\, nazývá se univerzum) a ■ zobrazením, které ■ každé konstantě ceí přiřadí nějaký prvek T> ■ každému funkčnímu symbolu f/n e JA přiřadí n-ární operaci nad T> ■ každému predikátovému symbolu p In e JA přiřadí n-ární relaci nad T> ■ Příklad: uspořádání na R ■ jazyk: predikátový symbol mensí/2 ■ interpretace: univerzum K; zobrazení: mensí(x,y) := x < y ■ Příklad: elementární aritmetika nad množinou N (včetně 0) ■ jazyk: konstanta zero, funční symboly s/l, plus/2 ■ interpretace: ■ 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é q)(X): každé proměnné X je přiřazen prvek 2 Hodnota termu (plus(s(zero),X)) = cp(s(zero)) + q>(X) = (1 + cp(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 \=v Q: formule Q označena pravda Nepravdivá formule 1 tfv Q. formule Q označena nepravda ■ příklad: p/1 predikátový symbol, tj. p s p := {(1), (3), (5>,...} '1 N p(zero) a p(s(zero)) iff '1 N p(zero) a 'i N p(s(zero)) iff {qp(zero)) e p a (q?(s(zero))) e p iff {qp(zero)) e p a <(1 + q?(zero)) e p iff <0)epa G lze odvodit G ■ rezoluční princip: z formulí F v A, G v -vl odvodit F v G F je dokazatelná z formulí A\, ■ ■ ■ ,An A\, ■ ■ ■ ,An\- F existuje-li důkaz F z A\, ■ ■ ■ ,An Dokazatelné formule v teorii T" nazýváme teorémy teorie T" Hana Rudová, Logické programování I, 21. března 2012 21 Predikátová logika ■ Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) ■ VY ((0 < Y) a ( 3X (X < Y))) je uzavřená formule ■ ( 3X (X < Y) ) není uzavřená formule ■ 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 řhf pak T 1= F (jestliže je něco dokazatelné, pak to platí) Odvozovací pravidla jsou úplná, jestliže jestliže T 1= F pak T V- F (jestliže něco platí, pak je to dokazatelné) ■ PL1: úplná a korektní dokazatelnost, tj. pro teorii T' s množinou axiomů JA platí: T' t= F právě když JA v- F Hana Rudová, Logické programování 1,21. března 201 2 22 Predikátová logika