Jakie jest minimalne rozszerzenie FO, które obejmuje klasę zwykłych języków?

Kontekst: relacje między logiką a automatami

Twierdzenie Büchiego stwierdza, że logika Monadic drugiego rzędu nad łańcuchami (MSO) przechwytuje klasę zwykłych języków. Dowód faktycznie pokazuje, że egzystencjalne MSO ( $\exists\text{MSO}$ lub EMSO ) nad łańcuchami wystarczy do przechwycenia zwykłych języków. Może to być nieco zaskakujące, ponieważ w ogólnych strukturach MSO jest bardziej wyraziste niż . $\exists\text{MSO}$

Moje (oryginalne) pytanie: minimalna logika dla zwykłych języków?

Czy istnieje logika, która w ciągu ogólnych struktur, jest ściśle mniej wyraziste niż $\exists\text{MSO}$ , ale to nadal oddaje klasę języków regularnych gdy rozpatrywana przez strun?

W szczególności chciałbym wiedzieć, jaki fragment języków zwykłych jest przechwytywany przez FO nad ciągami, gdy jest rozszerzany za pomocą operatora o najmniej ustalonym punkcie (FO + LFP). Wygląda na naturalnego kandydata na to, czego szukam (jeśli nie jest to $\exists\text{MSO}$ ).

Pierwsza odpowiedź

Zgodnie z odpowiedzią @ makoto-kanazawa , zarówno FO (LFP), jak i FO (TC) przechwytują więcej niż zwykłe języki, gdzie TC jest operatorem przechodniego zamykania relacji binarnych. Okaże się, czy TC może zostać zastąpiony przez innego operatora lub zestaw operatorów w taki sposób, że rozszerzenie przechwytuje dokładnie klasę zwykłych języków i żadnych innych.

Sama logika pierwszego rzędu, jak wiemy, nie wystarczy, ponieważ przechwytuje języki bez gwiazdek, odpowiednią podklasę zwykłych języków. Jako klasyczny przykład, język parzystości nie można wyrazić przy użyciu zdania FO. $\;\;=(aa)^*$

Zaktualizowane pytanie

Oto nowe brzmienie mojego pytania, które pozostaje bez odpowiedzi.

Jakie jest minimalne rozszerzenie logiki pierwszego rzędu, tak że FO + to rozszerzenie, po przejęciu ciągów, przechwytuje dokładnie klasę zwykłych języków?

W tym przypadku rozszerzenie jest minimalne, jeśli jest najmniej wyraziste (po przejęciu ogólnych struktur) spośród wszystkich rozszerzeń przechwytujących klasę zwykłych języków (po przejęciu ciągów).

— Janoma
źródło

Jeśli się nie mylę,

calculus jest rzeczywiście równoważny MSO z łańcuchami.

μ

$\mu$

— Sylvain

@Sylvain, jakieś odniesienia? Nic nie wiem o

-calculus.

μ

$\mu$

— Janoma

Wydaje się, że zostało to udowodnione w dx.doi.org/10.1109/LICS.1988.5137 dla nieskończonego drzewa oraz w dx.doi.org/10.1007/3-540-61604-7_60 dla równoważności z niezmiennym bisimulacją fragmentem MSO ponad dowolnymi strukturami.

— Sylvain,

Spoglądam na drugi artykuł, choć obawiam się, że wiele koncepcji jest dla mnie nowych. W szczególności nie wiedziałem o systemach przejściowych niezmiennych bisimulacji. Wygląda na to, że DFA są szczególnymi przypadkami systemu przejściowego, ale nie wiem, czy są niezmienne bisimulacyjne. Jeśli tak, to odpowiadałoby na część mojego pytania (dla zwykłych języków mogłaby istnieć inna, mniej ekspresyjna logika); jeśli tak nie jest, myślę, że nic nie można powiedzieć, ponieważ nadal może istnieć równoważność przy rozważaniu tylko łańcuchów.

— Janoma

