Syntaxe logického programu Backtracking, unifikace, aritmetika Term: ■ univerzální datová struktura (slouží také pro příkazy jazyka) ■ definovaný rekurzivně ■ konstanty: číselné, alfanumerické (začínají malým písmenem), ze speciálních znaků (operátory) ■ proměnné: pojmenované (alfanumerické řetězce začínající velkým písmenem), anonymní (začínají podtržítkem) ■ složený term: funktor, arita, argumenty struktury jsou opět termy Anatomie a sémantika logického programu ■ Program: množina predikátů (v jednom nebo více souborech). ■ Predikát (procedura) je seznam klauzulí s hlavou stejného jména a arity ■ Klauzule: věty ukončené tečkou, se skládají z hlavy a těla. Prázdné tělo mají fakta, neprázdné pak pravidla, existují také klauzule bez hlavy - direktivy. Hlavu tvoří literál (složený term), tělo seznam literálů. Literálům v těle nebo v dotazu říkáme cíle. Dotazem v prostředí interpretu se spouští programy či procedury. ■ př. otec(Otec,Dite) :- rodič(Otec,Dite), muz(Otec). rodic(petr, jana). :- otec(Otec, jana). Sémantika logického programu: procedury = databáze faktů a pravidel = logické formule Hana Rudová, Logické programování I, 6. března 2013 Backtracking, unifikace, aritmetika Hana Rudová, Logické programování I, 6. března 2013 Backtracking, unifikace, aritmetika SICStus Debugging ■ ' ' Ptcfog Pro/ectíin; jncdule.pro - Eclipse 1DK File Edit EICStu: ícu';; Ní-itjití ícinn Preis" Run lavorite: P- Debug s3"' » ■ | 3. s> JÍL =% | ^ ^ 4 Prolog Top-level Configuration [SlCStu: Launch Ccnficjuration Typel] $ Prolog Target = call: suffK([a,_7551,e],_1810) = my_predlf_lS10) „1 Prc-logTcp-levdP™^ °e Breakpoint: Value [a, .7551, SICStus Prolog VC10 4.2.3 nastavíme pracovní adresář pomocí File/Working directory, v případě potřeby nastavíme font Settings/Font a uložíme nastavení Settings/Save settings. Iniciální nastavení SICStus IDE v Eclipse pomocí Help->Cheat Sheets->lnitial set up of paths to installed SICStus Prolog s cestou "C:\Program Files\SICStus Prolog VC10 4.2.3\bin\sicstus-4.2.3.exe" návod: http://www.sics.se/sicstus/spider/site/prerequi si tes.html#SettingUp Hana Rudová, Logické programování I, 6. března 2013 5 Backtracking, unifikace, aritmetika SICStus Prolog: spouštění a přerušení výpočtu Spouštění programů/procedur/predikátů je zápis dotazů na příkazové řádce (v okně TopLevel, kurzor musí být na konci posledního řádku s | ?-), př. ?- predekCpetr,lenka). ?- predek(X.Y). Každý příkaz ukončujeme tečkou. Přerušení a zastavení cyklícího programu: pomocí ikony Restart Prolog z okna Toplevel Hana Rudová, Logické programování I, 6. března 2013 7 Backtracking, unifikace, aritmetika SICStus Prolog: konzultace ■ Otevření souboru: File->Open File ■ Přístup k příkazové řádce pro zadávání dotazů: SICStus->Open Toplevel ■ Načtení programu: tzv. konzultace přímo z Menu: SICStus->Consult Prolog Code (okno s programem aktivní) nebo zadáním na příkazový řádek po uložení souboru (Ctrl+S) ?- consult(rodokmen). pokud uvádíme celé jméno případně cestu, dáváme jej do apostrofů ?- consultC'D:\prolog\moje\programy\rodokmen.pl') . ■ V Eclipse lze nastavit Key bindings, pracovní adresář, ... Hana Rudová, Logické programování I, 6. března 2013 6 Backtracking, unifikace, aritmetika Příklad rodokmen rodič(petr, filip). muz(petr). rodicCpetr, lenka). muz(fi lip). rodicCpavel, jan). muz(pavel). rodicCadam, petr). muz(jan) . rodicCtomas, michal). muz(adam). rodicCmichal, radek). muz(tomas). rodic(eva, filip). muz(michal) rodicCjana, lenka). muz(radek). rodicCpavla, petr). rodicCpavla, tomas). zena(eva). rodicClenka, vera). zena(lenka) zena(pavla). zena(jana) . zena(vera). otec(Otec,Dite) :- rodič(Otec,Dite), muz(Otec). Hana Rudová, Logické programování I, 6. března 2013 8 Backtracking, unifikace, aritmetika Backtracking: příklady Backtracking: řešení příkladů V pracovním adresáři vytvořte program rodokmen.pl. Načtěte program v interpretu (konzultujte). V interpretu Sicstus Prologu pokládejte dotazy: ■ Je Petr otcem Lenky? ■ Je Petr otcem Jana? ■ Kdo je otcem Petra? ■ Jaké děti má Pavla? ■ Ma Petr dceru? ■ Které dvojice otec-syn známe? Hana Rudová, Logické programování I, 6. března 2013 Backtracking, unifikace, aritmetika Backtracking: příklady II Predikát potomek/2: potomek(Potomek,Předek) :- rodic(Predek,Potomek). potomek(Potomek,Předek) :- rodic(Predek,X), potomek(Potomek,X). Naprogramujte predikáty (pomocí rodic/2, muz/1, zena/l) ■ prababicka(Prababicka,Pravnouce) ■ nevíastni_bratr(NevJastni_bratr,Nevlastni_sourozenec) nápověda: využijte X \== Y (X a Y nejsou identické) Řešení: prababicka(Prababicka,Pravnouce):-rodic(Prababicka,Prarodič), zena(Prababicka), rodic(Prarodic,Rodič), rodic(Rodic,Pravnouce). Hana Rudová, Logické programování I, 6. března 2013 Backtracking, unifikace, aritmetika Středníkem si vyžádáme další řešení | ?- otec(petr,lenka). yes | ?- otecCpetr,jan). no | ?- otec(Kdo,petr). Kdo = adam ? ; no | ?- rodic(pavla.Dite). Dite = petr ? ; Dite = tomas ? ; no | ?- otecCpetr,Dcera),zena(Dcera). Dcera = lenka ? ; no | ?- otec(Otec,Syn),muz(Syn). Syn = fi 1 i p, Otec = petr ? ; Syn = jan, Otec = pavel ? ; Syn = petr, Otec = adam ? ; Syn = michal, Otec = tomas ? ; Syn = radek, Otec = michal ? ; no I ?- Hana Rudová, Logické programování I, 6. března 2013 Backtracking, unifikace, aritmetika Backtracking: řešení příkladů II nevlastni_bratr(Bratr,Sourozenec): rodic(X,Bratr), muz(Bratr), rodic(X,Sourozenec), /'■'•' tento test neni nutný, ale zvyšuje efektivitu Bratr \== Sourozenec, rodic(Y,Bratr), Y \== X, rodic(Z,Sourozenec), Z \== X, Z \== Y. /"' nevhodné umisteni testu - vypočet "bloudi" v neúspěšných vetvich */ nevíastni_bratr2(Bratr.Sourozenec):- rodic(X,Bratr), rodic(X,Sourozenec), rodic(Y,Bratr), rodic(Z,Sourozenec), Y \== X, Z \== X, Z \== Y, muz(Bratr). Hana Rudová, Logické programování I, 6. března 2013 Backtracking, unifikace, aritmetika Backtracking: porovnání Nahraďte ve svých programech volání predikátu rodic/2 následujícím predikátem rodic_v/2 rodic_v(X,Y) :-rodic(X,Y) ,pn'nt(X) ,pn'nt('? ') . Pozorujte rozdíly v délce výpočtu dotazu nevlastni_bratr(fi"lip,X) při změně pořadí testů v definici predikátu nevlastni_bratr/2 ■ varianta 1: testy co nejdříve správně ■ varianta 2: všechny testy umístěte na konec chybně Co uvidíme po nahrazení predikátu rodic/2 predikátem rodic_v/2 v predikátech nevlastni_bratr/2 a nevlastni_bratr2/2 a spuštění? Hana Rudová, Logické programování I, 6. března 2013 13 Backtracking, unifikace, aritmetika I ?- nevlastni_bratrCX,Y). petr? petr? petr? petr? eva? petr? jana? X = filip, Y = lenka ? ; petr? pavel? pavel? adam? adam? tomas? tomas? michal? michal? eva? eva? jana? pavla? pavla? pavla? adam? pavla? pavla? pavla? pavla? pavla? pavla? lenka? no I ?- nevlastni_bratr2(X,Y). petr? petr? petr? petr? eva? eva? petr? eva? petr? petr? petr? jana? eva? petr1: X = filip, Y = lenka ? ; petr? petr? petr? petr? eva? jana? petr? eva? petr? petr? petr? jana? jana? pel jana? pavel? pavel? pavel? pavel? adam? adam? adam? adam? pavla? pavla? adam? pavla? tomas? tomas? tomas? tomas? michal? michal? michal? michal? eva? eva? pf petr? eva? eva? petr? eva? jana? jana? petr? petr? jana? jana? petr? jana? pavl pavla? adam? adam? pavla? pavla? adam? pavla? pavla? adam? pavla? pavla? pavla1: pavla? pavla? pavla? adam? pavla? pavla? pavla? pavla? lenka? lenka? lenka? ler no Hana Rudová, Logické programování I, 6. března 2013 14 Backtracking, unifikace, aritmetika Backtracking: prohledávání stavového prostoru potomekCPotomek,Předek) :- rodic(Predek,Potomek). potomekCPotomek,Předek) :- rodicCPredek,X), potomekCPotomek,X). ■ Zkuste předem odhadnout (odvodit) pořadí, v jakém budou nalezeni potomci Pavly? :- potomekCX,pavla). ■ Jaký vliv má pořadí klauzulí a cílu v predikátu potomek/2 na jeho funkci? rodicCpetr, filip). rodicCpavel, jan). rodicCtomas, michal). rodicCeva, filip). rodicCpavla, petr). rodicClenka, vera). rodicCpetr, lenka). rodicCadam, petr). rodicCmichal, radek). rodicCjana, lenka). rodicCpavla, tomas). Hana Rudová, Logické programování I, 6. března 2013 Backtracking, unifikace, aritmetika Backtracking: řešení potomekCPotomek,Předek):-rodicCPredek,Potomek). potomekCPotomek,Předek):-rodicCPredek,X),potomekCPotomek,X). /'■'•' varianta la '■'•'/ potomekCPotomek,Předek):-rodicCPredek,X),potomekCPotomek,X). potomekCPotomek,Předek):-rodicCPredek,Potomek). /'■'•' varianta lb - jine poradi odpovedi, neprimi potomci maji přednost '■'•'/ potomekCPotomek,Předek):-rodicCPredek,Potomek). potomekCPotomek,Předek):-potomekCPotomek,X),rodicCPredek,X). /'■'•' varianta 2a - leva rekurze ve druhé klauzuli, na dotaz potomekCX, pavla) výpise odpovedi, pak cykli '■'•'/ potomekCPotomek,Předek):-potomekCPotomek,X),rodicCPredek,X). potomekCPotomek,Předek):-rodicCPredek,Potomek). /'■'•' varianta 2b - leva rekurze v prvni klauzuli, na dotaz potomekCX, pavla) hned cykli '■'•'/ Hana Rudová, Logické programování I, 6. března 2013 16 Backtracking, unifikace, aritmetika Unifikace:příklady Které unifikace jsou korektní, které ne a proč? Co je výsledkem provedených unifikací? 1. a(X)=b(X) 2. X=a(Y) 3. a(X)=a(X,X) 4. X=a(X) 5. jmeno(X,X)=jmeno(Petr,p"lus) 6. s(l,a(X,q(w)))=s(Y,a(2,Z)) 7. s(l,a(X,q(X)))=s(W,a(Z,Z)) 8. X=Y,P=R,s(l,a(P,q(R)))=s(Z,a(X,Y)) Neuspěje volání 1) a 3), ostatní ano, cyklické struktury vzniknou v případech 4),7) a 8) přestože u posledních dvou mají levá a pravá strana unifikace disjunktní množinyjmen proměnných. Hana Rudová, Logické programování I, 6. března 2013 Backtracking, unifikace, aritmetika Mechanismus unifikace I Unifikace v průběhu dokazování predikátu odpovídá předávání parametrů při provádění procedury, aleje důležité uvědomit si rozdíly. Celý proces si ukážeme na příkladu predikátu suma/3. suma(0,X,X) . /'•'••klauzule A*/ suma(sCX) ,Y,s(Z)) :-suma(X,Y,Z) . /'•••klauzule B*/ pomocí substitučních rovnic při odvozování odpovědi na dotaz ?- suma(sCO),s(0),X0). Hana Rudová, Logické programování I, 6. března 2013 Backtracking, unifikace, aritmetika Mechanismus unifikace II suma(0,X,X). /*A*/ suma(s(X),Y,s(Z)):-suma(X,Y,Z). /*B*/ ?- suma(sCO),s(0),X0). 1. dotaz unifikujeme s hlavou klauzule B, s A nejde unifikovat (1. argument) suma(sCO),s(0),X0) = suma(s(Xl),Yl,s(Zl)) ==> XI = 0, Yl = s(0), s(Zl) = X0 ==> suma(0,s(0),Z1) 2. dotaz (nový podcíl) unifikujeme s hlavou klauzule A, klauzuli B si poznačíme jako další možnost suma(0,s(0),Z1) = suma(0,X2,X2) X2 = s(0), Zl = s(0) ==> X0 = s(sCO)) X0 = s(sCO)) ; 2' dotaz z kroku 1. nejde unifikovat s hlavou klauzule B (1. argument) no Hana Rudová, Logické programování I, 6. března 2013 19 Backtracking, unifikace, aritmetika Vícesměrnost predikátů Logický program lze využít vícesměrně, například jako ■ výpočet kdo je otcem Petra? ?- otec(X, petr) . kolik je 1+1? ?- suma(s(0) ,s(0) ,X) . ■ test je Jan otcem Petra? ?- otec(jan, petr) . Je 1+1 2??- suma(s(0),s(0),s((0)) ). ■ generátor které dvojice otec-dítě známe? ?-otec(X,Y) . Které X a Y dávají v součtu 2? ?- suma(X, Y, s(s(0)) ). ... ale pozor na levou rekurzi, volné proměnné, asymetrii, ajiné záležitosti D.Ú. Následující dotazy ?-suma(X,s(0),z). ?-suma(s(0),x,Z). nedávají stejné výsledky. Zkuste šije odvodit pomocí substitučních rovnic. Hana Rudová, Logické programování I, 6. března 2013 20 Backtracking, unifikace, aritmetika Aritmetika Zavádíme z praktických důvodů, ale aritmetické predikátyjiž nejsou vícesměrné, protože v každém aritmetickém výrazu musí být všechny proměnné instaciovány číselnou konstantou. Důležitý rozdíl ve vestavěných predikátech is/2 vs. =/2 vs. =.=12 is/2: < konstanta nebo proměnná > is < aritmetický výraz > výraz na pravé straně je nejdříve aritmeticky vyhodnocen a pak unifikován s levou stranou =/2: < libovolný term > = < libovolný term > levá a pravá strana jsou unifikovány "=:="/2 "=\="/2 ">="/2 "=<"/2 < aritmetický výraz > =:= < aritmetický výraz > < aritmetický výraz > =\= < aritmetický výraz > < aritmetický výraz > =< < aritmetický výraz > < aritmetický výraz > >= < aritmetický výraz > levá i pravá strana jsou nejdříve aritmeticky vyhodnoceny a pak porovnány Hana Rudová, Logické programování I, 6. března 2013 Backtracking, unifikace, aritmetika Aritmetika: příklady II Jak se liší predikáty sl/3 a s2/3? Co umí sl/3 navíc oproti s2/3 a naopak? sl(0,X,X). sl(s(X),Y,s(Z)):-sl(X,Y,Z). s2(X,Y,Z):- Z i s X + Y. sl/3 je vícesměrný - umí sčítat, odečítat, generovat součty, ale pracuje jen s nezápornými celými čísly s2/3 umí pouze sčítat, ale také záporná a reálná čísla Aritmetika: příklady Jak se liší následující dotazy (na co se kdy ptáme)? Které uspějí (kladná odpověď), které neuspějí (záporná odpověď), a které jsou špatně (dojde k chybě)? Za jakých předpokladů by ty neúspěšné případně špatné uspěly? 1. X = Y + 1 2. X is Y + 1 3. X = Y 4. X == Y 5. 1 + 1 = 2 6. 2 = 1 + 1 7. 1 + 1 = 1 + 1 8. 1 + 1 is 1 + 1 9. 1 + 2 =:= 2 + 1 10. X \== Y 11. X =\= Y 12. 1 + 2 =\= 1 - 2 1 3. 1 <= 2 14. 1 =< 2 1 5. sin(X) is sin(2) 16. sin(X) = sin(2+Y) 1 7. sin(X) =:= sin(2+Y) Nápověda: '='/2 unifikace, '=='/2 test na identitu, '=:='/2 aritmetická rovnost, '\=='/2 negace testu na identitu, '=\='/2 aritmetická nerovnost Hana Rudová, Logické programování I, 6. března 2013 Backtracking, unifikace, aritmetika Závěr Dnešní látku jste pochopili dobře, pokud víte ■ jaký vliv má pořadí klauzulí a cílu v predikátu potomek/2 na jeho funkci, ■ jak umisťovat testy, aby byl prohledávaný prostor co nejmenší (příklad nevlastni_bratr/2), ■ k čemu dojde po unifikaci X=a(X), ■ proč neuspěje dotaz ?- X=2, sin(X) is sin(2). ■ za jakých předpokladů uspějí tyto cíle X=Y, X==Y, X=:=Y, ■ a umíte odvodit pomocí substitučních rovnic odpovedi na dotazy suma(X,s(0),Z) a suma(s(0),X,Z). Hana Rudová, Logické programování I, 6. března 2013 23 Backtracking, unifikace, aritmetika Hana Rudová, Logické programování I, 6. března 2013 24 Backtracking, unifikace, aritmetika