Paradygmaty programowania/Wykład 7: Programowanie w logice - przegląd

===Wprowadzenie=== Omawiamy jeszcze jeden z fundamentalnych paradygmatów programowania — programowanie w logice (lub programowanie logiczne — wcale nie ma tu sugestii, że inne paradygmaty są nielogiczne). W latach 80-tych XX wieku wiązano z nim olbrzymie nadzieje. Wydawało się, że to właśnie będzie paradygmat dominujący przez następne lata i że przyniesie rewelacyjne efekty, zwłaszcza w dziedzinie sztucznej inteligencji i szeroko rozumianej interakcji komputerów z ludźmi. Chociaż dotychczasowe rezultaty są skromniejsze od oczekiwań, warto przyjrzeć się temu zarodkowi niespełnionej rewolucji...

Wstęp

Na czym polega programowanie w logice? Zapisuje się stwierdzenia używając rachunku predykatów pierwszego rzędu. Wyniki powstają jako rezultat (automatycznego) wnioskowania. Języki programowania w logice nazywane są także językami deklaratywnymi, gdyż programy składają się nie z podstawień i sterowania przepływem, a z deklaracji. Jedynym rozpowszechnionym językiem tego rodzaju jest Prolog.

Poniżej omawiamy kilka wstępnych kwestii istotnych dla zrozumienia programowania w logice.

Rachunek predykatów pierwszego rzędu

