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 $B:-A_1,A_2,\dots ,A_m,$ co należy rozumieć jako implikację $A_1\wedge A_2\wedge \dots \wedge A_m\Rightarrow B$, gdzie $A_1,A_2,ldots,A_m$ i $B$ 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 $m=0$.

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 $1\to B$ 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 :- $C_1,C_2,\dots ,C_m$). Taka mplikacja, czyli $C\to 0$, 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:

0 :- zadowolony(Z).      (1)

Pamiętając o niejawnym kwantyfikatorze możemy je zapisać dokładniej jako Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall Z: \geq \textnormal{zadowolony}(Z), \textnormal{czyli} \geq \exist Z: \textnormal{zadowolony}(Z)} .

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

zadowolony(X) :- pracuje(X, Y), małafirma (Y)      (2)

Równoważnie piszemy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall X, Y: \geq \textnormal{zadowolony}(X)\rightarrow \geq [\textnormal{pracuje}(X, Y) \wedge \textnormal{małafirma}(Y)]} . Reguła odrywania pozwala nam teraz wywnioskować zależność, która staje się nowym celem:

0 :- pracuje(Z, Y), małafirma(Y).      (3)

"Po drodze" przemianowaliśmy zmienną X na Z. Innymi słowy, Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall Z, Y: \geq \textnormal{pracuje}(Z, Y) \vee \geq \textnormal{małafirma}(Y)} . 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:

pracuje(X, Y) :- poprostupracuje(X,Y).      (4)

Reguła ta, równoważna Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall X, Y: \geq \textnormal{pracuje}(X) \rightarrow \geq \textnormal{poprostupracuje}(X, Y)} , daje nam kolejny cel:

0 :- poprostupracuje(Z, Y), małafirma(Y).      (5)

Napotykamy fakt:

poprostupracuje(jan, abcSpzoo).      (6)

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

0 :- małafirma(abcSpzoo).      (7)

Skoro jednak program zawiera fakt:

małafirma abcSpzoo).      (8)

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

0 :- 1.

      (9)

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.