Krata subsumcji
Krata subsumpcji to struktura matematyczna używana w teoretycznych podstawach zautomatyzowanego dowodzenia twierdzeń i innych symbolicznych zastosowaniach obliczeniowych.
Definicja
Mówimy, że termin t 1 obejmuje termin t 2, jeśli istnieje podstawienie σ takie, że σ zastosowane do t 1 daje t 2 . W tym przypadku t1 jest również nazywane bardziej ogólnym niż t2 , a t2 jest nazywane bardziej szczegółowym niż t1 lub przypadkiem t1 .
Zbiór wszystkich terminów (pierwszego rzędu) nad danym podpisem można utworzyć jako siatkę nad częściową relacją porządku „ … jest bardziej szczegółowa niż… ” w następujący sposób:
- uznać dwa terminy za równe, jeśli różnią się tylko nazewnictwem zmiennych,
- dodać sztuczny element minimalny Ω ( termin przeokreślony ), który jest uważany za bardziej szczegółowy niż jakikolwiek inny termin.
Ta krata jest nazywana kratą subsumcji. Mówimy, że dwa terminy są unifikowalne, jeśli ich spotkanie różni się od Ω.
Nieruchomości
Złączenie i operacja spotkania w tej sieci nazywane są odpowiednio antyunifikacją i unifikacją . Zmienna x i sztuczny element Ω są odpowiednio górnym i dolnym elementem sieci. Każdy wyraz podstawowy , czyli każdy wyraz bez zmiennych, jest atomem sieci. Sieć ma nieskończone zstępujące łańcuchy , np. x , g ( x ), g ( g ( x )), g ( g ( g ( x ))), ..., ale nie nieskończone rosnące.
Jeśli f jest symbolem funkcji binarnej, g jest symbolem funkcji jednoargumentowej, a x i y oznaczają zmienne, to wyrazy f ( x , y ), f ( g ( x ), y ), f ( g ( x ), g ( y )), fa ( x , x ) i fa ( g ( x ), g ( x )) tworzą minimalną sieć niemodułową N 5 (patrz rys. 1); jego wygląd zapobiega modułowości sieci subsumpcji , a tym samym rozdzielności .
Zbiór terminów dających się ujednolicić z danym terminem nie musi być domknięty pod względem spełnienia; Fotka. 2 pokazuje kontrprzykład.
Oznaczając przez Gnd( t ) zbiór wszystkich podstawowych wystąpień terminu t , zachodzą następujące właściwości:
- t równa się połączeniu wszystkich członków Gnd( t ), zmiana nazwy modulo,
- t 1 jest przypadkiem t 2 wtedy i tylko wtedy, gdy Gnd( t 1 ) ⊆ Gnd( t 2 ),
- terminy z tym samym zestawem wystąpień naziemnych są równe przemianowaniu modulo,
- jeśli t jest spotkaniem t 1 i t 2 , to Gnd( t ) = Gnd( t 1 ) ∩ Gnd( t 2 ),
- jeśli t jest połączeniem t 1 i t 2 , to Gnd( t ) ⊇ Gnd( t 1 ) ∪ Gnd( t 2 ).
„Podsieć” terminów liniowych
Zbiór terminów liniowych , czyli terminów bez wielokrotnych wystąpień zmiennej, jest podpozycją sieci subsumcji i sam jest kratą. Ta sieć również zawiera N5 i minimalną nierozdzielną sieć M3 jako podsieci (patrz Rys. 3 i Rys. 4), a zatem nie jest modularna, nie mówiąc już o rozdzielczej.
Operacja meet daje zawsze ten sam wynik w siatce wszystkich wyrazów, jak w siatce wyrazów liniowych. Operacja łączenia w sieci wszystkich terminów daje zawsze instancję łączenia w sieci terminów liniowych; na przykład (podstawowe) wyrazy f ( a , a ) i f ( b , b ) mają połączenie f ( x , x ) i f ( x , y ) odpowiednio w sieci wszystkich wyrazów iw kratach liniowych. Ponieważ operacje łączenia na ogół się nie zgadzają, krata liniowa nie jest właściwie podsiecią sieci wszystkich wyrazów.
Złączenie i spotkanie dwóch właściwych wyrazów liniowych, tj. ich antyunifikacji i unifikacji, odpowiada odpowiednio przecięciu i zsumowaniu ich zbiorów ścieżek . Dlatego każda podsieć sieci wyrazów liniowych, która nie zawiera Ω, jest izomorficzna z siecią zadaną, a zatem rozdzielcza (patrz rys. 5).
Pochodzenie
Najwyraźniej sieć subsumpcji została po raz pierwszy zbadana przez Gordona D. Plotkina w 1970 roku.