free-withTests-ndet.tex

   1
   2 \subsection{áËÓÉÏÍÙ ÁÌÇÅÂÒÙ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ}\label{sec:KAT-axioms}
   3 \tNDNo{áÌÇÅÂÒÁ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ}\T ÜÔÏ \tD{ÁÌÇÅÂÒÁ ëÌÉÎÉ}{def:KA} ÓÏ
   4 ×ÓÔÒÏÅÎÎÏÊ ÂÕÌÅ×ÏÊ ÐÏÄÁÌÇÅÂÒÏÊ. æÏÒÍÁÌØÎÏ:
   5 %
   6 \begin{definition}[\cite{KAT-commutativity,KAT-complete-decidable,KA-modular-elimination}]
   7   \label{def:KAT}
   8   \tING{áÌÇÅÂÒÁ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ}\T ÜÔÏ ÓÔÒÕËÔÕÒÁ $\ka T = (K, B; +, \cdot, ^*,
   9   \nP, 0, 1)$,
  10   ÔÁËÁÑ, ÞÔÏ $\nP$\T ÕÎÁÒÎÙÊ ÏÐÅÒÁÔÏÒ, ÏÐÒÅÄÅÌ£ÎÎÙÊ ÔÏÌØËÏ ÎÁ $B$, É
  11   \begin{itemize}
  12   \item $\Stru{B; +, \cdot, 0, 1}$ Ñ×ÌÑÅÔÓÑ ÐÏÄÁÌÇÅÂÒÏÊ
  13     $\Stru{K; +, \cdot, 0, 1}$,
  14   \item $\ka K = (K; +, \cdot, ^*, 0, 1)$ Ñ×ÌÑÅÔÓÑ \tD{ÁÌÇÅÂÒÏÊ
  15       ëÌÉÎÉ}{def:KA},
  16   \item Á $\ba B = (B; +, \cdot, \nP, 0, 1)$\T \tD{ÂÕÌÅ×ÏÊ ÁÌÇÅÂÒÏÊ}.
  17   \end{itemize}
  18
  19   üÌÅÍÅÎÔÙ $B$ ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ \tING{ÔÅÓÔÁÍÉ}; ÉÎÄÕÃÉÒÏ×ÁÎÎÕÀ ÂÕÌÅ×Õ
  20   ÁÌÇÅÂÒÕ $\ba B$ ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ
  21   $\baTests(\ka T)$.
  22
  23   \KAT ÏÂÏÚÎÁÞÁÅÔ \tING{ËÁÔÅÇÏÒÉÀ ÁÌÇÅÂÒ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ É ÉÈ
  24     ÇÏÍÏÍÏÒÆÉÚÍÏ×},
  25   \KATc\T ÐÏÄËÁÔÅÇÏÒÉÀ \tING{*\dÎÅÐÒÅÒÙ×ÎÙÈ ÁÌÇÅÂÒ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ É ÉÈ
  26     ÇÏÍÏÍÏÒÆÉÚÍÏ×} (ïÐÒÅÄÅÌÅÎÉÅ~\ref{def:KA-cont} *\dÎÅÐÒÅÒÙ×ÎÏÓÔÉ
  27     ÐÒÉÍÅÎÉÍÏ Ë ÉÎÄÕÃÉÒÏ×ÁÎÎÏÊ ÁÌÇÅÂÒÏÊ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ $\ka T$
  28     ÁÌÇÅÂÒÅ ëÌÉÎÉ $\ka K$.)
  29 \end{definition}
  30 (ðÒÉ ÞÔÅÎÉÉ ×ÙÒÁÖÅÎÉÊ
  31 $\nP$ ÉÍÅÅÔ ÓÁÍÙÊ ÂÏÌØÛÏÊ ÐÒÉÏÒÉÔÅÔ ÓÒÅÄÉ ÏÐÅÒÁÃÉÊ, × ÏÓÔÁÌØÎÏÍ
  32 ÐÒÉÏÒÉÔÅÔ ÔÁËÏÊ ÖÅ, ËÁË ÄÌÑ ÁÌÇÅÂÒ ëÌÉÎÉ:
  33 $\nP, ^*, \cdot, +$.
  34 úÎÁË <<\KAT>> ÍÙ ÉÎÏÇÄÁ ÂÕÄÅÍ
  35 ÐÉÓÁÔØ ×ÍÅÓÔÏ ÓÌÏ× <<ÁÌÇÅÂÒÁ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ>>.)
  36
  37 ëÁË É ÁÌÇÅÂÒÙ ëÌÉÎÉ,
  38 ÍÎÏÇÉÅ ÅÓÔÅÓÔ×ÅÎÎÏ ×ÏÚÎÉËÁÀÝÉÅ ÁÌÇÅÂÒÙ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ *\dÎÅÐÒÅÒÙ×ÎÙ.
  39
  40 \begin{application}
  41 \tNDNo{áÌÇÅÂÒÁ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ} \cite{KAT-commutativity}\T ÜÔÏ ÒÁÓÛÉÒÅÎÉÅ ÐÏÎÑÔÉÑ
  42 \tDJust{ÁÌÇÅÂÒÙ ëÌÉÎÉ}, ÍÏÔÉ×ÉÒÏ×ÁÎÎÏÅ ÔÅÍ, ÞÔÏ ÐÒÏÇÒÁÍÍÙ ÓÏÓÔÏÑÔ ÉÚ
  43 ÂÁÚÏ×ÙÈ ÜÌÅÍÅÎÔÏ× Ä×ÕÈ ÓÏÒÔÏ×\T ÏÐÅÒÁÔÏÒÏ×, ÐÒÏÉÚ×ÏÄÑÝÉÈ ÐÒÅÏÂÒÁÚÏ×ÁÎÉÑ,
  44 É ÔÅÓÔÏ×, ÐÒÏ×ÅÒÑÀÝÉÈ, ×ÙÐÏÌÎÅÎÙ ÌÉ ËÁËÉÅ-ÔÏ ÕÓÌÏ×ÉÑ. ðÒÉ ÐÏÍÏÝÉ
  45 ÁÌÇÅÂÒ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ ÍÙ ÍÏÖÅÍ ÌÕÞÛÅ ÏÔÒÁÚÉÔØ ÜÔÏ ÒÁÚÌÉÞÉÅ × ÎÁÛÉÈ
  46 ÁÂÓÔÒÁËÔÎÙÈ ÍÏÄÅÌÑÈ.
  47 \end{application}
  48
  49 \subsection{îÅËÏÔÏÒÙÅ ×ÁÖÎÙÅ ÁÌÇÅÂÒÙ ëÌÉÎÉ}\label{sec:KAT-models}
  50 \todo{[ÒÁÚÏÂÒÁÔØÓÑ Ó ÕÐÏÔÒÅÂÌÅÎÉÅÍ ÓÌÏ× ÁÌÇÅÂÒÁ/ÍÏÄÅÌØ ÔÕÔ]}
  51
  52 úÄÅÓØ ÐÒÅÄÓÔÁ×ÌÅÎÙ ×ÁÖÎÙÅ ÄÌÑ ÎÁÓ ÍÏÄÅÌÉ \KAT. ïÎÉ ÒÏÄÓÔ×ÅÎÎÙ ÍÏÄÅÌÑÍ \KA,
  53 ÏÐÉÓÁÎÎÙÍ × òÁÚÄÅÌÅ~\ref{sec:KA-models}. ÷ ÏÔÌÉÞÉÅ ÏÔ ÁÌÇÅÂÒ ëÌÉÎÉ,
  54 ÆÏÒÍÁÌØÎÏÑÚÙËÏ×ÁÑ ÍÏÄÅÌØ ÄÌÑ ËÏÔÏÒÙÈ (òÁÚÄÅÌ~\ref{sec:KA-langmodels})
  55 ×ÏÓÐÒÉÎÉÍÁÌÁÓØ ÏÞÅÎØ ÅÓÔÅÓÔ×ÅÎÎÏ
  56 ××ÉÄÕ Ó×ÏÅÊ ÎÅÐÏÓÒÅÄÓÔ×ÅÎÎÏÊ Ó×ÑÚÉ Ó ÐÒÉ×ÙÞÎÏÊ ôÅÏÒÉÅÊ ÒÅÇÕÌÑÒÎÙÈ
  57 ÆÏÒÍÁÌØÎÙÈ ÑÚÙËÏ× É ËÏÎÅÞÎÙÈ Á×ÔÏÍÁÔÏ×, ÁÌÇÅÂÒÙ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ ÎÅ
  58 ÏÂÌÁÄÁÀÔ ÓÔÏÌØ ÖÅ ÅÓÔÅÓÔ×ÅÎÎÏ ×ÏÚÎÉËÁÀÝÅÊ ÍÏÄÅÌØÀ ÎÁ ÆÏÒÍÁÌØÎÙÈ
  59 ÑÚÙËÁÈ. úÁÔÏ ÒÅÌÑÃÉÏÎÎÙÅ É ÔÒÁÓÓÏ×ÙÅ ÍÏÄÅÌÉ \KAT\T ÚÎÁËÏÍÙÅ ÐÏÄÈÏÄÙ Ë
  60 ÉÚÕÞÅÎÉÀ ÓÅÍÁÎÔÉË ÐÒÏÇÒÁÍÍ, É ÏÎÉ ×Ï ÍÎÏÇÏÍ É ÐÏÂÕÄÉÌÉ ××ÅÄÅÎÉÅ ÔÁËÏÇÏ
  61 ÎÏ×ÏÇÏ ÏÂßÅËÔÁ ÉÚÕÞÅÎÉÑ ËÁË ÁÌÇÅÂÒÁ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ. ó ÎÉÈ ÍÙ É ÎÁÞÎ£Í.
  62
  63 \subsubsection{òÅÌÑÃÉÏÎÎÙÅ ÍÏÄÅÌÉ}
  64 \label{sec:KAT-relmodels}
  65
  66 áÎÁÌÏÇ õÔ×.~\ref{prop:rels-KA} É~\ref{prop:rels-cont}:
  67 \begin{proposition}\cite{KA-proof-theory}\label{prop:rels-KAT}
  68   ðÕÓÔØ $K = \Rels(U)$, $B = \{ S \in K \mid S \subseteq \id_U \}$;
  69   ÏÐÒÅÄÅÌÉÍ ÄÌÑ $\bt S \in B$:
  70   $$
  71   \n{\bt S} \eqdef \id_U \setminus \bt S.
  72   $$
  73   ôÏÇÄÁ ÓÔÒÕËÔÕÒÁ~$(K, B; \cup, \circ, ^*, \nP, \emptyset, \id_U )$\T
  74   *\dÎÅÐÒÅÒÙ×ÎÁÑ ÁÌÇÅÂÒÁ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ.
  75 \end{proposition}
  76
  77 \begin{definition}\label{def:relational-KA}
  78   áÌÇÅÂÒÁ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ~$\ka T$ \tING{ÒÅÌÑÃÉÏÎÎÁÑ}, ÅÓÌÉ ÏÎÁ Ñ×ÌÑÅÔÓÑ
  79   ÐÏÄÁÌÇÅÂÒÏÊ ÁÌÇÅÂÒÙ ÉÚ õÔ×.~\ref{prop:rels-KAT}
  80   ÄÌÑ ÎÅËÏÔÏÒÏÊ \tING{ÂÁÚÙ}~$U$.
  81
  82   \RKAT ÏÂÏÚÎÁÞÁÅÔ \tING{ËÁÔÅÇÏÒÉÀ ÒÅÌÑÃÉÏÎÎÙÈ ÁÌÇÅÂÒ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ É ÉÈ ÇÏÍÏÍÏÒÆÉÚÍÏ×}.
  83 \end{definition}
  84
  85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  86 \subsubsection{ôÒÁÓÓÏ×ÙÅ ÍÏÄÅÌÉ}\label{sec:KAT-tracemodels}
  87
  88 áÎÁÌÏÇ õÔ×.~\ref{prop:all-traces-KA}:
  89 \begin{proposition}\label{prop:all-traces-KAT}
  90   ðÕÓÔØ $K = 2^{\Trs(\kf F)}$, $B = 2^{Q_{\kf F}}$ (\te ÍÎÏÖÅÓÔ×Á
  91   ÔÒÁÓÓ ÄÌÉÎÙ~0);   ÏÐÒÅÄÅÌÉÍ ÄÌÑ $\bt S \in B$:
  92   $$
  93   \n{\bt S} \eqdef  Q_{\kf F} \setminus \bt S.
  94   $$
  95   óÔÒÕËÔÕÒÁ~$(K, B; \cup, \trCo, {}^*, \nP, \emptyset, Q_{\kf F} )$\T
  96   *\dÎÅÐÒÅÒÙ×ÎÁÑ ÁÌÇÅÂÒÁ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ.
  97 \end{proposition}
  98
  99 \begin{remark}
 100   çÏÍÏÍÏÒÆÉÚÍ ÁÌÇÅÂÒ ëÌÉÎÉ $\Ext\colon 2^{\Trs(\kf F)} \to
 101   \Rels(Q_{\kf F})$, ÏÐÒÅÄÅÌ£ÎÎÙÊ~\eqref{eq:Ext}:
 102   \begin{equation}
 103     \tag{\ref{eq:Ext}}
 104     \eqExt
 105   \end{equation}
 106   Ñ×ÌÑÅÔÓÑ É ÇÏÍÏÍÏÒÆÉÚÍÏÍ \KAT.
 107 \end{remark}
 108
 109 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 110 \subsubsection{æÏÒÍÁÌØÎÏÑÚÙËÏ×ÙÅ ÍÏÄÅÌÉ: ÎÁÓÙÝÅÎÎÙÅ ÓÔÒÏËÉ (<<guarded strings>>)}
 111 \label{sec:KAT-langmodels}
 112 ðÕÓÔØ $\Sigma$ É $T$ ËÏÎÅÞÎÙÅ ÁÌÆÁ×ÉÔÙ (ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ× É ÔÅÓÔÏ×).
 113
 114 ïÂÏÚÎÁÞÉÍ $\Atoms_T$ ÍÎÏÖÅÓÔ×Ï \tND{ÁÔÏÍÏ×}{?} (ÍÉÎÉÍÁÌØÎÙÈ ÎÅÎÕÌÅ×ÙÈ
 115 ÜÌÅÍÅÎÔÏ×) Ó×ÏÂÏÄÎÏÊ ÂÕÌÅ×ÏÊ ÁÌÇÅÂÒÙ, ÐÏÒÏÖÄ£ÎÎÏÊ $T$. (\Te ËÁÖÄÙÊ ÁÔÏÍ
 116 ÓÏÏÔÎÏÓÉÔÓÑ Ó ÎÅËÏÔÏÒÏÊ \tNDNo{ÜÌÅÍÅÎÔÁÒÎÏÊ ËÏÎßÀÎËÃÉÅÊ}, × ËÏÔÏÒÏÊ ÕÞÁÓÔ×ÕÀÔ
 117 ×ÓÅ ÓÉÍ×ÏÌÙ ÉÚ $T$; ÉÌÉ, ÐÏ-ÄÒÕÇÏÍÕ, Ó ÎÅËÏÔÏÒÙÍ ÏÔÏÂÒÁÖÅÎÉÅÍ $c\colon
 118 T \to \{ 0, 1 \}$, ÏÚÎÁÞÉ×ÁÀÝÉÍ ×ÓÅ ÐÒÏÐÏÚÉÃÉÏÎÁÌØÎÙÅ ÐÅÒÅÍÅÎÎÙÅ
 119 ÉÚ~$T$.)
 120
 121 \begin{definition}[\cite{KAT-complete-decidable,AGS,KAT-elimination}]\label{def:gs}
 122   \tING{îÁÓÙÝÅÎÎÏÊ ÓÔÒÏËÏÊ} (\tING{guarded string}\footnote{ðÅÒÅ×ÏÄ ÎÁ
 123     ÒÕÓÓËÉÊ ÎÅ ÄÏÓÌÏ×ÎÙÊ.}) ÎÁÄ~$\Sigma, T$
 124   ÎÁÚÙ×ÁÅÔÓÑ
 125   ËÏÎÅÞÎÁÑ ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÏÓÔØ~$\sigma$ ×ÉÄÁ:
 126   \begin{equation}
 127     \label{eq:gs}
 128     \alpha_0 a_0 \alpha_1 \dotsm \alpha_{n-1} a_{n-1} \alpha_n,
 129   \end{equation}
 130   ÇÄÅ $n \in \bbN \cup \{ 0 \}$ É
 131   \begin{align*}
 132     \alpha_i &\in \Atoms_T,
 133     &
 134     a_i &\in \Sigma.
 135   \end{align*}
 136
 137   \tING{íÎÏÖÅÓÔ×Ï ÎÁÓÙÝÅÎÎÙÈ ÓÔÒÏË ÎÁÄ~$\Sigma, T$} ÏÂÏÚÎÁÞÉÍ $\GS(\Sigma,T)$.
 138
 139   äÌÑ ÎÁÓÙÝÅÎÎÏÊ ÓÔÒÏËÉ~$\sigma$ ×ÉÄÁ~\eqref{eq:gs}
 140 %  \tING{ÄÌÉÎÁ~$\Len{\sigma}$} ÒÁ×ÎÁ $n$,
 141   \begin{align*}
 142     \First(\sigma) &\eqdef \alpha_0,
 143     &
 144     \Last(\sigma) &\eqdef \alpha_n.
 145   \end{align*}
 146
 147 \end{definition}
 148 ïÐÒÅÄÅÌÉÍ ÞÁÓÔÉÞÎÏ ÏÐÒÅÄÅÌ£ÎÎÕÀ ÏÐÅÒÁÃÉÀ \tING{ÓÏÅÄÉÎÅÎÉÑ ÎÁÓÙÝÅÎÎÙÈ ÓÔÒÏË}
 149 (ÄÌÑ~$\sigma$ É~$\tau$, Õ ËÏÔÏÒÙÈ $\Last(\sigma) = \First(\tau)$):
 150 \begin{definition}\label{def:gs-concat}
 151   äÌÑ ÎÁÓÙÝÅÎÎÙÈ ÓÔÒÏË $\sigma, \tau \in \GS(\Sigma,T)$:
 152   \begin{align*}
 153     \sigma &= \alpha_0 a_0 \alpha_1 \dotsm  \alpha_n,
 154     &
 155     \tau &= \beta_0 b_0 \beta_1 \dotsm \beta_m,
 156   \end{align*}
 157 ÏÐÒÅÄÅÌÉÍ:
 158   \begin{equation}
 159     \label{eq:gs-concat}
 160     \sigma \gsCo \tau \eqdef
 161     \begin{cases}
 162       \alpha_0 a_0 \alpha_1 \dotsm  \alpha_n b_0 \beta_1 \dotsm  \beta_m
 163       & \text{ÅÓÌÉ } \alpha_n = \beta_0,\\
 164       \text{ÎÅÏÐÒÅÄÅÌÅÎÏ}
 165       & \text{ÉÎÁÞÅ.}
 166     \end{cases}
 167   \end{equation}
 168 \end{definition}
 169
 170 ïÐÉÛÅÍ ÁÌÇÅÂÒÕ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ ÍÎÏÖÅÓÔ× ÎÁÓÙÝÅÎÎÙÈ ÓÔÒÏË.
 171
 172 \begin{definition}
 173   äÌÑ $A, B \subseteq \GS(\Sigma,T), \bt C \subseteq \Atoms_T$
 174   \begin{align}
 175     \n{\bt C} &\eqdef \Atoms_T \setminus \bt C\\
 176     \label{eq:gs-set-concat}
 177     A \gsCo B &\eqdef \{ \sigma \gsCo \tau \mid
 178     \sigma \in A,\, \tau \in B,\, \sigma \gsCo \tau \text{ ÓÕÝÅÓÔ×ÕÅÔ}\};\\
 179     \label{eq:gs-set-star}
 180     A^*  &\eqdef \bigcup_{n \in \bbN \cup \{ 0 \}} A^n,
 181   \end{align}
 182   ÇÄÅ
 183   \begin{align*}
 184     A^0 &\eqdef \Atoms_T
 185     &
 186     A^{n+1} &\eqdef A \gsCo A^n.
 187   \end{align*}
 188 \end{definition}
 189
 190 \begin{proposition}\label{prop:all-gs-KA}
 191   óÔÒÕËÔÕÒÁ~$(2^{\GS(\Sigma,T)}, 2^{\Atoms_{T}};
 192   \cup, \gsCo, {}^*, \nP, \emptyset, \Atoms_{T} )$\T
 193   *\dÎÅÐÒÅÒÙ×ÎÁÑ \KAT.
 194 \end{proposition}
 195 \begin{remark}\label{rem:gs-as-trace}
 196   îÁÓÙÝÅÎÎÁÑ ÓÔÒÏËÁ ÎÁÄ~$\Sigma,T$ ÐÏ ÓÕÔÉ Ñ×ÌÑÅÔÓÑ
 197   ÔÒÁÓÓÏÊ × ÛËÁÌÅ ëÒÉÐËÅ~$\kf G = (\Atoms_T, m_{\kf G})$,
 198   ÇÄÅ
 199   \begin{align*}
 200     m_{\kf G}(a) &\eqdef \Atoms_T \times \Atoms_T
 201     &
 202     & \text{ÄÌÑ } a \in \Sigma,\\
 203     m_{\kf G}(p) &\eqdef \{ \alpha \in \Atoms_T \mid \alpha \implic p \}
 204     &
 205     & \text{ÄÌÑ } p \in T.
 206   \end{align*}
 207   (íÙ ÔÏÌØËÏ ÄÌÑ ÎÁÇÌÑÄÎÏÓÔÉ ÏÐÒÅÄÅÌÅÎÉÊ ÎÅ ÏÐÒÅÄÅÌÉÌÉ ÓÒÁÚÕ \tDJust{ÎÁÓÙÝÅÎÎÕÀ ÓÔÒÏËÕ}
 208   ËÁË ÔÒÁÓÓÕ.)
 209
 210   \KAT, ÔÏÌØËÏ ÞÔÏ ÐÏÓÔÒÏÅÎÎÁÑ ÎÁ ÏÓÎÏ×Å ÎÁÓÙÝÅÎÎÙÈ ÓÔÒÏË, ÓÏ×ÐÁÄÁÅÔ Ó
 211   \KAT, ÐÏÌÕÞÁÅÍÏÊ × ÒÅÚÕÌØÔÁÔÅ ÏÂÝÅÊ ËÏÎÓÔÒÕËÃÉÉ ÄÌÑ ÔÒÁÓÓ
 212   ÉÚ òÁÚÄÅÌÁ~\ref{sec:KAT-tracemodels}.
 213
 214   \begin{example}
 215     \todo{[ÞÔÏ ÎÁÐÉÓÁÔØ?]}
 216   \end{example}
 217 \end{remark}
 218
 219
 220 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 221 \subsection{ðÒÏÇÒÁÍÍÙ: òÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ (Ó ÔÅÓÔÁÍÉ)}\label{sec:KAT-regexp}
 222 \begin{definition}[\cite{?,KA-modular-elimination,AGS}]\label{def:KAT-regexp}
 223 ðÕÓÔØ $\Sigma$ É $T$ ËÏÎÅÞÎÙÅ ÎÁÂÏÒÙ ÓÉÍ×ÏÌÏ×\DËÏÎÓÔÁÎÔ.
 224
 225 \tING{âÕÌÅ×ÓËÉÍÉ ÔÅÒÍÁÍÉ} ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ
 226 ÔÅÒÍÙ ÓÉÇÎÁÔÕÒÙ \tD{ÂÕÌÅ×ÏÊ ÁÌÇÅÂÒÙ}{def:bool-algebra}
 227 (\te $+, \cdot, \nP, 0, 1$),
 228 ÄÏÐÏÌÎÅÎÎÏÊ ËÏÎÓÔÁÎÔÁÍÉ ÉÚ~$T$.
 229
 230 ôÅÒÍÙ ÓÉÇÎÁÔÕÒÙ \tD{\KAT{}}{def:KAT} (\te $+, \cdot, ^*, \nP, 0, 1$),
 231 ÄÏÐÏÌÎÅÎÎÏÊ ËÏÎÓÔÁÎÔÁÍÉ ÉÚ~$\Sigma$ É $T$,
 232 × ËÏÔÏÒÙÈ ÏÔÒÉÃÁÎÉÅ $\nP$ ÒÁÚÒÅÛÁÅÔÓÑ ÐÒÉÍÅÎÑÔØ ÔÏÌØËÏ Ë
 233 \tING{ÂÕÌÅ×ÓËÉÍ ÔÅÒÍÁÍ},
 234 ÎÁÚÙ×ÁÀÔÓÑ \tING{ÒÅÇÕÌÑÒÎÙÍÉ ×ÙÒÁÖÅÎÉÑÍÉ ÎÁÄ~$\Sigma, T$}, ÉÌÉ
 235 \tING{ÒÅÇÕÌÑÒÎÙÍÉ ×ÙÒÁÖÅÎÉÑÍÉ Ó ÔÅÓÔÁÍÉ}.
 236 íÎÏÖÅÓÔ×Ï ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma, T$
 237 ÏÂÏÚÎÁÞÁÅÔÓÑ $\RExp_{\Sigma,T}$.
 238 üÌÅÍÅÎÔÙ~$\Sigma$ ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ
 239 \tING{ÂÁÚÏ×ÙÍÉ ÏÐÅÒÁÔÏÒÁÍÉ},
 240 $T$\T \tING{ÂÁÚÏ×ÙÍÉ ÔÅÓÔÁÍÉ}.
 241 \end{definition}
 242 \begin{table}[hbtp]
 243   \centering
 244 $$
 245 \begin{array}{lll}
 246 \text{ÂÕÌÅ×ÓËÉÅ ÔÅÒÍÙ}
 247 & \bt s, \bt t  \dotsc
 248 & \bt s ::= \langle\text{{\small ÂÁÚÏ×ÙÅ ÔÅÓÔÙ}}\rangle
 249 \ |\ 0\ |\ 1\ |\ \bt s + \bt t\ |\ \bt s \bt t\ |\ \n{\bt s} \\
 250 \text{ÔÅÒÍÙ}
 251 & s, t  \dotsc
 252 & s ::= \langle\text{{\small ÂÁÚÏ×ÙÅ ÏÐÅÒÁÔÏÒÙ}}\rangle
 253 \ |\ \bt s\ | \ s+t\ |\ st\ |\ s^*
 254 \end{array}
 255 $$
 256   \caption{ôÅÒÍÙ × ÏÐÒÅÄÅÌÅÎÉÉ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma, T$}
 257   \label{tab:KAT-regexp-bnf}
 258 \end{table}
 259
 260 \begin{remark}
 261   $\RExp_{\Sigma,T}$
 262   ÔÏÖÅ ÍÏÖÎÏ ÒÁÓÓÍÁÔÒÉ×ÁÔØ ËÁË ÁÌÇÅÂÒÕ Ó ÓÉÇÎÁÔÕÒÏÊ
 263   ÁÌÇÅÂÒÙ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ. ïÐÅÒÁÃÉÉ
 264   <<ÄÅÊÓÔ×ÕÀÔ>> ÓÉÎÔÁËÓÉÞÅÓËÉ: ÐÒÉÍÅÎ£ÎÎÙÅ Ë ÔÅÒÍÁÍ, ÏÎÉ ÓÏÓÔÁ×ÌÑÀÔ
 265   ÂÏÌÅÅ ÓÌÏÖÎÙÅ ÔÅÒÍÙ.
 266
 267   éÍÅÅÔ ÓÍÙÓÌ ÇÏ×ÏÒÉÔØ Ï ÇÏÍÏÍÏÒÆÎÙÈ ÏÔÏÂÒÁÖÅÎÉÑÈ $\RExp_{\Sigma,T}$
 268   × ÄÒÕÇÉÅ ÁÌÇÅÂÒÙ ÜÔÏÊ ÓÉÇÎÁÔÕÒÙ.
 269 \end{remark}
 270
 271 \begin{definition}
 272
 273 ïÔÏÂÒÁÖÅÎÉÅ $I\colon \Sigma \to \ka T, T \to \baTests(\ka K)$,
 274 ÇÄÅ $\ka T$\T ÁÌÇÅÂÒÁ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ, $\baTests(\ka K)$\T ÂÕÌÅ×Á
 275 ÐÏÄÁÌÇÅÂÒÁ~$\ka T$,
 276 ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ \tING{ÉÎÔÅÒÐÒÅÔÁÃÉÅÊ ÂÁÚÏ×ÙÈ ÓÉÍ×ÏÌÏ× (ÏÐÅÒÁÔÏÒÏ× É ÔÅÓÔÏ×)}.
 277
 278 $I$ ÏÄÎÏÚÎÁÞÎÏ ÐÒÏÄÏÌÖÁÅÔÓÑ ÄÏ ÇÏÍÏÍÏÒÆÉÚÍÁ ÎÁ ×Ó£
 279 $\RExp_{\Sigma,T}$, ÐÒÉ ÜÔÏÍ ÏÎ
 280 ÏÔÏÂÒÁÖÁÅÔ ÂÕÌÅ×ÓËÉÅ ÔÅÒÍÙ ÉÚ $\RExp_{\Sigma,T}$ ×~$\baTests(\ka T)$.
 281 %ÔÁË ÐÏÌÕÞÁÀÝÅÅÓÑ ÏÔÏÂÒÁÖÅÎÉÅ ÍÙ ÔÏÖÅ ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ $I$
 282 åÇÏ ÚÎÁÞÅÎÉÅ ÎÁ $s \in \RExp_{\Sigma,T}$ ÍÙ ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ
 283 ÐÒÏÓÔÏ $I(s)$ É ÎÁÚÙ×ÁÔØ ÅÇÏ ÚÎÁÞÅÎÉÅÍ
 284 ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ Ó ÔÅÓÔÁÍÉ~$s$ ÐÒÉ ÉÎÔÅÒÐÒÅÔÁÃÉÉ~$I$, ÉÌÉ,
 285 \tING{ÉÎÔÅÒÐÒÅÔÁÃÉÅÊ ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ Ó ÔÅÓÔÁÍÉ}~$s$.
 286 \end{definition}
 287
 288 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 289 \subsubsection{(ëÁÎÏÎÉÞÅÓËÉÅ) ÉÎÔÅÒÐÒÅÔÁÃÉÉ $\RExp_{\Sigma,T}$}
 290 \label{sec:KAT-regexp-interp}
 291 \todo{[ËÁÎÏÎÉÞ/ÓÔÁÎÄ -- ?]}
 292
 293 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 294 \paragraph{ôÒÁÓÓÏ×ÁÑ.}
 295
 296 \begin{definition}[\cite{KAT-elimination}]\label{def:interp-traces}
 297   ðÕÓÔØ $\kf F$ ÛËÁÌÁ ëÒÉÐËÅ ÎÁÄ~$\Sigma, T$.
 298   \tING{ëÁÎÏÎÉÞÅÓËÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ $\trI{\place}_{\kf F}\colon \RExp_{\Sigma,T} \to
 299   2^{\Trs(\kf F)}$ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma,T$}. ðÏÌÏÖÉÍ
 300 \begin{align*}
 301   \trI{a}_{\kf F} &\eqdef \{ u a v \mid (u,v) \in m_{\kf F}(a) \}
 302   \text{ ÄÌÑ } a \in \Sigma\\
 303   \trI{p}_{\kf F} &\eqdef m_{\kf F}(p)
 304   \text{ ÄÌÑ } p \in T
 305 \end{align*}
 306   É ÇÏÍÏÍÏÒÆÎÏ ÐÒÏÄÌÉÍ $\trI{\place}_{\kf F}$ ÎÁ ×Ó£~$\RExp_{\Sigma,T}$.
 307 \end{definition}
 308 \begin{definition}[\cite{KAT-elimination}]
 309   íÎÏÖÅÓÔ×Ï ÔÒÁÓÓ $A \subseteq \Trs(\kf F)$ ÎÁÚÙ×ÁÅÔÓÑ
 310   \tING{ÒÅÇÕÌÑÒÎÙÍ}, ÅÓÌÉ $A = \trI{ s }_{\kf F}$ ÄÌÑ ÎÅËÏÔÏÒÏÇÏ
 311   ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ $s \in \RExp_{\Sigma,T}$, ÇÄÅ $\kf F$\T ÛËÁÌÁ
 312   ëÒÉÐËÅ ÎÁÄ~$\Sigma,T$.
 313
 314   \tING{óÅÍÅÊÓÔ×Ï ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ× ÔÒÁÓÓ ×~$\kf F$} ÏÂÏÚÎÁÞÁÅÔÓÑ
 315   $\trReg_{\kf F}$.
 316   (<<$\trReg_{\kf F} \models \phi$>> ÚÎÁÞÉÔ
 317   <<$\trReg_{\kf F}, \trI{\place} \models \phi$>>. \todo{[ÐÏÌÕÞÛÅ ÂÙ ÎÁÐÉÓÁÔØ]})
 318 \end{definition}
 319 äÌÑ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ É ÛËÁÌ ëÒÉÐËÅ ÎÁÄ Ä×ÕÍÑ ÁÌÆÁ×ÉÔÁÍÉ\T ÂÁÚÏ×ÙÈ
 320 ÏÐÅÒÁÔÏÒÏ× É ÔÅÓÔÏ×:
 321 \begin{definition}[\cite{KAT-elimination}]
 322   ëÌÁÓÓ ËÁÎÏÎÉÞÅÓËÉÈ ÔÒÁÓÓÏ×ÙÈ ÉÎÔÅÒÐÒÅÔÁÃÉÊ:
 323   $$
 324   \TRACE \eqdef \{ (\trReg_{\kf F}, \trI{\place}_{\kf F})
 325   \mid \kf F \text{\T ÛËÁÌÁ ëÒÉÐËÅ} \}
 326   $$
 327 \end{definition}
 328
 329 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 330 \paragraph{òÅÌÑÃÉÏÎÎÁÑ.}
 331
 332 \begin{definition}[\cite{KAT-elimination}]\label{def:interp-traces}
 333   ðÕÓÔØ $\kf F$ ÛËÁÌÁ ëÒÉÐËÅ ÎÁÄ~$\Sigma, T$.
 334   \tING{ëÁÎÏÎÉÞÅÓËÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ $\relI{\place}_{\kf F}\colon \RExp_{\Sigma,T} \to
 335   \Rels(\kf F)$ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma,T$}. ðÏÌÏÖÉÍ
 336 \begin{align*}
 337   \relI{a}_{\kf F} &\eqdef  m_{\kf F}(a)
 338   \text{ ÄÌÑ } a \in \Sigma
 339   &
 340   \relI{p}_{\kf F} &\eqdef  \{ (u,u) \mid u \in m_{\kf F}(p) \}
 341   \text{ ÄÌÑ } p \in T
 342 \end{align*}
 343   É ÇÏÍÏÍÏÒÆÎÏ ÐÒÏÄÌÉÍ $\relI{\place}_{\kf F}$ ÎÁ ×Ó£~$\RExp_{\Sigma,T}$.
 344 \end{definition}
 345 \begin{definition}[\cite{KAT-elimination}]
 346   ïÔÎÏÛÅÎÉÅ $S \in \Rels(\kf F)$ ÎÁÚÙ×ÁÅÔÓÑ
 347   \tING{ÒÅÇÕÌÑÒÎÙÍ}, ÅÓÌÉ $S = \relI{ s }_{\kf F}$ ÄÌÑ ÎÅËÏÔÏÒÏÇÏ
 348   ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ $s \in \RExp_{\Sigma,T}$, ÇÄÅ $\kf F$\T ÛËÁÌÁ
 349   ëÒÉÐËÅ ÎÁÄ~$\Sigma,T$.
 350
 351   \tING{óÅÍÅÊÓÔ×Ï ÒÅÇÕÌÑÒÎÙÈ ÏÔÎÏÛÅÎÉÊ ÎÁ~$\kf F$} ÏÂÏÚÎÁÞÁÅÔÓÑ
 352   $\relReg_{\kf F}$.
 353   (<<$\relReg_{\kf F} \models \phi$>> ÚÎÁÞÉÔ
 354   <<$\relReg_{\kf F}, \relI{\place}_{\kf F} \models \phi$>>.
 355   \todo{[ÐÏÌÕÞÛÅ ÂÙ ÎÁÐÉÓÁÔØ, ÓÒÁ×ÎÉÔØ Ó $\Reg_{\Sigma}$.]})
 356 \end{definition}
 357 \begin{remark}
 358   \begin{align*}
 359     \Ext(\trI{s})_{\kf F} &= \relI{s}_{\kf F}
 360     &
 361     &\text{ÄÌÑ ÌÀÂÏÇÏ $s \in \RExp_{\Sigma,T}$.}
 362   \end{align*}
 363 \end{remark}
 364 \todo{[\REL?]}
 365
 366 \paragraph{æÏÒÍÁÌØÎÏÑÚÙËÏ×ÁÑ.}
 367 ðÒÅÄÌÏÖÅÎÎÁÑ ÆÏÒÍÁÌØÎÏÑÚÙËÏ×ÁÑ ÍÏÄÅÌØ \KAT (ÎÁ ÏÓÎÏ×Å ÎÁÓÙÝÅÎÎÙÈ
 368 ÓÔÒÏË; ÓÍ.\ òÁÚÄÅÌ~\ref{sec:KAT-langmodels})
 369 Ñ×ÌÑÅÔÓÑ ÞÁÓÔÎÙÍ ÓÌÕÞÁÅÍ ÔÒÁÓÓÏ×ÏÊ ÍÏÄÅÌÉ ÎÁ ÛËÁÌÅ ëÒÉÐËÅ~$\kf
 370 G$ (úÁÍÅÞÁÎÉÅ~\ref{rem:gs-as-trace}), ÐÏÜÔÏÍÕ ÓÌÅÄÕÀÝÅÅ ÏÐÒÅÄÅÌÅÎÉÅ
 371 ÄÁÎÏ ÎÁ ÏÓÎÏ×Å~$\trIP$:
 372 \begin{definition}\label{def:KAT-interp-gs}
 373   \tING{ëÁÎÏÎÉÞÅÓËÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ $G_{\Sigma,T}\colon \RExp_{\Sigma,T} \to
 374   2^{\GS(\Sigma,T)}$ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ ÎÁÄ~$\Sigma$}:
 375   $$
 376   G_{\Sigma,T}(s) \eqdef \trI{s}_{\kf G} \text{ ÄÌÑ } s \in \RExp_{\Sigma,T}.
 377   $$
 378 \end{definition}
 379 ðÒÏÓÌÅÖÉ×ÁÑ ÓÄÅÌÁÎÎÙÅ ÏÐÒÅÄÅÌÅÎÉÑ ÐÏÌÕÞÁÅÍ, ÞÔÏ ÐÏ ÓÕÔÉ $G$ ÅÓÔØ
 380 ÇÏÍÏÍÏÒÆÎÏÅ ÐÒÏÄÏÌÖÅÎÉÅ ÎÁ ×Ó£~$\RExp_{\Sigma,T}$
 381 ÔÁËÉÈ ÚÁÄÁÎÉÊ ÚÎÁÞÅÎÉÊ ÎÁ ÂÁÚÏ×ÙÈ $\Sigma$ É $T$:
 382 \begin{align*}
 383   G_{\Sigma,T}(a) &\eqdef \{ \alpha a \beta \mid \alpha, \beta \in \Atoms_T  \}
 384   \text{ ÄÌÑ } a \in \Sigma\\
 385   G_{\Sigma,T}(p) &\eqdef \{ \alpha \in \Atoms_T \mid \alpha \implic p \}
 386   \text{ ÄÌÑ } p \in T.
 387 \end{align*}
 388 \begin{example}
 389   $\Sigma = \{ a, b \},\; T = \{ p, q \}$.
 390   ôÏÇÄÁ, ÎÁÐÒÉÍÅÒ,
 391   \begin{align*}
 392     \begin{aligned}[t]
 393       G(p) = \{
 394       &(p\n{q}),\\
 395       &(pq)
 396       \},
 397     \end{aligned}
 398     &&
 399     \begin{aligned}[t]
 400       G(\n{p}q a p b) = \{
 401       &(\n{p}q) a (p\n{q}) b (\n{p}\n{q}),\\
 402       &(\n{p}q) a (p\n{q}) b (\n{p}  {q}),\\
 403       &(\n{p}q) a (p\n{q}) b (  {p}\n{q}),\\
 404       &(\n{p}q) a (p\n{q}) b (  {p}  {q}),\\
 405                                 %
 406       &(\n{p}q) a (p  {q}) b (\n{p}\n{q}),\\
 407       &(\n{p}q) a (p  {q}) b (\n{p}  {q}),\\
 408       &(\n{p}q) a (p  {q}) b (  {p}\n{q}),\\
 409       &(\n{p}q) a (p  {q}) b (  {p}  {q})
 410       \},
 411     \end{aligned}
 412     &&
 413     \begin{aligned}[t]
 414       G(p^*) = G(1) = \{
 415       & (\n{p}\n{q}),\\
 416       & (\n{p}  {q}),\\
 417       & (  {p}\n{q}),\\
 418       & (  {p}  {q})
 419       \}.
 420     \end{aligned}
 421   \end{align*}
 422   þÔÏ ËÁÓÁÅÔÓÑ ÐÏÓÌÅÄÎÅÇÏ ÒÁ×ÅÎÓÔ×Á, ÔÏ  ÜÔÏ ÎÅ ÓÐÅÃÉÆÉËÁ ËÏÎËÒÅÔÎÏÊ
 423   ÉÎÔÅÒÐÒÅÔÁÃÉÉ; ×ÏÏÂÝÅ: $\KAT \models \bt s^* = 1$, ÇÄÅ
 424   $\bt s$ ÂÕÌÅ×ÓËÉÊ ÔÅÒÍ (ÉÎÔÅÒÐÒÅÔÉÒÕÅÔÓÑ ËÁË ÔÅÓÔ).
 425 \end{example}
 426
 427 ðÏ ÁÎÁÌÏÇÉÉ Ó $\Reg_{\Sigma}$ ÄÌÑ \KA:
 428 \begin{definition}
 429   íÎÏÖÅÓÔ×Ï ÎÁÓÙÝÅÎÎÙÈ ÓÔÒÏË $A \subseteq \GS(\Sigma,T)$ ÎÁÚÙ×ÁÅÔÓÑ
 430   \tING{ÒÅÇÕÌÑÒÎÙÍ}, ÅÓÌÉ $A = G_{\Sigma,T}(s)$ ÄÌÑ ÎÅËÏÔÏÒÏÇÏ
 431   ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ $s \in \RExp_{\Sigma,T}$.
 432
 433   \tING{óÅÍÅÊÓÔ×Ï ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ× ÎÁÓÙÝÅÎÎÙÈ ÓÔÒÏË ÎÁÄ~$\Sigma,T$}
 434   ÏÂÏÚÎÁÞÁÅÔÓÑ
 435   $\Reg_{\Sigma,T}$.
 436   (<<$\Reg_{\Sigma,T} \models \phi$>> ÚÎÁÞÉÔ
 437   <<$\Reg_{\Sigma,T}, G \models \phi$>>. \todo{[ÐÏÌÕÞÛÅ ÂÙ ÎÁÐÉÓÁÔØ]})
 438 \end{definition}
 439
 440 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 441 \subsubsection{÷ÏÐÒÏÓÙ ÍÅÔÁÔÅÏÒÉÉ \KAT É $\RExp_{\Sigma,T}$}
 442 \todo{[ÔÅ ÖÅ]}
 443
 444
 445 %  ÎÅÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÅ
 446 \subsection{ðÒÏÇÒÁÍÍÙ: ÐÒÏÐÏÚÉÃÉÏÎÁÌØÎÙÅ ÓÈÅÍÙ}
 447 \label{sec:nps}
 448 (îÅÄÅÔ. ÓÈÅÍÙ ñÎÏ×Á.)
 449
 450 \begin{definition}
 451   ä×Å ÓÈÅÍÙ, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÅ
 452   Á×ÔÏÍÁÔÎÙÍ ×ÙÒÁÖÅÎÉÑÍ $s', s'' \in \AExp_{\Sigma,T}$
 453   \tING{\todo{[ÒÅÌÑÃÉÏÎÎÏ?]} ÜË×É×ÁÌÅÎÔÎÙ}, ÅÓÌÉ:
 454   \begin{equation}
 455     \label{eq:sch-equiv}
 456     \REL_{\Sigma,T} \models
 457     s' = s''.
 458   \end{equation}
 459 \end{definition}
 460
 461 \paragraph{ïÂÙÞÎÏÅ ÏÐÒÅÄÅÌÅÎÉÅ ÓÅÍÁÎÔÉËÉ.}
 462 \begin{definition}
 463   ðÕÓÔØ Ä×ÕÍ ÓÈÅÍÁÍ ÎÁÄ~$\Sigma, T$ ÓÏÏÔ×ÅÔÓÔ×ÕÀÔ Á×ÔÏÍÁÔÎÙÅ ×ÙÒÁÖÅÎÉÑ
 464   $s', s'' \in \AExp_{\Sigma,T}$.
 465   üÔÉ Ä×Å ÓÈÅÍÙ \tING{ÜË×É×ÁÌÅÎÔÎÙ ÎÁ ÛËÁÌÅ ëÒÉÐËÅ}~$\kf F$ ÎÁÄ~$\Sigma, T$, ÅÓÌÉ:
 466 \begin{equation}
 467   \label{eq:sch-equiv-on-kf}
 468   \relReg_{\kf F}' \models
 469   \Start \cdot s' = \Start \cdot s''.
 470 \end{equation}
 471 \end{definition}
 472 \todo{[$\relReg_{\kf F}'$\T ÓÏ $\Start$ × ÎÁÞÁÌÅ.]}
 473 üË×É×ÁÌÅÎÔÎÏÓÔØ ×ÏÏÂÝÅ\T ÜË×É×ÁÌÅÎÔÎÏÓÔØ ÎÁ ÌÀÂÏÊ ÛËÁÌÅ ëÒÉÐËÅ:
 474 \begin{definition}
 475   ä×Å ÓÈÅÍÙ, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÅ
 476   Á×ÔÏÍÁÔÎÙÍ ×ÙÒÁÖÅÎÉÑÍ $s', s'' \in \AExp_{\Sigma,T}$
 477   \tING{ÜË×É×ÁÌÅÎÔÎÙ × ÔÒÁÄÉÃÉÏÎÎÏÍ ÓÍÙÓÌÅ}, ÅÓÌÉ:
 478   \begin{equation}
 479     \label{eq:sch-equiv-trad}
 480     \RELT' \models
 481     \Start \cdot s' = \Start \cdot s''.
 482   \end{equation}
 483 \end{definition}
 484 \todo{[$\REL'$\T ÓÏ $\Start$ × ÎÁÞÁÌÅ.]}
 485 éÎÏÇÄÁ ÄÌÑ ÏÐÒÅÄÅÌÅÎÉÑ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ ÓÈÅÍ ÐÒÉ×ÌÅËÁÀÔ ÌÉÛØ <<ÍÏÄÅÌÉ,
 486 ÏÓÎÏ×ÁÎÎÙÅ  ÎÁ Ó×ÏÂÏÄÎÙÈ ÍÏÎÏÉÄÁÈ>>, ÎÏ ÏÔ ÜÔÏÇÏ ÏÐÒÅÄÅÌÅÎÉÅ ÎÅ ÍÅÎÑÅÔÓÑ:
 487 \begin{proposition}
 488 $$
 489 \eqref{eq:sch-equiv-trad} \iff
 490 \SIMPLE_{\Sigma,T} \models \Start \cdot s' = \Start \cdot s''.
 491 $$
 492 \end{proposition}
 493 \begin{proof}
 494   óÌÅÄÕÅÔ ÉÚ \todo{[???]}.
 495 \end{proof}
 496 \begin{proposition}
 497   $$
 498   \RELT' \models \Start \cdot s = \Start \cdot t
 499   \iff
 500   \RELT \models s = t.
 501   $$
 502 \end{proposition}
 503 ôÁË ÞÔÏ ÐÏËÁÚÁÎÁ ÜË×É×ÁÌÅÎÔÎÏÓÔØ <<ÔÒÁÄÉÃÉÏÎÎÏÇÏ>>
 504 ÏÐÒÅÄÅÌÅÎÉÑ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ~\eqref{eq:sch-equiv-trad} ÏÓÎÏ×ÎÏÍÕ~\eqref{eq:sch-equiv}.
 505
 506 \subsubsection{÷ÏÐÒÏÓÙ}
 507 \label{sec:free-withTests-ndet-rexpr-Qs}
 508
 509 ÷ÏÐÒÏÓÙ ÔÅ ÖÅ, ÞÔÏ É × òÁÚÄÅÌÅ~\ref{sec:free-plain-ndet-rexpr-Qs}.
 510
 511 \begin{enumerate}
 512 \item
 513 ïÔÌÉÞÁÀÔÓÑ ÌÉ ××ÅÄ£ÎÎÙÅ ÐÏÄËÌÁÓÓÙ \KAT (Ó ÔÏÞÎÏÓÔØÀ ÄÏ
 514 ÉÚÏÍÏÒÆÉÚÍÏ× ÁÌÇÅÂÒ)? ëÁË ÏÎÉ Ó×ÑÚÁÎÙ Ó ÁÎÁÌÏÇÁÍÉ ÂÅÚ ÔÅÓÔÏ×?
 515
 516 äÌÑ ËÌÁÓÓÏ× ÏÞÅ×ÉÄÎÙ ÔÁËÉÅ ×ÌÏÖÅÎÉÑ:
 517 \begin{gather}
 518   \label{eq:KA-classes-inclu-simple}
 519   \RELT \subseteq \RKAT \subseteq \KATc \subseteq \KAT\\
 520   \TRACET \subseteq \KAc\\
 521   \Reg_{\Sigma} \in \KAc
 522 \end{gather}
 523 \todo{[çÄÅ $\trReg_{\kf F}$, $\relReg_{\kf F}$?]}
 524 \begin{align}
 525   \label{eq:KAT-KA-inclu-simple}
 526   \KAT &\subseteq \KA,
 527   \\
 528   \KATc &\subseteq \KAc,
 529   \\
 530   \RKAT &\subseteq \RKA.
 531 \end{align}
 532
 533 õÞÅÓÔØ ÓÐÅÃÉÆÉÞÅÓËÉÅ ËÌÁÓÓÙ ÍÏÄÅÌÅÊ, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÅ ÏÐÒÅÄÅÌÅÎÉÑÍ
 534 ÓÅÍÁÎÔÉËÉ ÐÒÏÇÒÁÍÍ, ÜË×É×ÁÌÅÎÔÎÏÓÔÉ ÐÒÏÇÒÁÍÍ, ÎÁÐÒÉÍÅÒ, \todo{[??]}.
 535
 536 \item
 537 ïÔÌÉÞÁÀÔÓÑ ÌÉ ÔÅÏÒÉÉ \todo{[× ÑÚÙËÅ 1\dÇÏ ÐÏÒÑÄËÁ]} ××ÅÄ£ÎÎÙÈ
 538 ÐÏÄËÌÁÓÓÏ× \KAT?
 539 ëÁË ÏÎÉ Ó×ÑÚÁÎÙ Ó ÔÅÏÒÉÑÍÉ ÐÏÄËÌÁÓÓÏ× \KA?
 540
 541 \item
 542 ïÔÌÉÞÁÀÔÓÑ ÌÉ ÜË×ÁÃÉÏÎÁÌØÎÙÅ ÔÅÏÒÉÉ ××ÅÄ£ÎÎÙÈ ÐÏÄËÌÁÓÓÏ× \KAT?
 543
 544 \item óÕÝÅÓÔ×ÕÀÔ ÌÉ \todo{Ó×ÏÂÏÄÎÙÅ ÍÏÄÅÌÉ [ÔÁË?]} ÄÌÑ ÜÔÉÈ ËÌÁÓÓÏ×?
 545
 546
 547 \item òÁÚÒÅÛÉÍÙ ÌÉ ÜË×ÁÃÉÏÎÁÌØÎÙÅ ÔÅÏÒÉÉ ÜÔÉÈ ËÌÁÓÓÏ×?
 548
 549 é Ó ËÁËÉÍÉ ÄÒÕÇÉÍÉ ÐÒÏÂÌÅÍÁÍÉ Ó×ÑÚÁÎÁ ÐÒÏÂÌÅÍÁ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ?
 550 \todo{[ÄÒÕÇÉÅ ÐÒÏÂÌÅÍÙ]}
 551
 552
 553 \item íÅÓÔÏ ÐÒÏÂÌÅÍÙ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ × ÓÌÏÖÎÏÓÔÎÏÊ ÉÅÒÁÒÈÉÉ.
 554
 555
 556 \item ëÁËÉÅ ÍÏÖÎÏ ÎÁÚ×ÁÔØ ÉÎÔÅÒÅÓÎÙÅ ÏÓÏÂÙÅ ÐÏÄÓÌÕÞÁÉ?
 557
 558 \end{enumerate}
 559
 560
 561 \subsection{ïÔ×ÅÔÙ}
 562 \label{sec:free-withTests-Theory}
 563
 564 \paragraph{÷ËÌÀÞÅÎÉÑ ÐÏÄËÌÁÓÓÏ× \KAT É \KA.}
 565
 566 \subparagraph{ó×ÑÚÉ ÍÅÖÄÕ \KAT É \KA.}
 567 \begin{remark}\label{rem:KA-primitve-KAT}
 568 ìÀÂÁÑ \KAT Ñ×ÌÑÅÔÓÑ É \KA ÐÏ ÏÐÒÅÄÅÌÅÎÉÀ, *\dÎÅÐÒÅÒÙ×ÎÁÑ \KAT\T
 569 *\dÎÅÐÒÅÒÙ×ÎÏÊ \KA ÐÏ ÏÐÒÅÄÅÌÅÎÉÀ, É ÒÅÌÑÃÉÏÎÎÁÑ \KAT\T
 570 ÒÅÌÑÃÉÏÎÎÏÊ \KA (ÏÐÒÅÄÅÌÅÎÉÅ ÒÅÌÑÃÉÏÎÎÏÊ \KAT ÐÏ ÓÒÁ×ÎÅÎÉÀ Ó
 571 ÏÐÒÅÄÅÌÅÎÉÅÍ ÒÅÌÑÃÉÏÎÎÏÊ \KA ÎÁËÌÁÄÙ×ÁÅÔ ÄÏÐÏÌÎÉÔÅÌØÎÙÅ ÏÇÒÁÎÉÞÅÎÉÑ ÎÁ
 572 ÏÔÎÏÛÅÎÉÑ, É ÜÔÏ ÎÅ ÍÅÛÁÅÔ ÅÊ ÂÙÔØ ÒÅÌÑÃÉÏÎÎÏÊ \KA).
 573
 574 <<Ñ×ÌÑÅÔÓÑ>>
 575 ÚÎÁÞÉÔ <<\KAT $\ka T = \Stru{K, B; +, \cdot, ^*, \nP, 0,  1}$
 576 ÉÎÄÕÃÉÒÕÅÔ \KA $\ka K = \Stru{K; +, \cdot, ^*,  0,  1}$ Ó ÕËÁÚÁÎÎÙÍÉ
 577 Ó×ÏÊÓÔ×ÁÍÉ.
 578
 579 ïÂÒÁÔÎÏ. ìÀÂÁÑ \KA $\ka K = \Stru{K; +, \cdot, ^*,  0,  1}$ ÉÎÄÕÃÉÒÕÅÔ
 580 \KAT $\ka T = \Stru{K, B; +, \cdot, ^*, \nP, 0,  1}$ Ó ÐÒÏÓÔÅÊÛÅÊ
 581 ÂÕÌÅ×ÏÊ ÐÏÄÁÌÇÅÂÒÏÊ ÔÅÓÔÏ× ÎÁ $B = \{ 0, 1 \}$. *\dÎÅÐÒÅÒÙ×ÎÏÓÔØ É
 582 ÒÅÌÑÃÉÏÎÎÏÓÔØ ÐÒÉ ÜÔÏÍ ÓÏÈÒÁÎÑÀÔÓÑ.
 583 \end{remark}
 584
 585 \begin{remark}[\cite{KAT-commutativity}]
 586 ÷ ÔÏ ÖÅ ×ÒÅÍÑ ÐÏÐÙÔËÁ ÐÏÓÔÒÏÉÔØ ÐÏ $\ka K$ ÂÏÌÅÅ ÓÌÏÖÎÕÀ \KAT ÄÒÕÇÉÍ
 587 ÅÓÔÅÓÔ×ÅÎÎÙÍ ÓÐÏÓÏÂÏÍ ÎÅ ×ÓÅÇÄÁ ÐÒÉ×ÅÄ£Ô Ë ÕÓÐÅÈÕ:
 588 ÐÏÌÏÖÉÍ $B = \{ x \in K \mid x \leq 1 \}$.
 589 åÓÌÉ $\ka K$ ÒÅÌÑÃÉÏÎÎÁÑ,
 590 ÔÏ ÂÕÄÅÔ ÓÕÝÅÓÔ×Ï×ÁÔØ ÒÅÌÑÃÉÏÎÎÁÑ \KAT $\ka T$,
 591 ÓÏÄÅÒÖÁÝÁÑ $\Stru{K, B; +, \cdot, ^*, \nP, 0,  1}$. äÌÑ $(\min,
 592 +)$\DÁÌÇÅÂÒÙ ëÌÉÎÉ ÔÁË ÎÅ ÐÏÌÕÞÉÔÓÑ.
 593 \end{remark}
 594
 595 \paragraph{ôÅÏÒÉÉ ÐÏÄËÌÁÓÓÏ× \KAT É \KA.}
 596
 597 \subparagraph{ó×ÑÚÉ ÍÅÖÄÕ \KAT É \KA.}
 598 åÓÌÉ $\phi$\T ÆÏÒÍÕÌÁ × ÑÚÙËÅ \KA 1\dÇÏ ÐÏÒÑÄËÁ, ÔÏ
 599 \begin{align}
 600   \label{eq:KAT-KA-theories}
 601   \KA \models \phi &\iff \KAT \models \phi
 602   &
 603   \KAc \models \phi &\iff \KATc \models \phi
 604   &
 605   \RKA \models \phi &\iff \RKAT \models \phi.
 606 \end{align}
 607 üÔÏ ÓÌÅÄÕÅÔ ÉÚ úÁÍÅÞÁÎÉÑ~\ref{rem:KA-primitve-KAT}.
 608
 609 %%% Local Variables:
 610 %%% mode: latex
 611 %%% TeX-master: "main"
 612 %%% End: