Programowanie funkcyjne i programowanie w logice

6. SEMANTYKA  DEKLARATYWNA

                            – język programu P

              – zbiór wszystkich termów bazowych języka; zbiór nazywamy

                         uniwersum Herbranda dla języka

              – zbiór wszystkich bazowych atomów języka

atom bazowy               – formuła , gdzie P jest n argumentowy symbolem relacyjnym,

DEF. Zbiór sukcesów programu.

Zbiorem sukcesów programu P nazywamy zbiór:

              .

Inaczej: składa się z tych bazowych atomów A, dla których na pytanie A? (czy A zachodzi?) dostajemy odpowiedź obliczoną TAK.

UWAGA.

Odpowiedzią obliczoną dla , gdzie , jest zawsze , bo , jeśli .

PRZYKŁAD 6.1

Dla danego programu P ilustruje  wprowadzone wyżej pojęcia.

STRUKTURY  HERBRANDA

L – język pierwszego rzędu

DEF. Interpretacja Herbranda.

Interpretacją Herbranda dla języka L nazywamy interpretację M tego języka taką, że:

              – zbiór wszystkich termów bazowych języka L.

Interpretacja symboli funkcyjnych i stałych:

              dla stałych a,

              dla  , gdzie f jest n-argumentowym

            symbolem funkcyjnym.

Zatem w interpretacji Herbranda znaczenie stałych przedmiotowych i symboli funkcyjnych jest jednoznacznie określone, natomiast symbole relacyjne można interpretować dowolnie.

FAKT 6.1.

Jeżeli M jest interpretacją Herbranda języka L, to dla każdego termu  .

Dowód  faktu 6.1.

DEF.Interpretacja Herbranda programu.

Interpretacją Herbranda programu P nazywamy interpretację Herbranda języka .

R – symbol relacyjny.

Trzeba określić .

Dla dowolnej interpretacji M i :

              .

Jeżeli M jest interpretacją Herbranda, to

              .

Określamy więc

              .

Interpretacja M jest jednoznacznie wyznaczona przez.

Przyjmujemy, że .

Interpretacje Herbranda utożsamiamy z dowolnymi podzbiorami zbioru .

Dla  :     .

DEF. Model Herbranda programu.

Interpretację Herbranda nazywamy modelem Herbranda dla programu P,

jeżeli .

FAKT 6.2.

.

Dowód  faktu 6.2

WNIOSEK

Nie istnieje atom A, taki że , tzn. z programów definitywnych nie wynika żaden fakt negatywny.

PRZYKŁAD 6.2

Interpretacje i modele Herbranda programu P.             

FAKT 6.3.

Niech P będzie programem definitywnym, – atomami a – wszystkimi zmiennymi występującymi w tych atomach. Wówczas, jeżeli

              ,

to istnieje bazowe podstawienie

              ,     ,

takie że

              .

Dowód faktu 6.3.

DEF. Interpretacja.

TWIERDZENIE 6.1.

jest najmniejszym modelem Herbranda dla programu P.

Dowód.

I.     jest modelem dla programu P.

II.    jest najmniejszym modelem Herbranda dla programu P.

KONSTRUKCJA  MODELU  .

Określamy zbiory   dla   następująco:

                 – zbiór wszystkich bazowych konkretyzacji faktów programu P.

                 = istnieją    takie, że

                                  jest bazową konkretyzacją klauzuli z

Mamy: .

Oznaczamy: .

PRZYKLAD

Konstrukcja zbioru dla programu P

Program P:

              nieparzyste

              nieparzyste nieparzyste

____________________________________________

FAKT  6.4.

Dowód Faktu 6.4.

TWIERDZENIE  6.2. Słabe twierdzenie o pełności rezolucji liniowej.

Zbiór sukcesów programu P jest równy najmniejszemu modelowi Herbranda dla tego programu, czyli

                                          .

Dowód Tw. 6.2.

Przykład do Tw. 5.2  (silne twierdzenie o pełności rezolucji liniowej).

7. SLD  –  REZOLUCJA.

Linear resolution with Selection function for Definite clauses.

Rezolucja liniowa dla programów definitywnych z regułą selekcji.

Przy korzystaniu z rezolucji liniowej możemy mówić o dwóch „stopniach swobody”:

              a) realizując cel    dowolnie wybieramy podcel

                  do realizacji,

              b) dowolnie wybieramy klauzulę C programu P, którą będziemy unifikować  

               z wybranym podcelem.

REGUŁY  SELEKCJI

DEF. Reguła selekcji.

Regułą selekcji nazywamy funkcję R, która każdej skończonej derywacji liniowej  ,  takiej, że przyporządkowuje liczbę naturalną , gdzie k jest długością .

Najczęściej stosujemy regułę , którą nazywamy LEFT FERST (lewy najpierw), tzn. w celu wybierany jest zawsze podcel .

Możemy również stosować regułę RIGHT FIRST.

DEF. SLD derywacja / refutacja.

Liniową derywację / refutację zgodną z regułą selekcji R nazywamy SLD-derywacją / refutacją

zgodną z R.

TWIERDZENIE  7.1. O nieistotności reguł selekcji.

Niezależnie od wyboru reguł selekcji otrzymamy te same odpowiedzi obliczone dla z dokładnością do wariantu, tzn. jeżeli i są regułami selekcji i jest odpowiedzią obliczoną dla zgodną z , to istnieje odpowiedź obliczona zgodna z dla taka, że jest wariantem .

PRZYKŁAD 7.1.

Reguły selekcji.
REGUŁY  PRZESZUKIWAŃ

Przyjmujemy, że program jest ciągiem klauzul , tzn. liczy się kolejność klauzul w programie.

DEF. SLD-drzewo dla zgodne z R.

SLD-drzewo dla ...