Eliminacja kwantyfikatora - Quantifier elimination

Eliminacja kwantyfikatorów to pojęcie uproszczenia stosowane w logice matematycznej , teorii modeli i informatyce teoretycznej . Nieformalnie, wyrażone ilościowo stwierdzenie „ takie, że ” można postrzegać jako pytanie „Kiedy istnieje takie, że ?”, A stwierdzenie bez kwantyfikatorów można uznać za odpowiedź na to pytanie. ${\ Displaystyle \ istnieje x}$${\ displaystyle \ ldots}$${\displaystyle x}$${\ displaystyle \ ldots}$

Jednym ze sposobów klasyfikacji formuł jest ilość kwantyfikacji . Formuły o mniejszej głębokości alternatywy kwantyfikatora są uważane za prostsze, a formuły bez kwantyfikatorów za najprostsze. Teoria jest kwantyfikatorem eliminacji, gdy dla każdego wzoru istnieje inny wzór bez kwantyfikatorów, który jest równoważny do niego ( modulo tej teorii). ${\ displaystyle \ alpha}$${\ displaystyle \ alpha _ {QF}}$

Przykłady

Przykład z matematyki w szkole średniej mówi, że wielomian kwadratowy jednej zmiennej ma pierwiastek rzeczywisty wtedy i tylko wtedy, gdy jego wyróżnik jest nieujemny:

${\ Displaystyle \ istnieje x \ w \ mathbb {R}. (a \ neq 0 \ klin ax ^ {2} + bx + c = 0) \ \ \ Longleftrightarrow \ \ a \ neq 0 \ klin b ^ {2} -4ac \ geq 0}$

Tutaj zdanie po lewej stronie zawiera kwantyfikator , podczas gdy równoważne zdanie po prawej nie. ${\ Displaystyle \ istnieje x \ w \ mathbb {R}}$

Przykłady teorii, które zostały pokazane rozstrzygalne za pomocą eliminacji kwantyfikatora jest arytmetyka presburgera , ciało algebraicznie domknięte , prawdziwe zamknięte pola , atomless algebr Boole'a , termin algebry , gęste zlecenia liniowe , grupa przemienna , losowe wykresy , a także wielu ich kombinacji, takich jak Boolean algebra z arytmetyką Presburgera i algebry terminowe z kolejkami .

Eliminatorem kwantyfikatora dla teorii liczb rzeczywistych jako uporządkowanej grupy addytywnej jest eliminacja Fouriera-Motzkina ; dla teorii pola liczb rzeczywistych jest to twierdzenie Tarskiego – Seidenberga .

Eliminacja kwantyfikatora może być również wykorzystana do wykazania, że ​​„łączenie” rozstrzygających teorii prowadzi do nowych rozstrzygalnych teorii.

Algorytmy i rozstrzygalność

Jeśli teoria ma eliminację kwantyfikatora, można odpowiedzieć na konkretne pytanie: czy istnieje metoda określania dla każdego z nich ? Jeśli istnieje taka metoda, nazywamy ją algorytmem eliminacji kwantyfikatora . Jeśli istnieje taki algorytm, rozstrzygalność teorii sprowadza się do rozstrzygnięcia o prawdziwości zdań pozbawionych kwantyfikatorów . Zdania bez kwantyfikatorów nie mają zmiennych, więc często można obliczyć ich ważność w danej teorii, co umożliwia zastosowanie algorytmów eliminacji kwantyfikatorów do decydowania o ważności zdań. ${\ displaystyle \ alpha _ {QF}}$${\ displaystyle \ alpha}$

Pojęcia pokrewne

Różne koncepcje teorii modeli są związane z eliminacją kwantyfikatora i istnieją różne równoważne warunki.

Każda teoria pierwszego rzędu z eliminacją kwantyfikatorów jest modelem kompletnym . Odwrotnie, teoria modelu-zupełnego, której teoria uniwersalnych konsekwencji ma właściwość łączenia , ma eliminację kwantyfikatora.

