Tekst źródłowy strony Paradygmaty programowania/Wykład 14: Programowanie w logice w Prologu II

Kontynuujemy omawianie Prologu — najbardziej znanego języka programowania w logice. Tym razem chcemy bardziej szczegółowo zająć się zasadą działania interpretera. Pokażemy, że działanie to można postrzegać jako mechanizm automatycznego dowodzenia twierdzeń metodą rezolucji. Ponadto będziemy mówili o listach, będących naturalną i ważną w Prologu strukturą danych.

==Jak działa interpreter?==

Omawiając dotychczas sposób działania interpretera, nie wspominaliśmy zbyt wiele o matematycznych podstawach Prologu. Tymczasem Prolog powstał nie jako specyficzny system bazodanowy lub „dziwny interpreter do jeszcze dziwniejszych programów”, lecz jako system automatycznego dowodzenia twierdzeń, z solidnymi podstawami matematycznymi w postaci metody rezolucji. Zastosowanie Prologu do budowy baz danych lub do przetwarzania języka naturalnego to ważne, ale oczywiście nie jedyne możliwości tego języka, będące szczególnym przypadkiem dowodów przez rezolucję.

===Rezolucja===

Prześledzimy ponownie przykład udzielania odpowiedzi przez interpreter Prologu. Tym razem jednak zwrócimy baczniejszą uwagę na stosowane przy tym reguły wnioskowania.

Załóżmy, że mamy następujący program:

  poprostupracuje(jan, abcSpzoo).
  małafirma(abcSpzoo).
  zadowolony(X) :- pracuje(X, Y), małafirma(Y).
  pracuje(X, Y) :- poprostupracuje(X, Y).
  pracuje(X, Y) :- zarządza(X, Y).
  pracuje(X, Y) :- zastępujezarządcę(X, Y).

Przypomnijmy, jakie klauzule mogą występować w programie:
* Klauzule wyrażające zależności, postaci <math>B:- A_1, A_2, \ldots, A_m,</math> co należy rozumieć jako implikację <math>A_1 \wedge A_2 \wedge \ldots \wedge A_m \Rightarrow B</math>, gdzie <math>A_1, A_2, \ldots, A_m</math> i <math>B</math> są strukturami prologowymi, a wszystkie zmienne są w zasięgu niejawnego kwantyfikatora uniwersalnego.
* Klauzule stwierdzające fakty będące pojedynczymi strukturami. Także i tu zmienne (o ile występują) są w zasięgu niejawnego kwantyfikatora uniwersalnego. Jest to w istocie szczególny przypadek powyższych „ogólnych” klauzul dla <math>m = 0</math>.

Tu pora na uściślenie tego, co mówiliśmy o faktach i celach. W sensie składniowym jedne i drugie wyglądają podobnie, z tą różnicą, że cel można wpisać jako koniunkcję kilku struktur, a fakt — nie. W sensie logicznym jednak jest ważna różnica:
*Fakty można rozumieć jako ogólne klauzule, gdzie po prawej stronie znaku :- jest stwierdzenie zawsze prawdziwe. Jeśli oznaczmy je przez 1, to fakt jest klauzulą postaci B :- 1. Zauważmy, że implikacja <math>1 \Rightarrow B</math> jest równoważna po prostu B.
*Cele można rozumieć jako ogólne klauzule, gdzie po lewej stronie znaku :- jest stwierdzenie zawsze fałszywe. Jeśli oznaczymy je przez 0, to cel jest klauzulą postaci 0 :- C (lub ogólniej 0 :- <math>C_1, C_2, \ldots, C_m</math>). Taka implikacja, czyli <math>C \Rightarrow 0</math>, jest równoważna negacji celu.

Wróćmy do przykładowego programu. Jak widać, zawiera on regułę, mówiącą że jeśli ktoś pracuje w małej firmie, to jest zadowolony. Spróbujmy zadać pytanie, kto konkretnie jest więc zadowolony. Spodziewamy się oczywiście odpowiedzi, że „jan”...

