7738996308

Krok 2. Kiedy będziemy indukcyjnie tworzyć automaty dla podformuł naszej formuły, zauważymy, że będziemy musieli tworzyć również automaty dla formuł otwartych, tzn. postaci p{X\,..., X_n), gdzie Xi,..., X_n są zmiennymi wolnymi. Oprócz słowa będziemy więc musieli dostarczyć na wejściu naszego automatu również wartościowanie tych zmiennych (będących zbiorami pozycji w słowie). W tym celu rozszerzymy alfabet A do alfabetu A x {0, l}ⁿ: litera (a,ci,...,Cn) na pozycji p będzie oznaczała, że w rozważanym słowie na pozycji p jest litera a, oraz że p należy do JKi wtw., gdy e* = 1. Jeśli w naturalny sposób zdefiniujemy operator w <8> v, oznaczający takie właśnie podpisywanie jednego słowa pod drugim, to nowe słowo wejściowe nad rozszerzonym alfabetem będziemy mogli zapisać jako w <S> X\ ®... ® X„.

Przykładowo, dla słowa w = aababb oraz zbioru X\ będącego zbiorem liczb parzystych i zbioru X₂ będącego zbiorem liczb pierwszych uzyskamy następujące słowo nad rozszerzonym alfabetem:

w    =    a    a    b    a    b    b

Xi =    010101

X₂    =    0    1    1    0    1    o

Krok 3. Przez indukcję po rozmiarze ip(Xi,..., X_n) pokażemy, że język

L*¹.....^x" = {«> ®    ®    ® X_n :w |= ¥>(*!,..., *„)} C (4 x{0,l}ⁿ)*

jest regularny - określając automat, który go rozpoznaje.

W łatwy sposób możemy zdefiniować automaty rozpoznające atomowe formuły Xi C Xj, sing(Xj) oraz S(Xi,Xj). Na przykład automat rozpoznający Xi C Xj sprawdza, czy obecność jedynki w i-tym „wierszu” implikuje obecność jedynki w wierszu j-tym; automaty rozpoznające pozostałe dwa predykaty są równie proste.

Aby wykonać krok indukcyjny, wystarczy że znajdziemy automaty rozpoznające p V ip, ~"p oraz 3x<p(X) dla ip, ip rozpoznawanym przez automaty skończone - co jest równoważne zamkniętości języków regularnych odpowiednio na sumę, dopełnienie i rzutowanie. Zamkniętość na sumę i dopełnienie jest dobrze znanym faktem, musimy się jednak chwilę zastanowić nad tym, co właściwie oznacza rzutowanie języków regularnych.

Krok 4. Zakładając, że język zdefiniowany formułą 4*(Ai,..., X_n) jest rozpoznawany przez automat skończony A, chcemy pokazać automat dla języka:

<p(X₁,...,X_n-₁) = 3_Xrl$(X_I,...,X_n).

Szukany automat, działający nad alfabetem A x (0, l}^n_1, powinien po prostu niedeterministycznie zgadnąć ostatni wiersz zer i jedynek, definiujący zbiór X_n, i na rozszerzonym w ten sposób słowie (już nad alfabetem A x {0, l}ⁿ) powinien działać jak automat A. □

Wniosek. Udowodnione właśnie twierdzenie głosi, że dla każdej formuły MSO istnieje równoważny automat. Tworzy również dla każdego automatu równoważną mu formułę MSO postaci

3_Xl...3x_n

gdzie formuła $(Xj,... ,X_n) nie ma kwantyfikatorów po zmiennych drugiego rzędu. Oznacza to, że każda formuła MSO nad sygnaturą słów jest równoważna formule takiej właśnie postaci.