free-plain-ndet.tex

   1 \subsection{áËÓÉÏÍÙ ÁÌÇÅÂÒÙ ëÌÉÎÉ}\label{sec:KA-axioms}
   2
   3 \begin{definition}[\cite{KA-RegEv-completeness,KAT-completeness-decidability,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{(KA1)}
  14       \label{eq:KA1}\\
  15       1 + x^*x &= x^*
  16       &&\text{(KA2)}
  17       \label{eq:KA2}\\
  18       y + xz \leq z &\implic x^*y \leq z
  19       &&\text{(KA3)}
  20       \label{eq:KA3}\\
  21       y + zx \leq z &\implic yx^* \leq z
  22       &&\text{(KA4)}
  23       \label{eq:KA4}
  24     \end{align}
  25     üÔÏ\T \emph{ÁËÓÉÏÍÙ ÄÌÑ * ÁÌÇÅÂÒÙ ëÌÉÎÉ}.
  26   \end{itemize}
  27
  28   úÄÅÓØ $\leq$\T ÅÓÔÅÓÔ×ÅÎÎÙÊ ÞÁÓÔÉÞÎÙÊ ÐÏÒÑÄÏË, ÉÎÄÕÃÉÒÏ×ÁÎÎÙÊ ÎÁ
  29   ÉÄÅÍÐÏÔÅÎÔÎÏÍ ÐÏÌÕËÏÌØÃÅ $K$ ÓÔÒÕËÔÕÒÏÊ ×ÅÒÈÎÅÊ
  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-completeness-decidability,KA-RegEv-completeness}]
  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{(KA3$'$)}
  50     \label{eq:KA3'}\tag{$\ref{eq:KA3}'$}\\
  51     zx \leq z &\implic z x^* \leq z.
  52     &&\text{(KA4$'$)}
  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-completeness-decidability,KA-RegEv-completeness}]
  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-completeness-decidability}]
  82   ÷ ÐÒÉÓÕÔÓÔ×ÉÉ ÏÓÔÁÌØÎÙÈ ÁËÓÉÏÍ ÉÚ ÕÓÌÏ×ÉÑ *\dÎÅÐÒÅÒÙ×ÎÏÓÔÉ~\eqref{eq:KA*}
  83   ÓÌÅÄÕÀÔ\marginpar{ÓÅÍ. ÓÌÅÄÕÀÔ?}
  84   \eqref{eq:KA3}, \eqref{eq:KA4}, \eqref{eq:KA3'} ,\eqref{eq:KA4'}.
  85   ðÒÉ ÜÔÏÍ ÏÎÏ ÓÔÒÏÇÏ
  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 Á×ÔÏÍÁÔÏ× ÏËÁÖÅÔÓÑ \tNDNo{ÆÏÒÍÁÌØÎÏÑÚÙËÏ×ÙÅ ÍÏÄÅÌØ} ÄÌÑ ÁÌÇÅÂÒ ëÌÉÎÉ
 100 (ÏÐÉÓÁÎÁ × òÁÚÄÅÌÅ~\ref{sec:KA-langmodels}). äÒÕÇÉÅ ÐÒÉ×ÅÄ£ÎÎÙÅ ÚÄÅÓØ
 101 ÍÏÄÅÌÉ (× òÁÚÄÅÌÁÈ~\ref{sec:KA-relmodels} É~\ref{sec:KA-tracemodels})
 102 ×ÁÖÎÙ ÎÁÍ ÐÏÍÉÍÏ ÔÏÇÏ, ÞÔÏ ÏÎÉ ÐÒÏÓÔÏ ÉÎÔÅÒÅÓÎÙ ÓÁÍÉ ÐÏ ÓÅÂÅ,
 103 ÔÅÍ, ÞÔÏ ÉÍÅÀÔ ÁÎÁÌÏÇÉÉ × ÉÚ×ÅÓÔÎÙÈ ÐÏÄÈÏÄÁÈ Ë ÉÚÕÞÅÎÉÀ ÓÅÍÁÎÔÉË ÐÒÏÇÒÁÍÍ.
 104
 105 ðÒÉÍÅÒÙ ÉÚ ÜÔÏÇÏ òÁÚÄÅÌÁ, Á ÔÁËÖÅ ÄÒÕÇÉÅ ÐÒÉÍÅÒÙ,\T ÈÏÒÏÛÁÑ ÍÏÔÉ×ÁÃÉÑ ÉÚÕÞÅÎÉÑ
 106 ÏÂÝÉÈ Ó×ÏÊÓÔ× \tDJust{ÁÌÇÅÂÒ ëÌÉÎÉ}.
 107
 108 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 109 \subsubsection{æÏÒÍÁÌØÎÏÑÚÙËÏ×ÙÅ ÍÏÄÅÌÉ}
 110 \label{sec:KA-langmodels}
 111
 112 íÙ ÂÕÄÅÍ ÐÏÌØÚÏ×ÁÔØÓÑ ÓÌÅÄÕÀÝÉÍÉ ÂÁÚÏ×ÙÍÉ ÐÏÎÑÔÉÑÍÉ ôÅÏÒÉÉ ÆÏÒÍÁÌØÎÙÈ ÑÚÙËÏ×.
 113 ðÕÓÔØ $\Sigma$ ËÏÎÅÞÎÙÊ ÁÌÆÁ×ÉÔ.
 114 $$
 115 \begin{tabular}{lp{.5\textwidth}}
 116 & {\small ÏÂÏÚÎÁÞÅÎÉÅ}\\
 117 \tING{ËÏÎÅÞÎÙÅ ÓÔÒÏËÉ} ÎÁÄ~$\Sigma$
 118 %% &
 119 %% \\
 120 %% \tING{ÍÎÏÖÅÓÔ×Ï ËÏÎÅÞÎÙÈ ÓÔÒÏË}
 121 %% ÎÁÄ~$\Sigma$
 122 &
 123 $\Strs(\Sigma)$\T
 124 ÍÎÏÖÅÓÔ×Ï ËÏÎÅÞÎÙÈ ÓÔÒÏË
 125 ÎÁÄ~$\Sigma$
 126 \\
 127 \tING{ÐÕÓÔÁÑ ÓÔÒÏËÁ}
 128 &
 129 $\eStr$\\
 130 ÏÐÅÒÁÃÉÑ <<\tING{ËÏÎËÁÔÅÎÁÃÉÑ}>>
 131 &
 132 $\cdot$
 133 \end{tabular}
 134 $$
 135 ïÐÅÒÁÃÉÑ ËÏÎËÁÔÅÎÁÃÉÉ ÏÐÒÅÄÅÌÅÎÁ ÎÁ ×ÓÅÈ ÐÁÒÁÈ ÓÔÒÏË. (ðÒÉ
 136 ÚÁÐÉÓÉ ÍÏÖÎÏ ÏÐÕÓËÁÔØ ÚÎÁË $\cdot$.) óÌÏ×Ï <<ËÏÎÅÞÎÁÑ>> × ÏÔÎÏÛÅÎÉÉ
 137 ÓÔÒÏË ÍÏÖÎÏ ÏÐÕÓËÁÔØ.
 138
 139 \begin{proposition}
 140   óÔÒÕËÔÕÒÁ~$(\Strs(\Sigma); \cdot, \eStr)$\T ÍÏÎÏÉÄ.
 141 \end{proposition}
 142
 143 \begin{remark}
 144   $\Strs(\Sigma)$\T \tND{Ó×ÏÂÏÄÎÙÊ ÍÏÎÏÉÄ}{def:free-monoid} ÎÁÄ
 145 $\Sigma$, ÏÂÙÞÎÏ ÏÂÏÚÎÁÞÁÅÍÙÊ $\Sigma^*$; ÍÙ ×ÅÒÎ£ÍÓÑ Ë ÜÔÏÍÕ
 146 × ÏÐÒÅÄÅÌÅÎÉÉ~\ref{def:free-monoid}.
 147 \end{remark}
 148
 149 ôÅÐÅÒØ ÐÏÓÔÒÏÉÍ ÍÏÄÅÌØ ÄÌÑ ÁÌÇÅÂÒÙ ëÌÉÎÉ ÎÁ ÏÓÎÏ×Å ÐÏÎÑÔÉÊ ôÅÏÒÉÉ
 150 ÆÏÒÍÁÌØÎÙÈ ÑÚÙËÏ×.
 151 âÕÄÅÍ ÒÁÓÓÍÁÔÒÉ×ÁÔØ ÍÎÏÖÅÓÔ×Ï ×ÓÅÈ ÐÏÄÍÎÏÖÅÓÔ×~$\Strs(\Sigma)$\T $2^{\Strs(\Sigma)}$.
 152
 153 \begin{definition}
 154   äÌÑ $A, B \subseteq \Strs(\Sigma)$
 155   \begin{equation}
 156     \label{eq:set-concat}
 157     A \cdot B \eqdef \{ xy \mid x \in A, y \in B \}.
 158   \end{equation}
 159 \end{definition}
 160
 161 \begin{proposition}
 162   óÔÒÕËÔÕÒÁ~$(2^{\Strs(\Sigma)}; \cup, \cdot, \emptyset, \{ \eStr \} )$\T
 163   ÉÄÅÍÐÏÔÅÎÔÎÏÅ ÐÏÌÕËÏÌØÃÏ.
 164 \end{proposition}
 165
 166 \begin{definition}
 167   äÌÑ $A \subseteq \Strs(\Sigma)$
 168   \begin{equation}
 169     \label{eq:set-star}
 170     A^*  \eqdef \bigcup_{n \in \bbN \cup \{ 0 \}} A^n,
 171   \end{equation}
 172   ÇÄÅ
 173   \begin{align*}
 174     A^0 &\eqdef \{ \eStr\}
 175     &
 176     A^{n+1} &\eqdef A \cdot A^n.
 177   \end{align*}
 178 \end{definition}
 179
 180 \begin{proposition}\label{prop:all-str-KA}
 181   óÔÒÕËÔÕÒÁ~$(2^{\Strs(\Sigma)}; \cup, \cdot, {}^*, \emptyset, \{ \eStr \} )$\T
 182   ÁÌÇÅÂÒÁ ëÌÉÎÉ.
 183 \end{proposition}
 184
 185 \begin{proposition}\label{prop:all-str-cont}
 186   áÌÇÅÂÒÁ ëÌÉÎÉ~$(2^{\Strs(\Sigma)}; \cup, \cdot, {}^*, \emptyset, \{ \eStr \} )$
 187   *\dÎÅÐÒÅÒÙ×ÎÁ.
 188 \end{proposition}
 189 \begin{proof}
 190 *\dÎÅÐÒÅÒÙ×ÎÏÓÔØ ÓÌÅÄÕÅÔ ÉÚ ÏÐÒÅÄÅÌÅÎÉÑ $^*$ É ÄÉÓÔÒÉÂÕÔÉ×ÎÏÓÔÉ $\cdot$
 191 ÏÔÎÏÓÉÔÅÌØÎÏ ÂÅÓËÏÎÅÞÎÙÈ ÏÂßÅÄÉÎÅÎÉÊ:
 192 \begin{equation}
 193   \label{eq:str-cont}
 194   A \cdot B^* \cdot C
 195   = A \cdot
 196   \left( \bigcup_{n \in \bbN \cup \{ 0 \}} B^n \right)
 197   \cdot C
 198   = \bigcup_{n \in \bbN \cup \{ 0 \}} \left(
 199     A \cdot B^n \cdot C
 200     \right).
 201 \end{equation}
 202 äÉÓÔÒÉÂÕÔÉ×ÎÏÓÔØ ÏÂßÑÓÎÑÅÔÓÑ ÔÅÍ, ÞÔÏ ÏÂÁ ÜÔÉ ×ÙÒÁÖÅÎÉÑ ÏÂÏÚÎÁÞÁÀÔ ÍÎÏÖÅÓÔ×Ï
 203 $$
 204 \left\{ xyz \mid x \in A, z \in C, \exists n \left( y \in B^n \right) \right\}.
 205 $$
 206 \end{proof}
 207
 208 \begin{definition}\label{def:reg-over-str}
 209 íÉÎÉÍÁÌØÎÁÑ ÐÏÄÁÌÇÅÂÒÁ
 210 ÁÌÇÅÂÒÙ ëÌÉÎÉ~$(2^{\Strs(\Sigma)}; \cup, \cdot, {}^*, \emptyset, \{ \eStr \} )$,
 211 ÓÏÄÅÒÖÁÝÁÑ ÜÌÅÍÅÎÔÙ ×ÉÄÁ $\{ x \}$ ÄÌÑ ×ÓÅÈ ÓÔÒÏË $x \in \Strs(\Sigma)$, ÎÁÚÙ×ÁÅÔÓÑ
 212 \tING{ÁÌÇÅÂÒÏÊ ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ×} ÎÁÄ~$\Strs(\Sigma)$ É ÏÂÏÚÎÁÞÁÅÔÓÑ
 213 $\REG \Strs(\Sigma)$ ÉÌÉ, ËÏÒÏÞÅ, $\Reg_{\Sigma}$.
 214 \end{definition}
 215
 216 éÚ *\dÎÅÐÒÅÒÙ×ÎÏÓÔÉ ÁÌÇÅÂÒÙ ëÌÉÎÉ~$2^{\Strs(\Sigma)}$
 217 (õÔ×.~\ref{prop:all-str-cont})
 218 ÓÌÅÄÕÅÔ
 219 \begin{proposition}
 220   áÌÇÅÂÒÁ ëÌÉÎÉ $\REG \Strs(\Sigma)$ *\dÎÅÐÒÅÒÙ×ÎÁ.
 221 \end{proposition}
 222
 223 îÅÍÎÏÇÏ ÄÒÕÇÏÅ ÜË×É×ÁÌÅÎÔÎÏÅ ÏÐÒÅÄÅÌÅÎÉÅ ÓÅÍÅÊÓÔ×Á ÒÅÇÕÌÑÒÎÙÈ
 224 ÍÎÏÖÅÓÔ× ÓÔÒÏË ÂÕÄÅÔ ÕËÁÚÁÎÏ ÐÒÉ ÒÁÚÇÏ×ÏÒÅ ÏÂ ÉÎÔÅÒÐÒÅÔÁÃÉÉ
 225 \tND{ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ}{def:regexp} ×
 226 úÁÍÅÞÁÎÉÉ~\ref{rem:reg-by-basic}.
 227
 228 ïÐÒÅÄÅÌÅÎÉÅ~\ref{def:reg-over-str} É ×Ó£ ÐÒÏ×ÅÄ£ÎÎÏÅ ÐÏÓÔÒÏÅÎÉÅ ÌÅÇËÏ
 229 ÏÂÏÂÝÁÅÔÓÑ ÎÁ ÓÌÕÞÁÊ ÐÒÏÉÚ×ÏÌØÎÙÈ ÍÏÎÏÉÄÏ× ×ÍÅÓÔÏ $\Strs(\Sigma)$\T
 230 ÓÍ.~\ref{sec:reg-over-mo} \cite{KA-complexity}.
 231
 232 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 233 \subsubsection{òÅÌÑÃÉÏÎÎÙÅ ÍÏÄÅÌÉ}
 234 \label{sec:KA-relmodels}
 235
 236 íÙ ÂÕÄÅÍ ÐÏÌØÚÏ×ÁÔØÓÑ ÓÌÅÄÕÀÝÉÍÉ ÂÁÚÏ×ÙÍÉ ÐÏÎÑÔÉÑÍÉ <<ôÅÏÒÉÉ
 237 ÏÔÎÏÛÅÎÉÊ>> (ÓÍ.~òÁÚÄÅÌ~\ref{sec:relations}).
 238 ðÕÓÔØ $U$ ÍÎÏÖÅÓÔ×Ï.
 239 $$
 240 \begin{tabular}{p{.4\textwidth}p{.5\textwidth}}
 241 & {\small ÏÂÏÚÎÁÞÅÎÉÅ}\\
 242 \tING{ÏÔÎÏÛÅÎÉÅ} ÎÁ~$U$
 243 &
 244 $\Rels(U) \eqdef 2^{U \times U}$\T
 245 ÍÎÏÖÅÓÔ×Ï ÏÔÎÏÛÅÎÉÊ ÎÁ~$U$
 246 \\
 247 \tING{ÎÕÌÅ×ÏÅ ÏÔÎÏÛÅÎÉÅ}
 248 &
 249 $\emptyset$\\
 250 \tING{ÔÏÖÄÅÓÔ×ÅÎÎÏÅ ÏÔÎÏÛÅÎÉÅ}
 251 &
 252 $\id_U$\\
 253 \tING{ÏÂßÅÄÉÎÅÎÉÅ}
 254 &
 255 $\cup$\\
 256 \tING{ËÏÍÐÏÚÉÃÉÑ}
 257 &
 258 $\circ$\\
 259 \tING{ÒÅÆÌÅËÓÉ×ÎÏ\DÔÒÁÎÚÉÔÉ×ÎÏÅ ÚÁÍÙËÁÎÉÅ}
 260 &
 261 $^*$
 262 \end{tabular}
 263 $$
 264
 265 \begin{proposition}\label{prop:rels-KA}
 266   óÔÒÕËÔÕÒÁ~$(\Rels(U); \cup, \circ, ^*, \emptyset, \id_U )$\T
 267   ÁÌÇÅÂÒÁ ëÌÉÎÉ.
 268 \end{proposition}
 269
 270 \begin{proposition}\label{prop:rels-cont}
 271   áÌÇÅÂÒÁ ëÌÉÎÉ~$(\Rels(U); \cup, \circ, ^*, \emptyset, \id_U )$
 272   *\dÎÅÐÒÅÒÙ×ÎÁ.
 273 \end{proposition}
 274 ïÂÁ ÕÔ×ÅÒÖÄÅÎÉÑ ÎÅÔÒÕÄÎÏ ÐÒÏ×ÅÒÉÔØ.
 275 (äÏËÁÚÁÔÅÌØÓÔ×Ï *\dÎÅÐÒÅÒÙ×ÎÏÓÔÉ ÐÏÈÏÖÅ ÎÁ ÓÌÕÞÁÊ ÁÌÇÅÂÒÙ ÆÏÒÍÁÌØÎÙÈ
 276 ÑÚÙËÏ× (õÔ×.~\ref{prop:all-str-cont}).)
 277
 278 \begin{definition}\label{def:relational-KA}
 279   áÌÇÅÂÒÁ ëÌÉÎÉ~$\ka K$ \tING{ÒÅÌÑÃÉÏÎÎÁÑ}, ÅÓÌÉ ÏÎÁ Ñ×ÌÑÅÔÓÑ
 280   ÐÏÄÁÌÇÅÂÒÏÊ ÁÌÇÅÂÒÙ ëÌÉÎÉ~$(\Rels(U); \cup, \circ, ^*, \emptyset,
 281   \id_U)$
 282   ÄÌÑ ÎÅËÏÔÏÒÏÇÏ~$U$; $U$ ÎÁÚÙ×ÁÅÔÓÑ \tING{ÂÁÚÏÊ}~$\ka K$.
 283
 284   \RKA ÏÂÏÚÎÁÞÁÅÔ \tING{ËÁÔÅÇÏÒÉÀ ÒÅÌÑÃÉÏÎÎÙÈ ÁÌÇÅÂÒ ëÌÉÎÉ É ÉÈ ÇÏÍÏÍÏÒÆÉÚÍÏ×}.
 285 \end{definition}
 286
 287 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 288 \subsubsection{ôÒÁÓÓÏ×ÙÅ ÍÏÄÅÌÉ}\label{sec:KA-tracemodels}
 289 ôÒÁÓÓÙ × ÛËÁÌÁÈ ëÒÉÐËÅ ÂÙÌÉ ××ÅÄÅÎÙ × òÁÚÄÅÌÅ~\ref{sec:kframes}.
 290
 291 åÓÌÉ Õ ÔÒÁÓÓ $\sigma$ É $\tau$ $\Last(\sigma) = \First(\tau)$, ÔÏ ÉÈ
 292 ÍÏÖÎÏ ÓÏÅÄÉÎÉÔØ ÜÔÉÍÉ ËÏÎÃÁÍÉ:
 293 \begin{definition}\label{def:trace-concat}
 294   äÌÑ ÔÒÁÓÓ $\sigma$ É $\tau$ × ÛËÁÌÅ ëÒÉÐËÅ $\kf F$:
 295   \begin{align*}
 296     \sigma &= u_0 a_0 u_1 \dotsm  u_n,
 297     &
 298     \tau &= v_0 b_0 v_1 \dotsm  v_m,
 299   \end{align*}
 300 ÏÐÒÅÄÅÌÉÍ:
 301   \begin{equation}
 302     \label{eq:trace-concat}
 303     \sigma \trCo \tau \eqdef
 304     \begin{cases}
 305       u_0 a_0 u_1 \dotsm  u_n b_0 v_1 \dotsm  v_m
 306       & \text{ÅÓÌÉ } u_n = v_0,\\
 307       \text{ÎÅÏÐÒÅÄÅÌÅÎÏ}
 308       & \text{ÅÓÌÉ } u_n \ne v_0.
 309     \end{cases}
 310   \end{equation}
 311 \end{definition}
 312
 313 ïÐÉÛÅÍ ÁÌÇÅÂÒÕ ëÌÉÎÉ ÍÎÏÖÅÓÔ× ÔÒÁÓÓ \cite{?}.
 314
 315 \begin{definition}
 316   ðÕÓÔØ $\kf F = \Stru{Q_{\kf F}, m_{\kf F}}$ ÛËÁÌÁ ëÒÉÐËÅ.
 317   äÌÑ $A, B \subseteq \Trs(\kf F)$
 318   \begin{align}
 319     \label{eq:traces-concat}
 320     A \trCo B &\eqdef \{ \sigma \trCo \tau \mid
 321     \sigma \in A,\, \tau \in B,\, \sigma \trCo \tau \text{ ÓÕÝÅÓÔ×ÕÅÔ}\};\\
 322     \label{eq:traces-star}
 323     A^*  &\eqdef \bigcup_{n \in \bbN \cup \{ 0 \}} A^n,
 324   \end{align}
 325   ÇÄÅ
 326   \begin{align*}
 327     A^0 &\eqdef Q_{\kf F}
 328     &
 329     A^{n+1} &\eqdef A \trCo A^n.
 330   \end{align*}
 331 \end{definition}
 332
 333 \begin{proposition}\label{prop:all-traces-KA}
 334   óÔÒÕËÔÕÒÁ~$(2^{\Trs(\kf F)}; \cup, \trCo, {}^*, \emptyset, Q_{\kf F} )$\T
 335   *\dÎÅÐÒÅÒÙ×ÎÁÑ ÁÌÇÅÂÒÁ ëÌÉÎÉ.
 336 \end{proposition}
 337
 338 \paragraph{òÅÌÑÃÉÏÎÎÙÅ ÍÏÄÅÌÉ, ÏÓÎÏ×ÁÎÎÙÅ ÎÁ ÛËÁÌÁÈ ëÒÉÐËÅ}
 339 \begin{definition}[\cite{KAT-elimination}]\label{def:Ext}
 340   \tING{ëÁÎÏÎÉÞÅÓËÉÊ ÇÏÍÏÍÏÒÆÉÚÍ} $\Ext\colon 2^{\Trs(\kf F)} \to
 341   \Rels(Q_{\kf F})$
 342   ÁÌÇÅÂÒÙ ÍÎÏÖÅÓÔ× ÔÒÁÓÓ × ÛËÁÌÅ
 343   ëÒÉÐËÅ $\kf F$ × ÒÅÌÑÃÉÏÎÎÕÀ ÁÌÇÅÂÒÕ ëÌÉÎÉ ÎÁ $Q_{\kf F}$:
 344   \begin{equation}
 345     \label{eq:Ext}
 346     \Ext(A) \eqdef \{ (\First(\sigma), \Last(\sigma)) \mid \sigma \in
 347     A \}.
 348   \end{equation}
 349 \end{definition}
 350 \begin{application}
 351   åÓÌÉ ÓÍÏÔÒÅÔØ ÎÁ ÔÒÁÓÓÕ ËÁË ÎÁ ×ÏÚÍÏÖÎÕÀ ÉÓÔÏÒÉÀ ×ÙÞÉÓÌÅÎÉÑ ÐÒÏÇÒÁÍÍÙ
 352   (ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÏÓÔØ ÐÒÏÍÅÖÕÔÏÞÎÙÈ ÒÅÚÕÌØÔÁÔÏ×\DÓÏÓÔÏÑÎÉÊ ÐÁÍÑÔÉ),
 353   ÔÏ ÇÏÍÏÍÏÒÆÉÚÍ $\Ext$ ÎÁÄÏ ÐÏÎÉÍÁÔØ ËÁË ÐÏÌÕÞÅÎÉÅ ÉÚ ÉÓÔÏÒÉÊ
 354   ×ÙÞÉÓÌÅÎÉÊ ÏÔÎÏÛÅÎÉÑ <<ÎÁÞÁÌØÎÏÅ ÓÏÓÔÏÑÎÉÅ ÐÁÍÑÔÉ\T ÒÅÚÕÌØÔÁÔ>>
 355   (ÐÕÔ£Í ÚÁÂÙ×ÁÎÉÑ ÐÒÏÍÅÖÕÔÏÞÎÙÈ ÒÅÚÕÌØÔÁÔÏ×).
 356
 357   ÷ÎÅÛÎÅÍÕ ÎÁÂÌÀÄÁÔÅÌÀ ÍÏÖÅÔ ÂÙÔØ ÉÎÔÅÒÅÓÎÏ ÔÏÌØËÏ ÐÏÓÌÅÄÎÅÅ
 358   ÏÔÎÏÛÅÎÉÅ, ÈÁÒÁËÔÅÒÉÚÕÀÝÅÅ ËÏÎÅÞÎÙÊ ÒÅÚÕÌØÔÁÔ ×ÙÞÉÓÌÅÎÉÑ,
 359   ÎÏ ÄÌÑ ÔÏÇÏ, ÞÔÏÂÙ ÉÓÓÌÅÄÏ×ÁÔØ ÒÁÂÏÔÕ ÐÒÏÇÒÁÍÍÙ, ÍÏÖÅÔ ÂÙÔØ ÕÄÏÂÎÏ
 360   ÏÂÒÁÝÁÔØÓÑ Ó ÔÒÁÓÓÁÍÉ.
 361 \end{application}
 362
 363 \todo{[×ÓÔÁ×ÉÔØ ×ÓÀÄÕ ÐÒÏ ÔÏ, ËÁË ÐÒÉÍÅÎÑÔØ]}
 364
 365 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 366 \subsection{òÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ}\label{sec:regexp}
 367 \begin{definition}[\cite{?,KA-modular-elimination}]\label{def:regexp}
 368 ðÕÓÔØ $\Sigma$ ËÏÎÅÞÎÙÊ ÎÁÂÏÒ ÓÉÍ×ÏÌÏ×\DËÏÎÓÔÁÎÔ.
 369 ôÅÒÍÙ ÓÉÇÎÁÔÕÒÙ \tD{ÁÌÇÅÂÒÙ ëÌÉÎÉ}{def:KA} ($+, \cdot, ^*, 0, 1$),
 370 ÄÏÐÏÌÎÅÎÎÏÊ ËÏÎÓÔÁÎÔÁÍÉ ÉÚ~$\Sigma$, ÎÁÚÙ×ÁÀÔÓÑ \tING{ÒÅÇÕÌÑÒÎÙÍÉ
 371   ×ÙÒÁÖÅÎÉÑÍÉ ÎÁÄ $\Sigma$}.
 372 íÎÏÖÅÓÔ×Ï ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ
 373 ÏÂÏÚÎÁÞÁÅÔÓÑ $\RExp_\Sigma$.
 374 üÌÅÍÅÎÔÙ~$\Sigma$ ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ
 375 \tING{ÂÁÚÏ×ÙÍÉ ÏÐÅÒÁÔÏÒÁÍÉ}.
 376 \end{definition}
 377 \begin{table}[hbtp]
 378   \centering
 379 $$
 380 \begin{array}{lll}
 381 \text{ÔÅÒÍÙ}
 382 & s, t  \dotsc
 383 & s ::= \langle\text{ÂÁÚÏ×ÙÅ ÏÐÅÒÁÔÏÒÙ}\rangle
 384 \ |\ 0\ |\ 1\ |\ s+t\ |\ st\ |\ s^*
 385 \end{array}
 386 $$
 387   \caption{ôÅÒÍÙ × ÏÐÒÅÄÅÌÅÎÉÉ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma$}
 388   \label{tab:regexp-bnf}
 389 \end{table}
 390
 391 \begin{remark}
 392   $\RExp_\Sigma$ ÔÏÖÅ ÍÏÖÎÏ ÒÁÓÓÍÁÔÒÉ×ÁÔØ ËÁË ÁÌÇÅÂÒÕ ëÌÉÎÉ. ïÐÅÒÁÃÉÉ
 393   <<ÄÅÊÓÔ×ÕÀÔ>> ÓÉÎÔÁËÓÉÞÅÓËÉ: ÐÒÉÍÅÎ£ÎÎÙÅ Ë ÔÅÒÍÁÍ, ÏÎÉ ÓÏÓÔÁ×ÌÑÀÔ
 394   ÂÏÌÅÅ ÓÌÏÖÎÙÅ ÔÅÒÍÙ.
 395 \end{remark}
 396
 397 õÞÉÔÙ×ÁÑ ÜÔÏ ÚÁÍÅÞÁÎÉÅ, ÍÏÖÎÏ ÓËÁÚÁÔØ ÓÌÅÄÕÀÝÅÅ:
 398
 399 \tING{éÎÔÅÒÐÒÅÔÁÃÉÑ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ}\T ÜÔÏ ÇÏÍÏÍÏÒÆÉÚÍ $I\colon
 400 \RExp_{\Sigma} \to \ka K$, ÇÄÅ $\ka K$\T ÁÌÇÅÂÒÁ ëÌÉÎÉ. ïÎ ÏÄÎÏÚÎÁÞÎÏ
 401 ÏÐÒÅÄÅÌÑÅÔÓÑ ÚÎÁÞÅÎÉÑÍÉ ÎÁ~$\Sigma$. íÙ ÉÓÐÏÌØÚÕÅÍ ÔÁËÉÅ ÏÂÏÚÎÁÞÅÎÉÑ
 402 (×ÓÌÅÄ ÚÁ~\cite{KA-modular-elimination}):
 403 \begin{itemize}
 404 \item ðÕÓÔØ $\ka K$ ÁÌÇÅÂÒÁ ëÌÉÎÉ,
 405   $I\colon \RExp_{\Sigma} \to \ka K$\T ÉÎÔÅÒÐÒÅÔÁÃÉÑ,
 406   $\phi$\T ÆÏÒÍÕÌÁ Ó ÓÉÍ×ÏÌÁÍÉ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ× ÉÚ~$\Sigma$.
 407   ôÏÇÄÁ $\ka K, I \models \phi$ ÚÎÁÞÉÔ, ÞÔÏ $\ka K$ ÕÄÏ×ÌÅÔ×ÏÒÑÅÔ
 408   $\phi$ ÐÒÉ ÉÎÔÅÒÐÒÅÔÁÃÉÉ~$I$.
 409 \item $\ka K \models \phi$ ÚÎÁÞÉÔ, ÞÔÏ $\ka K, I \models \phi$
 410   ÄÌÑ ×ÓÑËÏÊ ÉÎÔÅÒÐÒÅÔÁÃÉÉ $I\colon \RExp_{\Sigma} \to \ka K$.
 411 \item ðÕÓÔØ $\class C$ ËÌÁÓÓ ÁÌÇÅÂÒ. ôÏÇÄÁ $\class C \models
 412   \phi$ ÚÎÁÞÉÔ, ÞÔÏ $\ka K \models \phi$ ÄÌÑ ×ÓÅÈ $\ka K \in \class C$.
 413 \item ðÕÓÔØ $\Phi$ ÍÎÏÖÅÓÔ×Ï ÆÏÒÍÕÌ. $\Phi \models \phi$
 414   ÚÎÁÞÉÔ, ÞÔÏ $\ka K, I \models \phi$ ÄÌÑ ×ÓÅÈ ÐÁÒ $\ka K, I$,
 415   ÕÄÏ×ÌÅÔ×ÏÒÑÀÝÉÈ $\Phi$ (\te ÔÁËÉÈ, ÞÔÏ $\ka K, I \models \psi$ ÄÌÑ
 416   ËÁÖÄÏÊ $\psi \in \Phi$).
 417 \end{itemize}
 418
 419 \subsubsection{(ëÁÎÏÎÉÞÅÓËÉÅ) ÉÎÔÅÒÐÒÅÔÁÃÉÉ}\label{sec:regexp-interp}
 420 \todo{[ËÁÎÏÎÉÞ/ÓÔÁÎÄ -- ?]}
 421
 422 \paragraph{æÏÒÍÁÌØÎÏÑÚÙËÏ×ÁÑ.}
 423 \begin{definition}\label{def:interp-str}
 424   \tING{ëÁÎÏÎÉÞÅÓËÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ $R_{\Sigma}\colon \RExp_{\Sigma} \to
 425   \Reg_{\Sigma}$ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma$}. ðÏÌÏÖÉÍ
 426   $$
 427   R_{\Sigma}(a) \eqdef a \text{ ÄÌÑ } a \in \Sigma
 428   $$
 429   É ÇÏÍÏÍÏÒÆÎÏ ÐÒÏÄÌÉÍ $R_{\Sigma}$ ÎÁ ×Ó£~$\RExp_{\Sigma}$.
 430 \end{definition}
 431 (ëÏÇÄÁ ÓÉÇÎÁÔÕÒÁ $\Sigma$ ÂÕÄÅÔ ÑÓÎÁ, ÍÙ ÂÕÄÅÍ ÏÐÕÓËÁÔØ Å£ × ÚÁÐÉÓÉ.)
 432 ìÅÇËÏ ×ÉÄÅÔØ, ÞÔÏ
 433 ÉÎÔÅÒÐÒÅÔÁÃÉÅÊ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÓÔÁÎÏ×ÑÔÓÑ ÒÅÇÕÌÑÒÎÙÅ ÍÎÏÖÅÓÔ×Á
 434 ÓÔÒÏË ÎÁÄ~$\Sigma$.
 435
 436 ïÂÅÝÁÎÎÏÅ ÐÒÏÓÔÏÅ ÎÁÂÌÀÄÅÎÉÅ ÎÁÄ ÎÁÛÉÍÉ ÏÐÒÅÄÅÌÅÎÉÑÍÉ:
 437 \begin{remark}\label{rem:reg-by-basic}
 438 \tD{áÌÇÅÂÒÁ ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ× ÓÔÒÏË}{def:reg-over-str}~$\Reg_{\Sigma}$
 439 ÎÅ ÉÚÍÅÎÉÔÓÑ, ÅÓÌÉ Å£ ÏÐÒÅÄÅÌÉÔØ ËÁË
 440 ÍÉÎÉÍÁÌØÎÕÀ ÐÏÄÁÌÇÅÂÒÕ, ÐÏÒÏÖÄÁÅÍÕÀ ÜÌÅÍÅÎÔÁÍÉ $R_{\Sigma}(a)\eqdef a$ ÄÌÑ
 441 $a \in \Sigma$.
 442 \end{remark}
 443
 444 \paragraph{ôÒÁÓÓÏ×ÁÑ.}
 445
 446 \begin{definition}[\cite{KAT-elimination}]\label{def:interp-traces}
 447   ðÕÓÔØ $\kf F$ ÛËÁÌÁ ëÒÉÐËÅ ÎÁÄ~$\Sigma$.
 448   \tING{ëÁÎÏÎÉÞÅÓËÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ $\trI{\place}_{\kf F}\colon \RExp_{\Sigma} \to
 449   2^{\Trs(\kf F)}$ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma$}. ðÏÌÏÖÉÍ
 450   $$
 451   \trI{a}_{\kf F} \eqdef \{ u a v \mid (u,v) \in m_{\kf F}(a) \}
 452   \text{ ÄÌÑ } a \in \Sigma
 453   $$
 454   É ÇÏÍÏÍÏÒÆÎÏ ÐÒÏÄÌÉÍ $\trI{\place}_{\kf F}$ ÎÁ ×Ó£~$\RExp_{\Sigma}$.
 455 \end{definition}
 456 \begin{definition}[\cite{KAT-elimination}]
 457   íÎÏÖÅÓÔ×Ï ÔÒÁÓÓ $A \subseteq \Trs(\kf F)$ ÎÁÚÙ×ÁÅÔÓÑ
 458   \tING{ÒÅÇÕÌÑÒÎÙÍ}, ÅÓÌÉ $A = \trI{ s }_{\kf F}$ ÄÌÑ ÎÅËÏÔÏÒÏÇÏ
 459   ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ $s \in \RExp_{\Sigma}$, ÇÄÅ $\kf F$\T ÛËÁÌÁ
 460   ëÒÉÐËÅ ÎÁÄ~$\Sigma$.
 461
 462   \tING{óÅÍÅÊÓÔ×Ï ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ× ÔÒÁÓÓ ×~$\kf F$} ÏÂÏÚÎÁÞÁÅÔÓÑ
 463   $\trReg_{\kf F}$.
 464   (<<$\trReg_{\kf F} \models \phi$>> ÚÎÁÞÉÔ
 465   <<$\trReg_{\kf F}, \trI{\place} \models \phi$>>. \todo{[ÐÏÌÕÞÛÅ ÂÙ ÎÁÐÉÓÁÔØ]})
 466 \end{definition}
 467 \begin{definition}[\cite{KAT-elimination}]
 468   ëÌÁÓÓ ËÁÎÏÎÉÞÅÓËÉÈ ÔÒÁÓÓÏ×ÙÈ ÉÎÔÅÒÐÒÅÔÁÃÉÊ:
 469   $$
 470   \TRACE \eqdef \{ (\trReg_{\kf F}, \trI{\place}_{\kf F})
 471   \mid \kf F \text{\T ÛËÁÌÁ ëÒÉÐËÅ} \}
 472   $$
 473 \end{definition}
 474
 475 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 476 \paragraph{òÅÌÑÃÉÏÎÎÁÑ.}
 477
 478 \begin{definition}[\cite{KAT-elimination}]\label{def:interp-traces}
 479   ðÕÓÔØ $\kf F$ ÛËÁÌÁ ëÒÉÐËÅ ÎÁÄ~$\Sigma$.
 480   \tING{ëÁÎÏÎÉÞÅÓËÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ $\relI{\place}_{\kf F}\colon \RExp_{\Sigma} \to
 481   \Rels(\kf F)$ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma$}. ðÏÌÏÖÉÍ
 482   $$
 483   \relI{a}_{\kf F} \eqdef  m_{\kf F}(a)
 484   \text{ ÄÌÑ } a \in \Sigma
 485   $$
 486   É ÇÏÍÏÍÏÒÆÎÏ ÐÒÏÄÌÉÍ $\relI{\place}_{\kf F}$ ÎÁ ×Ó£~$\RExp_{\Sigma}$.
 487 \end{definition}
 488 \begin{definition}[\cite{KAT-elimination}]
 489   ïÔÎÏÛÅÎÉÅ $S \in \Rels(\kf F)$ ÎÁÚÙ×ÁÅÔÓÑ
 490   \tING{ÒÅÇÕÌÑÒÎÙÍ}, ÅÓÌÉ $S = \relI{ s }_{\kf F}$ ÄÌÑ ÎÅËÏÔÏÒÏÇÏ
 491   ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ $s \in \RExp_{\Sigma}$, ÇÄÅ $\kf F$\T ÛËÁÌÁ
 492   ëÒÉÐËÅ ÎÁÄ~$\Sigma$.
 493
 494   \tING{óÅÍÅÊÓÔ×Ï ÒÅÇÕÌÑÒÎÙÈ ÏÔÎÏÛÅÎÉÊ ÎÁ~$\kf F$} ÏÂÏÚÎÁÞÁÅÔÓÑ
 495   $\relReg_{\kf F}$.
 496   (<<$\relReg_{\kf F} \models \phi$>> ÚÎÁÞÉÔ
 497   <<$\relReg_{\kf F}, \relI{\place}_{\kf F} \models \phi$>>.
 498   \todo{[ÐÏÌÕÞÛÅ ÂÙ ÎÁÐÉÓÁÔØ, ÓÒÁ×ÎÉÔØ Ó $\Reg_{\Sigma}$.]})
 499 \end{definition}
 500 \begin{remark}
 501   \begin{align*}
 502     \Ext(\trI{s}_{\kf F}) &= \relI{s}_{\kf F}
 503     &
 504     &\text{ÄÌÑ ÌÀÂÏÇÏ $s \in \RExp_{\Sigma}$.}
 505   \end{align*}
 506 \end{remark}
 507 \begin{definition}[\cite{KAT-elimination}]
 508   ëÌÁÓÓ ËÁÎÏÎÉÞÅÓËÉÈ ÒÅÌÑÃÉÏÎÎÙÈ ÉÎÔÅÒÐÒÅÔÁÃÉÊ, ÏÓÎÏ×ÁÎÎÙÈ ÎÁ ÛËÁÌÁÈ ëÒÉÐËÅ:
 509   $$
 510   \REL \eqdef \{ (\relReg_{\kf F}, \relI{\place}_{\kf F})
 511   \mid \kf F \text{\T ÛËÁÌÁ ëÒÉÐËÅ} \}
 512   $$
 513 \end{definition}
 514 \begin{question}
 515   \todo{$\REL \models \phi \iff \RKA \models \phi$?}
 516 \end{question}
 517
 518 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 519 \subsection{÷ÏÐÒÏÓÙ ÍÅÔÁÔÅÏÒÉÉ ÁÌÇÅÂÒ ëÌÉÎÉ É ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ}
 520 îÁÓ ÂÕÄÕÔ ÉÎÔÅÒÅÓÏ×ÁÔØ ÔÁËÉÅ ×ÏÐÒÏÓÙ.
 521
 522 \begin{enumerate}
 523 \item
 524 ïÔÌÉÞÁÀÔÓÑ ÌÉ ××ÅÄ£ÎÎÙÅ ËÌÁÓÓÙ ÁÌÇÅÂÒ ëÌÉÎÉ (Ó ÔÏÞÎÏÓÔØÀ ÄÏ
 525 ÉÚÏÍÏÒÆÉÚÍÏ× ÁÌÇÅÂÒ)?
 526
 527 äÌÑ ËÌÁÓÓÏ× ÏÞÅ×ÉÄÎÙ ÔÁËÉÅ ×ÌÏÖÅÎÉÑ:
 528 \begin{gather}
 529   \label{eq:KA-classes-incl}
 530   \REL \subseteq \RKA \subseteq \KAc \subseteq \KA\\
 531   \TRACE \subseteq \KAc\\
 532   \Reg_{\Sigma} \subseteq \KAc
 533 \end{gather}
 534
 535 \item
 536 ïÔÌÉÞÁÀÔÓÑ ÌÉ ÜË×ÁÃÉÏÎÁÌØÎÙÅ ÔÅÏÒÉÉ ××ÅÄ£ÎÎÙÈ ËÌÁÓÓÏ× ÁÌÇÅÂÒ ëÌÉÎÉ?
 537
 538 \item óÕÝÅÓÔ×ÕÀÔ ÌÉ \todo{Ó×ÏÂÏÄÎÙÅ ÍÏÄÅÌÉ [ÔÁË?]} ÄÌÑ ÜÔÉÈ ËÌÁÓÓÏ×?
 539
 540
 541 \item òÁÚÒÅÛÉÍÙ ÌÉ ÜË×ÁÃÉÏÎÁÌØÎÙÅ ÔÅÏÒÉÉ ÜÔÉÈ ËÌÁÓÓÏ×?
 542
 543 äÒÕÇÉÍÉ ÓÌÏ×ÁÍÉ, ÒÁÚÒÅÛÉÍÁ ÌÉ ÐÒÏÂÌÅÍÁ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ <<ÐÒÏÇÒÁÍÍ>>
 544 (ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ) × ÜÔÉÈ ËÌÁÓÓÁÈ?
 545
 546 é Ó ËÁËÉÍÉ ÄÒÕÇÉÍÉ ÐÒÏÂÌÅÍÁÍÉ Ó×ÑÚÁÎÁ ÐÒÏÂÌÅÍÁ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ?
 547 îÁÐÒÉÍÅÒ, ËÁË Ó×ÑÚÁÎÁ ÐÒÏÂÌÅÍÁ ×ËÌÀÞÅÎÉÑ É ÐÒÏÂÌÅÍÁ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ?
 548 (îÁ ÜÔÏÔ ×ÏÐÒÏÓ ÏÔ×ÅÔ ÐÒÏÓÔÏÊ ××ÉÄÕ ÏÐÒÅÄÅÌÅÎÉÑ ×ËÌÀÞÅÎÉÑ ÞÅÒÅÚ
 549 ÒÁ×ÅÎÓÔ×Ï ÎÁ ÓÔÒ.~\pageref{eq:KA-order} ×~\eqref{eq:KA-order}:
 550   \begin{equation}\tag{\ref{eq:KA-order}}
 551     x \leq y \equivdef x + y = y.)
 552   \end{equation}
 553
 554 \todo{[ÄÒÕÇÉÅ ÐÒÏÂÌÅÍÙ]}
 555
 556
 557 \item íÅÓÔÏ ÐÒÏÂÌÅÍÙ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ × ÓÌÏÖÎÏÓÔÎÏÊ ÉÅÒÁÒÈÉÉ.
 558
 559
 560 \item ëÁËÉÅ ÍÏÖÎÏ ÎÁÚ×ÁÔØ ÉÎÔÅÒÅÓÎÙÅ ÏÓÏÂÙÅ ÐÏÄÓÌÕÞÁÉ?
 561
 562   íÏÖÎÏ ÌÉ ÎÁÌÏÖÉÔØ ÒÁÚÕÍÎÙÅ ÏÇÒÁÎÉÞÅÎÉÑ ÎÁ ËÌÁÓÓ ÍÏÄÅÌÅÊ É
 563   ÓÉÎÔÁËÓÉÞÅÓËÉÅ ËÏÎÓÔÒÕËÃÉÉ ÔÁË, ÞÔÏÂÙ ÈÁÒÁËÔÅÒÉÓÔÉËÉ ÒÁÚÒÅÛÉÍÏÓÔÉ ÉÚÍÅÎÉÌÉÓØ?
 564
 565 \end{enumerate}
 566
 567 ÷ ÜÔÏÍ ÐÒÏÓÔÏÍ ÓÌÕÞÁÅ (ÐÒÏÓÔÏÍ\T ÐÏ ÓÒÁ×ÎÅÎÉÀ Ó ÔÅÍÉ, ÞÔÏ ÒÁÓÓÍÁÔÒÉ×ÁÀÔÓÑ ×
 568 ÓÌÅÄÕÀÝÉÈ çÌÁ×ÁÈ \ref{cha:free-withTests}, \ref{cha:hypo-plain},
 569 \ref{cha:hypo-withTests})
 570 ÍÎÏÇÉÅ ÏÔ×ÅÔÙ ÈÏÒÏÛÏ ÉÚ×ÅÓÔÎÙ. ïÎÉ ÔÅÓÎÏ Ó×ÑÚÁÎÙ É Ó ÍÅÔÁÔÅÏÒÉÅÊ
 571 ËÏÎÅÞÎÙÈ Á×ÔÏÍÁÔÏ× (òÁÚÄÅÌ~\ref{sec:NFA}).
 572
 573 \begin{application}
 574 ÷ ÔÏÍ, ËÁËÉÅ ×ÏÐÒÏÓÙ ÏÂ ÁÌÇÅÂÒÁÈ ëÌÉÎÉ ÍÙ ÈÏÔÉÍ ×ÙÑÓÎÉÔØ, ÍÙ ÉÓÈÏÄÉÍ
 575 ÉÚ ÖÅÌÁÎÉÑ ÉÓÓÌÅÄÏ×ÁÔØ ÁÂÓÔÒÁËÃÉÉ ÐÒÏÇÒÁÍÍ, ÏÓÏÂÅÎÎÏ, ðü ÐÒÏÇÒÁÍÍ. íÙ
 576 ÒÁÓÓÍÁÔÒÉ×ÁÅÍ ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ ËÁË ÁÂÓÔÒÁËÔÎÙÅ <<ÌÉÎÅÊÎÏ>>
 577 ÚÁÐÉÓÁÎÎÙÅ ÐÒÏÇÒÁÍÍÙ, ÓÅÍÁÎÔÉËÕ ÐÒÏÇÒÁÍÍ ÍÙ ÍÏÄÅÌÉÒÕÅÍ ÐÒÉ ÐÏÍÏÝÉ
 578 ÁÌÇÅÂÒ ëÌÉÎÉ.
 579
 580 äÏÐÕÝÅÎÉÅ ÎÁÛÅÇÏ ÉÓÓÌÅÄÏ×ÁÎÉÑ ÐÒÏÇÒÁÍÍ ÍÏÖÅÔ ÓÏÓÔÏÑÔØ × ÔÏÍ, ÞÔÏ
 581 <<ÕÓÔÒÏÊÓÔ×Ï>> ÒÅÁÌØÎÏÊ ÓÅÍÁÎÔÉËÉ ÐÒÏÇÒÁÍÍ ÐÒÅÄÓÔÁ×ÌÑÅÔ ÓÏÂÏÊ ÁÌÇÅÂÒÕ
 582 ëÌÉÎÉ.
 583
 584 \end{application}
 585
 586 \subsubsection{ïÔ×ÅÔÙ}
 587
 588 \begin{remark}
 589   óÔÒÏËÕ $\sigma$ ÉÚ $\Strs(\Sigma)$ ÍÏÖÎÏ ÒÁÓÓÍÁÔÒÉ×ÁÔØ ËÁË
 590   ÒÅÇÕÌÑÒÎÏÅ ×ÙÒÁÖÅÎÉÅ ÉÚ $\RExp_{\Sigma}$. üÔÏ ÎÁÂÌÀÄÅÎÉÅ ÐÏÍÏÖÅÔ
 591   ÕÓÔÁÎÏ×ÉÔØ, ÞÔÏ $\Reg_{\Sigma}$ Ó×.Í. \KAc.
 592 \end{remark}
 593
 594 \begin{corollary}[\cite{?}]
 595   $\Reg_{\Sigma}$ Ñ×ÌÑÅÔÓÑ \tD{Ó×ÏÂÏÄÎÏÊ}{def:free-model} \KA,
 596   ÐÏÒÏÖÄ£ÎÎÏÊ $\Sigma$.
 597 \end{corollary}
 598
 599
 600 %%% Local Variables:
 601 %%% mode: latex
 602 %%% TeX-master: "main"
 603 %%% End: