Programowanie funkcyjne i programowanie w logice
__________________________________________________________________________________________
3. UNIFIKACJA ( UZGADNIANIE).
Podstawienie złożone.
Niech
Podstawienie otrzymujemy ze zbioru
przez usunięcie:
– elementów takich, że
PRZYKŁAD 3.1.
Składanie podstawień.
DEF. Wyrażenia proste.
Wyrażeniami prostymi nazywamy termy i atomy (formuły atomowe).
Wprowadzamy oznaczenia:
E – wyrażenie proste
– zbiór zmiennych występujących w E
– ograniczenie podstawienia do zbioru ; jest to postawienie takie, że
dla oraz dla
DEF. Przemianowanie zmiennych.
Przemianowaniem zmiennych w wyrażeniu E nazywamy postawienie takie, że
dla
DEF. Wariant wyrażenia prostego.
Jeżeli jest przemianowaniem zmiennych w wyrażeniu E, to wyrażenie nazywamy wariantem wyrażenia E.
PRZYKŁAD 3.2.
Warianty.
FAKT 3.1.
Jeżeli F jest wariantem wyrażenia E, to E jest wariantem wyrażenia F.
FAKT 3.2.
Jeżeli istnieją podstawienia , takie, że i , to wyrażenie F jest wariantem wyrażenia E.
Dowód FAKTU 3.2.
DEF. Obraz zbioru przez podstawienie.
Obrazem zbioru wyrażeń S przez podstawienie nazywamy zbiór
Jeżeli , to
DEF.Unifikator zbioru wyrażeń.
Niech . Podstawienie nazywamy unifikatorem zbioru S, jeżeli ( jest jednoelementowy).
Wówczas mówimy, że podstawienie unifikuje zbiór S.
PRZYKŁAD 3.3.
Unifikator zbioru wyrażeń
DEF. Najogólniejszy unifikator zbioru wyrażeń –MGU (most general unifier)
Podstawienie nazywamy najogólniejszym unifikatorem zbioru S, jeżeli spełnia warunki:
a) jest unifikatorem zbioru S,
b) dla każdego unifikatora zbioru S istnieje podstawienie takie, że .
PRZYKŁAD 3.4.
MGU.
FAKT 3.3.
Jeżeli i są najogólniejszymi unifikatorami zbioru S, to i są wariantami.
Dowód FAKTU 3.3.
DEF. Zbiór niezgodności zbioru wyrażeń.
Niech S będzie skończonym zbiorem wyrażeń zawierającym więcej niż jedno wyrażenie: , .
Zbiór niezgodności D dla zbioru wyrażeń S tworzymy następująco.
Znajdujemy pierwszą od lewej pozycję, na której przynajmniej dwa wyrażenia ze zbioru S mają różne symbole. Na tej pozycji w każdym wyrażeniu znajduje się zmienna, stała, symbol funkcyjny lub symbol relacyjny. Z każdego wyrażenia do zbioru D włączamy to podwyrażenie, które zaczyna się na znalezionej pozycji.
Zbiór niezgodności.
FAKT 3.4.
Jeżeli D jest zbiorem niezgodności dla zbioru S oraz podstawienie unifikuje zbiór S, to unifikuje zbiór D.
Dowód FAKTU 3.4.
FAKT 3.5.
Niech D będzie zbiorem niezgodności dla S. Jeżeli podstawienie unifikuje zbior S, to istnieje zmienna x i term t, nie zawierający zmiennej x ( ) takie, że oraz .
Dowód FAKTU 3.5.
Algorytm 3.1. Algorytm unifikacji – procedura poszukiwania MGU
Wejście: skończony zbiór wyrażeń prostych S
Wyjście: MGU dla S, jeśli S jest unifikowalny; nie , w przeciwnym przypadku.
1) .
2) Wyznaczamy zbiór .
Jeżeli jest jednoelementowy, to STOP; wyjście: .
W przeciwnym przypadku wyznaczamy zbiór niezgodności dla .
3) Wybieramy w zbiorze parę x, t taką, że , oraz ,
przyjmujemy i wracamy do punktu 2) algorytmu przy .
Jeżeli nie ma takiej pary, to STOP; wyjście nie.
TWIERDZENIE 3.1. O unifikacji.
Jeżeli zbiór S jest unifikowalny, to algorytm kończy pracę z wyjściem będącym MGU zbioru S. Jeżeli S nie jest unifikowalny, to algorytm kończy pracę z wyjściem nie.
PRZYKŁAD 3.5.
Unifikacja zbioru wyrażeń.
_________________________________________________________________________________________
Maria Bulińska 25
Wujek_Misiek