Modele teorii uniwersalnych konsekwencji teorii są właśnie podstrukturami modeli . Teoria rzędów liniowych nie ma eliminacji kwantyfikatora. Jednak teoria jej uniwersalnych konsekwencji ma właściwość łączenia. ${\ Displaystyle T}$${\ Displaystyle T}$

Podstawowe pomysły

Aby konstruktywnie wykazać, że teoria ma eliminację kwantyfikatora, wystarczy pokazać, że możemy wyeliminować kwantyfikator egzystencjalny zastosowany do koniunkcji literałów , to znaczy pokazać, że każda formuła postaci:

${\ Displaystyle \ istnieje x. \ bigwedge _ {i = 1} ^ {n} L_ {i}}$

gdzie każdy jest literałem, jest odpowiednikiem formuły bez kwantyfikatora. Rzeczywiście, załóżmy, że wiemy, jak wyeliminować kwantyfikatory z koniunkcji literałów, to jeśli jest to formuła bez kwantyfikatorów, możemy zapisać ją w rozłącznej postaci normalnej${\ displaystyle L_ {i}}$${\ displaystyle F}$

${\ Displaystyle \ bigvee _ {j = 1} ^ {m} \ bigwedge _ {i = 1} ^ {n} L_ {ij}}$

i wykorzystaj fakt, że

${\ Displaystyle \ istnieje x. \ bigvee _ {j = 1} ^ {m} \ bigwedge _ {i = 1} ^ {n} L_ {ij}}$

jest równa

${\ Displaystyle \ bigvee _ {j = 1} ^ {m} \ istnieje x. \ bigwedge _ {i = 1} ^ {n} L_ {ij}.}$

Wreszcie, aby wyeliminować uniwersalny kwantyfikator

${\ displaystyle \ forall xF}$

gdzie jest bez kwantyfikatora, przekształcamy w dysjunktywną postać normalną i wykorzystujemy fakt, który jest równoważny${\ displaystyle F}$${\ displaystyle \ lnot F}$${\ displaystyle \ forall xF}$${\ Displaystyle \ lnot \ istnieje x. \ lnot F.}$

Związek z rozstrzygalnością

We wczesnej teorii modeli eliminacja kwantyfikatorów była wykorzystywana do wykazania, że ​​różne teorie mają właściwości, takie jak rozstrzygalność i kompletność . Powszechną techniką było pokazanie najpierw, że teoria dopuszcza eliminację kwantyfikatorów, a następnie udowodnienie rozstrzygalności lub kompletności poprzez rozważenie tylko formuł bez kwantyfikatorów. Ta technika może być wykorzystana do wykazania, że arytmetyka Presburgera jest rozstrzygalna.

Teorie mogą być rozstrzygalne, ale nie pozwalają na eliminację kwantyfikatora. Ściśle mówiąc, teoria addytywnych liczb naturalnych nie dopuszczała eliminacji kwantyfikatora, ale była to ekspansja addytywnych liczb naturalnych, która okazała się rozstrzygalna. Ilekroć teoria jest rozstrzygalna, a język jej prawidłowych wzorów jest policzalny , można rozszerzyć teorię o policzalne wiele relacji, aby wyeliminować kwantyfikator (na przykład można wprowadzić dla każdej formuły teorii symbol relacji, który wiąże wolne zmienne wzoru).

Przykład: Nullstellensatz dla algebraicznie zamkniętych ciał i różniczkowo zamkniętych ciał .

Zobacz też

• Rozkład algebraiczny cylindryczny
• Teoria eliminacji
• Eliminacja koniunkcji

Uwagi

Bibliografia

• Viktor Kuncak i Martin Rinard. „ Podtypy strukturalne typów nierekurencyjnych są rozstrzygalne ”. W osiemnastym dorocznym sympozjum IEEE na temat logiki w informatyce, 2003.