TFA: Korektury

03-recursive/recursive.tex

@@ -901,36 +901,51 @@ narazili jsme na \em{obousměrný konečný automat} neboli TFA \em{(two-way fin
 Nebyl by to výstižnější model výpočtů v~konstantním prostoru než konečný automat?
 Nyní dokážeme, že to vyjde nastejno -- každý jazyk přijímaný obousměrným automatem je regulární.
 
-Připomeňme definici: TFA je Turingův stroj, který dostane vstup $\|<|\alpha\|>|$
+\theorem{Obousměrné konečné automaty přijímají právě regulární jazyky.}
+
+\proof
+Připomeňme definici TFA: je to Turingův stroj, který dostane vstup $\|<|\alpha\|>|$
 a nemá ho povoleno měnit. Navíc na levé zarážce~$\|<|$ nesmí vykonat pohyb doleva
 a na pravé zarážce~$\|>|$ nesmí jít doprava. Aby byl TFA podobnější konečným automatům,
 výpočet začíná s~hlavou na prvním znaku slova~$\alpha$. To je ale detail: TFA můžeme snadno upravit,
 aby výpočet začínal na~$\|<|$ -- stačí přidat nový počáteční stav, v~němž provedeme jeden pohyb
 hlavou doprava a přejdeme do původního počátečního stavu.
 
-Uvažme TFA rozpoznávající nějaký jazyk~$L$.
-Nechť $\alpha$ značí vstup automatu a $n$ jeho délku.
-Dodefinujme $\alpha[-1] = \|<|$ a $\alpha[n] = \|>|$.
+Každý regulární jazyk je určitě přijímán nějakým TFA, který vznikne přímočarým
+překladem příslušného DFA. Opačná implikace je méně triviální.
+Uvažme TFA rozpoznávající nějaký jazyk~$L$ a jeho výpočet nad nějakým vstupem~$\alpha$
+délky~$n$. Do vstupu ještě doplníme zarážky $\alpha[-1] = \|<|$ a $\alpha[n] = \|>|$.
 
-Představme si, že jsme někde uvnitř výpočtu, hlava stojí na $i$-tém políčku slova~$\alpha$,
-stroj se právě přepíná ze stavu~$s$ do~$s'$ a chystá se odejít doprava do nějakého suffixu $\alpha[i+1:{}]$.
+Potřebujeme se nějak vyrovnat s~tím, že automat se může během výpočtu na jedno
+políčko vracet opakovaně. Představme si, že se díváme dovnitř výpočtu, hlava zrovna stojí
+na $i$-tém políčku slova~$\alpha$, stroj se právě přepíná ze stavu~$s$ do~$s'$ a chystá se
+odejít doprava do nějakého suffixu $\alpha[i+1:{}]$.
 Jak bude výpočet pokračovat? Jedna možnost je, že se stroj po čase vrátí zprava na $i$-té políčko v~nějakém novém stavu,
 přičemž nic kromě stavu stroje se nezměnilo (na pásku nemůžeme zapisovat).
 Nebo se předtím stroj stihl zastavit a přijmout/odmítnout.
 Případně se stroj zacyklil v~nekonečné smyčce, což rovněž odpovídá odmítnutí vstupu.
 
-Formálně můžeme chování stroje na suffixu vstupu $\alpha[i:{}]$ popsat nějakou funkcí~$f_i(s)$,
-která počátečnímu stavu~$s\in Q\setminus\{q_+, q_-\}$ přiřadí stav~$s'\in Q$, v~němž stroj odchází
-ze suffixu doleva. Pokud je $s=q_+$, stroj se místo odejití doleva zastavil a přijal.
-Pokud $s=q_-$, stroj odmítl zastavením nebo zacyklením se.
+Z~této úvahy plyne, že kdybychom znali chování stroje na suffixu $\alpha[i+1:{}]$
+(jakému vstupnímu stavu odpovídá jaký výstupní), mohli bychom pomocí něj určit,
+co bude stroj dělat na políčku~$\alpha[i]$, aniž bychom se dívali na následující
+znaky. Z~toho bychom mohli určit chování na suffixu $\alpha[i:{}]$ a tak dále.
+Zkusme to provést.
+
+Chování stroje na suffixu vstupu $\alpha[i:{}]$ popíšeme nějakou funkcí~$f_i(s)$.
+Ta dostane počáteční stav~$s\in Q\setminus\{q_+, q_-\}$, v~němž stroj vstoupí
+na $\alpha[i]$. Výsledkem funkce je koncový stav~$s'\in Q$, v~němž stroj odchází
+ze suffixu doleva. Pokud je $s'=q_+$, stroj se místo odejití doleva zastavil a přijal.
+Pokud $s'=q_-$, stroj odmítl zastavením nebo zacyklením se.
 
 Ukážeme, jak sestrojit funkci~$f_i$, pokud už známe~$f_{i+1}$.
-Chceme-li stanovit $f(s)$, budeme konstruovat posloupnost stavů $s_0$, $s_1$, $s_2$, \dots.
+Chceme-li stanovit $f(s)$, budeme konstruovat posloupnost stavů $s_0$, $s_1$, $s_2$, \dots{}
+při jednotlivých návštěvách políčka $\alpha[i]$.
 Na počátku položíme $s_0=s$.
 
-Nechť známe~$s_j$. Podíváme se, co stroj provede, přečte-li ve stavu~$s_j$ znak~$\alpha[i]$.
+Nyní budeme z~libovolného~$s_j$ počítat $s_{j+1}$.
+Podíváme se, co stroj provede, přečte-li ve stavu~$s_j$ znak~$\alpha[i]$.
 Vyhodnotíme tedy přechodovou funkci $\delta(s_j, \alpha[i])$, čímž získáme instrukci, která
-přechází do stavu~$s'_j$, zapisuje nezměněný znak~$\alpha[i]$ a možná pohybuje hlavou:
+přechází do nějakého stavu~$s'_j$, zapisuje nezměněný znak~$\alpha[i]$ a možná pohybuje hlavou:
 
 \list{o}
 \:Pokud hlava odchází doleva, položíme $f_i(s) = s'_j$ a jsme hotovi.
@@ -945,7 +960,7 @@ stav roven $q_+$, $q_-$, případně některému z~předchozích stavů v~poslou
 
 Všimněte si, že funkce~$f_i$ je jednoznačně určena funkcí~$f_{i+1}$ a znakem $\alpha[i]$.
 To nám dává návod na sestrojení konečného automatu, který bude procházet vstupem zprava doleva
-a postupně přepočítávat funkci~$f_i$. Stavy automaty odpovídají všem funkcím z~$Q\setminus\{q_+,q_-\}$ do~$Q$,
+a postupně přepočítávat funkci~$f_i$. Stavy automatu odpovídají všem funkcím z~$Q\setminus\{q_+,q_-\}$ do~$Q$,
 takže jich je konečně mnoho.
 
 Zbývá dořešit, jak automat začne a jak skončí.
@@ -956,8 +971,12 @@ pohybovat doprava. Funkce~$f_n$ je tedy nezávislá na vstupu, takže může pos
 počáteční stav automatu.
 
 Až automat přečte levou zarážku~$\|<|$, bude jeho stav roven funkci~$f_{-1}$.
-Nyní do této funkce dosadíme počáteční stav~$q_0$ původního TFA.
-Je-li $f_{-1}(q_0)$ rovno~$q_+$, vstup přijmeme, jinak odmítneme.
+Ta popisuje chování na celém vstupu. Takže do ní chceme dosadit počáteční stav~$q_0$
+původního TFA.
+Je-li $f_{-1}(q_0)$ rovno~$q_+$, vstup přijmeme.
+Pokud je rovno~$q_-$, tak odmítneme.
+Nic jiného nemůže funkce vrátit, protože by to znamenalo, že automat z~\|<| odešel doleva, a~to nesmí.
+Přijímací stavy tedy odpovídají těm funkcím~$f$, pro něž je $f(q_0)=q_+$.
 
 Tím jsme sestrojili automat dosvědčující regularitu. Ovšem ne původního jazyka~$L$,
 nýbrž jazyka $L' = L\rev\cdot\{\|<|\}$, v~němž jsou slova pozpátku a ukončená zarážkou.
@@ -966,7 +985,9 @@ Teď si stačí uvědomit, že z~regularity~$L'$ plyne regularita~$L\rev$ a z~n
 Regularitu $L\rev$ můžeme zdůvodnit cvičením \exref{quotex}, protože $L\rev$ je kvocient $L' / \{\|<|\}$.
 Nebo to lze provést přímo úpravou koncových stavů: za koncové prohlásíme ty stavy, z~nichž vede přechod
 před znak~$\|<|$ do některého z~původních koncových stavů.
-Regularitu~$L$ dostaneme z~uzavřenosti regulárních výrazů na otočení (cvičení \exref{regrev}).
+Regularitu~$L$ dostaneme z~uzavřenosti regulárních jazyků na otočení (cvičení \exref{regrev}).
+
+\qed
 
 \exercises