Tu zaczyna się istota metody rezolucji. Otóż pytanie zadajemy (być może o tym nie wiedząc...) w formie zanegowanej; stąd właśnie wspomniana powyżej interpretacja celu jako implikacji 0 :- C. Oczywiście owego zera nie trzeba wpisywać — interpreter sam rozpoznaje kontekst. Udowodnienie celu przebiega teraz według schematu dowodu nie wprost: korzystając z posiadanego programu i negacji celu, interpreter stara się dojść do sprzeczności — co dowodzi prawdziwości celu. Dodajmy, że w praktyce często interesuje nas nie tylko samo udowodnienie celu, ale także wartości zmiennych, przy których osiągana jest prawdziwość celu. Wartości te pojawiają się tak czy inaczej w trakcie rezolucji.

Zatem nasze pytanie to:


{{wzor|pie|1|
0 :- zadowolony(Z).}}                                                                                 

Pamiętając o niejawnym kwantyfikatorze, możemy je zapisać dokładniej jako <math>\forall Z: \neg \textnormal{zadowolony}(Z), \textnormal{czyli} \neg \exists Z: \textnormal{zadowolony}(Z)</math>.

Szukamy teraz reguły pasującej do powyższego celu. Jedyna taka reguła to:


{{wzor|dru|2|
zadowolony(X) :- pracuje(X, Y), małafirma (Y)}}           


Równoważnie piszemy <math>\forall X, Y: \neg \textnormal{zadowolony}(X)\Rightarrow \neg [\textnormal{pracuje}(X, Y) \wedge \textnormal{małafirma}(Y)]</math>. Reguła odrywania pozwala nam teraz wywnioskować zależność, która staje się nowym celem:


{{wzor|trz|3|
0 :- pracuje(Z, Y), małafirma(Y).}}


„Po drodze” przemianowaliśmy zmienną X na Z. Innymi słowy, <math>\forall Z, Y: \neg \textnormal{pracuje}(Z, Y) \vee \neg \textnormal{małafirma}(Y)</math>. W dalszych poszukiwaniach trzeba więc znaleźć osobę, która pracuje w małej firmie. Zaczynamy od znalezienia kogoś, kto (w ogóle) pracuje. Pierwsza napotkana reguła to:


{{wzor|czw|4|
pracuje(X, Y) :- poprostupracuje(X,Y).}}


Reguła ta, równoważna <math>\forall X, Y: \neg \textnormal{pracuje}(X) \Rightarrow \neg \textnormal{poprostupracuje}(X, Y)</math>, daje nam kolejny cel:


{{wzor|pia|5|
0 :- poprostupracuje(Z, Y), małafirma(Y).}}
       
                                                                    
Napotykamy fakt:


{{wzor|szo|6|
poprostupracuje(jan, abcSpzoo).}}


W ten sposób dowód redukuje się do:


{{wzor|sio|7|
0 :- małafirma(abcSpzoo).}}


Skoro jednak program zawiera fakt:


{{wzor|osm|8|
małafirma(abcSpzoo).}}


... równoważny małafirma(abcSpzoo) :- 1, to otrzymujemy:


{{wzor|dzi|9|
0 :- 1.}}


Jest to pożądana sprzeczność — co kończy dowód.


Podsumujmy, jak przebiega dowód przez rezolucję. Zakładamy negację celu (bowiem rezolucja to dowód nie wprost). Następnie w poszczególnych krokach stosujemy regułę odrywania do dotychczasowego celu i klauzul programu, by otrzymać nowy cel — aż do uzyskania sprzeczności. Mówimy tu oczywiście o sytuacji, gdy dowód udało się doprowadzić do pomyślnego końca. Co będzie w przeciwnym razie — omówimy nieco później.

===Uzgadnianie (unifikacja)===