• Rozważamy rachunek predykatów w zakresie takim, jaki wykorzystywany jest w Prologu.
• Term to funktor (symbol stanowiący nazwę relacji) z listą parametrów atomowych, np. człowiek(jerzy), lubi(adam, jabłko).
• Zauważmy, że stała jest szczególnym przypadkiem termu (bezparametrowym).
• Stwierdzenie to jeden lub więcej termów połączonych spójnikami (negacja Ř, alternatywa Ú, koniunkcja Ů, równoważność Ű, implikacja Ţ/Ü).
• W stwierdzeniach mogą pojawiać się zmienne związane kwantyfikatorami (uniwersalny ", egzystencjalny $).

Klauzule

• W Prologu nie używa się kwantyfikatorów; w zamian za to stwierdzenia zapisuje się w postaci klauzul.
• Ogólna postać klauzuli jest następująca:

A1 Ů A2 Ů ... Ů Am Ţ B1 Ú B2 Ú ... Ú Bn, gdzie Ai i Bi są termami.

• A1 Ů A2 Ů ... Ů Am to poprzednik klauzuli, zaś B1 Ú B2 Ú ... Ú Bn — następnik.
• Każde stwierdzenie można zapisać w formie klauzuli. Istnieje algorytm, który to robi.
• W Prologu używa się postaci jeszcze prostszej — klauzul Horna, czyli klauzul, które w następniku mają zero lub jeden term (n = 0 lub n = 1).
• Klauzule z termem w następniku („z głową”) wyrażają zależności.
• Klauzule z pustym następnikiem („bez głowy”) to po prostu stwierdzenia faktów.

Rezolucja

• Jest to metoda wnioskowania, którą można stosować do opisanych tu stwierdzeń.
• Podstawowa reguła jest następująca: wiedząc że P Ţ Q oraz R Ţ S, wnioskujemy że P Ţ S, o ile tylko Q i R dają się zunifikować.
• Z technicznego punktu widzenia, osiąga się to przez wyliczenie Q Ú S oraz P Ů R i usunięcie termów, które występują po obydwu stronach T.
• Występowanie zmiennych w stwierdzeniach powoduje, że w trakcie rezolucji trzeba znaleźć takie wartości dla tych zmiennych, które pozwolą na odpowiednie dopasowanie.
• Unifikacja to proces znajdowania wartości dla zmiennych, dzięki którym uzyskamy Q = R.
• Podstawianie pod zmienne tymczasowych wartości pozwalających na unifikację zwane jest instancjonowaniem. Mówimy też o utożsamieniu zmiennej z wartością.
• Unifikacja często wymaga nawrotów: Zmienna jest instancjonowana, lecz dopasowanie nie udaje się. Zmienną instancjonuje się wówczas inną wartością itd.

Dowodzenie twierdzeń za pomocą rezolucji

• Tworzymy zbiór stwierdzeń zawierający założenia twierdzenia (hipotezy) i negację tezy twierdzenia (cel).
• Hipotezy można uważać za bazę danych.
• Za pomocą rezolucji dochodzimy do sprzeczności.
• To dowodzi twierdzenia.
• Zasada jest prosta, ale złożoność czasowa może być barierą nie do pokonania...

Prolog

Prolog wywodzi się z prac badawczych prowadzonych w latach 70-tych XX wieku w Marsylii i w Edynburgu. Opracowany został z myślą o przetwarzaniu języka naturalnego i automatycznym dowodzeniu twierdzeń. W latach 80-tych stworzono też wersje na (ówczesne) mikrokomputery, np. bardzo udaną wersję micro-Prolog.

Termy

• Term w Prologu to stała, zmienna lub struktura.
• Stała może być atomem (składnia — jak typowy identyfikator lub napis ujęty w apostrofy) lub liczbą całkowitą.
• Nazwy zmiennych zaczynają się od dużej litery.
• Instancjonowanie zmiennych następuje wyłącznie w trakcie rezolucji. Trwa tylko do czasu osiągnięcia celu.
• Struktura ma postać funktor(listaParametrów), gdzie parametry są atomami, zmiennymi lub innymi strukturami.

Stwierdzenia

• Stwierdzenia występują w dwóch formach, odpowiadających klauzulom Horna z głową i bez głowy.
• Klauzula bez głowy to pojedyncza struktura, którą interpretujemy jako fakt (tzn. zakładamy, że stwierdzenie jest prawdziwe).
• Klauzula z głową zawiera następnik będący pojedynczą strukturą i poprzednik będący strukturą lub koniunkcją kilku struktur.
• Obydwie formy stwierdzeń kończy się kropką. W klauzulach z głową następnik od poprzednika oddziela się znakiem „:-”.
• Przykład klauzuli z głową:

     dziadek(X, Z) :- ojciec(X, Y), ojciec(Y, Z).

• Można przyjąć, że przez każdą klauzulą stoi niejawny kwantyfikator uniwersalny, wiążący zmienne tej klauzuli.
• Program prologowy to zbiór stwierdzeń takich, jak opisano powyżej.

Cel

• Stwierdzenie, które chcemy udowodnić (lub obalić, tzn. udowodnić jego fałszywość), nazywamy celem.
• Pod względem składniowym cel to klauzula bez głowy.
• Rozróżnienie pomiędzy celem a faktem (będącym częścią programu) bierze się z trybu wpisywania w interpreterze.
• Po wpisaniu celu interpreter Prologu odpowie „tak” lub „nie”.
• Odpowiedź „tak” oznacza, że udało się udowodnić cel przy podanych w programie założeniach.
• Odpowiedź „nie” oznacza, że udało się obalić cel lub że nie udało się go udowodnić przy podanych założeniach.
• Jeśli cel jest stwierdzeniem złożonym, każda z zawartych w nim struktur zwana jest podcelem.
• Cel może zawierać zmienne. W takim przypadku Prolog znajdzie instancje, dla których cel jest prawdziwy.

Rezolucja w Prologu

• Prolog stosuje metodę zstępującą, tzn. zaczyna od celu i próbuje znaleźć ciąg pasujących stwierdzeń, które prowadzą do pewnego zbioru faktów w programie.
• Ów ciąg stanowi dowód celu.
• Zauważmy, że można by stosować metodą wstępującą, tzn. zacząć od faktów w programie i próbować dojść do celu.
• Metoda wstępująca byłaby dobra przy dużym zbiorze rozwiązań; przy małym lepsza jest metoda zstępująca.
• Dla stwierdzeń złożonych używane jest przeszukiwanie w głąb, tzn. najpierw znajduje się dowód dla pierwszego podcelu, a potem przetwarza się następne podcele.
• Jeśli Prologowi nie uda się udowodnić jednego z podcelów, porzuca ów podcel i wraca do poprzednich podcelów, próbując znaleźć alternatywne rozwiązania. Proces ten zwany jest nawracaniem.
• Przeszukiwanie bazy danych postępuje zawsze od pierwszego stwierdzenia do ostatniego.

Arytmetyka

• W oryginalnym Prologu dostępna jest tylko arytmetyka na liczbach całkowitych.
• Dla uproszczenia zapisu wprowadzono infiksowe operatory arytmetyczne i operator is.
• Stosuje się go do zunifikowania zmiennej (która musi być nie zainstancjonowana) z wartością wyrażenia arytmetycznego.
• Przykład: X is 2 * Y + 3.
• To nie to samo, co podstawienie.

Przykład

• Poniższa „baza danych” zawiera informacje o czasie przejścia (np. w minutach) i dystansie (np. w metrach) pokonanym przez turystów, identyfikowanych jako t1, t2 i t3.

czas(t1, 120).

czas(t2, 90).

czas(t3, 135).

dystans(t1, 9600).

dystans(t2, 8100).

dystans(t3, 13500).

• Funktor prędkość(X, Y) pozwala policzyć średnią prędkość osoby X (lub sprawdzić, że wynosi ona Y). Zauważmy, że umieszczenie struktury „Y is D/C” jako ostatniej jest istotne; dzięki temu Prolog najpierw instancjonuje zmienne D i C przez dopasowanie do faktów, a potem wylicza (lub sprawdza) wartość Y.

prędkość(X, Y) :- czas(X, C), dystans(X, D), Y is D/C.

• Interpreterowi Prologu można teraz zadawać pytania w rodzaju:

prędkość(t1, X).

prędkość(t2, 65).

prędkość(X, 100).

• Odpowiedzi interpretera do kolejnych pytań to: X = 80, Nie, X = t3. Zauważmy, że nazwy zmiennych użytych w pytaniu (celu) nie mają związku z nazwami w programie.

Listy

• Listy w Prologu to dowolnej długości ciągi elementów (atomów, termów, także innych list).
• Składnia podobna jest do ML-a: nawiasy kwadratowe, elementy rozdzielana przecinkami.
• Nie ma jawnych funkcji do tworzenia i rozkładania list.
• Z uwagi na dopasowywanie, wystarcza odpowiednie użycie zapisu [X | Y], gdzie X jest głową, a Y — ogonem listy.

Przykłady

• Łączenie list można zapisać tak:

append([], Lst, Lst).

append([G | L1], L2, [G | L3]) :- append(L1, L2, L3).

• Odwracanie listy:

reverse([], []).

reverse([G | Og], Lst) :- reverse(Og, Wyn), append(Wyn, [G], Lst).

• Sprawdzanie przynależności do listy:

member(El, [El | _]).

member(El, [_ | Lst]) :- member(El, Lst).

• Uwaga — znak podkreślenia oznacza anonimową zmienną, która może być dopasowana do czegokolwiek.

Przykład działania interpretera

• Rozważmy następujący program:

lubi(jan, tatry).

lubi(jan, beskidy).

lubi(jerzy, beskidy).

lubi(jerzy, bieszczady).

lubi(józef, sudety).

lubi(justyna, gświętokrzyskie).

bratniadusza(X, Y) :- lubi(X, S), lubi(Y, S), X <> Y.

• Co się dzieje, gdy zadamy pytanie bratniadusza(jan, X)?
• Następuje utożsamienie zmiennej X w definicji bratniadusza(...) z atomem jan; sytuacja jest zatem taka, jakbyśmy mieli

bratniadusza(jan, Y) :- lubi(jan, S), lubi(Y, S).

• Interpreter szuka dowodu dla pierwszego podcelu, czyli lubi(jan, S). Pierwsza możliwość to utożsamienie S z atomem tatry.
• Interpreter przechodzi do dowodu drugiego podcelu, czyli teraz lubi(Y, tatry). Jedyna możliwość to utożsamienie Y z atomem jan.
• W tej sytuacji trzeci podcel nie daje się udowodnić. Potrzebny jest nawrót.
• Nawrót do drugiego podcelu nic nie daje — nie ma alternatywnego instancjonowania dla Y, a S zostało zainstancjonowane wcześniej.
• Następuje zatem nawrót do pierwszego podcelu i alternatywne instancjonowanie zmiennej S na atom beskidy.
• W kolejnym kroku mamy ponownie utożsamienie Y z atomem jan i ponownie nawrót przy X<>Y.
• Tym razem jednak wystarcza nawrót do drugiego podcelu i alternatywne instancjonowanie Y na jerzy.
• Trzeci podcel nie stwarza teraz problemu...
• Mamy zatem X = jan, Y = jerzy, S = beskidy i odpowiedź interpretera X = jerzy.