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

Wstęp

John McCarthy (1927-2011)
Zobacz biografię

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 $\neg$, alternatywa $\vee$, koniunkcja $\wedge$, równoważność $\Leftrightarrow$, implikacja $\Rightarrow /\Leftarrow$).
• W stwierdzeniach mogą pojawiać się zmienne związane kwantyfikatorami (uniwersalny $\forall$, egzystencjalny $\exists$).

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:

     $A_{1}\vee A_{2}\vee \ldots \vee A_{m}\Rightarrow B_{1}\wedge B_{2}\wedge \ldots \wedge B_{n},$

gdzie $A_{i}$ i $B_{i}$ są termami.

• $A_{1}\vee A_{2}\vee \ldots \vee A_{m}$ to poprzednik klauzuli, zaś $B_{1}\wedge B_{2}\wedge \ldots \wedge B_{n}$ — 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 (dla $m$ > 0) lub fakty (dla $m$ = 0).
• Klauzule z pustym następnikiem („bez głowy”) są używane do wyrażenia celu — czyli tego, co ma zostać udowodnione.

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 $\Rightarrow$ Q oraz R $\Rightarrow$ S, wnioskujemy że P $\Rightarrow$ S, o ile tylko Q i R dają się zunifikować.
• Z technicznego punktu widzenia, osiąga się to przez wyliczenie Q $\wedge$ S oraz P $\vee$ 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ą.
• Pojedyncza struktura z kropką na końcu to fakt (tzn. zakładamy, że stwierdzenie jest prawdziwe).
• Stwierdzenie zawierające następnik będący pojedynczą strukturą i poprzednik będący strukturą lub koniunkcją kilku struktur to zależność; zapisujemy ją z kropką na końcu, a następnik od poprzednika oddzielamy znakiem „:-”.
• Przykłady:

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

• Można przyjąć, że przed 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.
• Formalnie jest to klauzula bez głowy; składniowo wygląda tak samo, jak fakt.
• 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 rozdzielone 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.