7738996306

1.2 Twierdzenie Biichiego

Pokażemy, że odpowiednią logiką do opisywania języków regularnych jest logika MSO (monadic second-order logie), która zezwala na kwantyfikowanie po elementach oraz po zbiorach elementów.

Twierdzenie 2 (Biichi 60, Elgot 61, Trachtenbrot 62). Dla języka L C A* następujące warunki są równoważne:

1. L jest regularny

2. L jest definiowalny w logice MSO(s).

Zanim udowodnimy to twierdzenie, stworzymy formułę MSO opisującą język (aa)’, co pozwoli nam dostrzec ogólną metodę konstruowania formuł MSO dla języków regularnych. Słowa o parzystej liczbie liter możemy opisać jako takie słowa, w których możemy zaznaczyć co drugą pozycję tak, by zaznaczyć pierwszą pozycję i nie zaznaczyć ostatniej. Za pomocą formuły logicznej możemy to wyrazić następująco:

!V* 3j)<a; y € X    pierwsza pozycja jest zaznaczona

V* 3y>x y 0 X    ostatnia pozycja nie jest zaznaczona

V*V_vs{x,y) -> (x € X *-* y & X) zaznaczona jest co druga pozycja

Przyjrzyjmy się teraz automatowi rozpoznającemu ten język. Automat ten ma dwa stany: akceptujący qo, będący stanem początkowym i nieakceptujący q\. Tranzycje opisane literą a prowadzą ze stanu qn do qi oraz z qi do <jo- Oznacza to, że przy wczytywaniu słowa należącego do języka, automat po wczytaniu pierwszej pozycji będzie w stanie q\, po wczytaniu ostatniej pozycji będzie w stanie go (innymi słowy — nie będzie w stanie gi), oraz będzie w stanie go co dwie pozycje. Zauważmy, że zbiór pozycji, po wczytaniu których automat przejdzie do stanu gi, jest właśnie zbiorem X spełniającym powyższą formułę. To nie przypadek.

W ogólnym przypadku będziemy tworzyć formułę na podstawie automatu rozpoznającego dany język: będziemy kwantyfikować po zbiorach wyznaczających pozycje, w których automat przechodzi daną tranzy-cją. W treści formuły wymusimy, by wyznaczone stany odpowiadały akceptującemu biegowi automatu na danym słowie. Poniżej pokażemy to w formalny sposób.

Uwaga. W powyższej formule korzystaliśmy z relacji porządku, ale nie stanowi to nadużycia — porządek jest w MSO definiowalny za pomocą następnika:

x < y — V*(z € X A (V_U'_V(u £ X A s(u, v)) —* v £ X)) —> y 6 X

(jeśli x € X i X jest zamknięty ze względu na operację następnika, to y € X).

Dowód („=>”)

Udowodnimy, że dla każdego automatu skończonego A = (Q,Qi,S,A,F) istnieje równoważna formuła ip £ MSO(s) taka, że = L^. Załóżmy, że tranzycje automatu to 6 = {(gi,oi,pi),... ,(gn,u„,Pn)}, gdzie krotka (qi,ai,pi) oznacza „automat będący w stanie g, po wczytaniu litery m przechodzi do stanu p”. Zauważmy, że każdej pozycji w słowie możemy w naturalny sposób przypisać tranzycję - tę tranzycję, którą przechodzi automat wczytując literę na danej pozycji. Bieg automatu na danym słowie możemy jednoznacznie wyznaczyć określając, na jakich pozycjach automat przechodzi daną tranzycją. Utworzymy teraz formułę, która będzie spełniona dokładnie przez te słowa, dla których istnieje akceptujący bieg automatu:

6