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

From Studia Informatyczne

Wstęp

John McCarthy (1927-2011)Zobacz biografię
Enlarge
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.