Przyjrzyjmy się teraz, jak wygląda jeden krok rezolucji — tu bowiem kryje się pominięte w powyższym przykładzie ''uzgadnianie'' (inaczej — ''unifikacja'').
*Mamy cel (lub podcel, czyli jeden z czynników koniunkcji stanowiącej cel), powiedzmy C oraz klauzulę programu <math>B :- A_1, A_2, \ldots, A_m</math>.
*Żeby dało się zastosować regułę odrywania, musimy ''uzgodnić'' (''zunifikować'') B i C.
*Polega to na znalezieniu takiego podstawienia pod zmienne w B i C, by B i C stały się identyczne; podstawienie takie zwane jest ''unifikatorem''.
*Teraz zastępujemy C przez <math>A_1, A_2, \ldots, A_m</math> i stosujemy znaleziony przed chwilą unifikator.
*W ten sposób otrzymujemy nowy cel.

Powyższy opis to sposób użycia reguły odrywania, przedstawiony z technicznymi szczegółami. W szczególności, jeśli wybrana do rezolucji klauzula to fakt (<math>m = 0</math>), to cel C zostaje zastąpiony przez zawsze prawdziwe puste ciało klauzuli, czyli „znika” — a zatem C jest udowodniony.

Na razie nie mamy ustalonego sposobu, jak wybierać podcel, gdy cel jest koniunkcją kilku podcelów oraz jak wybierać klauzulę programu. Oczywiste jest, że musimy wybrać klauzulę, której głowa daje się uzgodnić z celem (np. funktor w B musi być taki sam jak w C). Może jednak zdarzyć się, że głowy kilku klauzul dają się uzgodnić z wybranym celem. Ta kwestia nie jest rozstrzygnięta w definicji samej rezolucji, jest natomiast ustalona w Prologu — do czego niebawem wrócimy.

Zobaczmy, jak wyglądały unifikatory w przykładowej rezolucji:
*Unifikator dla (1) i (2) to [X/Z], czyli przemianowanie zmiennej X na Z (świadomie użyliśmy wcześniej nazwy Z, żeby było co przemianowywać...).
*Unifikator dla (3) i (4) to ponownie [X/Z].
*Unifikator dla (5) i (6) to [Z/jan, Y/abcSpzoo].
*Unifikator dla (7) i (8) jest pusty — nie ma tu czego unifikować.

