free-plain-ndet.tex

   1 \subsection{áËÓÉÏÍÙ ÁÌÇÅÂÒÙ ëÌÉÎÉ}\label{sec:KA-axioms}
   2
   3 \begin{definition}[\cite{KA-regevents-complete,KAT-complete-decidable,KA-modular-elimination}]
   4   \label{def:KA}
   5   \tING{áÌÇÅÂÒÁ ëÌÉÎÉ}\T ÜÔÏ ÓÔÒÕËÔÕÒÁ $(K; +, \cdot, ^*, 0, 1)$,
   6   ÔÁËÁÑ, ÞÔÏ
   7   \begin{itemize}
   8   \item $(K; +, \cdot, 0, 1)$ Ñ×ÌÑÅÔÓÑ \tD{ÉÄÅÍÐÏÔÅÎÔÎÙÍ
   9       ÐÏÌÕËÏÌØÃÏÍ}{def:ISr},
  10   \item É ÓÏÂÌÀÄÁÀÔÓÑ ÄÏÐÏÌÎÉÔÅÌØÎÙÅ Ó×ÏÊÓÔ×Á:
  11     \begin{align}
  12       1 + xx^* &= x^*
  13       &&\text{(*--1)}
  14       \label{eq:KA1}\\
  15       1 + x^*x &= x^*
  16       &&\text{(*--2)}
  17       \label{eq:KA2}\\
  18       y + xz \leq z &\implic x^*y \leq z
  19       &&\text{(*--3)}
  20       \label{eq:KA3}\\
  21       y + zx \leq z &\implic yx^* \leq z
  22       &&\text{(*--4)}
  23       \label{eq:KA4}
  24     \end{align}
  25     üÔÏ\T \emph{ÁËÓÉÏÍÙ ÁÌÇÅÂÒÙ ëÌÉÎÉ ÄÌÑ *}.
  26   \end{itemize}
  27
  28   úÄÅÓØ $\leq$\T ÅÓÔÅÓÔ×ÅÎÎÙÊ ÞÁÓÔÉÞÎÙÊ ÐÏÒÑÄÏË, ÉÎÄÕÃÉÒÏ×ÁÎÎÙÊ ÎÁ
  29   ÉÄÅÍÐÏÔÅÎÔÎÏÍ ÐÏÌÕËÏÌØÃÅ $(K; +, \cdot, 0, 1)$ ÓÔÒÕËÔÕÒÏÊ ×ÅÒÈÎÅÊ
  30   ÐÏÌÕÒÅÛ£ÔËÉ~$\Stru{K; +, 0}$:
  31   \begin{equation}\label{eq:KA-order}
  32     x \leq y \equivdef x + y = y, \tag{\ref{eq:ISr-order}}
  33   \end{equation}
  34   Á $\sup$ ÂÕÄÅÔ ÏÂÏÚÎÁÞÁÔØ ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÊ ÓÕÐÒÅÍÕÍ.
  35
  36   \KA ÏÂÏÚÎÁÞÁÅÔ \tING{ËÁÔÅÇÏÒÉÀ ÁÌÇÅÂÒ ëÌÉÎÉ É ÉÈ ÇÏÍÏÍÏÒÆÉÚÍÏ×}.
  37 \end{definition}
  38 (úÄÅÓØ É ÄÁÌØÛÅ ×ÍÅÓÔÏ $x \cdot y$ ÐÉÛÅÔÓÑ ÐÒÏÓÔÏ $xy$.
  39 ðÒÉ ÞÔÅÎÉÉ ×ÙÒÁÖÅÎÉÊ ÐÒÉÏÒÉÔÅÔ ÏÐÅÒÁÃÉÊ ÔÁËÏÊ: $^*, \cdot, +$, ÔÁË ÞÔÏ <<$x + yz^*$>>
  40 ÞÉÔÁÅÔÓÑ ËÁË <<$x + (y \cdot (z^*))$>>. úÎÁË <<\KA>> ÍÙ ÉÎÏÇÄÁ ÂÕÄÅÍ
  41 ÐÉÓÁÔØ ×ÍÅÓÔÏ ÓÌÏ× <<ÁÌÇÅÂÒÁ ëÌÉÎÉ>>.)
  42
  43 \begin{remark}[\cite{KAT-complete-decidable,KA-regevents-complete}]
  44   ÷ÍÅÓÔÏ KA3~\eqref{eq:KA3} É KA4~\eqref{eq:KA4}
  45   ÍÏÖÎÏ ÂÙÌÏ ÂÙ ×ÚÑÔØ ÜË×É×ÁÌÅÎÔÎÙÅ
  46   ÁËÓÉÏÍÙ:
  47   \begin{align}
  48     xz \leq r &\implic x^* z \leq z
  49     &&\text{(*--3$'$)}
  50     \label{eq:KA3'}\tag{$\ref{eq:KA3}'$}\\
  51     zx \leq z &\implic z x^* \leq z.
  52     &&\text{(*--4$'$)}
  53     \label{eq:KA4'}\tag{$\ref{eq:KA4}'$}
  54   \end{align}
  55 \end{remark}
  56
  57 \todo{[* -- ÍÏÄÅÌÉÒÏ×ÁÎÉÅ ÐÒÏÇÒÁÍÍ (ÃÉËÌÏ×);
  58   ÉÓÓÌÅÄÏ×ÁÎÉÅ ëá ÓÆÏËÕÓÉÒÏ×ÁÎÏ ÎÁ ÎÅÊ.]}
  59 éÎÔÕÉÔÉ×ÎÏÅ ÐÏÎÉÍÁÎÉÅ ÓÍÙÓÌÁ ÏÐÅÒÁÃÉÉ $^*$ ÔÁËÏ×Ï:
  60 \begin{align*}
  61   y^* &= 1 + y + y^2 + \dotsb,
  62   \intertext{ÉÌÉ × ÂÏÌÅÅ ÏÂÝÅÍ ×ÉÄÅ:}
  63   xy^*z &= 1 + xyz + xy^2z + \dotsb;
  64 \end{align*}
  65 ÅÇÏ ÏÔÒÁÖÁÅÔ ÓÌÅÄÕÀÝÅÅ ÏÐÒÅÄÅÌÅÎÉÅ.
  66 \begin{definition}[\cite{KAT-complete-decidable,KA-regevents-complete}]
  67   áÌÇÅÂÒÁ ëÌÉÎÉ Ñ×ÌÑÅÔÓÑ \tING{*\dÎÅÐÒÅÒÙ×ÎÏÊ}, ÅÓÌÉ ÏÎÁ ÕÄÏ×ÌÅÔ×ÏÒÑÅÔ
  68   ÓÌÅÄÕÀÝÅÍÕ \todo{[inifinitary]} ÕÓÌÏ×ÉÀ:
  69   \begin{align}
  70     \label{eq:KA*}
  71     xy^*z &= \sup_{n \in \bbN \cup \{ 0 \}} x y^n z,
  72     &&\text{(*\dÎÅÐÒÅÒÙ×ÎÏÓÔØ)}
  73   \end{align}
  74   ÇÄÅ
  75   \begin{align*}
  76     y^0 &\eqdef 1
  77     & y^{n+1} &\eqdef yy^{n}.
  78   \end{align*}
  79   \KAc ÏÂÏÚÎÁÞÁÅÔ \tING{ËÁÔÅÇÏÒÉÀ *\dÎÅÐÒÅÒÙ×ÎÙÈ ÁÌÇÅÂÒ ëÌÉÎÉ É ÉÈ ÇÏÍÏÍÏÒÆÉÚÍÏ×}.
  80 \end{definition}
  81 \begin{remark}[\cite{KAT-complete-decidable}]
  82   ÷ ÐÒÉÓÕÔÓÔ×ÉÉ ÏÓÔÁÌØÎÙÈ ÁËÓÉÏÍ ÉÚ ÕÓÌÏ×ÉÑ *\dÎÅÐÒÅÒÙ×ÎÏÓÔÉ~\eqref{eq:KA*}
  83   ÓÌÅÄÕÀÔ\marginpar{ÓÅÍ. ÓÌÅÄÕÀÔ?}
  84   \eqref{eq:KA3}, \eqref{eq:KA4}, \eqref{eq:KA3'}, \eqref{eq:KA4'}.
  85   ðÒÉ ÜÔÏÍ *\dÎÅÐÒÅÒÙ×ÎÏÓÔØ ÓÔÒÏÇÏ
  86   ÓÉÌØÎÅÅ ÉÈ\T × ÔÏÍ ÓÍÙÓÌÅ, ÞÔÏ ÓÕÝÅÓÔ×ÕÀÔ ÁÌÇÅÂÒÙ ëÌÉÎÉ, ÎÅ
  87   Ñ×ÌÑÀÝÉÅÓÑ *\dÎÅÐÒÅÒÙ×ÎÙÍÉ \cite{KA-closedSr}.
  88
  89   ÷ÐÏÌÎÅ ÏÖÉÄÁÅÍÏ, ÞÔÏ
  90   ÍÎÏÇÉÅ ÅÓÔÅÓÔ×ÅÎÎÏ ×ÏÚÎÉËÁÀÝÉÅ ÍÏÄÅÌÉ ÁÌÇÅÂÒ ëÌÉÎÉ *\dÎÅÐÒÅÒÙ×ÎÙ.
  91 \end{remark}
  92 \todo{[ÎÅÐÏÎÑÔÎÏ, ËÁË  ÐÒÏÉÚÎÏÓÉÔØ <<*-ÎÅÐÒÅÒÙ×ÎÏÓÔØ>> ÐÏ-ÒÕÓÓËÉ]}
  93
  94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  95 \subsection{îÅËÏÔÏÒÙÅ ×ÁÖÎÙÅ ÁÌÇÅÂÒÙ ëÌÉÎÉ}\label{sec:KA-models}
  96 \todo{[ÒÁÚÏÂÒÁÔØÓÑ Ó ÕÐÏÔÒÅÂÌÅÎÉÅÍ ÓÌÏ× ÁÌÇÅÂÒÁ/ÍÏÄÅÌØ ÔÕÔ]}
  97
  98 ïÐÉÓÁÎÎÙÅ ÚÄÅÓØ ÁÌÇÅÂÒÙ ëÌÉÎÉ (ÉÌÉ ÉÈ ÐÏÄÁÌÇÅÂÒÙ) ÍÙ ÂÕÄÅÍ
  99 ÉÓÐÏÌØÚÏ×ÁÔØ ËÁË ÍÏÄÅÌÉ ÄÌÑ ÉÎÔÅÒÐÒÅÔÁÃÉÉ ÐÒÏÇÒÁÍÍ.
 100
 101 ðÒÉÍÅÒÙ ÉÚ ÜÔÏÇÏ òÁÚÄÅÌÁ ÐÏËÁÖÕÔ, ÞÔÏ ÐÏÎÑÔÉÅ \tDJust{ÁÌÇÅÂÒ ëÌÉÎÉ}
 102 ÉÍÅÅÔ ÓÍÙÓÌ, ÏÂÏÂÝÁÅÔ ÓÕÝÅÓÔ×ÅÎÎÙÅ Ó×ÏÊÓÔ×Á ÎÅÓËÏÌØËÉÈ ÍÏÄÅÌÅÊ.
 103 üÔÉ É ÄÒÕÇÉÅ ÐÒÉÍÅÒÙ\T ÈÏÒÏÛÁÑ ÍÏÔÉ×ÁÃÉÑ ÉÚÕÞÅÎÉÑ ÏÂÝÉÈ Ó×ÏÊÓÔ×
 104 ÁÌÇÅÂÒ ëÌÉÎÉ.
 105
 106 èÏÒÏÛÏ ÚÎÁËÏÍÏÊ ÐÏ ôÅÏÒÉÉ ÒÅÇÕÌÑÒÎÙÈ ÆÏÒÍÁÌØÎÙÈ ÑÚÙËÏ× É ËÏÎÅÞÎÙÈ
 107 Á×ÔÏÍÁÔÏ× ÏËÁÖÅÔÓÑ \tNDNo{ÆÏÒÍÁÌØÎÏÑÚÙËÏ×ÙÅ ÍÏÄÅÌØ} ÄÌÑ ÁÌÇÅÂÒ ëÌÉÎÉ
 108 (ÏÐÉÓÁÎÁ × òÁÚÄÅÌÅ~\ref{sec:KA-langmodels}). äÒÕÇÉÅ ÐÒÉ×ÅÄ£ÎÎÙÅ ÚÄÅÓØ
 109 ÍÏÄÅÌÉ (× òÁÚÄÅÌÁÈ~\ref{sec:KA-relmodels} É~\ref{sec:KA-tracemodels})
 110 ×ÁÖÎÙ ÎÁÍ ÐÏÍÉÍÏ ÔÏÇÏ, ÞÔÏ ÏÎÉ ÐÒÏÓÔÏ ÉÎÔÅÒÅÓÎÙ ÓÁÍÉ ÐÏ ÓÅÂÅ,
 111 ÔÅÍ, ÞÔÏ ÉÍÅÀÔ ÁÎÁÌÏÇÉÉ × ÉÚ×ÅÓÔÎÙÈ ÐÏÄÈÏÄÁÈ Ë ÉÚÕÞÅÎÉÀ ÓÅÍÁÎÔÉË ÐÒÏÇÒÁÍÍ.
 112
 113 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 114 \subsubsection{áÌÇÅÂÒÙ ÆÏÒÍÁÌØÎÙÈ ÑÚÙËÏ×}
 115 \label{sec:KA-langmodels}
 116
 117 íÙ ÂÕÄÅÍ ÐÏÌØÚÏ×ÁÔØÓÑ ÓÌÅÄÕÀÝÉÍÉ ÂÁÚÏ×ÙÍÉ ÐÏÎÑÔÉÑÍÉ ôÅÏÒÉÉ ÆÏÒÍÁÌØÎÙÈ ÑÚÙËÏ×.
 118 ðÕÓÔØ $\Sigma$ ËÏÎÅÞÎÙÊ ÁÌÆÁ×ÉÔ.
 119 $$
 120 \begin{tabular}{lp{.5\textwidth}}
 121 & {\small ÏÂÏÚÎÁÞÅÎÉÅ}\\
 122 \tING{ËÏÎÅÞÎÙÅ ÓÔÒÏËÉ} ÎÁÄ~$\Sigma$
 123 %% &
 124 %% \\
 125 %% \tING{ÍÎÏÖÅÓÔ×Ï ËÏÎÅÞÎÙÈ ÓÔÒÏË}
 126 %% ÎÁÄ~$\Sigma$
 127 &
 128 $\Strs(\Sigma)$\T
 129 ÍÎÏÖÅÓÔ×Ï ËÏÎÅÞÎÙÈ ÓÔÒÏË
 130 ÎÁÄ~$\Sigma$
 131 \\
 132 \tING{ÐÕÓÔÁÑ ÓÔÒÏËÁ}
 133 &
 134 $\eStr$\\
 135 ÏÐÅÒÁÃÉÑ <<\tING{ËÏÎËÁÔÅÎÁÃÉÑ}>>
 136 &
 137 $\cdot$
 138 \end{tabular}
 139 $$
 140 ïÐÅÒÁÃÉÑ ËÏÎËÁÔÅÎÁÃÉÉ ÏÐÒÅÄÅÌÅÎÁ ÎÁ ×ÓÅÈ ÐÁÒÁÈ ÓÔÒÏË. (ðÒÉ
 141 ÚÁÐÉÓÉ ÍÏÖÎÏ ÏÐÕÓËÁÔØ ÚÎÁË $\cdot$.) óÌÏ×Ï <<ËÏÎÅÞÎÁÑ>> × ÏÔÎÏÛÅÎÉÉ
 142 ÓÔÒÏË ÍÏÖÎÏ ÏÐÕÓËÁÔØ.
 143
 144 \begin{remark}\label{rem:str-monoid}
 145   óÔÒÕËÔÕÒÁ~$(\Strs(\Sigma); \cdot, \eStr)$\T ÍÏÎÏÉÄ.
 146 \end{remark}
 147
 148 \begin{remark}
 149   \todo{[ÐÅÒÅÄÅÌÁÔØ ÓÏÏÔ×. ÔÏÍÕ, ÇÄÅ ÎÁÄÏ Ó×ÏÂ.]}
 150   $\Strs(\Sigma)$\T \tND{Ó×ÏÂÏÄÎÙÊ ÍÏÎÏÉÄ}{def:free-monoid} ÎÁÄ
 151 $\Sigma$, ÏÂÙÞÎÏ ÏÂÏÚÎÁÞÁÅÍÙÊ $\Sigma^*$; ÍÙ ×ÅÒÎ£ÍÓÑ Ë ÜÔÏÍÕ
 152 × ÏÐÒÅÄÅÌÅÎÉÉ~\ref{def:free-monoid}.
 153 \end{remark}
 154
 155 ôÅÐÅÒØ ÐÏÓÔÒÏÉÍ ÍÏÄÅÌØ ÄÌÑ ÁÌÇÅÂÒÙ ëÌÉÎÉ ÎÁ ÏÓÎÏ×Å ÐÏÎÑÔÉÊ ôÅÏÒÉÉ
 156 ÆÏÒÍÁÌØÎÙÈ ÑÚÙËÏ×.
 157 âÕÄÅÍ ÒÁÓÓÍÁÔÒÉ×ÁÔØ ÍÎÏÖÅÓÔ×Ï ×ÓÅÈ ÐÏÄÍÎÏÖÅÓÔ×~$\Strs(\Sigma)$\T $2^{\Strs(\Sigma)}$.
 158
 159 \begin{definition}
 160   äÌÑ $X, Y \subseteq \Strs(\Sigma)$
 161   \begin{equation}
 162     \label{eq:set-concat}
 163     X \cdot Y \eqdef \{ xy \mid x \in X, y \in Y \}.
 164   \end{equation}
 165 \end{definition}
 166
 167 \begin{proposition}
 168   óÔÒÕËÔÕÒÁ~$(2^{\Strs(\Sigma)}; \cup, \cdot, \emptyset, \{ \eStr \} )$\T
 169   ÉÄÅÍÐÏÔÅÎÔÎÏÅ ÐÏÌÕËÏÌØÃÏ.
 170 \end{proposition}
 171
 172 \begin{definition}
 173   äÌÑ $X \subseteq \Strs(\Sigma)$
 174   \begin{equation}
 175     \label{eq:set-star}
 176     X^*  \eqdef \bigcup_{n \in \bbN \cup \{ 0 \}} X^n,
 177   \end{equation}
 178   ÇÄÅ
 179   \begin{align*}
 180     X^0 &\eqdef \{ \eStr\}
 181     &
 182     X^{n+1} &\eqdef X \cdot X^n.
 183   \end{align*}
 184 \end{definition}
 185
 186 \begin{proposition}\label{prop:all-str-KA}
 187   óÔÒÕËÔÕÒÁ~$(2^{\Strs(\Sigma)}; \cup, \cdot, {}^*, \emptyset, \{ \eStr \} )$\T
 188   ÁÌÇÅÂÒÁ ëÌÉÎÉ.
 189 \end{proposition}
 190
 191 \begin{proposition}\label{prop:all-str-cont}
 192   áÌÇÅÂÒÁ ëÌÉÎÉ~$(2^{\Strs(\Sigma)}; \cup, \cdot, {}^*, \emptyset, \{ \eStr \} )$
 193   *\dÎÅÐÒÅÒÙ×ÎÁ.
 194 \end{proposition}
 195 \begin{proof}
 196 *\dÎÅÐÒÅÒÙ×ÎÏÓÔØ ÓÌÅÄÕÅÔ ÉÚ ÏÐÒÅÄÅÌÅÎÉÑ $^*$ É ÄÉÓÔÒÉÂÕÔÉ×ÎÏÓÔÉ $\cdot$
 197 ÏÔÎÏÓÉÔÅÌØÎÏ ÂÅÓËÏÎÅÞÎÙÈ ÏÂßÅÄÉÎÅÎÉÊ:
 198 \begin{equation}
 199   \label{eq:str-cont}
 200   X \cdot Y^* \cdot Z
 201   = X \cdot
 202   \left( \bigcup_{n \in \bbN \cup \{ 0 \}} Y^n \right)
 203   \cdot Z
 204   = \bigcup_{n \in \bbN \cup \{ 0 \}} \left(
 205     X \cdot Y^n \cdot Z
 206     \right).
 207 \end{equation}
 208 äÉÓÔÒÉÂÕÔÉ×ÎÏÓÔØ ÏÂßÑÓÎÑÅÔÓÑ ÔÅÍ, ÞÔÏ ÏÂÁ ÜÔÉ ×ÙÒÁÖÅÎÉÑ ÏÂÏÚÎÁÞÁÀÔ ÍÎÏÖÅÓÔ×Ï
 209 $$
 210 \left\{ xyz \mid x \in X, z \in Z, \exists n \left( y \in Y^n \right) \right\}.
 211 $$
 212 \end{proof}
 213
 214 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 215 \subsubsection{òÅÌÑÃÉÏÎÎÙÅ ÍÏÄÅÌÉ}
 216 \label{sec:KA-relmodels}
 217
 218 íÙ ÂÕÄÅÍ ÐÏÌØÚÏ×ÁÔØÓÑ ÓÌÅÄÕÀÝÉÍÉ ÂÁÚÏ×ÙÍÉ ÐÏÎÑÔÉÑÍÉ <<ôÅÏÒÉÉ
 219 ÏÔÎÏÛÅÎÉÊ>> (ÓÍ.~òÁÚÄÅÌ~\ref{sec:relations}).
 220 ðÕÓÔØ $U$ ÍÎÏÖÅÓÔ×Ï.
 221 $$
 222 \begin{tabular}{p{.4\textwidth}p{.5\textwidth}}
 223 & {\small ÏÂÏÚÎÁÞÅÎÉÅ}\\
 224 \tING{ÏÔÎÏÛÅÎÉÅ} ÎÁ~$U$
 225 &
 226 $\Rels(U) \eqdef 2^{U \times U}$\T
 227 ÍÎÏÖÅÓÔ×Ï ÏÔÎÏÛÅÎÉÊ ÎÁ~$U$
 228 \\
 229 \tING{ÎÕÌÅ×ÏÅ ÏÔÎÏÛÅÎÉÅ}
 230 &
 231 $\emptyset$\\
 232 \tING{ÔÏÖÄÅÓÔ×ÅÎÎÏÅ ÏÔÎÏÛÅÎÉÅ}
 233 &
 234 $\id_U$\\
 235 \tING{ÏÂßÅÄÉÎÅÎÉÅ}
 236 &
 237 $\cup$\\
 238 \tING{ËÏÍÐÏÚÉÃÉÑ}
 239 &
 240 $\circ$\\
 241 \tING{ÒÅÆÌÅËÓÉ×ÎÏ\DÔÒÁÎÚÉÔÉ×ÎÏÅ ÚÁÍÙËÁÎÉÅ}
 242 &
 243 $^*$
 244 \end{tabular}
 245 $$
 246
 247 \begin{proposition}\label{prop:rels-KA}
 248   óÔÒÕËÔÕÒÁ~$(\Rels(U); \cup, \circ, ^*, \emptyset, \id_U )$\T
 249   ÁÌÇÅÂÒÁ ëÌÉÎÉ.
 250 \end{proposition}
 251
 252 \begin{proposition}\label{prop:rels-cont}
 253   áÌÇÅÂÒÁ ëÌÉÎÉ~$(\Rels(U); \cup, \circ, ^*, \emptyset, \id_U )$
 254   *\dÎÅÐÒÅÒÙ×ÎÁ.
 255 \end{proposition}
 256 ïÂÁ ÕÔ×ÅÒÖÄÅÎÉÑ ÎÅÔÒÕÄÎÏ ÐÒÏ×ÅÒÉÔØ.
 257 (äÏËÁÚÁÔÅÌØÓÔ×Ï *\dÎÅÐÒÅÒÙ×ÎÏÓÔÉ ÐÏÈÏÖÅ ÎÁ ÓÌÕÞÁÊ ÁÌÇÅÂÒÙ ÆÏÒÍÁÌØÎÙÈ
 258 ÑÚÙËÏ× (õÔ×.~\ref{prop:all-str-cont}).)
 259
 260 \begin{definition}\label{def:relational-KA}
 261   áÌÇÅÂÒÁ ëÌÉÎÉ~$\ka K$ \tING{ÒÅÌÑÃÉÏÎÎÁÑ}, ÅÓÌÉ ÏÎÁ Ñ×ÌÑÅÔÓÑ
 262   ÐÏÄÁÌÇÅÂÒÏÊ ÁÌÇÅÂÒÙ ëÌÉÎÉ~$(\Rels(U); \cup, \circ, ^*, \emptyset,
 263   \id_U)$
 264   ÄÌÑ ÎÅËÏÔÏÒÏÇÏ~$U$; $U$ ÎÁÚÙ×ÁÅÔÓÑ \tING{ÂÁÚÏÊ}~$\ka K$.
 265
 266   \RKA ÏÂÏÚÎÁÞÁÅÔ \tING{ËÁÔÅÇÏÒÉÀ ÒÅÌÑÃÉÏÎÎÙÈ ÁÌÇÅÂÒ ëÌÉÎÉ É ÉÈ ÇÏÍÏÍÏÒÆÉÚÍÏ×}.
 267 \end{definition}
 268
 269 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 270 \subsubsection{ôÒÁÓÓÏ×ÙÅ ÍÏÄÅÌÉ}\label{sec:KA-tracemodels}
 271 ôÒÁÓÓÙ × ÛËÁÌÁÈ ëÒÉÐËÅ ÂÙÌÉ ××ÅÄÅÎÙ × òÁÚÄÅÌÅ~\ref{sec:kframes}.
 272
 273 åÓÌÉ Õ ÔÒÁÓÓ $\sigma$ É $\tau$ $\Last(\sigma) = \First(\tau)$, ÔÏ ÉÈ
 274 ÍÏÖÎÏ <<ÓÏÅÄÉÎÉÔØ>> ÜÔÉÍÉ ËÏÎÃÁÍÉ:
 275 \begin{definition}\label{def:trace-concat}
 276   äÌÑ ÔÒÁÓÓ $\sigma$ É $\tau$ × ÛËÁÌÅ ëÒÉÐËÅ $\kf F$:
 277   \begin{align*}
 278     \sigma &= u_0 a_0 u_1 \dotsm  u_n,
 279     &
 280     \tau &= v_0 b_0 v_1 \dotsm  v_m,
 281   \end{align*}
 282 ÏÐÒÅÄÅÌÉÍ:
 283   \begin{equation}
 284     \label{eq:trace-concat}
 285     \sigma \trCo \tau \eqdef
 286     \begin{cases}
 287       u_0 a_0 u_1 \dotsm  u_n b_0 v_1 \dotsm  v_m
 288       & \text{ÅÓÌÉ } u_n = v_0,\\
 289       \text{ÎÅÏÐÒÅÄÅÌÅÎÏ}
 290       & \text{ÅÓÌÉ } u_n \ne v_0.
 291     \end{cases}
 292   \end{equation}
 293 \end{definition}
 294
 295 ïÐÉÛÅÍ ÁÌÇÅÂÒÕ ëÌÉÎÉ ÍÎÏÖÅÓÔ× ÔÒÁÓÓ \cite{?}.
 296
 297 \begin{definition}
 298   ðÕÓÔØ $\kf F = \Stru{Q_{\kf F}, m_{\kf F}}$ ÛËÁÌÁ ëÒÉÐËÅ.
 299   äÌÑ $X, Y \subseteq \Trs(\kf F)$
 300   \begin{align}
 301     \label{eq:traces-concat}
 302     X \trCo Y &\eqdef \{ \sigma \trCo \tau \mid
 303     \sigma \in X,\, \tau \in Y,\, \sigma \trCo \tau \text{ ÓÕÝÅÓÔ×ÕÅÔ}\};\\
 304     \label{eq:traces-star}
 305     X^*  &\eqdef \bigcup_{n \in \bbN \cup \{ 0 \}} X^n,
 306   \end{align}
 307   ÇÄÅ
 308   \begin{align*}
 309     X^0 &\eqdef Q_{\kf F}
 310     &
 311     X^{n+1} &\eqdef X \trCo X^n.
 312   \end{align*}
 313 \end{definition}
 314
 315 \begin{proposition}\label{prop:all-traces-KA}
 316   óÔÒÕËÔÕÒÁ~$(2^{\Trs(\kf F)}; \cup, \trCo, {}^*, \emptyset, Q_{\kf F} )$\T
 317   *\dÎÅÐÒÅÒÙ×ÎÁÑ ÁÌÇÅÂÒÁ ëÌÉÎÉ.
 318 \end{proposition}
 319
 320 \paragraph{òÅÌÑÃÉÏÎÎÙÅ ÍÏÄÅÌÉ, ÏÓÎÏ×ÁÎÎÙÅ ÎÁ ÛËÁÌÁÈ ëÒÉÐËÅ}
 321 \newcommand*{\eqExt}{\Ext(X) \eqdef \{ (\First(\sigma), \Last(\sigma)) \mid \sigma \in
 322     X \}}
 323 \begin{definition}[\cite{KAT-elimination}]\label{def:Ext}
 324   \tING{ëÁÎÏÎÉÞÅÓËÉÊ ÇÏÍÏÍÏÒÆÉÚÍ} $\Ext\colon 2^{\Trs(\kf F)} \to
 325   \Rels(Q_{\kf F})$
 326   ÁÌÇÅÂÒÙ ÍÎÏÖÅÓÔ× ÔÒÁÓÓ × ÛËÁÌÅ
 327   ëÒÉÐËÅ $\kf F$ × ÒÅÌÑÃÉÏÎÎÕÀ ÁÌÇÅÂÒÕ ëÌÉÎÉ ÎÁ $Q_{\kf F}$:
 328   \begin{equation}
 329     \label{eq:Ext}
 330     \eqExt.
 331   \end{equation}
 332 \end{definition}
 333 \begin{application}
 334   åÓÌÉ ÓÍÏÔÒÅÔØ ÎÁ ÔÒÁÓÓÕ ËÁË ÎÁ ×ÏÚÍÏÖÎÕÀ ÉÓÔÏÒÉÀ ×ÙÞÉÓÌÅÎÉÑ ÐÒÏÇÒÁÍÍÙ
 335   (ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÏÓÔØ ÐÒÏÍÅÖÕÔÏÞÎÙÈ ÒÅÚÕÌØÔÁÔÏ×\DÓÏÓÔÏÑÎÉÊ ÐÁÍÑÔÉ),
 336   ÔÏ ÇÏÍÏÍÏÒÆÉÚÍ $\Ext$ ÎÁÄÏ ÐÏÎÉÍÁÔØ ËÁË ÐÏÌÕÞÅÎÉÅ ÉÚ ÉÓÔÏÒÉÊ
 337   ×ÙÞÉÓÌÅÎÉÊ ÏÔÎÏÛÅÎÉÑ <<ÎÁÞÁÌØÎÏÅ ÓÏÓÔÏÑÎÉÅ ÐÁÍÑÔÉ\T ÒÅÚÕÌØÔÁÔ>>
 338   (ÐÕÔ£Í ÚÁÂÙ×ÁÎÉÑ ÐÒÏÍÅÖÕÔÏÞÎÙÈ ÒÅÚÕÌØÔÁÔÏ×).
 339
 340   ÷ÎÅÛÎÅÍÕ ÎÁÂÌÀÄÁÔÅÌÀ ÍÏÖÅÔ ÂÙÔØ ÉÎÔÅÒÅÓÎÏ ÔÏÌØËÏ ÐÏÓÌÅÄÎÅÅ
 341   ÏÔÎÏÛÅÎÉÅ, ÈÁÒÁËÔÅÒÉÚÕÀÝÅÅ ËÏÎÅÞÎÙÊ ÒÅÚÕÌØÔÁÔ ×ÙÞÉÓÌÅÎÉÑ,
 342   ÎÏ ÄÌÑ ÔÏÇÏ, ÞÔÏÂÙ ÉÓÓÌÅÄÏ×ÁÔØ ÒÁÂÏÔÕ ÐÒÏÇÒÁÍÍÙ, ÍÏÖÅÔ ÂÙÔØ ÕÄÏÂÎÏ
 343   ÏÂÒÁÝÁÔØÓÑ Ó ÔÒÁÓÓÁÍÉ.
 344 \end{application}
 345
 346 \todo{[×ÓÔÁ×ÉÔØ ×ÓÀÄÕ ÐÒÏ ÔÏ, ËÁË ÐÒÉÍÅÎÑÔØ]}
 347
 348 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 349 \subsection{ðÒÏÇÒÁÍÍÙ: ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ}\label{sec:regexp}
 350 \begin{definition}[\cite{?,KA-modular-elimination}]\label{def:regexp}
 351 ðÕÓÔØ $\Sigma$\T ËÏÎÅÞÎÙÊ ÎÁÂÏÒ ÓÉÍ×ÏÌÏ×\DËÏÎÓÔÁÎÔ.
 352 ôÅÒÍÙ ÓÉÇÎÁÔÕÒÙ \tD{ÁÌÇÅÂÒÙ ëÌÉÎÉ}{def:KA} (\te $+, \cdot, ^*, 0, 1$),
 353 ÄÏÐÏÌÎÅÎÎÏÊ ËÏÎÓÔÁÎÔÁÍÉ ÉÚ~$\Sigma$, ÎÁÚÙ×ÁÀÔÓÑ \tING{ÒÅÇÕÌÑÒÎÙÍÉ
 354   ×ÙÒÁÖÅÎÉÑÍÉ ÎÁÄ $\Sigma$}.
 355 íÎÏÖÅÓÔ×Ï ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ
 356 ÏÂÏÚÎÁÞÁÅÔÓÑ $\RExp_\Sigma$.
 357 üÌÅÍÅÎÔÙ~$\Sigma$ ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ
 358 \tING{ÂÁÚÏ×ÙÍÉ ÏÐÅÒÁÔÏÒÁÍÉ}.
 359 \end{definition}
 360 \begin{table}[hbtp]
 361   \centering
 362 $$
 363 \begin{array}{lll}
 364 \text{ÔÅÒÍÙ}
 365 & s, t  \dotsc
 366 & s ::= \langle\text{ÂÁÚÏ×ÙÅ ÏÐÅÒÁÔÏÒÙ}\rangle
 367 \ |\ 0\ |\ 1\ |\ s+t\ |\ st\ |\ s^*
 368 \end{array}
 369 $$
 370   \caption{ôÅÒÍÙ × ÏÐÒÅÄÅÌÅÎÉÉ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma$}
 371   \label{tab:regexp-bnf}
 372 \end{table}
 373
 374 \begin{remark}
 375   $\RExp_\Sigma$ ÔÏÖÅ ÍÏÖÎÏ ÒÁÓÓÍÁÔÒÉ×ÁÔØ ËÁË ÁÌÇÅÂÒÕ Ó ÓÉÇÎÁÔÕÒÏÊ
 376   ÁÌÇÅÂÒÙ ëÌÉÎÉ. ïÐÅÒÁÃÉÉ
 377   <<ÄÅÊÓÔ×ÕÀÔ>> ÓÉÎÔÁËÓÉÞÅÓËÉ: ÐÒÉÍÅÎ£ÎÎÙÅ Ë ÔÅÒÍÁÍ, ÏÎÉ ÓÏÓÔÁ×ÌÑÀÔ
 378   ÂÏÌÅÅ ÓÌÏÖÎÙÅ ÔÅÒÍÙ.
 379
 380   éÍÅÅÔ ÓÍÙÓÌ ÇÏ×ÏÒÉÔØ Ï ÇÏÍÏÍÏÒÆÎÙÈ ÏÔÏÂÒÁÖÅÎÉÑÈ $\RExp_\Sigma$
 381   × ÄÒÕÇÉÅ ÁÌÇÅÂÒÙ ÜÔÏÊ ÓÉÇÎÁÔÕÒÙ.
 382 \end{remark}
 383
 384 \paragraph{úÎÁÞÅÎÉÑ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ.}
 385 \begin{definition}
 386 ïÔÏÂÒÁÖÅÎÉÅ $I\colon \Sigma \to \ka K$, ÇÄÅ $\ka K$\T ÁÌÇÅÂÒÁ ëÌÉÎÉ,
 387 ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ \tING{ÉÎÔÅÒÐÒÅÔÁÃÉÅÊ ÂÁÚÏ×ÙÈ ÓÉÍ×ÏÌÏ× (ÏÐÅÒÁÔÏÒÏ×)}.
 388
 389 $I$ ÏÄÎÏÚÎÁÞÎÏ ÐÒÏÄÏÌÖÁÅÔÓÑ ÄÏ ÇÏÍÏÍÏÒÆÉÚÍÁ ÎÁ ×Ó£
 390 $\RExp_{\Sigma}$.
 391 %ÔÁË ÐÏÌÕÞÁÀÝÅÅÓÑ ÏÔÏÂÒÁÖÅÎÉÅ ÍÙ ÔÏÖÅ ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ $I$
 392 åÇÏ ÚÎÁÞÅÎÉÅ ÎÁ $s \in \RExp_\Sigma$ ÍÙ ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ
 393 ÐÒÏÓÔÏ $I(s)$ É ÎÁÚÙ×ÁÔØ ÅÇÏ ÚÎÁÞÅÎÉÅÍ
 394 ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ~$s$ ÐÒÉ ÉÎÔÅÒÐÒÅÔÁÃÉÉ~$I$, ÉÌÉ,
 395 \tING{ÉÎÔÅÒÐÒÅÔÁÃÉÅÊ ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ}~$s$.
 396 \end{definition}
 397
 398 \subsubsection{(ëÁÎÏÎÉÞÅÓËÉÅ) ÉÎÔÅÒÐÒÅÔÁÃÉÉ}\label{sec:regexp-interp}
 399 \todo{[ËÁÎÏÎÉÞ/ÓÔÁÎÄ -- ?]}
 400
 401 \paragraph{æÏÒÍÁÌØÎÏÑÚÙËÏ×ÁÑ.}
 402
 403 \begin{definition}\label{def:interp-str}
 404   \tING{ëÁÎÏÎÉÞÅÓËÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ $R_{\Sigma}$
 405     ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma$ × ÁÌÇÅÂÒÅ ÍÎÏÖÅÓÔ×
 406   ÓÔÒÏË~$2^{\Strs(\Sigma)}$}
 407   ÏÐÒÅÄÅÌÑÅÔÓÑ ÔÁËÉÍÉ ÚÎÁÞÅÎÉÑÍÉ ÎÁ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÁÈ:
 408   $$
 409   R_{\Sigma}(a) \eqdef \{ a \} \text{ ÄÌÑ } a \in \Sigma.
 410   $$
 411 \end{definition}
 412 (ëÏÇÄÁ ÓÉÇÎÁÔÕÒÁ $\Sigma$ ÂÕÄÅÔ ÑÓÎÁ, ÍÙ ÂÕÄÅÍ ÏÐÕÓËÁÔØ Å£ × ÚÁÐÉÓÉ.)
 413 %% ìÅÇËÏ ×ÉÄÅÔØ, ÞÔÏ
 414 %% ÉÎÔÅÒÐÒÅÔÁÃÉÅÊ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÓÔÁÎÏ×ÑÔÓÑ ÒÅÇÕÌÑÒÎÙÅ ÍÎÏÖÅÓÔ×Á
 415 %% ÓÔÒÏË ÎÁÄ~$\Sigma$.
 416
 417 \begin{definition}\label{def:reg-by-basic}
 418   íÎÏÖÅÓÔ×Ï ÓÔÒÏË~$X \subseteq \Strs(\Sigma)$ ÎÁÚÙ×ÁÅÔÓÑ
 419   \tING{ÒÅÇÕÌÑÒÎÙÍ}, ÅÓÌÉ $X = R_{\Sigma}(s)$ ÄÌÑ ÎÅËÏÔÏÒÏÇÏ
 420   ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ $s \in \RExp_{\Sigma}$.
 421
 422   \tING{óÅÍÅÊÓÔ×Ï ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ× ÓÔÒÏË ÎÁÄ~$\Sigma$} ÏÂÏÚÎÁÞÁÅÔÓÑ
 423   $\Reg_{\Sigma}$. (ôÅÍ ÓÁÍÙÍ, $\Reg_{\Sigma}$\T ÍÉÎÉÍÁÌØÎÁÑ
 424   ÐÏÄÁÌÇÅÂÒÁ ÁÌÇÅÂÒÙ ëÌÉÎÉ $2^{\Strs(\Sigma)}$, ÐÏÒÏÖÄÁÅÍÁÑ
 425   ÜÌÅÍÅÎÔÁÍÉ $\{ a \}$ ÄÌÑ $a \in \Sigma$ (ÜÔÏ ÚÎÁÞÅÎÉÑ $R_{\Sigma}(a)$).
 426   (<<$\Reg_{\Sigma} \models \phi$>> ÚÎÁÞÉÔ
 427   <<$\Reg_{\Sigma}, R_\Sigma \models \phi$>>.
 428   \todo{[ÈÏÔÉÍ ÌÉ $R_{\Sigma}$ ÐÏ ÕÍÏÌÞÁÎÉÀ?]})
 429 \end{definition}
 430 %
 431 (íÏÖÎÏ ×ÓÔÒÅÔÉÔØ É ÄÒÕÇÏÅ ÐÏÈÏÖÅÅ ÜË×É×ÁÌÅÎÔÎÏÅ ÏÐÒÅÄÅÌÅÎÉÅ ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ×
 432 ÓÔÒÏË, ÅÓÔÅÓÔ×ÅÎÎÏ ×ÏÚÎÉËÁÀÝÅÅ
 433 ÐÒÉ ÏÂÏÂÝÅÎÉÉ ËÏÎÓÔÒÕËÃÉÉ $\Reg_\Sigma$ ÎÁ ÐÒÏÉÚ×ÏÌØÎÙÅ ÍÏÎÏÉÄÙ\T
 434 ÓÍ.~úÁÍÅÞÁÎÉÅ~\label{rem:reg-over-str}.)
 435
 436 \paragraph{ôÒÁÓÓÏ×ÁÑ.}
 437
 438 \begin{definition}[\cite{KAT-elimination}]\label{def:interp-traces}
 439   ðÕÓÔØ $\kf F$ ÛËÁÌÁ ëÒÉÐËÅ ÎÁÄ~$\Sigma$.
 440   \tING{ëÁÎÏÎÉÞÅÓËÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ $\trI{\place}_{\kf F}$
 441   ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma$ × ÁÌÇÅÂÒÅ ÍÎÏÖÅÓÔ×
 442   ÔÒÁÓÓ~$2^{\Trs(\kf F)}$} ÏÐÒÅÄÅÌÑÅÔÓÑ ÔÁË:
 443   $$
 444   \trI{a}_{\kf F} \eqdef \{ u a v \mid (u,v) \in m_{\kf F}(a) \}
 445   \text{ ÄÌÑ } a \in \Sigma.
 446   $$
 447 \end{definition}
 448 \begin{definition}[\cite{KAT-elimination}]
 449   íÎÏÖÅÓÔ×Ï ÔÒÁÓÓ $X \subseteq \Trs(\kf F)$ ÎÁÚÙ×ÁÅÔÓÑ
 450   \tING{ÒÅÇÕÌÑÒÎÙÍ}, ÅÓÌÉ $X = \trI{ s }_{\kf F}$ ÄÌÑ ÎÅËÏÔÏÒÏÇÏ
 451   ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ $s \in \RExp_{\Sigma}$, ÇÄÅ $\kf F$\T ÛËÁÌÁ
 452   ëÒÉÐËÅ ÎÁÄ~$\Sigma$.
 453
 454   \tING{óÅÍÅÊÓÔ×Ï ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ× ÔÒÁÓÓ ×~$\kf F$} ÏÂÏÚÎÁÞÁÅÔÓÑ
 455   $\trReg_{\kf F}$.
 456   (<<$\trReg_{\kf F} \models \phi$>> ÚÎÁÞÉÔ
 457   <<$\trReg_{\kf F}, \trI{\place} \models \phi$>>. \todo{[ÐÏÌÕÞÛÅ ÂÙ ÎÁÐÉÓÁÔØ]})
 458 \end{definition}
 459 \begin{definition}[\cite{KAT-elimination}]
 460   ëÌÁÓÓ ËÁÎÏÎÉÞÅÓËÉÈ ÔÒÁÓÓÏ×ÙÈ ÉÎÔÅÒÐÒÅÔÁÃÉÊ:
 461   $$
 462   \TRACE \eqdef \{ (\trReg_{\kf F}, \trI{\place}_{\kf F})
 463   \mid \kf F \text{\T ÛËÁÌÁ ëÒÉÐËÅ} \}
 464   $$
 465 \end{definition}
 466
 467 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 468 \paragraph{òÅÌÑÃÉÏÎÎÁÑ.}
 469
 470 \begin{definition}[\cite{KAT-elimination}]\label{def:interp-traces}
 471   ðÕÓÔØ $\kf F = (Q_{\kf F}, m_{\kf F})$ ÛËÁÌÁ ëÒÉÐËÅ ÎÁÄ~$\Sigma$.
 472   \tING{ëÁÎÏÎÉÞÅÓËÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ $\relI{\place}_{\kf F}$
 473     ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma$ × ÁÌÇÅÂÒÅ ÏÔÎÏÛÅÎÉÊ~$\Rels(Q_{\kf F})$}
 474   ÏÐÒÅÄÅÌÑÅÔÓÑ ÔÁË:
 475   $$
 476   \relI{a}_{\kf F} \eqdef  m_{\kf F}(a)
 477   \text{ ÄÌÑ } a \in \Sigma.
 478   $$
 479 \end{definition}
 480 \begin{definition}[\cite{KAT-elimination}]
 481   ðÕÓÔØ $\kf F = (Q_{\kf F}, m_{\kf F})$ ÛËÁÌÁ ëÒÉÐËÅ ÎÁÄ~$\Sigma$.
 482   ïÔÎÏÛÅÎÉÅ $S \in \Rels(Q_{\kf F})$ ÎÁÚÙ×ÁÅÔÓÑ
 483   \tING{ÒÅÇÕÌÑÒÎÙÍ}, ÅÓÌÉ $S = \relI{ s }_{\kf F}$ ÄÌÑ ÎÅËÏÔÏÒÏÇÏ
 484   ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ $s \in \RExp_{\Sigma}$.
 485
 486   \tING{óÅÍÅÊÓÔ×Ï ÒÅÇÕÌÑÒÎÙÈ ÏÔÎÏÛÅÎÉÊ ÎÁ~$\kf F$} ÏÂÏÚÎÁÞÁÅÔÓÑ
 487   $\relReg_{\kf F}$.
 488   (<<$\relReg_{\kf F} \models \phi$>> ÚÎÁÞÉÔ
 489   <<$\relReg_{\kf F}, \relI{\place}_{\kf F} \models \phi$>>.
 490   \todo{[ÐÏÌÕÞÛÅ ÂÙ ÎÁÐÉÓÁÔØ, ÓÒÁ×ÎÉÔØ Ó $\Reg_{\Sigma}$.]})
 491 \end{definition}
 492 \begin{remark}
 493   \begin{align*}
 494     \Ext(\trI{s}_{\kf F}) &= \relI{s}_{\kf F}
 495     \text{ ÄÌÑ ÌÀÂÏÇÏ $s \in \RExp_{\Sigma}$.}
 496   \end{align*}
 497 \end{remark}
 498 \begin{definition}[\cite{KAT-elimination}]
 499   ëÌÁÓÓ \todo{[ËÁÎÏÎÉÞÅÓËÉÈ?]} ÒÅÌÑÃÉÏÎÎÙÈ ÉÎÔÅÒÐÒÅÔÁÃÉÊ,
 500   ÏÓÎÏ×ÁÎÎÙÈ ÎÁ ÛËÁÌÁÈ ëÒÉÐËÅ:
 501   $$
 502   \REL \eqdef \{ (\relReg_{\kf F}, \relI{\place}_{\kf F})
 503   \mid \kf F \text{\T ÛËÁÌÁ ëÒÉÐËÅ} \}
 504   $$
 505 \end{definition}
 506
 507 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 508 \subsection{æÏÒÍÕÌÙ, ÔÅÏÒÉÉ, ÐÒÏÂÌÅÍÁ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ}
 509 \label{sec:theories-equivalence}
 510
 511 \todo{[ÐÅÒÅÎÅÓÔÉ × ïÂÝÅÅ?]}
 512
 513 íÙ ÉÓÐÏÌØÚÕÅÍ ÔÁËÉÅ ÏÂÏÚÎÁÞÅÎÉÑ
 514 (×ÓÌÅÄ ÚÁ~\cite{KA-modular-elimination}):
 515
 516 \todo{[ÞÔÏ ÚÁ ÆÏÒÍÕÌÙ?]}
 517
 518 \begin{itemize}
 519 \item ðÕÓÔØ $\ka K$ ÁÌÇÅÂÒÁ ëÌÉÎÉ,
 520   $I\colon \Sigma \to \ka K$\T ÉÎÔÅÒÐÒÅÔÁÃÉÑ,
 521   $\phi$\T ÆÏÒÍÕÌÁ Ó ÓÉÍ×ÏÌÁÍÉ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ× ÉÚ~$\Sigma$.
 522   ôÏÇÄÁ $\ka K, I \models \phi$ ÚÎÁÞÉÔ, ÞÔÏ $\ka K$ ÕÄÏ×ÌÅÔ×ÏÒÑÅÔ
 523   $\phi$ ÐÒÉ ÉÎÔÅÒÐÒÅÔÁÃÉÉ~$I$.
 524 \item ðÕÓÔØ $\Gamma \subseteq \{ (\ka K, I) \mid \ka \in \KA,\,
 525   I\colon \Sigma \to \ka K \text{\T ÉÎÔÅÒÐÒÅÔÁÃÉÑ} \}$
 526   (\te ÎÅËÏÔÏÒÏÅ ÍÎÏÖÅÓÔ×Ï ÐÁÒ ÍÏÄÅÌÅÊ É ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÈ
 527   ÉÎÔÅÒÐÒÅÔÁÃÉÊ).
 528   ôÏÇÄÁ $\Gamma \models \phi$ ÚÎÁÞÉÔ,
 529   ÞÔÏ $\ka K, I \models \phi$ ÄÌÑ ×ÓÅÈ $(\ka K,I) \in \Gamma$.
 530 \item $\ka K \models \phi$ ÚÎÁÞÉÔ, ÞÔÏ $\ka K, I \models \phi$
 531   ÄÌÑ ×ÓÑËÏÊ ÉÎÔÅÒÐÒÅÔÁÃÉÉ $I\colon \Sigma \to \ka K$.
 532 \item ðÕÓÔØ $\class C$ ËÌÁÓÓ ÁÌÇÅÂÒ. ôÏÇÄÁ $\class C \models
 533   \phi$ ÚÎÁÞÉÔ, ÞÔÏ $\ka K \models \phi$ ÄÌÑ ×ÓÅÈ $\ka K \in \class C$.
 534 \item ðÕÓÔØ $\Psi$ ÍÎÏÖÅÓÔ×Ï ÆÏÒÍÕÌ. $\Psi \models \phi$
 535   ÚÎÁÞÉÔ, ÞÔÏ $\ka K, I \models \phi$ ÄÌÑ ×ÓÅÈ ÐÁÒ $(\ka K, I)$,
 536   ÕÄÏ×ÌÅÔ×ÏÒÑÀÝÉÈ $\Psi$ (\te ÔÁËÉÈ, ÞÔÏ $\ka K, I \models \psi$ ÄÌÑ
 537   ËÁÖÄÏÊ $\psi \in \Psi$). \todo{[ÎÕÖÎÏ ÌÉ? ëÁË ÓÏÇÌÁÓÕÅÔÓÑ Ó $\Gamma|\Psi$?]}
 538 \end{itemize}
 539
 540 \begin{application}
 541 æÏÒÍÁÌØÎÏ ÍÙ ÐÏËÁ ÄÁÌÉ
 542 ÔÏÌØËÏ ÏÄÎÏ ÏÐÒÅÄÅÌÅÎÉÅ ÔÏÇÏ, ÞÔÏ ÍÙ ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ ÐÒÏÇÒÁÍÍÁÍÉ\T
 543 ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ $\RExp_\Sigma$\T
 544 ÁÂÓÔÒÁËÔÎÙÅ <<ÌÉÎÅÊÎÏ>> ÚÁÐÉÓÁÎÎÙÅ ÐÒÏÇÒÁÍÍÙ. äÁÌØÛÅ ÂÕÄÕÔ É ÄÒÕÇÉÅ
 545 ×ÉÄÙ ÐÒÏÇÒÁÍÍ.
 546 óÅÍÁÎÔÉËÕ ÒÅÁÌØÎÙÈ ÐÒÏÇÒÁÍÍ × ÒÁÍËÁÈ  ÎÁÛÅÇÏ ÐÏÄÈÏÄÁ ÍÙ <<ÍÏÄÅÌÉÒÕÅÍ>> ÐÒÉ ÐÏÍÏÝÉ
 547 ÁÌÇÅÂÒ ëÌÉÎÉ; ÜÔÏ\T ÎÁÉÂÏÌÅÅ ÏÂÝÅÅ ÄÏÐÕÝÅÎÉÅ Ï ÓÅÍÁÎÔÉËÅ
 548 × ÎÁÛÅÍ ÉÓÓÌÅÄÏ×ÁÎÉÉ. é ÍÙ ÖÅÌÁÅÍ ÉÓÓÌÅÄÏ×ÁÔØ ÓÅÍÁÎÔÉÞÅÓËÉÅ Ó×ÏÊÓÔ×Á
 549 ÁÂÓÔÒÁËÃÉÊ ÐÒÏÇÒÁÍÍ, ÏÓÏÂÅÎÎÏ ÐÒÏÂÌÅÍÙ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ.
 550
 551 òÁÚÒÅÛÉÍÏÓÔØ ÐÒÏÂÌÅÍÙ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ ÐÒÏÇÒÁÍÍ ÍÙ ÂÕÄÅÍ ÐÏÎÉÍÁÔØ ËÁË
 552 ÒÁÚÒÅÛÉÍÏÓÔØ ÜË×ÁÃÉÏÎÁÌØÎÏÊ ÔÅÏÒÉÉ $\EOf \class C$, ÇÄÅ $\class C$\T
 553 ËÌÁÓÓ ÁÌÇÅÂÒ ëÌÉÎÉ (ÉÌÉ ÁÌÇÅÂÒ É ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÈ ÉÎÔÅÒÐÒÅÔÁÃÉÊ),
 554 ÄÏÐÕÓÔÉÍÙÈ × ËÁÞÅÓÔ×Å ÓÅÍÁÎÔÉËÉ ÐÒÏÇÒÁÍÍ ÐÒÉ ÎÁÛÅÊ
 555 ÁÂÓÔÒÁËÃÉÉ. îÁÐÒÉÍÅÒ, ÅÓÌÉ ÍÙ ÄÅÌÁÅÍ ÔÏÌØËÏ ÓÁÍÙÅ ÏÂÝÉÅ ÄÏÐÕÝÅÎÉÑ Ï
 556 ÓÅÍÁÎÔÉËÅ ÐÒÏÇÒÁÍÍ, ×ÏÚÍÏÖÎÙÅ × ÒÁÍËÁÈ ÎÁÛÅÇÏ ÐÏÄÈÏÄÁ,
 557 ÔÏ ÎÁÓ ÉÎÔÅÒÅÓÕÅÔ ×ÏÐÒÏÓ Ï ÒÁÚÒÅÛÉÍÏÓÔÉ $\EOf\KA$ ËÁË ÒÅÁÌÉÚÁÃÉÑ ÎÁ
 558 ÔÅÈÎÉÞÅÓËÏÍ ÕÒÏ×ÎÅ ×ÏÐÒÏÓÁ Ï ÐÒÏÂÌÅÍÅ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ ÐÒÏÇÒÁÍÍ ÎÁ
 559 ÐÒÅÄÍÅÔÎÏÍ ÕÒÏ×ÎÅ. ðÒÉ ÂÏÌÅÅ Ö£ÓÔËÉÈ ÕÓÌÏ×ÉÑÈ ÎÁ ÓÅÍÁÎÔÉËÕ\T $\EOf
 560 \KAc$. åÓÌÉ ÍÙ ÄÏÐÕÓËÁÅÍ ÔÏÌØËÏ ÒÅÌÑÃÉÏÎÎÕÀ ÓÅÍÁÎÔÉËÕ ÄÌÑ ÎÁÛÉÈ
 561 ÐÒÏÇÒÁÍÍ, ÔÏ ÎÁÓ ÉÎÔÅÒÅÓÕÅÔ $\EOf \RKA$. îÕ É ÐÒÉ ËÌÁÓÓÉÞÅÓËÏÊ
 562 ÆÏÒÍÁÌØÎÏÑÚÙËÏ×ÏÊ ÓÅÍÁÎÔÉËÅ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ðü ÒÅÇÕÌÑÒÎÙÈ
 563 ×ÙÒÁÖÅÎÉÑ ÄÌÑ ÎÁÓ\T ÜÔÏ ÒÁÚÒÅÛÅÎÉÅ $\EOf \{ (\Reg_\Sigma, R_\Sigma)
 564 \mid \Sigma \text{\T ËÏÎÅÞÎÙÊ ÁÌÆÁ×ÉÔ} \}$.
 565
 566 úÁÍÅÔÉÍ, ÞÔÏ ÏÂÙÞÎÏ ÍÙ ÉÎÔÅÒÅÓÕÅÍÓÑ ÁÌÇÏÒÉÔÍÏÍ ÐÒÏ×ÅÒËÉ
 567 ÜË×É×ÁÌÅÎÔÎÏÓÔÉ ÐÒÏÇÒÁÍÍ, <<ÕÎÉ×ÅÒÓÁÌØÎÙÍ>> ÐÏ ÏÔÎÏÛÅÎÉÀ Ë
 568 ÐÁÒÁÍÅÔÒÕ~$\Sigma$, \te ÏÄÎÉÍ ÁÌÇÏÒÉÔÍÏÍ, ËÏÔÏÒÙÊ ÂÕÄÅÔ ÐÒÏ×ÅÒÑÔØ
 569 ÜË×É×ÁÌÅÎÔÎÏÓÔØ ÐÁÒÙ ÐÏÄÁÎÎÙÈ ÎÁ ×ÈÏÄ ÐÒÏÇÒÁÍÍ, × ËÁËÏÍ ÂÙ ËÏÎÅÞÎÏÍ
 570 ÁÌÆÁ×ÉÔÅ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ× ÏÎÉ ÎÉ ÂÙÌÉ ÓÏÓÔÁ×ÌÅÎÙ. üÔÏ ×ÐÏÌÎÅ
 571 ÓÏÏÔ×ÅÔÓÔ×ÕÅÔ ÎÁÛÅÍÕ ÔÅÈÎÉÞÅÓËÏÍÕ ÕÒÏ×ÎÀ, ÇÄÅ ÍÙ ÇÏ×ÏÒÉÍ Ï
 572 ÒÁÚÒÅÛÉÍÏÓÔÉ ÜË×ÁÃÉÏÎÁÌØÎÏÊ ÔÅÏÒÉÉ $\EOf \class C$, ÓÏÓÔÏÑÝÅÊ ÉÚ
 573 ÒÁ×ÅÎÓÔ× ÐÒÏÇÒÁÍÍ ×Ï ×ÓÅÈ ×ÏÚÍÏÖÎÙÈ ÁÌÆÁ×ÉÔÁÈ.
 574
 575 áÎÁÌÏÇÉÞÎÏ ÜÔÏÍÕ ÓÌÕÞÁÀ, × ÓÌÕÞÁÅ, ËÏÇÄÁ ÍÙ ÄÅÌÁÅÍ ÄÏÐÏÌÎÉÔÅÌØÎÙÅ
 576 ÄÏÐÕÝÅÎÉÑ Ï ÓÅÍÁÎÔÉËÅ, ÍÙ ÉÎÔÅÒÅÓÕÅÍÓÑ Horn\DÔÅÏÒÉÑÍÉ ($\HOf \class
 577 C$) ×ÍÅÓÔÏ ÜË×ÁÃÉÏÎÁÌØÎÙÈ\T \sm çÌÁ×Ù~\ref{cha:hypo-plain},
 578 \ref{cha:hypo-withTests}.
 579 \end{application}
 580
 581 \begin{remark}[$\REL$ É $\RKA$]
 582   ÷ ÜÔÏÍ ÚÁÍÅÞÁÎÉÉ ÍÙ ÐÒÏÓÔÏ ÓÄÅÌÁÅÍ ÂÏÌÅÅ Ñ×ÎÙÍÉ ÎÅËÏÔÏÒÙÅ
 583   ÏÓÏÂÅÎÎÏÓÔÉ ÄÁÎÎÙÈ ÎÁÍÉ ÏÐÒÅÄÅÌÅÎÉÊ $\REL$ É $\RKA$.
 584
 585   ñÓÎÏ, ÞÔÏ ÄÌÑ ×ÓÑËÏÊ ÒÅÌÑÃÉÏÎÎÏÊ ÁÌÇÅÂÒÙ ëÌÉÎÉ~$\ka K$ É ÎÅËÏÔÏÒÏÊ
 586   ÉÎÔÅÒÐÒÅÔÁÃÉÉ $I\map \Sigma \to \ka K$ ÐÏÄÁÌÇÅÂÒÁ~$I(\RExp_\Sigma)$
 587   ÁÌÇÅÂÒÙ~$\ka K$,
 588   Ñ×ÌÑÀÝÁÑÓÑ ÏÂÒÁÚÏÍ $\RExp_\Sigma$ ÐÒÉ ÉÎÔÅÒÐÒÅÔÁÃÉÉ~$I$, ÂÕÄÅÔ
 589   ÉÚÏÍÏÒÆÎÁ ÎÅËÏÔÏÒÏÊ $\relReg_{\kf F}$, Á ÉÍÅÎÎÏ, ÎÁ ÛËÁÌÅ ëÒÉÐËÅ $\kf F =
 590   (I(\RExp_\Sigma), I)$ ÎÁÄ~$\Sigma$.
 591   éÚÏÍÏÒÆÉÚÍ ÂÕÄÅÔ ÔÁËÏÊ:
 592   $$
 593   I(s) \mapsto \relI{s}_{\kf F}
 594   \text{ ÄÌÑ $s \in \RExp_{\Sigma}$.}
 595   $$
 596
 597   üÌÅÍÅÎÔÁÒÎÙÅ ÔÅÏÒÉÉ
 598   ÁÌÇÅÂÒÙ~$\ka K$ (ÍÎÏÖÅÓÔ×Ï ÆÏÒÍÕÌ ÑÚÙËÁ ÐÅÒ×ÏÇÏ ÐÏÒÑÄËÁ, ËÏÔÏÒÙÅ
 599   ×ÅÒÎÙ × $\ka K$) É ÁÌÇÅÂÒÙ~$\relReg_{\kf F}$ ÒÁÚÌÉÞÎÙ.
 600
 601   îÏ ÄÌÑ ×ÙÑÓÎÅÎÉÑ ÒÁ×ÅÎÓÔ×Á ÉÎÔÅÒÐÒÅÔÁÃÉÊ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ
 602   ÒÁÚÎÉÃÙ ÍÅÖÄÕ ÎÉÍÉ ÜÔÉÍÉ ÁÌÇÅÂÒÁÍÉ ÎÅÔ:
 603   $$
 604   \ka K, I \models s = t
 605   \iff
 606   I(\ka K), I \models s = t
 607   \iff
 608   \relReg_{\kf F}, \relIP_{\kf F} \models s = t
 609   $$
 610   ÄÌÑ ×ÓÑËÉÈ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ~$s$ É~$t$ ÎÁÄ~$\Sigma$.
 611   éÌÉ × ÄÒÕÇÉÈ ÏÂÏÚÎÁÞÅÎÉÑÈ:
 612   $$
 613   \EOf \{ (\ka K, I) \}
 614   =
 615   \EOf \{ (I(\ka K), I) \}
 616   =
 617   \EOf \{ (\relReg_{\kf F}, \relIP_{\kf F}) \}.
 618   $$
 619   ðÒÉÈÏÄÉÍ Ë ×Ù×ÏÄÕ, ÞÔÏ $\EOf \REL = \EOf \RKA$.
 620
 621   ôÅ ÖÅ ÒÁÓÓÕÖÄÅÎÉÑ ÍÏÖÎÏ ÐÏ×ÔÏÒÉÔØ É ÄÌÑ \tD{ÕÎÉ×ÅÒÓÁÌØÎÙÈ
 622   Horn\DÆÏÒÍÕÌ}{def:Horn-formula} É ÐÒÉÊÔÉ Ë ×Ù×ÏÄÕ, ÞÔÏ
 623   $\HOf \REL = \HOf \RKA$.
 624
 625   äÌÑ ÃÅÌÅÊ ÎÁÛÉÈ ÉÓÓÌÅÄÏ×ÁÎÉÊ ÍÅÖÄÕ $\REL$ É $\RKA$ ÎÅÔ ÒÁÚÎÉÃÙ.
 626
 627   \todo{[ïÔÌÉÞÎÙ ÌÉ ÜÌÅÍÅÎÔÁÒÎÙÅ ÔÅÏÒÉÉ $\RKA$ É $\REL$?]}
 628 \end{remark}
 629
 630 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 631 \subsection{÷ÏÐÒÏÓÙ ÍÅÔÁÔÅÏÒÉÉ ÁÌÇÅÂÒ ëÌÉÎÉ É ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ}
 632 \label{sec:rexpr-Qs}
 633 îÁÓ ÂÕÄÕÔ ÉÎÔÅÒÅÓÏ×ÁÔØ ×ÏÐÒÏÓÙ ÏÂ ÁÌÇÅÂÒÁÈ ëÌÉÎÉ (ÉÚ ÖÅÌÁÎÉÑ ÌÕÞÛÅ
 634 ÐÏÎÑÔØ ÉÈ Ó×ÏÊÓÔ×Á):
 635
 636 \begin{enumerate}
 637 \item
 638 ïÔÌÉÞÁÀÔÓÑ ÌÉ ××ÅÄ£ÎÎÙÅ ËÌÁÓÓÙ ÁÌÇÅÂÒ ëÌÉÎÉ (Ó ÔÏÞÎÏÓÔØÀ ÄÏ
 639 ÉÚÏÍÏÒÆÉÚÍÏ× ÁÌÇÅÂÒ)?
 640
 641 äÌÑ ËÌÁÓÓÏ× ÓÒÁÚÕ ÏÞÅ×ÉÄÎÙ ÔÁËÉÅ ×ÌÏÖÅÎÉÑ:
 642 \begin{equation}
 643   \label{eq:KA-classes-incl}
 644   \begin{aligned}
 645     \{ \relReg_{\kf F} \} \subsetneq \REL \subsetneq \RKA &\subseteq \KAc \subseteq \KA\\
 646     \{ \trReg_{\kf F} \} \subsetneq \TRACE &\subseteq \KAc\\
 647     \{ \Reg_{\Sigma} \} &\subsetneq \KAc
 648   \end{aligned}
 649 \end{equation}
 650
 651 õÞÅÓÔØ ÓÐÅÃÉÆÉÞÅÓËÉÅ ËÌÁÓÓÙ ÍÏÄÅÌÅÊ, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÅ ÏÐÒÅÄÅÌÅÎÉÑÍ
 652 ÓÅÍÁÎÔÉËÉ ÐÒÏÇÒÁÍÍ, ÜË×É×ÁÌÅÎÔÎÏÓÔÉ ÐÒÏÇÒÁÍÍ, ÎÁÐÒÉÍÅÒ, \todo{[ÐÏÔÏÍ,
 653   ÇÄÅ Á×ÔÏÍÁÔÙ, É × ÄÒÕÇÉÈ çÌÁ×ÁÈ??]}.
 654
 655 \item
 656 ïÔÌÉÞÁÀÔÓÑ ÌÉ ÜÌÅÍÅÎÔÁÒÎÙÅ ÔÅÏÒÉÉ ××ÅÄ£ÎÎÙÈ ËÌÁÓÓÏ× ÁÌÇÅÂÒ ëÌÉÎÉ?
 657
 658 üÔÏ ÄÁÓÔ ×ÏÚÍÏÖÎÏÓÔØ ÌÕÞÛÅ ÐÏÎÑÔØ ÉÈ Ó×ÏÊÓÔ×Á. îÏ ÓÐÅÃÉÁÌØÎÏ ÜÔÏÍÕ
 659 ×ÏÐÒÏÓÕ × ÜÔÏÊ ÒÁÂÏÔÅ ÍÙ ÎÅ ÕÄÅÌÑÅÍ ×ÎÉÍÁÎÉÅ.
 660
 661 \end{enumerate}
 662
 663 é ×ÏÐÒÏÓÙ, Ó×ÑÚÁÎÎÙÅ Ó ÓÅÍÁÎÔÉËÏÊ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ:
 664
 665 \begin{enumerate}
 666
 667 \item
 668 ïÔÌÉÞÁÀÔÓÑ ÌÉ ÜË×ÁÃÉÏÎÁÌØÎÙÅ ÔÅÏÒÉÉ ××ÅÄ£ÎÎÙÈ ËÌÁÓÓÏ× ÁÌÇÅÂÒ ëÌÉÎÉ?
 669
 670 óÒÁÚÕ ÏÞÅ×ÉÄÎÙ ÔÁËÉÅ ×ÌÏÖÅÎÉÑ (ÕÞÉÔÙ×ÁÑ úÁÍÅÞÁÎÉÅ~\ref{rem:REL-RKA}:
 671 \begin{equation}
 672 \label{eq:EKA-incl}
 673 \begin{aligned}
 674   \EOf\{ \relReg_{\kf F} \} \supseteq \EOf\REL = \EOf\RKA
 675   &\supseteq \EOf\KAc \supseteq \EOf\KA\\
 676   \EOf\{ \trReg_{\kf F} \} \supseteq \EOf\TRACE &\supseteq \EOf\KAc\\
 677   \EOf\{ \Reg_{\Sigma} \} &\supseteq \EOf\KAc
 678 \end{aligned}
 679 \end{equation}
 680
 681 \item óÕÝÅÓÔ×ÕÀÔ ÌÉ Ó×ÏÂÏÄÎÙÅ ÁÌÇÅÂÒÙ \todo{(ÏÐÒÅÄ?)} × ÜÔÉÈ ËÌÁÓÓÁÈ?
 682 ëÁË ÏÎÉ ÕÓÔÒÏÅÎÙ?
 683
 684 úÎÁÎÉÅ Ï Ó×ÏÂÏÄÎÙÈ ÁÌÇÅÂÒÁÈ ÐÏÍÏÖÅÔ ÒÁÓÓÕÖÄÁÔØ É ÄÅÌÁÔØ ×Ù×ÏÄÙ ÐÏ
 685 ÄÒÕÇÉÍ ×ÏÐÒÏÓÁÍ ÏÂ ÜÔÉÈ ËÌÁÓÓÁÈ.
 686
 687 \todo{[éÎÏÇÄÁ ÏÔ×ÅÔ Ï ÓÕÝÅÓÔ×Ï×ÁÎÉÉ/ÓÔÒÏÅÎÉÉ Ó×ÏÂÏÄÎÙÈ ÁÌÇÅÂÒ ÍÏÖÅÔ
 688   ÂÙÔØ ÄÁÎ ÏÂÝÉÍÉ ÓÒÅÄÓÔ×ÁÍÉ õÎÉ×ÅÒÓÁÌØÎÏÊ ÁÌÇÅÂÒÙ É ôÅÏÒÉÉ
 689   ËÁÔÅÇÏÒÉÊ.]}
 690
 691 \item òÁÚÒÅÛÉÍÙ ÌÉ ÜË×ÁÃÉÏÎÁÌØÎÙÅ ÔÅÏÒÉÉ ÜÔÉÈ ËÌÁÓÓÏ×?
 692
 693 ëÁË ÕÖÅ ÇÏ×ÏÒÉÌÏÓØ × ðÒÉÍÅÞÁÎÉÉ~\ref{appl:equa-equiv-problem},
 694 ÜÔÏÔ ×ÏÐÒÏÓ ÄÌÑ ÎÁÓ ËÁË ÒÁÚ É ÅÓÔØ ×ÏÐÒÏÓ Ï
 695 ÐÒÏÂÌÅÍÅ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ ÐÒÏÇÒÁÍÍ.
 696
 697 é Ó ËÁËÉÍÉ ÄÒÕÇÉÍÉ ÐÒÏÂÌÅÍÁÍÉ Ó×ÑÚÁÎÁ ÒÁÚÒÅÛÉÍÏÓÔØ ÜË×ÁÃÉÏÎÁÌØÎÙÈ
 698 ÔÅÏÒÉÊ (ÐÒÏÂÌÅÍÁ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ)?
 699 îÁÐÒÉÍÅÒ, ËÁË Ó×ÑÚÁÎÁ ÐÒÏÂÌÅÍÁ ×ËÌÀÞÅÎÉÑ É ÐÒÏÂÌÅÍÁ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ?
 700 (îÁ ÜÔÏÔ ×ÏÐÒÏÓ ÏÔ×ÅÔ ÐÒÏÓÔÏÊ: ÏÎÉ Ó×ÏÄÑÔÓÑ ÄÒÕÇ Ë ÄÒÕÇÕ.
 701 éÚ-ÚÁ ÏÐÒÅÄÅÌÅÎÉÑ ×ËÌÀÞÅÎÉÑ ÞÅÒÅÚ
 702 ÒÁ×ÅÎÓÔ×Ï ÎÁ ÓÔÒ.~\pageref{eq:KA-order} ×~\eqref{eq:KA-order}:
 703   \begin{equation}\tag{\ref{eq:KA-order}}
 704     x \leq y \equivdef x + y = y,
 705   \end{equation}
 706   ÞÔÏÂÙ ÐÒÏ×ÅÒÉÔØ ×ËÌÀÞÅÎÉÅ <<$\ka K, I \models s \leq t$>>,
 707   ÄÏÓÔÁÔÏÞÎÏ ÕÍÅÔØ ÐÒÏ×ÅÒÉÔØ ÒÁ×ÅÎÓÔ×Ï <<$\ka K, I \models s + t =
 708   t$>>. îÁÏÂÏÒÏÔ:
 709   $$
 710   \ka K, I \models s = t
 711   \iff
 712   \begin{cases}
 713   \ka K, I \models s \leq t\\
 714   \ka K, I \models s \geq t
 715   \end{cases}
 716   $$
 717   ÷ ÓÌÕÞÁÅ ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÈ ÐÒÏÇÒÁÍÍ, ÒÁÓÓÍÁÔÒÉ×ÁÅÍÙÈ × ÄÒÕÇÉÈ
 718   òÁÚÄÅÌÁÈ, ÏÔ×ÅÔ ÓÏ×ÓÅÍ ÎÅ ÔÁËÏÊ ÐÒÏÓÔÏÊ, \tk $s+t$ ÍÏÖÅÔ ÎÅ ÐÏÐÁÓÔØ
 719   × ËÌÁÓÓ ÒÁÓÓÍÁÔÒÉ×ÁÅÍÙÈ ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÈ ÐÒÏÇÒÁÍÍ, É
 720   ÚÎÁÞÉÔ, ÒÁ×ÅÎÓÔ×Ï <<$\ka K, I \models s + t = s$>>
 721   ÍÏÖÅÔ ÎÅ ÓÏÏÔ×ÅÔÓÔ×Ï×ÁÔØ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÈ ÐÒÏÇÒÁÍÍ.)
 722
 723 \todo{[ÄÒÕÇÉÅ ÐÒÏÂÌÅÍÙ]}
 724
 725 \item íÅÓÔÏ ÐÒÏÂÌÅÍÙ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ × ÉÅÒÁÒÈÉÉ ÓÌÏÖÎÏÓÔÅÊ (\todo{×ÙÞÉÓÌÉÍÙÈ
 726   É ÎÅ×ÙÞÉÓÌÉÍÙÈ}).
 727
 728 \item ëÁËÉÅ ÍÏÖÎÏ ÎÁÚ×ÁÔØ ÉÎÔÅÒÅÓÎÙÅ ÏÓÏÂÙÅ ÐÏÄÓÌÕÞÁÉ?
 729
 730   íÏÖÎÏ ÌÉ ÎÁÌÏÖÉÔØ ÒÁÚÕÍÎÙÅ ÏÇÒÁÎÉÞÅÎÉÑ ÎÁ ËÌÁÓÓ ÍÏÄÅÌÅÊ É
 731   ÓÉÎÔÁËÓÉÞÅÓËÉÅ ËÏÎÓÔÒÕËÃÉÉ ÔÁË, ÞÔÏÂÙ ÈÁÒÁËÔÅÒÉÓÔÉËÉ ÒÁÚÒÅÛÉÍÏÓÔÉ ÉÚÍÅÎÉÌÉÓØ?
 732
 733 \end{enumerate}
 734
 735 ÷ ÜÔÏÍ ÐÒÏÓÔÏÍ ÓÌÕÞÁÅ (ÐÒÏÓÔÏÍ\T ÐÏ ÓÒÁ×ÎÅÎÉÀ Ó ÔÅÍÉ, ÞÔÏ ÒÁÓÓÍÁÔÒÉ×ÁÀÔÓÑ ×
 736 ÓÌÅÄÕÀÝÉÈ çÌÁ×ÁÈ \ref{cha:free-withTests}, \ref{cha:hypo-plain},
 737 \ref{cha:hypo-withTests})
 738 ÍÎÏÇÉÅ ÏÔ×ÅÔÙ ÈÏÒÏÛÏ ÉÚ×ÅÓÔÎÙ. ïÎÉ ÐÒÉÎÁÄÌÅÖÁÔ ôÅÏÒÉÉ
 739 ËÏÎÅÞÎÙÈ Á×ÔÏÍÁÔÏ×. ë ÔÏÍÕ ÖÅ, ÎÁ ÎÉÈ ÌÅÇÞÅ ÏÔ×ÅÞÁÔØ, ÉÍÅÑ × ×ÉÄÕ
 740 ÓÒÁÚÕ Ä×Á
 741 ×ÉÄÁ ÐÒÏÇÒÁÍÍ: \tDJust{ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ} É \tND{ËÏÎÅÞÎÙÅ
 742   Á×ÔÏÍÁÔÙ}{def:nfa}, ËÏÔÏÒÙÅ ÍÙ É ××ÅÄ£Í × ÒÁÓÓÍÏÔÒÅÎÉÅ × ÓÌÅÄÕÀÝÅÍ
 743 òÁÚÄÅÌÅ~\ref{sec:nfa}, ÐÏÓÌÅ ÞÅÇÏ ÂÕÄÅÍ ÏÔ×ÅÞÁÔØ ÎÁ ×ÏÐÒÏÓÙ.
 744
 745 \subsubsection{ðÒÏÓÔÙÅ ÏÔ×ÅÔÙ ÎÁ ×ÏÐÒÏÓÙ Ï ËÌÁÓÓÁÈ ÁÌÇÅÂÒ}
 746 îÁ ×ÏÐÒÏÓÙ ÐÅÒ×ÏÊ ÇÒÕÐÐÙ ÓÒÁÚÕ ÄÁÄÉÍ ÏÔ×ÅÔÙ.
 747
 748 \begin{proposition} (\cite{KA-closedSr}).
 749   $\KAc \subsetneq \KA$.
 750 \end{proposition}
 751 ÷Ï-ÐÅÒ×ÙÈ, \tND{tropical semiring}{def:tropicalSr} ÍÏÖÅÔ ÓÌÕÖÉÔØ
 752 ÐÒÉÍÅÒÏÍ \KA, ÎÏ ÎÅ \KAc \cite{??}.
 753 ÷Ï-×ÔÏÒÙÈ, Ó×ÉÄÅÔÅÌØÓÔ×ÏÍ ÜÔÏÇÏ
 754 ÍÏÖÅÔ ÂÙÔØ ÔÏ, ÞÔÏ:
 755 \begin{equation}
 756   \label{eq:H-differ'}\tag{\ref{eq:H-differ}}
 757   \HornOf\RKA \supsetneq  \HornOf\KAc \supsetneq \HornOf\KA
 758 \end{equation}
 759 ËÁË ÓÌÅÄÓÔ×ÉÅ ÒÁÚÎÏÊ ÓÌÏÖÎÏÓÔÉ ÒÁÚÒÅÛÅÎÉÑ ÜÔÉÈ ÔÅÏÒÉÊ,
 760 ÓÍ.\ õÔ×.~\ref{prop:HKAc-HKA}, \ref{prop:HRKA-HKAc}.
 761
 762 éÚ~\eqref{eq:H-differ'} ÓÌÅÄÕÅÔ É ÒÁÚÌÉÞÉÅ ÜÌÅÍÅÎÔÁÒÎÙÈ ÔÅÏÒÉÊ ÜÔÉÈ
 763   ËÌÁÓÓÏ×, É ÓÁÍÉÈ ËÌÁÓÓÏ×.
 764
 765 éÔÁË:
 766 \begin{equation}
 767   \label{eq:KA-classes-incl-A}
 768   \begin{aligned}
 769     \{ \relReg_{\kf F} \} \subsetneq \REL \subsetneq \RKA &\subsetneq \KAc \subsetneq \KA\\
 770     \{ \trReg_{\kf F} \} \subsetneq \TRACE &\Qm\subseteq \KAc\\
 771     \{ \Reg_{\Sigma} \} &\subsetneq \KAc
 772   \end{aligned}
 773 \end{equation}
 774 \begin{equation}
 775 \label{eq:EKA-incl}
 776 \begin{aligned}
 777   \ThOf\REL \Qm\supseteq \ThOf\RKA
 778   &\supsetneq \ThOf\KAc \supsetneq \ThOf\KA\\
 779   \ThOf\TRACE & \Qm\supseteq \ThOf\KAc\\
 780   \ThOf\{ \Reg_{\Sigma} \} &\Qm{\Over{$\Sigma$}\supseteq} \ThOf\KAc
 781 \end{aligned}
 782 \end{equation}
 783
 784 \begin{question}
 785   íÅÓÔÏ $\TRACE$ × ÓÉÓÔÅÍÅ ×ÌÏÖÅÎÉÊ.
 786 \end{question}
 787
 788
 789
 790 \subsection{ðÒÏÇÒÁÍÍÙ: ËÏÎÅÞÎÙÅ Á×ÔÏÍÁÔÙ}
 791 \label{sec:nfa}
 792
 793 ïÄÉÎ ÓÐÏÓÏÂ ÚÁÐÉÓÉ ÐÒÏÇÒÁÍÍ, <<ÌÉÎÅÊÎÙÊ>>\T ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ\T Õ
 794 ÎÁÓ ÂÙÌ.
 795 íÙ ÈÏÔÉÍ ÒÁÂÏÔÁÔØ É Ó ÄÒÕÇÉÍ ÓÐÏÓÏÂÏÍ ÚÁÐÉÓÉ ÐÒÏÇÒÁÍÍ.
 796 íÙ ÉÍÅÅÍ × ×ÉÄÕ
 797 ÐÒÅÄÓÔÁ×ÌÅÎÉÅ ÐÒÏÇÒÁÍÍÙ (ÓÉÎÔÁËÓÉÞÅÓËÏÊ ÓÔÏÒÏÎÙ ÐÒÏÇÒÁÍÍÙ)
 798 × ×ÉÄÅ ÇÒÁÆÁ.
 799 ôÁË ËÁË × ÎÁÛÅÍ ÐÏÎÉÍÁÎÉÉ ÎÁ ×ÅÒÈÎÅÍ ÐÒÅÄÍÅÔÎÏÍ
 800 ÕÒÏ×ÎÅ ÜÔÏ ÏÂßÅËÔÙ ÏÄÎÏÇÏ ÒÏÄÁ
 801 (ÞÔÏ <<ÌÉÎÅÊÎÙÅ>> ÐÒÏÇÒÁÍÍÙ, ÞÔÏ <<ÇÒÁÆÏ×ÙÅ>>),
 802 ÏÔÎÏÓÉÔÅÌØÎÏ ËÏÔÏÒÙÈ ÍÙ ÚÁÄÁ£ÍÓÑ ÔÅÍÉ ÖÅ ÓÁÍÙÍÉ ×ÏÐÒÏÓÁÍÉ ÐÒÅÄÍÅÔÎÏÇÏ ÕÒÏ×ÎÑ,
 803 ÍÙ
 804 ÈÏÔÉÍ, ÞÔÏÂÙ É ÔÅÈÎÉÞÅÓËÏÍ ÕÒÏ×ÎÅ × ÎÁÛÅÍ ÉÓÓÌÅÄÏ×ÁÎÉÉ
 805 ÐÒÏÑ×ÌÑÌÁÓØ ÁÎÁÌÏÇÉÑ.
 806
 807 æÏÒÍÁÌØÎÏ ÅÝ£ ÏÄÉÎ ÓÐÏÓÏÂ ÚÁÐÉÓÉ ÐÒÏÇÒÁÍÍ ÂÕÄÅÔ ÏÓÎÏ×ÁÎ ÎÁ ÍÁÔÒÉÃÁÈ.
 808 õÄÁÞÎÏ ÌÉ ÆÏÒÍÁÌØÎÏÅ ÕÓÔÒÏÊÓÔ×Ï, ËÏÔÏÒÏÅ Õ ÎÁÓ ÐÏÌÕÞÉÔÓÑ, ÎÅ ÏÞÅÎØ
 809 ÐÏÎÑÔÎÏ: ÓÔÒÁÄÁÅÔ ÌÉ ÏÎÏ ÎÅÄÏÏÂÏÝÅÎÉÅÍ ÉÌÉ ÐÅÒÅÏÂÏÝÅÎÉÅÍ, ÏÔÒÁÖÁÅÔ ÌÉ
 810 ÓÕÔØ ÐÒÅÄÍÅÔÎÏÇÏ ÕÒÏ×ÎÑ?
 811
 812
 813 \subsubsection{íÁÔÒÉÞÎÙÅ ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ É ÁÌÇÅÂÒÙ ÍÁÔÒÉÃ}
 814
 815 íÎÏÖÅÓÔ×Ï ÍÁÔÒÉÃ ÒÁÚÍÅÒÁ $m \times n$, ÓÏÓÔÁ×ÌÅÎÎÙÈ ÉÚ ÜÌÅÍÅÎÔÏ×~$C$,
 816 ÍÙ ÏÂÏÚÎÁÞÁÅÍ $C^{m \times n}$. üÌÅÍÅÎÔ Ó ÉÎÄÅËÓÏÍ $i,j$ × ÍÁÔÒÉÃÅ $x
 817 \in C^{m \times n}$ ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ $x[i,j]$. âÏÌÅÅ ÏÂÝÅÅ
 818 ÏÂÏÚÎÁÞÅÎÉÅ: ÓÔÏÌÂÃÙ É ÓÔÒÏËÉ ÍÁÔÒÉÃÙ ÐÒÏÉÎÄÅËÓÉÒÏ×ÁÎÙ ÎÅ ÎÁÔÕÒÁÌØÎÙÍÉ
 819 ÞÉÓÌÁÍÉ, Á ÜÌÅÍÅÎÔÁÍÉ ÍÎÏÖÅÓÔ× $Q', Q''$. ôÏÇÄÁ ÍÎÏÖÅÓÔ×Ï ÔÁËÉÈ
 820 ÍÁÔÒÉÃ ÎÁÚ $C$\T $C^{Q' \times Q''}$; ÜÌÅÍÅÎÔ ÔÁËÏÊ ÍÁÔÒÉÃÙ $x$
 821 ÏÂÏÚÎÁÞÁÅÔÓÑ $x[u,v]$, ÇÄÅ $u \in Q'$, $v \in Q''$.
 822
 823 \newcommand*{\Terms}{Z}
 824 âÕÄÅÍ ÒÁÓÓÍÁÔÒÉ×ÁÔØ \tING{ÍÁÔÒÉÞÎÙÅ ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ}
 825 $\MRExp(\Terms)$\T <<ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ ÎÁÄ ÍÁÔÒÉÃÁÍÉ>>, ÓÏÓÔÁ×ÌÅÎÎÙÍÉ
 826 × Ó×ÏÀ ÏÞÅÒÅÄØ ÉÚ ÔÅÒÍÏ×~$\Terms$ ÎÅËÏÔÏÒÏÇÏ ÑÚÙËÁ.
 827
 828 \begin{table}[hbtp]
 829   \centering
 830 $$
 831 \begin{array}{lll}
 832 \parbox{7em}{ÓÉÎÔ.\ ÍÁÔÒÉÃÙ ÔÉÐÁ~$m \times n$}
 833 & \smatr{s}{m}{n}, \smatr{t}{m}{n}, \dotsc
 834 & \langle\text{{\small ÜÌÅÍÅÎÔÙ } $\Terms^{m \times n}$}\rangle\\
 835 \parbox{7em}{ÔÅÒÍÙ ÔÉÐÁ~$m \times n$}
 836 & \matrt{s}{m}{n}, \matrt t{m}{n}, \dotsc
 837 & \matrt{s}{m}{n} ::= \smatr{s}{m}{n}
 838 \ |\ \matrt{s}{m}{n}+\matrt{t}{m}{n}\ |\ \matrt{s}{m}{k} \cdot \matrt{t}{k}{n}
 839 \ |\ \matrt{s}{m}{n}^*
 840 \end{array}
 841 $$
 842   \caption{ôÅÒÍÙ × ÏÐÒÅÄÅÌÅÎÉÉ ÍÁÔÒÉÞÎÙÈ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Terms$}
 843   \label{tab:KA-mregexp-bnf}
 844 \end{table}
 845 ôÅÒÍÙ ÔÏÌØËÏ ÏÄÎÏÇÏ ÔÉÐÁ $m \times n$
 846 ÍÙ ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ $\MRExp_{m \times n}(\Terms)$
 847
 848 \tING{á×ÔÏÍÁÔÎÙÅ ÍÁÔÒÉÃÙ} ÎÁÄ~$\Sigma$\T ÍÁÔÒÉÃÙ ÓÏÓÔÁ×ÌÅÎÎÙÅ ÉÚ
 849 ÔÅÒÍÏ×-\emph{ÐÒÏÓÔÙÈ ÓÕÍÍ} ÎÁÄ~$\Sigma$.
 850 \begin{table}[hbtp]
 851   \centering
 852 $$
 853 \begin{array}{lll}
 854 \text{ÐÒÏÓÔÙÅ ÐÒÏÉÚ×ÅÄÅÎÉÑ}
 855 & \sigma, \tau  \dotsc
 856 & \sigma ::= \langle\text{{\small ÂÁÚÏ×ÙÅ ÏÐÅÒÁÔÏÒÙ}}\rangle
 857 \ |\ 1\ |\ \sigma \tau\\
 858 \text{ÐÒÏÓÔÙÅ ÓÕÍÍÙ}
 859 & \srterm s, \srterm t  \dotsc
 860 & \srterm s ::= \sigma
 861 \ |\ 0\ |\ \srterm s+\srterm t\\
 862 \end{array}
 863 $$
 864   \caption{ôÅÒÍÙ, ÉÓÐÏÌØÚÕÅÍÙÅ × ÏÐÒÅÄÅÌÅÎÉÉ Á×ÔÏÍÁÔÎÙÈ ÍÁÔÒÉÃ ÎÁÄ~$\Sigma$}
 865   \label{tab:KA-mregexp-bnf}
 866 \end{table}
 867
 868 á×ÔÏÍÁÔÎÙÅ ÍÁÔÒÉÃÙ\T ÞÁÓÔÎÙÊ ÓÌÕÞÁÊ ÍÁÔÒÉÃ, ÓÏÓÔÁ×ÌÅÎÎÙÈ ÉÚ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ
 869 ÎÁÄ~$\Sigma$.
 870
 871 ÷ ÒÅÚÕÌØÔÁÔÅ ÔÁËÏÇÏ ÏÐÒÅÄÅÌÅÎÉÑ
 872 ËÌÁÓÓ ÏÂßÅËÔÏ×, ËÏÔÏÒÙÅ ÍÙ ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ \tND{ËÏÎÅÞÎÙÍÉ
 873   Á×ÔÏÍÁÔÁÍÉ}{def:nfa},
 874 ÎÅ ÓÌÉÛËÏÍ ÒÁÓÈÏÄÉÔÓÑ Ó ÔÅÍ, ÞÔÏ ÔÒÁÄÉÃÉÏÎÎÏ ÎÁÚÙ×ÁÅÔÓÑ
 875 ËÏÎÅÞÎÙÍÉ Á×ÔÏÍÁÔÁÍÉ (ÎÅ ÓÌÉÛËÏÍ ÛÉÒÏË, ÎÏ ÄÏÓÔÁÔÏÞÅÎ, ÞÔÏÂÙ ×ËÌÀÞÉÔØ
 876 ÐÒÉ×ÙÞÎÙÅ ÏÂÝÉÅ ÏÐÒÅÄÅÌÅÎÉÑ).
 877
 878
 879 \paragraph{áÌÇÅÂÒÙ ëÌÉÎÉ ÍÁÔÒÉÃ.}
 880
 881 ÷ \cite{KA-regevents-complete},
 882 \cite[Lecture~7]{KA-lect02} ÐÏËÁÚÁÎÏ ËÁË ÄÌÑ ÌÀÂÏÊ
 883 ÁÌÇÅÂÒÙ ëÌÉÎÉ $\ka K$ ÍÏÖÎÏ ÏÐÒÅÄÅÌÉÔØ ÁÌÇÅÂÒÕ ëÌÉÎÉ $\kaMat(\ka K, n,
 884 n)$ Ë×ÁÄÒÁÔÎÙÈ ÍÁÔÒÉÃ ÒÁÚÍÅÒÁ $n
 885 \times n$, ÓÏÓÔÏÑÝÉÈ ÉÚ ÜÌÅÍÅÎÔÏ× $\ka K$, É ×ÏÏÂÝÅ, ÁÌÇÅÂÒÕ,
 886 ÜÌÅÍÅÎÔÁÍÉ ËÏÔÏÒÏÊ ÂÕÄÕÔ ÍÁÔÒÉÃÙ ÐÒÏÉÚ×ÏÌØÎÙÈ ÒÁÚÍÅÒÏ× (ÏÐÅÒÁÃÉÉ
 887 ÄÏÌÖÎÙ ÐÒÉÍÅÎÑÔØÓÑ Ó ÕÞ£ÔÏÍ ÒÁÚÍÅÒÏ×).
 888
 889 \todo{[ÔÏÞÎÅÅ]}
 890
 891 ðÒÉ ÜÔÏÍ ÐÏÄÁÌÇÅÂÒÁ Ë×ÁÄÒÁÔÎÙÈ ÍÁÔÒÉÃ ÎÁÄ $\ka K$ ÒÁÚÍÅÒÁ $1 \times 1$
 892 ÂÕÄÅÔ ÉÚÏÍÏÒÆÎÁ $\ka K$.
 893
 894 \paragraph{éÎÔÅÒÐÒÅÔÁÃÉÉ.}
 895 íÙ ÍÏÖÅÍ ÐÒÏÄÏÌÖÉÔØ ÉÎÔÅÒÐÒÅÔÁÃÉÀ $\Terms$ × ÎÅËÏÔÏÒÏÊ ÁÌÇÅÂÒÅ
 896 ëÌÉÎÉ~$\ka K$
 897 ÄÏ ÉÎÔÅÒÐÒÅÔÁÃÉÉ ÍÁÔÒÉÞÎÙÈ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ × \tND{ÁÌÇÅÂÒÁÈ ëÌÉÎÉ
 898   ÍÁÔÒÉÃ}{def:KA-of-matr} ÎÁÄ $\ka K$. óÅÊÞÁÓ ÂÕÄÅÔ ÐÏËÁÚÁÎÏ ËÁË.
 899
 900 \todo{[ÈÏÔÅÌ ÐÅÒÅÄÅÌÁÔØ. þÔÏ?]}
 901
 902 éÚ $I\colon \RExp_{\Sigma} \to \ka K$ ÐÏÌÕÞÁÅÍ
 903 \begin{align*}
 904 I\colon
 905 &\MRExp_{1 \times 1}(\RExp_{\Sigma}) \to \kaMat(\ka K, 1,1),\\
 906 &\vdots\\
 907 &\MRExp_{m \times n}(\RExp_{\Sigma}) \to \kaMat(\ka K, m,n),\\
 908 \vdots
 909 \end{align*}
 910 ÔÁË:
 911 $$
 912 I\colon
 913 \begin{pmatrix}
 914   s_{11} & \dotsc & s_{1n}\\
 915   \vdots && \vdots\\
 916   s_{m1} & \dotsc & s_{mn}
 917 \end{pmatrix}
 918 \mapsto
 919 \begin{pmatrix}
 920   I(s_{11}) & \dotsc & I(s_{1n})\\
 921   \vdots && \vdots\\
 922   I(s_{m1}) & \dotsc & I(s_{mn})
 923 \end{pmatrix}
 924 $$
 925
 926
 927 \subsubsection{ëÏÎÅÞÎÙÅ Á×ÔÏÍÁÔÙ: ÍÁÔÒÉÞÎÏÅ ÏÐÒÅÄÅÌÅÎÉÅ}
 928
 929 \paragraph{óÉÎÔÁËÓÉÓ.}
 930
 931 \begin{definition}[ÓÉÎÔÁËÓÉÓ Á×ÔÏÍÁÔÏ×]\label{def:nfa}
 932   \tING{ëÏÎÅÞÎÙÊ Á×ÔÏÍÁÔ ÎÁÄ $\Sigma$} Ó $n$ ÓÏÓÔÏÑÎÉÑÍÉ\T ÜÔÏ ÔÒÏÊËÁ:
 933   \begin{equation}
 934     \label{eq:nfa}
 935     (\smatr{I}{1}{n}, \smatr{M}{n}{n}, \smatr{F}{1}{n}),
 936   \end{equation}
 937   ÇÄÅ
 938   $\smatr{I}{1}{n}$, $\smatr{M}{n}{n}$, $\smatr{F}{1}{n}$\T
 939   Á×ÔÏÍÁÔÎÙÅ ÍÁÔÒÉÃÙ ÎÁÄ $\Sigma$ ÕËÁÚÁÎÎÙÈ ÔÉÐÏ×.
 940
 941   íÎÏÖÅÓÔ×Ï ËÏÎÅÞÎÙÈ Á×ÔÏÍÁÔÏ× ÎÁÄ~$\Sigma$ ÏÂÏÚÎÁÞÁÅÔÓÑ $\NFA_\Sigma$.
 942 \end{definition}
 943
 944 \begin{definition}[ÓÉÎÔÁËÓÉÓ Á×ÔÏÍÁÔÏ×]\label{def:nfa}
 945   ëÁÖÄÏÍÕ ËÏÎÅÞÎÏÍÕ Á×ÔÏÍÁÔÕ~\eqref{eq:nfa} ÎÁÄ $\Sigma$ ÓÏÏÔ×ÅÔÓÔ×ÕÅÔ
 946   ÍÁÔÒÉÞÎÏÅ ÒÅÇÕÌÑÒÎÏÅ ×ÙÒÁÖÅÎÉÅ:
 947   \begin{equation}
 948     \label{eq:nfa-exp}
 949     \smatrAny{I} \smatrAny{M}^* \transp{\smatrAny{F}},
 950   \end{equation}
 951   ÇÄÅ $\transp{\place}$\T ÎÁÛÅ ÍÅÔÁÏÂÏÚÎÁÞÅÎÉÅ ÄÌÑ ÔÒÁÎÓÐÏÎÉÒÏ×ÁÎÎÏÊ ÍÁÔÒÉÃÙ.
 952
 953   ÷ÙÒÁÖÅÎÉÑ ÔÁËÏÇÏ ×ÉÄÁ ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ \tING{Á×ÔÏÍÁÔÎÙÍÉ} (ÉÌÉ
 954   \tING{×ÙÒÁÖÅÎÉÑÍÉ ÐÏ×ÅÄÅÎÉÑ} Á×ÔÏÍÁÔÁ).
 955   \tING{íÎÏÖÅÓÔ×Ï Á×ÔÏÍÁÔÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ}~$\Sigma$ ÏÂÏÚÎÁÞÁÅÔÓÑ
 956   $\AExp_\Sigma$.
 957
 958   $\AExp_\Sigma$ É $\NFA_\Sigma$ ÎÁÈÏÄÑÔÓÑ ×Ï ×ÚÁÉÍÎÏ ÏÄÎÏÚÎÁÞÎÏÍ ÓÏÏÔ×ÅÔÓÔ×ÉÉ.
 959 \end{definition}
 960 ðÏÜÔÏÍÕ ÄÁÌØÛÅ ÍÙ ÂÕÄÅÍ ÏÂÙÞÎÏ ÐÒÏÓÔÏ ÇÏ×ÏÒÉÔØ ÏÂ Á×ÔÏÍÁÔÎÙÈ
 961 ×ÙÒÁÖÅÎÉÑÈ. ðÏÞÅÍÕ ÂÙÌÁ ×ÙÂÒÁÎÁ ÉÍÅÎÎÏ ÔÁËÁÑ ÆÏÒÍÁ Á×ÔÏÍÁÔÎÏÇÏ
 962 ×ÙÒÁÖÅÎÉÑ, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÅÇÏ ËÏÎÅÞÎÏÍÕ Á×ÔÏÍÁÔÕ, ÏÂßÑÓÎÉÔ
 963 ÒÁÓÓËÁÚ Ï ÓÅÍÁÎÔÉËÅ Á×ÔÏÍÁÔÏ×: <<ÚÎÁÞÅÎÉÅ>> ËÏÎÅÞÎÏÇÏ Á×ÔÏÍÁÔÁ ÍÙ
 964 ÏÐÒÅÄÅÌÑÅÍ ÐÒÏÓÔÏ ËÁË ÉÎÔÅÒÐÒÅÔÁÃÉÀ ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÅÇÏ Á×ÔÏÍÁÔÎÏÇÏ ×ÙÒÁÖÅÎÉÑ.
 965
 966 \paragraph{óÅÍÁÎÔÉËÁ.}
 967 \begin{definition}
 968 ÷ ÁÌÇÅÂÒÅ ëÌÉÎÉ $\ka K$ ÐÒÉ ÉÎÔÅÒÐÒÅÔÁÃÉÉ $I\colon \Sigma \to \ka K$
 969 \tING{ÐÏ×ÅÄÅÎÉÅ Á×ÔÏÍÁÔÁ}~\eqref{eq:nfa}\cite{inductive-*-Sr}
 970 (ÚÎÁÞÅÎÉÅ Á×ÔÏÍÁÔÁ)\T ÜÔÏ
 971 ÉÎÔÅÒÐÒÅÔÁÃÉÑ Á×ÔÏÍÁÔÎÏÇÏ ×ÙÒÁÖÅÎÉÑ~\eqref{eq:nfa-exp}:
 972 \begin{equation}
 973   \label{eq:nfa-value}
 974   I\left(\smatrAny{I} \smatrAny{M}^* \transp{\smatrAny{F}})\right).
 975 \end{equation}
 976 \end{definition}
 977
 978 üË×É×ÁÌÅÎÔÎÏÓÔØ Ä×ÕÈ Á×ÔÏÍÁÔÏ×
 979 \begin{align}
 980   \label{eq:2nfas}
 981   &(\smatrAny{I}', \smatrAny{M}', \smatrAny{F}')
 982   &&(\smatrAny{I}'', \smatrAny{M}'', \smatrAny{F}'')
 983 \end{align}
 984 ×ÙÒÁÖÁÅÔÓÑ ÆÏÒÍÕÌÏÊ\DÒÁ×ÅÎÓÔ×ÏÍ ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÈ Á×ÔÏÍÁÔÎÙÈ ×ÙÒÁÖÅÎÉÊ:
 985 \begin{equation}
 986   \label{eq:nfa-equiv}
 987   \smatrAny{I}' \smatrAny{M}'^* \transp{\smatrAny{F}'}
 988   =
 989   \smatrAny{I}'' \smatrAny{M}''^* \transp{\smatrAny{F}''}.
 990 \end{equation}
 991
 992 \begin{definition}
 993 ðÕÓÔØ Á×ÔÏÍÁÔÎÙÅ ×ÙÒÁÖÅÎÉÑ $s', s'' \in \AExp_\Sigma$ ÓÏÏÔ×ÅÔÓÔ×ÕÀÔ
 994 Ä×ÕÍ Á×ÔÏÍÁÔÁÍ ÎÁÄ~$\Sigma$.
 995 üÔÉ Á×ÔÏÍÁÔÙ ÜË×É×ÁÌÅÎÔÎÙ × ËÌÁÓÓÅ ÁÌÇÅÂÒ~$\class C \subseteq \KA$, ÅÓÌÉ:
 996 \begin{equation}
 997   \label{eq:nfa-equiv-value}
 998   \class C
 999   \models
1000   s' = s''.
1001 \end{equation}
1002 \end{definition}
1003
1004 \subsubsection{ó×ÑÚØ Ó ÄÒÕÇÉÍÉ ÉÚ×ÅÓÔÎÙÍÉ ÏÐÒÅÄÅÌÅÎÉÑÍÉ}
1005 \label{sec:nfa-other-values}
1006
1007 \paragraph{óÉÎÔÁËÓÉÓ: ÓÉÓÔÅÍÁ ÐÅÒÅÈÏÄÏ×.}
1008 íÁÔÒÉÞÎÏÅ ïÐÒÅÄÅÌÅÎÉÅ~\ref{def:nfa} ÓÉÎÔÁËÓÉÓÁ ËÏÎÅÞÎÏÇÏ Á×ÔÏÍÁÔÁ ÎÁÄ
1009 $\Sigma$ ËÁË
1010 ÔÒÏÊËÉ $(\smatr{I}{1}{n}, \smatr{M}{n}{n}, \smatr{F}{1}{n})$
1011 ÌÅÇËÏ ÚÁÍÅÎÉÔØ ÎÁ ÏÐÒÅÄÅÌÅÎÉÅ ËÏÎÅÞÎÏÇÏ Á×ÔÏÍÁÔÁ
1012 ËÁË ÓÉÓÔÅÍÙ ÐÅÒÅÈÏÄÏ×
1013 $\au A = (Q, \Delta, \smatrAny{I}, \smatrAny{F})$,
1014 ÇÄÅ $Q$\T \tING{ÍÎÏÖÅÓÔ×Ï ÓÏÓÔÏÑÎÉÊ} Á×ÔÏÍÁÔÁ,
1015 $\Delta \subseteq Q \times \Strs(\Sigma) \times Q$\T
1016 \tING{ÏÔÎÏÛÅÎÉÅ ÐÅÒÅÈÏÄÏ×} (ÐÏÍÅÞÅÎÎÙÅ ÓÔÒÏËÁÍÉ ÐÅÒÅÈÏÄÙ),
1017 $\smatrAny{I}, \smatrAny{F} \subseteq \Strs(\Sigma) \times Q$\T
1018 \tING{×ÈÏÄÙ} É \tING{×ÙÈÏÄÙ} × Á×ÔÏÍÁÔ (ÐÏÍÅÞÅÎÎÙÅ ÓÔÒÏËÁÍÉ).
1019
1020 âÕÄÅÍ ÄÌÑ ÎÁÇÌÑÄÎÏÓÔÉ ÏÂÏÚÎÁÞÁÔØ Ó ÐÏÍÏÝØÀ ÓÔÒÅÌÏÞÅË ÜÌÅÍÅÎÔÙ ÓÉÓÔÅÍÙ
1021 ÐÅÒÅÈÏÄÏ×:
1022 \begin{align*}
1023 &\text{ÐÅÒÅÈÏÄÙ\T
1024 ÜÌÅÍÅÎÔÙ $\Delta \subseteq Q \times \Strs(\Sigma) \times Q$}
1025 &&(u, \sigma, v)
1026 &&\left(u \transition{\sigma} v\right)\\
1027 &\text{×ÈÏÄÙ\T
1028 ÜÌÅÍÅÎÔÙ $\smatrAny{I} \subseteq \Strs(\Sigma) \times Q$}
1029 &&(\sigma, u)
1030 &&\left(\Entry{\sigma} u\right)\\
1031 &\text{×ÙÈÏÄÙ\T
1032 ÜÌÅÍÅÎÔÙ $\transp{\smatrAny{F}} \subseteq Q \times \Strs(\Sigma)$}
1033 &&(u, \sigma)
1034 &&\left(u \Exit{\sigma}\right)
1035 \end{align*}
1036
1037 óÏÏÔ×ÅÔÓÔ×ÉÅ ÍÅÖÄÕ Ä×ÕÍÑ ÐÒÅÄÓÔÁ×ÌÅÎÉÑÍÉ ÕÓÔÁÎÏ×ÉÍ ÔÁË.
1038 ÷Ï-ÐÅÒ×ÙÈ, ÐÕÓÔØ Õ ÎÁÓ ÓÒÁÚÕ ÍÁÔÒÉÃÙ $\smatrAny{I}, \smatrAny{M},
1039 \smatrAny{F})$ ÉÎÄÅËÓÉÒÕÀÔÓÑ ÎÅ ÎÁÔÕÒÁÌØÎÙÍÉ ÞÉÓÌÁÍÉ, Á ÜÌÅÍÅÎÔÁÍÉ
1040 $Q$, $\size{Q} = n$.
1041 $$
1042 \left(u \transition{\sigma} v\right) \in \Delta
1043 \iffdef
1044 \smatrAny{M}[u,v] = \dotsb + \sigma + \dotsb
1045 $$
1046 É ÁÎÁÌÏÇÉÞÎÏ ÄÌÑ ×ÈÏÄÏ× É ×ÙÈÏÄÏ×.
1047
1048 ëÁË É ÄÌÑ ÛËÁÌ ëÒÉÐËÅ (\sm ïÐÒ.~\ref{def:trace}), ÍÙ ÏÐÒÅÄÅÌÑÅÍ ÔÒÁÓÓÙ
1049 × Á×ÔÏÍÁÔÁÈ\DÓÉÓÔÅÍÁÈ ÐÅÒÅÈÏÄÏ×; $\Trs(\au A)$\T ÍÎÏÖÅÓÔ×Ï ÔÒÁÓÓ ×
1050 Á×ÔÏÍÁÔÅ~$\au A$.
1051
1052 éÎÏÇÄÁ ÎÁÍ ÂÕÄÅÔ ÕÄÏÂÎÏ ÓÍÏÔÒÅÔØ ÎÁ ËÏÎÅÞÎÙÊ Á×ÔÏÍÁÔ ÎÅ ËÁË ÎÁ
1053 ÍÁÔÒÉÃÕ, Á ËÁË ÎÁ ÓÉÓÔÅÍÕ ÐÅÒÅÈÏÄÏ× (ÍÙ ÜÔÏ ÂÕÄÅÍ ÄÅÌÁÔØ,  ËÏÇÄÁ ÍÙ
1054 ÂÕÄÅÍ ÇÏ×ÏÒÉÔØ Ï ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÈ Á×ÔÏÍÁÔÁÈ).
1055
1056 \paragraph{óÅÍÁÎÔÉËÁ: ÑÚÙË, ÒÁÓÐÏÚÎÁ×ÁÅÍÙÊ Á×ÔÏÍÁÔÏÍ\T <<ÇÌÏÂÁÌØÎÏÅ ÏÐÒÅÄÅÌÅÎÉÅ>>.}
1057 $R_\Sigma(s)$\T ÉÎÔÅÒÐÒÅÔÁÃÉÀ Á×ÔÏÍÁÔÎÏÇÏ ×ÙÒÁÖÅÎÉÑ $s$ × ÍÏÄÅÌÉ
1058 ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ× ÓÔÒÏË $\Reg_\Sigma$\T ÐÒÉÎÑÔÏ ÎÁÚÙ×ÁÔØ
1059 \tNDNo{ÑÚÙËÏÍ, ÒÁÓÐÏÚÎÁ×ÁÅÍÙÊ Á×ÔÏÍÁÔÏÍ}.
1060
1061 üÔÏ ÏÐÒÅÄÅÌÅÎÉÅ ÏÔÒÁÖÁÅÔ ÔÁËÏÅ ÔÒÁÄÉÃÉÏÎÎÏÅ <<ÇÌÏÂÁÌØÎÏÅ>> ÏÐÒÅÄÅÌÅÎÉÅ
1062 ÑÚÙËÁ, ÒÁÓÐÏÚÎÁ×ÁÅÍÏÇÏ Á×ÔÏÍÁÔÏÍ\DÓÉÓÔÅÍÏÊ ÐÅÒÅÈÏÄÏ× $\au A$:
1063 \begin{multline}
1064   \label{eq:nfa-global-value}
1065   R'(\au A) \eqdef
1066   \bigcup_{\sigma \in \Trs(\au A)}
1067   \left\{ \smatrAny{I}[\First(\sigma)] \Label(\sigma)
1068     \smatrAny{F}[\Last(\sigma)] \right\}
1069   =
1070   \\
1071   =
1072   \sup_{\sigma \in \Trs(\au A)}
1073   R_\Sigma \left(\smatrAny{I}[\First(\sigma)] \Label(\sigma)
1074     \smatrAny{F}[\Last(\sigma)] \right).
1075 \end{multline}
1076 (\emph{<<çÌÏÂÁÌØÎÏÅ>>}, ÐÏÔÏÍÕ ÞÔÏ ÏÎÏ ÏÓÎÏ×ÁÎÏ ÎÁ ÇÌÏÂÁÌØÎÏÍ
1077  Ó×ÏÊÓÔ×Å
1078 ÓÉÓÔÅÍÙ ÐÅÒÅÈÏÄÏ×, ÐÒÅÄÓÔÁ×ÌÑÀÝÅÊ Á×ÔÏÍÁÔ; ×ÔÏÒÏÅ ×ÙÒÁÖÅÎÉÅ
1079 ×~\eqref{eq:nfa-global-value} ÄÁÎÏ ÐÏÌÎÏÓÔØÀ × ÔÅÒÍÉÎÁÈ ÏÐÅÒÁÃÉÊ \KA.)
1080
1081 \paragraph{óÅÍÁÎÔÉËÁ:  <<ÒÁÂÏÔÁ>> ÎÁ ÂÅÓËÏÎÅÞÎÙÈ ÌÅÎÔÁÈ.}
1082 \begin{definition}
1083 ðÒÏÓÔÅÊÛÁÑ ÛËÁÌÁ ëÒÉÐËÅ ÎÁÄ~$\Sigma$, ÉÍÅÀÝÁÑ ÏÄÉÎ ÐÅÒÅÈÏÄ,
1084 ÏÂÏÚÎÁÞÁÅÔÓÑ $\kfLetter(a) \eqdef ( \{ 0, 1 \}, m)$, ÇÄÅ $a \in \Sigma$:
1085 \begin{align*}
1086 m(a) &\eqdef (0,1)
1087 &
1088 m(b) &\eqdef \emptyset \text{ ÄÌÑ $b \neq a$.}
1089 \end{align*}
1090 \end{definition}
1091
1092 \begin{definition}
1093 ûËÁÌÁ ëÒÉÐËÅ $\kfITape(\omega)$, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÁÑ ÂÅÓËÏÎÅÞÎÏÊ ÌÅÎÔÅ, ÎÁ
1094 ËÏÔÏÒÏÊ ÚÁÐÉÓÁÎÁ ÂÅÓËÏÎÅÞÎÁÑ ÓÔÒÏËÁ $\omega$ × ÁÌÆÁ×ÉÔÅ~$\Sigma$:
1095 $$
1096 \omega = a_1 a_2 \dotsm
1097 $$
1098 ÐÏÌÕÞÁÅÔÓÑ ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÙÍ ÓÏÅÄÉÎÅÎÉÅÍ ÛËÁÌ ëÒÉÐËÅ $\kfLetter(a_i)$, $i = 1,
1099 \dotsc$ (\te \tD{ÏÂßÅÄÉÎÅÎÉÅÍ}{def:kf-union} É
1100 \tD{ÏÔÏÖÄÅÓÔ×ÌÅÎÉÅÍ}{def:kf-link} ÐÏÓÌÅÄÎÅÇÏ ÓÏÓÔÏÑÎÉÑ ÐÅÒ×ÏÊ
1101 ÛËÁÌÙ Ó ÐÅÒ×ÙÍ ÓÏÓÔÏÑÎÉÅÍ ×ÔÏÒÏÊ).
1102
1103 $$
1104 \ITAPES_\Sigma
1105 \eqdef \{ (\relReg_{\kfITape(\omega)}, \relIP)
1106 \mid \omega \text{\T ÂÅÓËÏÎÅÞÎÁÑ ÓÔÒÏËÁ ×~$\Sigma$} \}
1107 $$
1108 $$
1109 \ITAPES \eqdef \{ (\relReg_{\kfITape(\omega)}, \relIP) \mid \omega \text{\T ÂÅÓËÏÎÅÞÎÁÑ
1110   ÓÔÒÏËÁ} \}
1111 $$
1112 \end{definition}
1113
1114 <<çÌÏÂÁÌØÎÏÅ>> ÏÐÒÅÄÅÌÅÎÉÅ~\eqref{eq:nfa-global-value}
1115 É ÎÁ <<ÂÅÓËÏÎÅÞÎÙÈ ÌÅÎÔÁÈ>>\T
1116 Ä×Á ÜË×É×ÁÌÅÎÔÎÙÈ ÓÐÏÓÏÂÁ ÏÐÒÅÄÅÌÅÎÉÑ ÓÅÍÁÎÔÉËÉ Á×ÔÏÍÁÔÁ:
1117 \begin{proposition}
1118   $$
1119   \ITAPES \models s = t
1120   \iff
1121   \Reg_\Sigma \models s = t
1122   $$
1123   (÷×ÉÄÕ ôÅÏÒÅÍÙ ëÌÉÎÉ~\ref{th:Kleene} ÔÕÔ ÎÁ ÓÁÍÏÍ ÄÅÌÅ ÎÅ×ÁÖÎÏ,
1124   ÉÍÅÅÍ ÌÉ ÍÙ × ×ÉÄÕ ÒÅÇÕÌÑÒÎÙÅ ÉÌÉ Á×ÔÏÍÁÔÎÙÅ ×ÙÒÁÖÅÎÉÑ ÎÁÄ $\Sigma$.)
1125 \end{proposition}
1126 ôÁËÉÅ ÍÏÄÅÌÉ ÍÙ ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ \tING{ÕÎÉ×ÅÒÓÁÌØÎÙÍÉ}
1127 \cite{KAT-schematology} ÄÌÑ ÜË×ÁÃÉÏÎÁÌØÎÏÊ ÔÅÏÒÉÉ ËÌÁÓÓÁ ÄÒÕÇÉÈ ÍÏÄÅÌÅÊ; ÚÄÅÓØ:
1128 $\Reg_\Sigma$ ÕÎÉ×ÅÒÓÁÌØÎÁ ÄÌÑ $\EOf \ITAPES$.
1129
1130 \paragraph{óÅÍÁÎÔÉËÁ: <<ÒÁÂÏÔÁ>> ÎÁ ËÏÎÅÞÎÙÈ ÌÅÎÔÁÈ.}
1131 \begin{definition}
1132 ûËÁÌÁ ëÒÉÐËÅ $\kfFTape'(\sigma)$, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÁÑ ÌÅÎÔÅ, ÎÁ
1133 ËÏÔÏÒÏÊ ÚÁÐÉÓÁÎÁ ËÏÎÅÞÎÁÑ ÓÔÒÏËÁ $\sigma$ × ÁÌÆÁ×ÉÔÅ~$\Sigma$:
1134 $$
1135 \sigma = a_1 a_2 \dotsm a_n
1136 $$
1137 ÐÏÌÕÞÁÅÔÓÑ ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÙÍ  ÓÏÅÄÉÎÅÎÉÅÍ ÛËÁÌ ëÒÉÐËÅ $\kfLetter(a_i)$, $i = 1,
1138 \dotsc, n$.
1139
1140 $$
1141 \FTAPES_\Sigma'
1142 \eqdef \{ (\relReg_{\kfFTape'(\sigma)}, \relIP)
1143 \mid \sigma \text{\T ËÏÎÅÞÎÁÑ ÓÔÒÏËÁ ×~$\Sigma$} \}
1144 $$
1145 $$
1146 \FTAPES' \eqdef \{ (\relReg_{\kfFTape'(\sigma)}, \relIP) \mid \sigma \text{\T ËÏÎÅÞÎÁÑ ÓÔÒÏËÁ} \}
1147 $$
1148 \end{definition}
1149
1150 \begin{definition}
1151 ðÕÓÔØ $\Sigma \cap \{ \Stop \} = \emptyset$.
1152 \tING{ûËÁÌÁ ëÒÉÐËÅ $\kfFTape(\sigma)$, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÁÑ ÌÅÎÔÅ, ÎÁ
1153 ËÏÔÏÒÏÊ ÚÁÐÉÓÁÎÁ ËÏÎÅÞÎÁÑ ÓÔÒÏËÁ $\sigma$ × ÁÌÆÁ×ÉÔÅ~$\Sigma$ :
1154 $$
1155 \sigma = a_1 a_2 \dotsm a_n
1156 $$
1157 Ó ÏÇÒÁÎÉÞÉÔÅÌÅÍ}
1158 ÐÏÌÕÞÁÅÔÓÑ ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÙÍ ÓÏÅÄÉÎÅÎÉÅÍ ÛËÁÌ ëÒÉÐËÅ $\kfLetter(a_i)$, $i = 1,
1159 \dotsc, n$, É $\kfLetter(\Stop)$.
1160 $$
1161 \Accepts(\sigma) \eqdef
1162 (\relReg_{\kfFTape(\sigma)}, \relIP)
1163 $$
1164 $$
1165 \FTAPES_\Sigma
1166 \eqdef \{  \Accepts(\sigma)
1167 \mid \sigma \text{\T ËÏÎÅÞÎÁÑ ÓÔÒÏËÁ ×~$\Sigma$} \}
1168 $$
1169 $$
1170 \FTAPES \eqdef \{ \Accepts(\sigma) \mid \sigma \text{\T ËÏÎÅÞÎÁÑ
1171   ÓÔÒÏËÁ × ÁÌÆÁ×ÉÔÅ ÂÅÚ $\Stop$} \}
1172 $$
1173 \end{definition}
1174
1175 ðÕÓÔØ $\Sigma \cap \{ \Stop \} = \emptyset$.
1176 \tING{á×ÔÏÍÁÔ ÎÁÄ~$\Sigma$ ÐÒÉÎÉÍÁÅÔ ËÏÎÅÞÎÕÀ ÓÔÒÏËÕ}~$\sigma$ ×
1177 ÁÌÆÁ×ÉÔÅ $\Sigma$, ÅÓÌÉ ÄÌÑ ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÅÇÏ ÜÔÏÍÕ Á×ÔÏÍÁÔÕ
1178 Á×ÔÏÍÁÔÎÏÇÏ ×ÙÒÁÖÅÎÉÑ~$s \in \AExp_\Sigma$:
1179 $$
1180 \Accepts(\sigma) \models s \cdot \Stop \neq 0.
1181 $$
1182 ÷ ÜÔÏÍ ÓÌÕÞÁÅ $\relI{s \cdot \Stop}_{\kfFTape(\sigma)} = (u,v)$, ÇÄÅ
1183 $u$ É~$v$\T <<ÐÅÒ×ÏÅ>> É <<ÐÏÓÌÅÄÎÅÅ>> ÓÏÓÔÏÑÎÉÅ ÛËÁÌÙ
1184 ëÒÉÐËÅ~$\kfFTape(\sigma)$.
1185
1186 üÔÏ ÏÐÒÅÄÅÌÅÎÉÅ ÏÔÒÁÖÁÅÔ ÔÁËÏÅ ÔÒÁÄÉÃÉÏÎÎÏÅ ÏÐÒÅÄÅÌÅÎÉÅ ÓÅÍÁÎÔÉËÉ
1187 Á×ÔÏÍÁÔÁ, ÏÓÎÏ×ÁÎÎÏÅ ÎÁ ÒÁÓÓÍÏÔÒÅÎÉÉ ÒÁÂÏÔÙ Á×ÔÏÍÁÔÁ ÎÁ ËÁÖÄÏÊ ÉÚ
1188 ÏÔÄÅÌØÎÙÈ ÌÅÎÔ:
1189 $$
1190 \au A \text{ ÐÒÉÎÉÍÁÅÔ ÓÔÒÏËÕ $\sigma$ }
1191 \iffdef
1192 \au A \text{ ÐÒÉ ÒÁÂÏÔÅ ÎÁ ÌÅÎÔÅ ÓÏ ÓÌÏ×ÏÍ $\sigma$ ÐÅÒÅÈÏÄÉÔ ÉÚ
1193   ÎÁÞÁÌØÎÏÇÏ ÓÏÓÔÏÑÎÉÑ × ËÏÎÅÞÎÏÅ.}
1194 $$
1195 é ÔÏÇÄÁ
1196 $$
1197 R''(\au A) \eqdef
1198 \{ \sigma \mid \au A \text{ ÐÒÉÎÉÍÁÅÔ ÓÔÒÏËÕ $\sigma$ } \}.
1199 $$
1200
1201 <<çÌÏÂÁÌØÎÏÅ>> ÏÐÒÅÄÅÌÅÎÉÅ~\eqref{eq:nfa-global-value}
1202 É ÎÁ <<ËÏÎÅÞÎÙÈ ÌÅÎÔÁÈ>>\T
1203 Ä×Á ÜË×É×ÁÌÅÎÔÎÙÈ ÓÐÏÓÏÂÁ ÏÐÒÅÄÅÌÅÎÉÑ ÓÅÍÁÎÔÉËÉ Á×ÔÏÍÁÔÁ:
1204
1205 \begin{proposition}[üË×É×ÁÌÅÎÔÎÏÓÔØ Ä×ÕÈ ÓÅÍÁÎÔÉË.]
1206   ðÕÓÔØ $\Sigma \cap \{ \Stop \} = \emptyset$.
1207   $$
1208   \FTAPES \models s \cdot \Stop = t \cdot \Stop
1209   \iff
1210   \Reg_\Sigma \models s =t,
1211   $$
1212   ÇÄÅ $s$ É $t$ ÏÐÑÔØ\T Á×ÔÏÍÁÔÎÙÅ ÉÌÉ ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ ÎÁÄ~$\Sigma$.
1213 \end{proposition}
1214 \Te ÔÕÔ ÕÔ×ÅÒÖÄÁÅÔÓÑ, ÞÔÏ
1215 $\Reg_\Sigma$ × ÎÅËÏÔÏÒÏÍ ÓÍÙÓÌÅ ÕÎÉ×ÅÒÓÁÌØÎÁ ÄÌÑ $\EOf \FTAPES$
1216 (ÔÏÞÎÅÅ, ÄÌÑ ÜË×ÁÃÉÏÎÁÌØÎÏÊ ÔÅÏÒÉÉ, ÓÏÓÔÏÑÝÅÊ ÔÏÌØËÏ ÉÚ ÒÁ×ÅÎÓÔ× Ó
1217 $\Stop$ × ËÏÎÃÅ).
1218
1219 \subsubsection{÷ÏÐÒÏÓÙ}
1220 \begin{definition}
1221   üË×ÁÃÉÏÎÁÌØÎÕÀ ÔÅÏÒÉÀ ËÌÁÓÓÁ~$\class C$ ÁÌÇÅÂÒ ëÌÉÎÉ, ÓÏÓÔÏÑÝÕÀ ÉÚ
1222   ÆÏÒÍÕÌ\DÒÁ×ÅÎÓÔ× Á×ÔÏÍÁÔÎÙÈ ×ÙÒÁÖÅÎÉÊ, ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ
1223   $\EAutOf\class C$.
1224 \end{definition}
1225
1226 ÷ÏÐÒÏÓÙ Ï ÓÅÍÁÎÔÉËÅ ËÏÎÅÞÎÙÈ Á×ÔÏÍÁÔÏ× ÎÁÍ ÉÎÔÅÒÅÓÎÙ ÔÅ ÖÅ, ÞÔÏ É Ï
1227 ÓÅÍÁÎÔÉËÅ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ, ÐÅÒÅÞÉÓÌÅÎÎÙÅ ×
1228 òÁÚÄÅÌÅ~\ref{sec:rexpr-Qs}, Á ÔÁËÖÅ:
1229 \begin{enumerate}
1230 \item
1231   ëÁË Ó×ÑÚÁÎÙ $\EOf \class C$ É $\EAutOf\class C$ ÄÌÑ $\class C \subseteq \KA$?
1232 \end{enumerate}
1233
1234
1235
1236 \subsection{ôÅÏÒÅÍÁ ëÌÉÎÉ}
1237 \label{sec:Kleene-th}
1238 ëÌÁÓÓÉÞÅÓËÏÊ ÔÅÏÒÅÍÏÊ ôÅÏÒÉÉ ËÏÎÅÞÎÙÈ Á×ÔÏÍÁÔÏ× Ñ×ÌÑÅÔÓÑ ôÅÏÒÅÍÁ
1239 ëÌÉÎÉ, ÕÔ×ÅÒÖÄÁÀÝÁÑ ÓÏ×ÐÁÄÅÎÉÅ ÓÅÍÅÊÓÔ× Á×ÔÏÍÁÔÎÙÈ É ÒÅÇÕÌÑÒÎÙÈ
1240 ÑÚÙËÏ×:
1241 \begin{theorem}[ëÌÉÎÉ]\label{th:Kleene}
1242   äÌÑ ÌÀÂÏÇÏ $s \in \RExp_\Sigma$
1243   ÓÕÝÅÓÔ×ÕÅÔ $s' \in \AExp_\Sigma$, ÔÁËÏÅ, ÞÔÏ
1244   \begin{equation}
1245     \label{eq:Kleene-th}
1246     R_\Sigma(s) = R_\Sigma(s'),
1247   \end{equation}
1248   É ÎÁÏÂÏÒÏÔ, ÄÌÑ ÌÀÂÏÇÏ $s \in \AExp_\Sigma$
1249   ÓÕÝÅÓÔ×ÕÅÔ $s'' \in \RExp_\Sigma$, ÔÁËÏÅ, ÞÔÏ
1250   $R_\Sigma(s) = R_\Sigma(s'')$.
1251
1252   óÏÏÔ×ÅÔÓÔ×ÉÑ ÍÅÖÄÕ~$\AExp_\Sigma$ É~$\RExp_\Sigma$ (É × ÔÕ, É ×
1253   ÄÒÕÇÕÀ ÓÔÏÒÏÎÕ) ×ÙÞÉÓÌÉÍÙÅ.
1254 \end{theorem}
1255 %% \begin{proof}
1256 %%   ðÏÓÔÒÏÅÎÉÑ, ÐÒÉ×ÏÄÑÝÉÅ Ë ÄÏËÁÚÁÔÅÌØÓÔ×Õ, ÎÅ ÉÚÍÅÎÑÀÔÓÑ
1257 %%   É × ÂÏÌÅÅ ÏÂÝÅÍ ÓÌÕÞÁÅ ôÅÏÒÅÍÙ ëÌÉÎÉ, ÒÁÓÓÍÏÔÒÅÎÎÏÍ
1258 %%   ×~òÁÚÄÅÌÅ~\ref{sec:hypo-plain-Kleene-th}, \sm ÚÁÍÅÞÁÎÉÑ Ë
1259 %%   ÄÏËÁÚÁÔÅÌØÓÔ×Õ ÔÁÍ.
1260 %% \end{proof}
1261 \begin{remark}
1262 ôÅÍ ÓÁÍÙÍ $\EOf \Reg_\Sigma$ É $\EAOf \Reg_\Sigma$ ×ÙÞÉÓÌÉÍÏ Ó×ÏÄÑÔÓÑ
1263 ÄÒÕÇ Ë ÄÒÕÇÕ (\todo{\tNDNo{$m$\dÓ×ÏÄÑÔÓÑ} \cite{VerShen-computable}?}):
1264 $$
1265 \Reg_\Sigma \models s = t
1266 \iff
1267 \Reg_\Sigma \models s' = t',
1268 $$
1269 ÇÄÅ $\place'$\T ÕÓÔÁÎÏ×ÌÅÎÎÏÅ ×ÙÞÉÓÌÉÍÏÅ ÓÏÏÔ×ÅÔÓÔ×ÉÅ ÍÅÖÄÕ Á×ÔÏÍÁÔÎÙÍÉ É
1270 ÒÅÇÕÌÑÒÎÙÍÉ ×ÙÒÁÖÅÎÉÑÍÉ (ÉÌÉ ÎÁÏÂÏÒÏÔ).
1271 \end{remark}
1272
1273 íÏÖÎÏ ÚÁÍÅÔÉÔØ, ÇÌÑÄÑ ÎÁ ÐÏÓÔÒÏÅÎÉÑ × ÄÏËÁÚÁÔÅÌØÓÔ×Å ôÅÏÒÅÍÙ ëÌÉÎÉ
1274 (ËÏÔÏÒÏÅ ÍÙ ÔÕÔ ÎÅ ÐÒÉ×ÅÌÉ),
1275 ÞÔÏ ÓÐÒÁ×ÅÄÌÉ×ÏÓÔØ~\eqref{eq:Kleene-th} ÎÅ ÚÁ×ÉÓÉÔ ÏÔ
1276 ×ÙÂÏÒÁ ÁÌÇÅÂÒÙ ëÌÉÎÉ É ÉÎÔÅÒÐÒÅÔÁÃÉÉ: ÏÎÁ ÚÁ×ÉÓÉÔ ÔÏÌØËÏ ÏÔ
1277 ÏÐÒÅÄÅÌÅÎÉÊ ÏÐÅÒÁÃÉÊ ÎÁÄ ÍÁÔÒÉÃÁÍÉ; ÓÏÏÔ×ÅÔÓÔ×ÉÑ $\place'$ É
1278 $\place''$\T ÓÉÎÔÁËÓÉÞÅÓËÉÅ ÐÒÅÏÂÒÁÚÏ×ÁÎÉÑ.
1279 \cite[Theorem~9.4]{inductive-*-Sr} ÐÒÉ×ÏÄÉÔ ÄÏËÁÚÁÔÅÌØÓÔ×Ï ôÅÏÒÅÍÙ ëÌÉÎÉ
1280 ÄÌÑ ÅÝ£ ÂÏÌÅÅ ÛÉÒÏËÏÇÏ ËÌÁÓÓÁ ÓÔÒÕËÔÕÒ, ÞÅÍ ÁÌÇÅÂÒÙ ëÌÉÎÉ\T
1281 \tNDNo{Conway semirings}\T ÔÁËÉÈ ÓÔÒÕËÔÕÒ, ËÏÔÏÒÙÅ ÄÏÐÕÓËÁÀÔ ÐÏÓÔÒÏÅÎÉÅ
1282 ÉÎÄÕÃÉÒÏ×ÁÎÎÙÈ ÁÌÇÅÂÒ ÍÁÔÒÉÃ ÐÏ ÔÅÍ ÖÅ ÐÒÁ×ÉÌÁÍ.
1283
1284 ôÁË ÞÔÏ ×ÅÒÎÁ
1285 \begin{theorem}[ëÌÉÎÉ]\label{th:KA-Kleene}
1286   äÌÑ ÌÀÂÏÇÏ $s \in \RExp_\Sigma$
1287   ÓÕÝÅÓÔ×ÕÅÔ $s' \in \AExp_\Sigma$, ÔÁËÏÅ, ÞÔÏ
1288   \begin{equation}
1289     \label{eq:KA-Kleene-th}
1290     \KA \models s = s',
1291   \end{equation}
1292   É ÎÁÏÂÏÒÏÔ, ÄÌÑ ÌÀÂÏÇÏ $s \in \AExp_\Sigma$
1293   ÓÕÝÅÓÔ×ÕÅÔ $s'' \in \RExp_\Sigma$, ÔÁËÏÅ, ÞÔÏ
1294   ×ÅÒÎÏ~\eqref{eq:KA-Kleene-th}.
1295
1296   óÏÏÔ×ÅÔÓÔ×ÉÑ $\place'$ É $\place''$
1297   ÍÅÖÄÕ~$\RExp_\Sigma$ É~$\AExp_\Sigma$
1298   ×ÙÞÉÓÌÉÍÙ.
1299 \end{theorem}
1300 \begin{remark}
1301 ôÅÍ ÓÁÍÙÍ $\EOf \KA$ É $\EAOf \KA$ ×ÙÞÉÓÌÉÍÏ Ó×ÏÄÑÔÓÑ
1302 ÄÒÕÇ Ë ÄÒÕÇÕ (\todo{\tNDNo{$m$\dÓ×ÏÄÑÔÓÑ} \cite{VerShen-computable}?}):
1303 $$
1304 \KA \models s = t
1305 \iff
1306 \KA \models s' = t',
1307 $$
1308 ÇÄÅ $\place'$\T ÕÓÔÁÎÏ×ÌÅÎÎÏÅ ×ÙÞÉÓÌÉÍÏÅ ÓÏÏÔ×ÅÔÓÔ×ÉÅ ÍÅÖÄÕ Á×ÔÏÍÁÔÎÙÍÉ É
1309 ÒÅÇÕÌÑÒÎÙÍÉ ×ÙÒÁÖÅÎÉÑÍÉ (ÉÌÉ ÎÁÏÂÏÒÏÔ).
1310
1311 ôÏ ÖÅ ×ÅÒÎÏ É ÐÒÏ ÌÀÂÏÊ ÐÏÄËÌÁÓÓ $\class C \subseteq \KA$:
1312 $\EOf \class C$ É $\EAOf \class C$ ×ÙÞÉÓÌÉÍÏ Ó×ÏÄÑÔÓÑ
1313 ÄÒÕÇ Ë ÄÒÕÇÕ.
1314
1315 ïÔ ÄÏÂÁ×ÌÅÎÉÑ ÄÏÐÕÝÅÎÉÊ ÓÉÔÕÁÃÉÑ ÎÅ ÍÅÎÑÅÔÓÑ.
1316 $\HOf \class C$ É $\HAOf \class C$ ×ÙÞÉÓÌÉÍÏ Ó×ÏÄÑÔÓÑ
1317 ÄÒÕÇ Ë ÄÒÕÇÕ:
1318 $$
1319 \class C \models E \implic s = t
1320 \iff
1321 \class C \models E \implic s' = t'.
1322 $$
1323 \end{remark}
1324
1325 ä×Á ÓÐÏÓÏÂÁ ÚÁÐÉÓÉ ÐÒÏÇÒÁÍÍ (<<ÌÉÎÅÊÎÙÅ>> ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ É
1326 <<ÇÒÁÆÏÙÅ>>/ÍÁÔÒÉÞÎÙÅ Á×ÔÏÍÁÔÙ) ÐÏËÁ ÏËÁÚÙ×ÁÀÔÓÑ ÄÌÑ ÎÁÛÅÇÏ ÉÓÓÌÅÄÏ×ÁÎÉÑ
1327 ×ÚÁÉÍÏÚÁÍÅÎÑÅÍÙ. òÁÚÎÉÃÁ ÐÏÑ×ÉÔÓÑ ÐÒÉ ××ÅÄÅÎÉÉ ÐÏÎÑÔÉÑ
1328 \tND{ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÏÇÏ ËÏÎÅÞÎÏÇÏ Á×ÔÏÍÁÔÁ}{def:dfa},
1329 ËÏÔÏÒÏÍÕ ÎÅ ÎÁÊÄ£ÔÓÑ ÅÓÔÅÓÔ×ÅÎÎÏÇÏ
1330 ÁÎÁÌÏÇÁ ÄÌÑ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ, É ÐÒÅÏÂÒÁÚÏ×ÁÎÉÊ ÔÁËÉÈ Á×ÔÏÍÁÔÏ×.
1331
1332
1333 åÓÔØ É ÄÒÕÇÉÅ ÏÂÏÂÝÅÎÉÑ ôÅÏÒÅÍÙ ëÌÉÎÉ, ÓÍ., ÎÁÐÒÉÍÅÒ,
1334 ÓÌÕÞÁÊ Ó ËÒÁÔÎÏÓÔÑÍÉ × ôÅÏÒÅÍÅ~\ref{th:multi-Kleene-th}).
1335
1336
1337 \subsection{ó×ÏÂÏÄÎÁÑ ÍÏÄÅÌØ}
1338 \label{sec:free-plain-freeModels}
1339 \begin{remark} \cite{???}
1340   óÔÒÏËÕ $\sigma$ ÉÚ $\Strs(\Sigma)$ ÍÏÖÎÏ ÒÁÓÓÍÁÔÒÉ×ÁÔØ ËÁË
1341   ÒÅÇÕÌÑÒÎÏÅ ×ÙÒÁÖÅÎÉÅ ÉÚ $\RExp_{\Sigma}$
1342   (\tND{ÍÏÎÏÉÄÎÏÅ}{def:monoid-rexp}, \te × ËÏÔÏÒÏÍ ÉÓÐÏÌØÚÏ×ÁÎÙ ÔÏÌØËÏ
1343   ÏÐÅÒÁÃÉÉ ÓÉÇÎÁÔÕÒÙ ÍÏÎÏÉÄÁ\T $1, \cdot$).
1344   á ÜÌÅÍÅÎÔ $C \in  \Reg_\Sigma$ ÍÏÖÎÏ ÒÁÓÓÍÁÔÒÉ×ÁÔØ ËÁË ÍÎÏÖÅÓÔ×Ï
1345   ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma$ (ÍÏÎÏÉÄÎÙÈ).
1346   üÔÏ ÎÁÂÌÀÄÅÎÉÅ ÐÏÍÏÖÅÔ
1347   ÕÓÔÁÎÏ×ÉÔØ, ÞÔÏ $\Reg_{\Sigma}$\T Ó×ÏÂÏÄÎÁÑ ÍÏÄÅÌØ \KAc.
1348 \end{remark}
1349
1350 \begin{theorem}\cite{???}, \cite[Lecture~5]{KA-lect02}.
1351   $\Reg_\Sigma$
1352   Ñ×ÌÑÅÔÓÑ \tD{Ó×ÏÂÏÄÎÏÊ}{def:free-model} ÁÌÇÅÂÒÏÊ ×~\KAc,
1353   ÐÏÒÏÖÄ£ÎÎÏÊ~$\Sigma$.
1354 \end{theorem}
1355 \begin{proof}
1356   äÏËÁÚÁÔÅÌØÓÔ×Ï ÍÏÖÎÏ ÐÏÓÍÏÔÒÅÔØ × \cite{??}, ÏÎÏ ÏÓÎÏ×ÁÎÏ ÎÁ
1357   ÄÏËÁÚÁÔÅÌØÓÔ×Å ÓÌÅÄÕÀÝÅÊ ÌÅÍÍÙ:
1358   \begin{lemma}\label{lem:I-by-reg}
1359     $$
1360     I(s t r) = \sup_{\tau \in R_\Sigma(t)} I(s \tau r).
1361     $$
1362     (óÕÝÅÓÔ×Ï×ÁÎÉÅ ÜÔÏÇÏ $\sup$ ÔÏÖÅ ÔÒÅÂÕÅÔ ÄÏËÁÚÁÔÅÌØÓÔ×Á.)
1363   \end{lemma}
1364   \begin{remark}
1365     üÔÏ\T ÏÂÏÂÝÅÎÉÅ *\dÎÅÐÒÅÒÙ×ÎÏÓÔÉ (× ÐÒÉÍÅÎÅÎÉÉ Ë $a^*$, ÇÄÅ $a \in
1366     \Sigma$):
1367     $I(s a^* r) = \sup_{\tau \in R_\Sigma(a^*)} I(s \tau r)$, ×ÅÄØ
1368     $R_\Sigma(a^*) = \{ a^i \mid i \in \bbN \cup \{ 0 \} \}$.
1369   \end{remark}
1370   äÏËÁÚÁÔÅÌØÓÔ×Ï ìÅÍÍÙ ÐÒÏÉÓÈÏÄÉÔ ÐÏ ÉÎÄÕËÃÉÉ ÐÏ ÓÔÒÏÅÎÉÀ $t$.
1371   \todo{[ÞÔÏ ÉÓÐ-ÓÑ × Ä-×Å?]}
1372
1373   éÚ ìÅÍÍÙ~\ref{lem:I-by-reg} ÓÌÅÄÕÅÔ
1374   $$
1375   R_\Sigma(s) = R_\Sigma(t)
1376   \implies
1377   I(s) = I(t).
1378   $$
1379 \end{proof}
1380 \begin{proposition}
1381   \label{prop:Reg-Rel-iso}
1382   \cite{??}.
1383   $\Reg_\Sigma \in \RKA$ (= <<$\Reg_\Sigma$ ÉÚÏÍÏÒÆÎÁ ÎÅËÏÔÏÒÏÍÕ
1384   ÜÌÅÍÅÎÔÕ~$\RKA$>>).
1385
1386   á ÉÍÅÎÎÏ $\Reg_\Sigma$ ÉÚÏÍÏÒÆÎÁ $\relReg_{\kf F_{\Strs(\Sigma)}}$.
1387 \end{proposition}
1388 \begin{proof}\cite{??}, \cite[Lecture~20]{KA-lect02}.
1389   éÚÏÍÏÒÆÉÚÍ $h$:
1390   \begin{equation}
1391     \label{eq:h-Reg-rel}
1392     h(C) \eqdef \{ (\sigma, \sigma \tau) \mid \sigma \in \Strs(\Sigma),
1393     \tau \in C \}
1394   \end{equation}
1395   ÷Ï-ÐÅÒ×ÙÈ, ÌÅÇËÏ ÐÒÏ×ÅÒÉÔØ, ÞÔÏ $h$ ÇÏÍÏÍÏÒÆÉÚÍ.
1396
1397   ÷Ï-×ÔÏÒÙÈ, ÞÔÏ $h$ ×ÚÁÉÍÎÏ ÏÄÎÏÚÎÁÞÎÏÅ ÓÏÏÔ×ÅÔÓÔ×ÉÅ.
1398   ðÏËÁÖÅÍ, ÞÔÏ
1399   $$
1400   (\sigma, \sigma \tau) \in h(C)
1401   \iff
1402   \tau \in C.
1403   $$
1404   óÐÒÁ×Á ÎÁÌÅ×Ï\T ÐÏ ÏÐÒÅÄÅÌÅÎÉÀ~\eqref{eq:h-Reg-rel} ÏÔÏÂÒÁÖÅÎÉÑ~$h$.
1405   óÌÅ×Á ÎÁÐÒÁ×Ï\T \tk $Strs(\Sigma)$\T \tD{ÍÏÎÏÉÄ Ó ÌÅ×ÙÍ
1406     ÓÏËÒÁÝÅÎÉÅÍ}{def:Mo-leftcancel} É ÓÔÁÌÏ ÂÙÔØ:
1407   $$
1408   (\sigma, \sigma \tau) \in h(C)
1409   \overset{\text{ÐÏ ÏÐÒ~\eqref{eq:h-Reg-rel}}}{\implies}
1410   \exists \tau' \in C ( \sigma \tau' = \sigma \tau )
1411   \overset{\text{ÓÏËÒ.}}{\implies}
1412   \exists \tau' \in C ( \tau' = \tau )
1413   \implies \tau \in C.
1414   $$
1415 \end{proof}
1416 \begin{corollary}
1417 \cite{???}.
1418   $\Reg_\Sigma$
1419   Ñ×ÌÑÅÔÓÑ \tD{Ó×ÏÂÏÄÎÏÊ}{def:free-model} ÁÌÇÅÂÒÏÊ × \RKA,
1420   ÐÏÒÏÖÄ£ÎÎÏÊ $\Sigma$.
1421 \end{corollary}
1422
1423 \begin{lemma}\label{lem:isoA}
1424   \cite[Lecture~9]{KA-lect02}
1425   åÓÌÉ Á×ÔÏÍÁÔÙ, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÅ Á×ÔÏÍÁÔÎÙÍ ×ÙÒÁÖÅÎÉÑÍ $s$ É $t$,
1426   ÉÚÏÍÏÒÆÎÙ, ÔÏ
1427   $$
1428   \KA \models s = t.
1429   $$
1430 \end{lemma}
1431 óÌÅÄÕÀÝÁÑ ÔÅÏÒÅÍÁ ÉÓÐÏÌØÚÕÅÔ ÕÔ×ÅÒÖÄÅÎÉÑ Ï \tND{ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÈ
1432   ËÏÎÅÞÎÙÈ Á×ÔÏÍÁÔÁÈ}{def:dfa}, ËÏÔÏÒÙÅ ÍÙ ÒÁÓÓÍÏÔÒÉÍ ×
1433 òÁÚÄÅÌÅ~\ref{sec:free-plain-det}.
1434
1435 \begin{theorem}
1436   \cite{KA-regevents-complete}, \cite[Lecture~9]{KA-lect02}.
1437   $\Reg_\Sigma$
1438   Ñ×ÌÑÅÔÓÑ \tD{Ó×ÏÂÏÄÎÏÊ}{def:free-model} ÁÌÇÅÂÒÏÊ × \KA,
1439   ÐÏÒÏÖÄ£ÎÎÏÊ $\Sigma$.
1440 \end{theorem}
1441 \begin{proof}
1442 äÏËÁÚÁÔÅÌØÓÔ×Ï ÏÓÎÏ×Ù×ÁÅÔÓÑ ÎÁ ÔÏÍ, ÞÔÏ Ó×ÅÄÅÎÉÅ ËÏÎÅÞÎÏÇÏ Á×ÔÏÍÁÔÁ Ë
1443 ËÁÎÏÎÉÞÅÓËÏÍÕ ×ÉÄÕ (\sm úÁÍÅÞÁÎÉÅ~\ref{rem:canonA})\T ÜË×É×ÁÌÅÎÔÎÏÅ
1444 ÐÒÅÏÂÒÁÚÏ×ÁÎÉÅ ÐÒÉ ÁËÓÉÏÍÁÈ \KA, Á Õ Á×ÔÏÍÁÔÏ×, ÒÁÓÐÏÚÎÁÀÝÉÈ ÏÄÎÏ É ÔÏ
1445 ÖÅ ÒÅÇÕÌÑÒÎÏÅ ÍÎÏÖÅÓÔ×Ï ËÁÎÏÎÉÞÅÓËÉÊ ×ÉÄ ÏÄÉÎ (\sm
1446 ôÅÏÒÅÍÕ~\ref{th:minA-unique}).
1447
1448 óÈÅÍÁ ÄÏËÁÚÁÔÅÌØÓÔ×Á ÔÁËÁÑ \cite[Lectures~8--9]{KA-lect02}. ðÕÓÔØ
1449 $$
1450 \Reg_\Sigma \models s = t.
1451 $$
1452 ÷Ï-ÐÅÒ×ÙÈ, ÂÕÄÅÍ ÒÁÂÏÔÁÔØ Ó ËÏÎÅÞÎÙÍÉ Á×ÔÏÍÁÔÁÍÉ $s', t' \in
1453 \AExp_\Sigma$:
1454 \begin{align}
1455   \label{eq:KA-complete-Kleene}
1456   &\begin{aligned}
1457     \KA &\models s = s'\\
1458     \KA &\models t = t'
1459   \end{aligned}
1460   &&\text{(ÐÏ ôÅÏÒÅÍÅ ëÌÉÎÉ)}\\
1461   \intertext{úÁÔÅÍ ÄÅÔÅÒÍÉÎÉÚÉÒÕÅÍ Á×ÔÏÍÁÔÙ:}
1462   &\begin{aligned}
1463     \KA &\models s' = \detA(s')\\
1464     \KA &\models t' = \detA(t')
1465   \end{aligned}
1466   &&\text{(ÐÏ ìÅÍÍÅ~\ref{lem:KA-detA})}\\
1467   \intertext{úÁÔÅÍ ÍÉÎÉÍÉÚÉÒÕÅÍ Á×ÔÏÍÁÔÙ:}
1468   &\begin{aligned}
1469     \KA &\models \detA(s') = \minA(\detA(s'))\\
1470     \KA &\models \detA(t') = \minA(\detA(t'))
1471   \end{aligned}
1472   &&\text{(ÐÏ ìÅÍÍÅ~\ref{lem:KA-minA})}\\
1473   \intertext{÷×ÉÄÕ ÅÄÉÎÓÔ×ÅÎÎÏÓÔÉ ÍÉÎÉÍÁÌØÎÏÇÏ ËÏÎÅÞÎÏÇÏ
1474     ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÏÇÏ Á×ÔÏÍÁÔÁ (ôÅÏÒÅÍÁ~\ref{th:minA-unique}),
1475     ÒÁÓÐÏÚÎÁÀÝÅÇÏ $C = R_\Sigma(s') = R_\Sigma(t')$:}
1476   &\KA \models  \minA(\detA(s')) = \minA(\detA(t'))
1477   &&\text{(ÐÏ ìÅÍÍÅ~\ref{lem:KA-isoA} ÏÂ ÉÚÏÍÏÒÆÉÚÍÅ)}\\
1478   \intertext{äÅÌÁÅÍ ×Ù×ÏÄ:}
1479   &\KA \models  s = t.
1480 \end{align}
1481 \end{proof}
1482
1483
1484 \subsection{éÔÏÇÉ}
1485 \label{sec:free-plain-ndet-As}
1486
1487 \paragraph{òÁÚÒÅÛÉÍÏÓÔØ.}
1488 äÁ, $\EquaOf\{ \Reg_{\Sigma} \} = \EquaOf\RKA = \EquaOf\KAc = \EquaOf\KA$
1489 ÒÁÚÒÅÛÉÍÁ. ëÁË: îÁÐÒÉÍÅÒ,
1490 ÍÉÎÉÍÉÚÁÃÉÑ ËÏÎÅÞÎÏÇÏ Á×ÔÏÍÁÔÁ, ÐÒÅÄÓÔÁ×ÌÑÀÝÅÇÏ ÒÅÇÕÌÑÒÎÏÅ
1491 ×ÙÒÁÖÅÎÉÅ. á×ÔÏÍÁÔ ÌÅÇËÏ ÓÔÒÏÉÔÓÑ ÐÏ ×ÙÒÁÖÅÎÉÀ (Ô.ëÌÉÎÉ × ÏÄÎÕ ÓÔÏÒÏÎÕ).
1492
1493 \paragraph{óÌÏÖÎÏÓÔØ.}
1494 $\PSPACE$-ÐÏÌÎÁ. \cite{?}\todo{???}
1495
1496
1497 \paragraph{ðÏÄÓÌÕÞÁÉ.}
1498 äÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÅ Á×ÔÏÍÁÔÙ Ó ÚÁÍÅÔÎÏ ÍÅÎØÛÅÊ ÓÌÏÖÎÏÓÔØÀ ÐÒÏÂÌÅÍÙ
1499 ÜË×-ÔÉ, ÒÁÓÓÍÏÔÒÅÎÙ × òÁÚÄÅÌÅ~\ref{sec:free-plain-det}.
1500
1501 éÔÁË:
1502
1503 \newcommand*{\KAndetAnsws}{
1504 $\KA \supsetneq \KAc \supsetneq \RKA \supsetneq \REL \ni \Reg_{\Sigma}$,
1505 $\REL \supsetneq \FTAPES \not\ni \Reg_{\Sigma}$.
1506 %$\REL \supsetneq \ITAPES  \notni \Reg_{\Sigma}$,
1507
1508 $\EOf\KA = \EOf \KAc = \EOf \RKA = \EOf \REL
1509 \Over{$\Sigma$}{=} \EOf \Reg_{\Sigma} = \EOf \FTAPES_\Sigma$,
1510 $\Reg_{\Sigma}$\T Ó×ÏÂÏÄÎÁÑ ÍÏÄÅÌØ, ÐÏÌÕÞÁÅÔÓÑ ËÁË $\REG \Sigma^*$,
1511 $\Sigma^* = \mo M_0(\emptyset)$ (\sm úÁÍÅÞÁÎÉÅ~\ref{rem:REG-Strs}).
1512
1513 òÁÚÒÅÛÉÍÁ, \PSPACE{}\dÐÏÌÎÁ.
1514 }
1515 \KAndetAnsws
1516
1517
1518 %%% Local Variables:
1519 %%% mode: latex
1520 %%% TeX-master: "main"
1521 %%% End: