%% -*- mode: latex; TeX-master: "compilerbau.tex"; -*-

\begin{slide}{Minimierung von det. Aut. (I)}

\kopf{$ $Id: min.tex,v 1.1 2011-10-16 14:06:16 waldmann Exp $ $}

Idee: Zustände zusammenlegen, die \glqq das gleiche\grqq\ tun.

Das \glqq gleich\grqq\ muß man aber passend definieren:

benutze Folge von Äquivalenz-Relationen $\sim_0, \sim_1, \ldots$ auf $Q$

\bigskip

$p \sim_k q \iff$ Zustände $p$ und $q$ verhalten sich 
für alle Eingaben der Länge $\le k$ \emph{beobachtbar} gleich:

\[ \forall w \in \Sigma^{\le k}: w \in L(A,p) \leftrightarrow w \in L(A,q). \]

äquivalent ist induktive Definition:
\begin{itemize}
\item $(p \sim_0 q) :\iff (p \in F \leftrightarrow q \in F)$
\item $(p \sim_{k+1} q) :\iff (p \sim_k q) \wedge
  \forall c\in\Sigma: T(p,c) \sim_k T(q,c)$.
\end{itemize}

\end{slide}



\begin{slide}{Minimierung von det. Aut. (II)}

Nach Definition ist jeder Relation eine Verfeinerung 
der Vorgänger: $\sim_0 \supseteq \sim_1 \supseteq \ldots$.
Da die Trägermenge $Q$ endlich ist,
kann man nur endlich oft verfeinern,
und es gibt ein $k$ mit $\sim_k = \sim_{k+1} = \ldots$.
Wir setzen $\sim := \sim_k$.

Konstruiere $A ' = (Q', S', F', T')$ mit
\begin{itemize}\itemsep 2pt
\item $Q' = Q/\sim$ (Äquivalenzklassen)
\item $S' = [s]_{\sim}$ (die Äq.-Klasse des Startzustands)
\item $F' = \{ [f]_{\sim} \mid f \in F \}$ (Äq.-Kl. v. akzt. Zust.)
\item für alle $(p,c,q)\in T: ([p]_{\sim},c,[q]_{\sim})\in T'$.
\end{itemize}

Satz: Wenn $A$ vollständig und deterministisch, \\
dann ist $A'$ ein kleinster vollst. det. Aut mit $L(A') = L(A)$.


\end{slide}