Ciekawym zjawiskiem, z punktu widzenia programisty, jest efekt zastosowania unifikatora [X/Z] dla np. ([[#pie|1]]) i ([[#dru|2]]). Otóż jest to wspominane już utożsamienie dwóch zmiennych — tu zmiennej Z z celu ([[#pie|1]]) i zmiennej X z klauzuli ([[#dru|2]]). Generalnie, z punktu widzenia programisty, zastosowanie unifikatora to ukonkretnienie zmiennych. Innymi słowy, unifikacja to takie ukonkretnienie zmiennych, by uzyskać zgodność odpowiednich termów.

Zauważmy, że w ogólności wybór unifikatora nie jest jednoznaczny. Przykładowo, dla ([[#pie|1]]) i ([[#dru|2]]) równie dobrze można wziąć [Z/X]. Dopóki jednak chodzi tylko o przemianowywanie zmiennych, wybór ten jest bez większego znaczenia. Ważne jest natomiast, by interpreter szukał zawsze unifikatora ''najogólniejszego''; zdefiniujmy, na czym to polega.

Mówimy, że unifikator <math>\alpha</math> jest ''ogólniejszy'' niż <math>\beta</math>, jeśli istnieje podstawienie <math>\gamma</math> takie, że <math>\beta</math> daje się uzyskać jako <math>\alpha</math> z podstawieniem <math>\gamma</math>. Unifikator jest ''najogólniejszy'' dla danej pary termów, jeśli jest ogólniejszy niż jakikolwiek inny dla tej pary.

Wybór najogólniejszego unifikatora także nie jest jednoznaczny, ale nietrudno pokazać, że dwa różne najogólniejsze unifikatory różnią się tylko przemianowaniem zmiennych. Zatem wybór ten jest jednoznaczny z dokładnością do nazw zmiennych.

Rozważmy prosty przykład dwóch termów, X oraz t(Y).
*Oczywiście najogólniejszy unifikator to podstawienie [X/t(Y)].
*Nietrudno wskazać inne unifikatory, np. [X/t(abc), Y/abc].
*Gołym okiem widać, że ten pierwszy jest ogólniejszy; ten drugi da się bowiem wyrazić jako złożenie pierwszego i podstawienia [Y/abc].

Zaletą najogólniejszego unifikatora jest to, że biorąc go, nie tracimy żadnych rozwiązań, które mogą się wyłonić po bardziej szczegółowych podstawieniach. Oczywiste jest, że gdybyśmy dokonali uzgodnienia z użyciem unifikatora innego niż najogólniejszy, to niektóre rozwiązania przestałyby wchodzić w grę. W powyższym przykładzie najogólniejszy unifikator [X/t(Y)] zostawia nam pełną swobodę doboru wartości Y, natomiast [X/t(abc), Y/abc] ukonkretnia Y do atomu abc.

Stąd też kolejna obserwacja — skutkiem rezolucji może być osiągnięcie celu bez całkowitego ukonkretnienia wszystkich zmiennych. Modyfikując nieznacznie powyższy przykład, możemy napisać poniższy programik:

  s(t(_)).
  t(_).

Po wpisaniu celu s(X) dostaniemy odpowiedź X = t(Y) — czyli najogólniejszą możliwą. Notabene, druga klauzula programu nie jest właściwie potrzebna.

Uwaga techniczna: wynik wyświetlony przez interpreter może nie wyglądać tak zgrabnie ze względu na sposób nazywania nie ukonkretnionych zmiennych. O ile „X” pozostanie iksem (bo taką nazwę wpisaliśmy w celu), to np. SWI-Prolog zamiast „Y” wypisuje nazwę w rodzaju _G269... W ogólności interpreter wyświetla złożenie wszystkich zastosowanych unifikatorów, po zawężeniu do tych zmiennych, które pojawiały się we wpisanym przez użytkownika celu.

Poza szczególnym przypadkiem, unifikację da się wykonać w czasie liniowym względem sumy długości uzgadnianych termów. Ów szczególny przypadek to występowanie zmiennej w termie będącym konkretyzacją tej zmiennej, np. przy próbie uzgodnienia X i t(X) — co prowadzi do nieskończonej struktury cyklicznej. Wykrycie takich sytuacji jest algorytmicznie kosztowne, więc interpretery Prologu często tego nie robią, przerzucając odpowiedzialność na programistę...

Oczywiście nie każde dwa termy da się zunifikować. Przykładowo, nie istnieje unifikator dla termów t(1) i t(2) ani dla termów s(1, X) i s(X, 2), ani („tym bardziej”) dla termów s(X) i t(X). To jest konkretna przyczyna, dla której rezolucja może się nie powieść.

Podsumujmy: Dla danych dwóch termów (w praktyce jest to bieżący cel i głowa wybranej klauzuli programu) uzgodnienie polega na znalezieniu podstawienia pod zmienne, które sprawi, że termy te staną się identyczne. Z punktu widzenia programisty owo podstawienie to ukonkretnienie zmiennych. Uzgodnienie może okazać się niemożliwe; mówimy wtedy, że unifikacja ''zawodzi''.

===Wybór klauzul do uzgodnienia i nawroty===

Tym samym dochodzimy do pytania, w jaki sposób interpreter wybiera podcele i klauzule do unifikacji, i co się dzieje, gdy unifikacja zawodzi.

Otóż Prolog stosuje prostą zasadę. Po pierwsze, jeśli cel składa się z kilku podcelów, to udowadnia się je kolejno, od lewej do prawej. Pamiętajmy, że nawet jeśli pierwotny cel składał się tylko z jednej części, to w kolejnych krokach rezolucji najprawdopodobniej będziemy otrzymywali cele wieloczęściowe. Po drugie, jeśli w danym kroku jest do wyboru kilka klauzul, których głowy dają się uzgodnić z celem, to wybierana jest pierwsza od góry (w sensie położenia w tekście programu).

Całość można opisać jako drzewo, którego korzeniem jest pierwotny cel wpisany przez użytkownika. Potomkiem wierzchołka x jest nowy cel dający się uzyskać z x w jednym kroku rezolucji. Dla pełności obrazu, krawędź łączącą wierzchołek z uzyskanym z niego nowym celem można opatrzyć etykietą oznaczającą użytą w tym kroku klauzulę i unifikator. Zauważmy, że liściem w tym drzewie może być wierzchołek oznaczający pomyślne zakończenie rezolucji (0 :- 1) lub cel, którego nie da się z niczym uzgodnić.

Działanie interpretera to teraz konstruowanie powyższego drzewa w głąb. Co się dzieje, gdy w pewnym momencie uzgodnienie zawodzi? Interpreter wycofuje ostatni krok rezolucji, anulując poczynione wtedy uzgodnienie, i bierze następną klauzulę, której głowa daje się uzgodnić z bieżącym celem. Odpowiada to wyjściu w drzewie o jeden poziom w górę i przejściu do innego potomka. Sytuację taką nazywamy ''nawrotem''.

Po nawrocie może się okazać, że nie ma już innych klauzul, które pozwoliłyby utworzyć następnego potomka. Konieczny jest wówczas nawrót o jeden poziom wyżej i rozważenie alternatywnych klauzul na tamtym poziomie. Jeśli nawrót sięgnie aż do korzenia i nie ma alternatywnych klauzul do uzgodnienia, oznacza to "zawód globalny" — interpreter odpowiada: Nie.

Zauważmy jednak, że jeśli zadaliśmy cel zawierający zmienne, to ów zawód globalny oznacza jedynie, że nie ma już więcej odpowiedzi. Wiąże się to z mechanizmem "nawrotu po sukcesie": po dojściu rezolucji do liścia (0 :- 1) interpreter wykonuje nawrót, by móc wygenerować inne rozwiązania. Nawrót następuje zatem zawsze po dojściu do liścia — zarówno "pomyślnego", jak i "niepomyślnego". Dzięki temu, jeśli zadamy pytanie ze zmiennymi, to otrzymamy wszystkie możliwe (w sensie rezolucji) rozwiązania.

Pewną kontrolę nad mechanizmem nawrotów daje ''odcięcie''. Jest to bezargumentowy funktor zapisywany jako ! (wykrzyknik). Dojście do niego powoduje, że wszystkie uzgodnienia dokonane od chwili wykorzystania w rezolucji klauzuli zawierającej owo odcięcie do chwili dojścia do niego jako podcelu zostają uznane za ostateczne, tzn. nie mogą zostać anulowane.

Rozważmy przykładową klauzulę:

  ''a(X) :- b(X), c(X), !, d(X).''

Dojście do odcięcia uniemożliwia nawrót do podcelów b(X) i c(X). Jeśli zatem zawiedzie d(X), to zawiedzie całe a(X).

==Listy==

Dla tych, którzy zapoznali się z językami funkcyjnymi, np. z Haskellem, listy są z pewnością naturalną i wygodną strukturą danych — zwłaszcza gdy są wbudowanym mechanizmem języka, uwalniającym programistę od zarządzania pamięcią, dowiązywania wskaźników itp. Tak właśnie jest w Prologu; dodatkowo listy dobrze wkomponowują się w mechanizm uzgadniania, dzięki czemu niejednokrotnie użyteczne programy można zapisać w sposób zwarty i czytelny.

Czytelnik pamięta być może dwa ostatnie zadania z pierwszej części wykładu o Prologu. Funktory skł i koniec, które się tam pojawiły, były w istocie konstruktorami list. "Prawdziwe" listy prologowe są skonstruowane tak samo, tyle że zeroargumentowym operatorem oznaczającym listę pustą jest [], zaś operatorem składania list jest kropka. Dodatkowo w język wbudowane są udogodnienia syntaktyczne, pozwalające zapisywać listy w sposób bardziej czytelny dla ludzkiego oka. Nie zmienia to jednak faktu, że listy są szczególnym rodzajem termów, przeto podlegają takim samym regułom np. przy dopasowaniach.

Przyjrzyjmy się paru przykładom list zapisanych w sposób "zwyczajny" i "formalny":
*[abc, def, gh] to w zapisie formalnym .(abc, .(def, .(gh, [])))
*[[1, 2], [3]] — .(.(1, .(2, [])), .(.(3, []), []))
*[[[]]] — .(.([], []), [])

Zapis ułatwia też pionowa kreska. Zamiast pisać .(''głowa, ogon''), można pisać [''głowa'' | ''ogon'']. Notabene, jak widać, pierwszy element listy tradycyjnie nazywany jest głową, zaś lista złożona z pozostałych elementów — ogonem. Lista pusta nie ma głowy. Zapisu tego można również używać w nieco ogólniejszej postaci [<math>e_1, e_2, \ldots, e_n</math> |''ogon''].

Listy z powyższych przykładów można by więc również zapisać jako:
*[abc | [def | [gh | []]]]
*[ [1 | [2 | []]] | [ [3 | []] | []]]
*[[[] | []] | []]

Sens zapisu z kreską uwidacznia się oczywiście nie dla konkretnych list, lecz w dopasowaniach. Rozważmy poniższą klauzulę:

  ''złóżlistę(G, Og, [G | Og]).''

Napisaliśmy właśnie program, który może zarówno rozdzielić listę na głowę i ogon, jak i złożyć listę z podanej głowy i ogona... Rzecz polega oczywiście na odpowiednim uzgodnieniu zmiennych w chwili użycia tej klauzuli do rezolucji. Przykładowo, wpisując cel: złóżlistę(1, [2, 3], X), dostaniemy odpowiedź: X = [1, 2, 3], zaś wpisując: złóżlistę (X, Y, [1, 2, 3]), otrzymamy X = 1, Y = [2, 3].

Korzystając ze sposobności, zauważmy, jaki jest prologowy styl pisania tego, co w innych językach nazwalibyśmy funkcjami. Otóż definiujemy funktor, w którym jeden parametr (lub więcej) jest przeznaczony do wyprowadzenia wyniku. W odróżnieniu od języków imperatywnych i funkcyjnych, w Prologu nie ma jednak podziału na parametry wejściowe i wyjściowe; w obydwu przypadkach do przekazania wartości wykorzystujemy uzgadnianie. Pozwala to często pisać funktory, które w zależności od sposobu użycia wyliczają jeden z argumentów (niekoniecznie zawsze ten sam) lub sprawdzają, czy wynik jest taki, jak podano wśród parametrów. Tak właśnie jest z funktorem złóżlistę; notabene, ta definicja jest urodziwa z jeszcze jednego powodu — cała definicja mieści się w nagłówku.

Nieco inna jest sytuacja, gdy chcemy stworzyć odpowiednik predykatu (funkcji o wyniku typu logicznego). Tego typu funktory najczęściej pisze się tak, by przy wyniku pozytywnym ich użycie powiodło się, zaś przy negatywnym — zawiodło (mamy tu na myśli rezultat uzgodnienia). Przykładem takiego funktora może być poniższy funktor sprawdzający, czy podana zmienna jest listą — a ściślej, czy podana zmienna daje się uzgodnić z listą.

  ''lista([]).
  lista([_ | Og]) :- lista(Og).''

Popatrzmy na klasyczny program do sprawdzania przynależności elementu do listy.

  ''należy(X, [X | _]).
  należy(X, [_ | Og]) :- należy(X, Og).''

Ponownie otrzymujemy program "wielofunkcyjny"; za jego pomocą możemy nie tylko sprawdzać przynależność do listy, ale i przejrzeć listę, np. wpisując cel należy(X, [1, 2, 3, 4]). Pouczająca jest próba wywołania w postaci np. należy(abc, X) — proszę porównać rezultat z wynikiem ostatniego zadania z pierwszej części wykładu. Zauważmy, że dwa powyższe przykłady to programy, w których jedna klauzula to fakt, a druga opisuje zależność rekurencyjną. Jest to typowy schemat definicji funktorów działających na listach. Więcej takich przykładów pojawi się w zadaniach.