Dwa skończone słowa , postrzegane jako układy przejściowe, są dwupodstawowe, jeśli są izomorficzne. (W notacjach drugiego artykułu słowo

można postrzegać jako układ przejściowy

a_{1} \dots a_{n}

$a_1\cdots a_n$

Σ^{*}

$\Sigma^\ast$

Σ = 2^{P r o p}

$\Sigma=2^{\mathit{Prop}}$

⟨ {1, \dots, n}, 1, {(i, i + 1) ∣ i < n}, {i ∣ p \in a_{i}}_{p \in P r o p} ⟩

$\langle\{1,\dots,n\},1,\{(i,i+1)\mid i<n\},\{i\mid p\in a_i\}_{p\in\mathit{Prop}}\rangle$

— Sylvain

Odpowiedzi:

FO (LFP) przechwytuje PTIME na uporządkowanych strukturach, a łańcuchy są uporządkowanymi strukturami. Tak więc języki definiowane przez FO (LFP) obejmują wszystkie zwykłe języki i wiele więcej. http://dx.doi.org/10.1016/S0019-9958(86)80029-8

Podręcznik Ebbinghausa i Fluma zawiera ćwiczenie, w którym prosi się o pokazanie FO (TC ^ 1) (logika pierwszego rzędu rozszerzonego o przechodnie zamykanie relacji binarnych) jest równoważne MSO na łańcuchach. W tym samym ćwiczeniu jako przykład użyto aby pokazać, że FO (TC ^ 2) jest bardziej wyraziste niż MSO na łańcuchach. Wszystkie formuły FO (TC) są wyraźnie równoważne formułom FO (LFP). $\{ a^n b^n \mid n \geq 1 \}$

— Makoto Kanazawa
źródło

Doskonały. Nie wiem, co masz na myśli przez TC ^ 1 i TC ^ 2, czy to literówka? O ile wiem, w książce wspominasz, że użyto notacji FO (TC) do rozszerzenia FO z zamknięciem przechodnim i FO (DTC) do rozszerzenia FO z deterministycznym zamknięciem przechodnim , która jest zdefiniowana inaczej. Jednak nie znalazłem wspomnianego ćwiczenia. Pozostaje sprawdzić, czy istnieje operator mniej wyrazisty niż TC, który wciąż pozwala na przechwytywanie zwykłych języków. Odpowiednio zaktualizuję moje pytanie.

— Janoma

Ta odpowiedź jest nieco spóźniona, ale wiadomo, że można uzyskać wszystkie i tylko zwykłe języki, dołączając uogólniony kwantyfikator grupy dla każdej grupy skończonej (lub równoważnie dla każdej skończonej prostej grupy). Np. Patrz „Zwykłe języki definiowane przez Lindstrom Quantifiers” autorstwa Zoltana Esiky i Kim G. Larsen, pod adresem http://www.brics.dk/RS/03/28/BRICS-RS-03-28.pdf .

Co więcej, jest to optymalne w tym sensie, że zwykły język będzie definiowalny tylko wtedy, gdy dostępne będą kwantyfikatory dla każdej grupy dzielącej jego monoid składniowy.

— Ben Standeven
źródło

To ćwiczenie 8.6.3 na stronie 221 drugiego wydania podręcznika Ebbinghaus i Fluma „ Teoria modeli skończonych” . Notacja FO (TC $^r$ ) jest tam wyjaśnione. FO (TC $^r$ ) może tworzyć przechodnie zamknięcie $2r$ relacja -aryjna, traktowana jako relacja binarna $r$ -platki

Znalazłem kilka referencji, które mogą Cię zainteresować.

FO (TC $^1$ ) nazywa się FO (MTC) (logika pierwszego rzędu z monadycznym zamknięciem przechodnim) w dziesięciu artykułach Cate i Segoufin z 2010 r . Dowodzi to między innymi, że FO (MTC) jest ściśle mniej wyraziste niż MSO na skończonych drzewach.

Artykuł Bargury i Makowsky'ego z 1992 r. Pokazuje, że deterministyczne monadyczne przechodnie przechodnie - FO (DTC $^1$ ) w notacji Ebbinghaus i Flum - wystarczy zdefiniować zwykłe języki strunowe (patrz Twierdzenie 5 w tym artykule).

— Makoto Kanazawa
źródło