general.tex

   1 \section{ûËÁÌÙ ëÒÉÐËÅ É ÔÒÁÓÓÙ}\label{sec:kframes}
   2
   3
   4 \subsection{ûËÁÌÙ ëÒÉÐËÅ ÎÁÄ~$\Sigma$}
   5 \label{sec:kframes-sigma}
   6
   7 ðÕÓÔØ $\Sigma$ ËÏÎÅÞÎÙÊ ÁÌÆÁ×ÉÔ (ÂÕÄÅÍ ÇÏ×ÏÒÉÔØ, \tNDNo{ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ×}).
   8
   9 \begin{definition}\label{def:kframe-op}
  10   \tING{ûËÁÌÁ ëÒÉÐËÅ} ÎÁÄ~$\Sigma$\T ÜÔÏ ÓÔÒÕËÔÕÒÁ $(Q, m)$, ÇÄÅ $Q$\T
  11   ÍÎÏÖÅÓÔ×Ï ÓÏÓÔÏÑÎÉÊ, Á
  12   \begin{align*}
  13     m\colon &\Sigma \to 2^{Q \times Q}.
  14   \end{align*}
  15 \end{definition}
  16
  17 \begin{application}
  18 åÓÌÉ ÍÙ ÉÍÅÅÍ ÄÅÌÏ Ó ÐÒÏÇÒÁÍÍÁÍÉ, ÓÏÓÔÁ×ÌÅÎÎÙÍÉ ÉÚ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ×,
  19 ÔÏ <<ÏÐÉÓÁÎÉÅ>> ÓÅÍÁÎÔÉËÉ ÐÒÏÇÒÁÍÍ ÍÙ ÍÏÖÅÍ ÏÓÎÏ×Ù×ÁÔØ ÎÁ <<ÏÐÉÓÁÎÉÉ>>
  20 ÓÅÍÁÎÔÉËÉ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ× É ÏÂÝÉÈ ÐÒÁ×ÉÌÁÈ ÓÅÍÁÎÔÉÞÅÓËÏÊ
  21 ËÏÍÐÏÚÉÃÉÉ. óÅÍÁÎÔÉËÕ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ×\T ÏÓÏÂÅÎÎÏÓÔÉ ÉÈ ÐÏ×ÅÄÅÎÉÑ\T
  22 ÍÙ ÍÏÖÅÍ ÐÒÅÄÓÔÁ×ÉÔØ × ×ÉÄÅ ÛËÁÌÙ ëÒÉÐËÅ. ($m$ ÐÏËÁÚÙ×ÁÅÔ ËÁË ËÁÖÄÙÊ
  23 ÏÐÅÒÁÔÏÒ ÍÏÖÅÔ ÉÚÍÅÎÉÔØ ÔÅËÕÝÅÅ <<ÓÏÓÔÏÑÎÉÅ ÐÁÍÑÔÉ ×ÙÞÉÓÌÉÔÅÌØÎÏÊ
  24 ÍÁÛÉÎÙ>>\T ÜÌÅÍÅÎÔ ÍÎÏÖÅÓÔ×Á~$Q$.)
  25 \end{application}
  26
  27
  28 \subsubsection{ïÐÅÒÁÃÉÉ ÎÁÄ ÛËÁÌÁÍÉ ëÒÉÐËÅ}
  29
  30 âÏÌÅÅ ÓÌÏÖÎÕÀ ÛËÁÌÕ ëÒÉÐËÅ ÍÏÖÎÏ ÏÂÒÁÚÏ×ÁÔØ ÉÚ ÂÏÌÅÅ ÐÒÏÓÔÙÈ, ÐÒÉÍÅÎÉ×
  31 Ë ÎÉÍ, ÎÁÐÒÉÍÅÒ, ÏÄÎÕ ÉÚ ÓÌÅÄÕÀÝÉÈ ÏÐÅÒÁÃÉÊ.
  32
  33 \begin{definition}
  34   ðÕÓÔØ $\Sigma_1$ É $\Sigma_2$ ËÏÎÅÞÎÙÅ ÁÌÆÁ×ÉÔÙ, $\Sigma_1 \cap
  35   \Sigma_2 = \emptyset$. \tING{ðÒÑÍÙÍ ÐÒÏÉÚ×ÅÄÅÎÉÅÍ} ÛËÁÌÙ ëÒÉÐËÅ $\kf
  36   F_1 = (Q_1, m_1)$ ÎÁÄ~$\Sigma_1$ É ÛËÁÌÙ ëÒÉÐËÅ $\kf F_2 = (Q_2,
  37   m_2)$ ÎÁÄ~$\Sigma_2$ ÎÁÚÙ×ÁÅÔÓÑ ÛËÁÌÁ ëÒÉÐËÅ $(Q_1 \times Q_2, m)$,
  38   ÇÄÅ
  39   \begin{align}
  40     \label{eq:kf-product-a1}
  41     m(a_1) &\eqdef \{ ( (u_1, u_2), (v_1, v_2) ) \mid
  42     (u_1, v_1) \in m_1(a_1),
  43     u_2 = v_2
  44     \}
  45     &&\text{ÄÌÑ $a_1 \in \Sigma_1$}\\
  46     \label{eq:kf-product-a2}
  47     m(a_2) &\eqdef \{ ( (u_1, u_2), (v_1, v_2) ) \mid
  48     u_1 = v_1,
  49     (u_2, v_2) \in m_2(a_2)
  50     \}
  51     &&\text{ÄÌÑ $a_2 \in \Sigma_2$.}
  52   \end{align}
  53
  54   ïÂÏÚÎÁÞÁÅÔÓÑ $\kfProduct(\kf F_1, \kf F_2)$ ÉÌÉ $\kf F_1 \times \kf F_2$.
  55 \end{definition}
  56 \begin{example}
  57 \todo{[]}
  58 \end{example}
  59
  60 \begin{definition}
  61   ðÕÓÔØ $\kf F_1 = (Q_1, m_1)$ É $\kf F_2 = (Q_2, m_2)$\T ÛËÁÌÙ ëÒÉÐËÅ
  62   ÎÁÄ~$\Sigma$.
  63   %, É $u \in Q_1$, $v \in Q_2$.
  64   \tING{ïÂßÅÄÉÎÅÎÉÅÍ ÛËÁÌ ëÒÉÐËÅ $\kf F_1$ É $\kf F_2$} ÎÁÚÏ×£Í ÎÏ×ÕÀ
  65   ÛËÁÌÕ ëÒÉÐËÅ $(Q_1 \cup Q_2, m)$, ÇÄÅ $m$ ÒÁ×ÎÁ $m_1$ ÎÁ
  66   ÜÌÅÍÅÎÔÁÈ~$Q_1$ É $m_2$ ÎÁ ÜÌÅÍÅÎÔÁÈ~$Q_2$.
  67
  68   ïÂÏÚÎÁÞÁÅÔÓÑ $\kfUnion(\kf F_1, \kf F_2)$ ÉÌÉ
  69   $\kf F_1 \cup \kf F_2$.
  70 \end{definition}
  71 \begin{example}
  72   \todo{[]}
  73 \end{example}
  74
  75 \begin{definition}
  76   ðÕÓÔØ $\kf F = (Q, m)$ ÛËÁÌÁ ëÒÉÐËÅ ÎÁÄ~$\Sigma$,
  77   É $u,v \in Q$.
  78   òÅÚÕÌØÔÁÔÏÍ ÏÐÅÒÁÃÉÉ \tING{ÏÔÏÖÄÅÓÔ×ÌÅÎÉÑ ÓÏÓÔÏÑÎÉÊ} $u$ É $v$ ×
  79   ÛËÁÌÅ ëÒÉÐËÅ $\kf F$
  80   ÂÕÄÅÔ ÎÏ×ÁÑ ÛËÁÌÁ ëÒÉÐËÅ $\kf F'$ ÎÁÄ~$\Sigma$, ËÏÔÏÒÁÑ ÐÏÌÕÞÁÅÔÓÑ
  81   \todo{[ÐÏÎÑÔÎÏ ËÁË]}
  82
  83   ïÂÏÚÎÁÞÁÅÔÓÑ $\kfLink(\kf F, u, v)$.
  84 \end{definition}
  85 \begin{example}
  86   \todo{[]}
  87 \end{example}
  88
  89
  90 \subsubsection{ó×ÏÊÓÔ×Á ÛËÁÌ ëÒÉÐËÅ}
  91
  92 îÁ ÓÏÓÔÏÑÎÉÑÈ ÛËÁÌÙ ëÒÉÐËÅ ÍÙ ××ÏÄÉÍ ÏÔÎÏÛÅÎÉÅ ÄÏÓÔÉÖÉÍÏÓÔÉ $\coLe$,
  93 ÐÏÎÑÔÉÅ ÐÏÄÛËÁÌÙ $\kf F|_u$, Ó×ÑÚÁÎÎÏÊ Ó ÎÅËÏÔÏÒÙÍ ÓÏÓÔÏÑÎÉÅÍ $u$
  94 (×ËÌÀÞÁÅÔ ×ÓÅ ÄÏÓÔÉÖÉÍÙÅ ÉÚ $u$ ÓÏÓÔÏÑÎÉÑ),
  95 ÏÔÒÅÚËÁ $[u,v]$ × ÛËÁÌÅ, Ó ËÏÎÃÁÍÉ\T ÐÁÒÏÊ
  96 ÓÏÓÔÏÑÎÉÊ $u,v$, ÇÄÅ $v$ ÄÏÓÔÉÖÉÍÏ ÉÚ $u$.
  97
  98
  99 \begin{definition}
 100   ûËÁÌÁ ëÒÉÐËÅ $\kf F = (Q, m)$ \tING{ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÁÑ}, ÅÓÌÉ ×Ï
 101   ×ÓÑËÏÍ ÍÎÏÖÅÓÔ×Å $\{ v \mid (u,v) \in m(a) \}$ ÄÌÑ ËÁÖÄÏÇÏ $a \in
 102   \Sigma, u \in Q$ ÎÅ ÂÏÌØÛÅ ÏÄÎÏÇÏ ÜÌÅÍÅÎÔÁ. âÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ ÅÇÏ
 103   $m(a, u)$.
 104 \end{definition}
 105
 106
 107 \begin{definition}
 108   ûËÁÌÁ ëÒÉÐËÅ $\kf F = (Q, m)$ \tING{ÓÁÍÏ×ÌÏÖÉÍÁÑ}, ÅÓÌÉ ÄÌÑ ×ÓÑËÉÈ
 109   Ä×ÕÈ ÓÏÓÔÏÑÎÉÊ $u,v \in Q$, ÔÁËÉÈ ÞÔÏ $v$ \tNDNo{ÄÏÓÔÉÖÉÍÏ} ÉÚ $u$,
 110   ÓÕÝÅÓÔ×ÕÅÔ ÇÏÍÏÍÏÒÆÉÚÍ $\kf F$ × ÓÅÂÑ,
 111   ÐÅÒÅ×ÏÄÑÝÉÊ $u$ × $v$.
 112 \end{definition}
 113
 114 \begin{definition}
 115   ûËÁÌÁ ëÒÉÐËÅ $\kf F = (Q, m)$ \tING{ÏÄÎÏÒÏÄÎÁÑ} (ÓÁÍÏÎÁÌÏÖÉÍÁÑ),
 116   ÅÓÌÉ ÄÌÑ ×ÓÑËÉÈ
 117   Ä×ÕÈ ÓÏÓÔÏÑÎÉÊ $u,v \in Q$ ÓÕÝÅÓÔ×ÕÅÔ ÉÚÏÍÏÒÆÉÚÍ ÍÅÖÄÕ $\kf F|_u$ É
 118   $\kf F|_v$.
 119 \end{definition}
 120
 121
 122 \subsubsection{ûËÁÌÙ ëÒÉÐËÅ, ÏÓÎÏ×ÁÎÎÙÅ ÎÁ ÍÏÎÏÉÄÁÈ}
 123
 124 ðÕÓÔØ $\mo M = (Q_{\mo M}; \cdot, 1_{\mo M})$\T
 125 ÎÅËÏÔÏÒÙÊ ÍÏÎÏÉÄ Ó ÐÏÒÏÖÄÁÀÝÉÍÉ ÜÌÅÍÅÎÔÁÍÉ $\Sigma$.
 126
 127 \begin{definition}
 128 âÕÄÅÍ ÇÏ×ÏÒÉÔØ, ÞÔÏ \tING{× ÏÓÎÏ×Å  ÛËÁÌÙ ëÒÉÐËÅ $\kf F$
 129 ÎÁÄ~$\Sigma$  ÌÅÖÉÔ ÍÏÎÏÉÄ}~$\mo M$, ÅÓÌÉ  $\kf F = (Q_{\mo M}, m)$ É
 130 \begin{align}
 131   m(a) = \{ (w, wa) \mid w \in Q_{\mo M} \}
 132   &\text{ ÄÌÑ $a \in \Sigma$.}
 133 \end{align}
 134 ôÁËÕÀ ÛËÁÌÕ ÏÂÏÚÎÁÞÉÍ $\kf F_{\mo M}$.
 135 \end{definition}
 136 \begin{remark}
 137 ûËÁÌÁ ëÒÉÐËÅ ÎÁÄ~$\Sigma$
 138 <<ÉÍÅÅÔ × ÏÓÎÏ×ÁÎÉÉ>>
 139 ÎÅËÏÔÏÒÙÊ ÍÏÎÏÉÄ Ó ÐÏÒÏÖÄÁÀÝÉÍÉ ÜÌÅÍÅÎÔÁÍÉ~$\Sigma$,
 140 \IFF
 141 ÏÎÁ
 142 ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÁÑ É ÓÁÍÏ×ÌÏÖÉÍÁÑ.
 143 \end{remark}
 144 \begin{remark}
 145 ûËÁÌÁ ëÒÉÐËÅ ÎÁÄ~$\Sigma$
 146 <<ÉÍÅÅÔ × ÏÓÎÏ×ÁÎÉÉ>>
 147 ÎÅËÏÔÏÒÙÊ ÍÏÎÏÉÄ Ó ÌÅ×ÙÍ ÓÏËÒÁÝÅÎÉÅÍ Ó ÐÏÒÏÖÄÁÀÝÉÍÉ ÜÌÅÍÅÎÔÁÍÉ~$\Sigma$,
 148 \IFF
 149 ÏÎÁ
 150 ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÁÑ É ÏÄÎÏÒÏÄÎÁÑ.
 151 \end{remark}
 152
 153 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 154 \subsection{ûËÁÌÙ ëÒÉÐËÅ ÎÁÄ~$\Sigma, T$}
 155 \label{sec:kframes-sigma-t}
 156
 157 ðÕÓÔØ $\Sigma$ É $T$ ËÏÎÅÞÎÙÅ ÁÌÆÁ×ÉÔÙ (ÂÕÄÅÍ ÇÏ×ÏÒÉÔØ,
 158 \tNDNo{ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ×} É \tNDNo{ÂÁÚÏ×ÙÈ ÔÅÓÔÏ×}).
 159
 160 \begin{definition}\label{def:kframe-op-tests}
 161   \tING{ûËÁÌÁ ëÒÉÐËÅ} ÎÁÄ~$\Sigma, T$\T ÜÔÏ ÓÔÒÕËÔÕÒÁ $(Q, m)$, ÇÄÅ $Q$\T
 162   ÍÎÏÖÅÓÔ×Ï ÓÏÓÔÏÑÎÉÊ, Á
 163   \begin{align*}
 164     m\colon &\Sigma \to 2^{Q \times Q}
 165     &
 166     m\colon &T \to 2^{Q}.
 167   \end{align*}
 168 \end{definition}
 169
 170 \todo{[× ÄÒÕÇÏÊ ÔÅÒÍÉÎÏÌÏÇÉÉ -- ÜÔÏ ÓËÏÒÅÅ ÍÏÄÅÌØ ëÒÉÐËÅ, ÐÏ ÓÒÁ×ÎÅÎÉÀ
 171   ÓÏ ÛËÁÌÏÊ ëÒÉÐËÅ ÔÏÌØËÏ ÎÁÄ $\Sigma$]}
 172
 173 \begin{remark}
 174 ÷ÓÑËÁÑ ÛËÁÌÁ ëÒÉÐËÅ $\kf F$ ÎÁÄ~$\Sigma, T$ ÉÎÄÕÃÉÒÕÅÔ ÛËÁÌÕ ëÒÉÐËÅ
 175 $\kf F'$ ÎÁÄ~$\Sigma$ (ÅÓÔÅÓÔ×ÅÎÎÙÍ ÏÂÒÁÚÏÍ, ÏÔÂÒÁÓÙ×ÁÎÉÅÍ ÌÉÛÎÅÊ ÓÔÒÕËÔÕÒÙ).
 176 \end{remark}
 177
 178 \begin{application}
 179 ûËÁÌÁ ëÒÉÐËÅ ÔÁËÏÇÏ ×ÉÄÁ ÍÏÖÅÔ ÓÌÕÖÉÔØ ÐÒÅÄÓÔÁ×ÌÅÎÉÅÍ ÓÅÍÁÎÔÉËÉ
 180 ÂÁÚÏ×ÙÈ ÜÌÅÍÅÎÔÏ× ÐÒÏÇÒÁÍÍ,
 181 ÅÓÌÉ ÍÙ ÉÍÅÅÍ ÄÅÌÏ Ó ÐÒÏÇÒÁÍÍÁÍÉ, ÓÏÓÔÁ×ÌÅÎÎÙÍÉ ÕÖÅ ÉÚ ÜÌÅÍÅÎÔÏ× Ä×ÕÈ
 182 ÓÏÒÔÏ×\T ÏÐÅÒÁÔÏÒÏ× É ÔÅÓÔÏ×.
 183 \end{application}
 184
 185 \subsubsection{ïÐÅÒÁÃÉÉ ÎÁÄ ÛËÁÌÁÍÉ ëÒÉÐËÅ}
 186
 187 ïÐÅÒÁÃÉÉ \tDJust{ÐÒÑÍÏÇÏ ÐÒÏÉÚ×ÅÄÅÎÉÑ}, \tDJust{ÏÂßÅÄÉÎÅÎÉÑ} É
 188 \tDJust{ÏÔÏÖÄÅÓÔ×ÌÅÎÉÑ ÓÏÓÔÏÑÎÉÊ}
 189 ÎÁÄ ÛËÁÌÁÍÉ ëÒÉÐËÅ ÎÁÄ ÁÌÆÁ×ÉÔÁÍÉ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ× É ÔÅÓÔÏ×
 190 ÏÐÒÅÄÅÌÑÀÔÓÑ ÔÁË ÖÅ, ËÁË É ÄÌÑ ÛËÁÌ ëÒÉÐËÅ ÐÒÏÓÔÏ ÎÁÄ ÁÌÆÁ×ÉÔÏÍ
 191 ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ×, ÐÒÉ ÜÔÏÍ Ë ÏÐÒÅÄÅÌÅÎÉÑÍ~\eqref{eq:kf-product-a1}
 192 É~\eqref{eq:kf-product-a2} ÄÌÑ ÐÒÑÍÏÇÏ ÐÒÏÉÚ×ÅÄÅÎÉÑ ÄÏÂÁ×ÌÑÀÔÓÑ ÔÁËÉÅ:
 193 \begin{align}
 194   \label{eq:kf-product-p1}
 195   m(p_1) &\eqdef \{ (u_1, u_2) \mid
 196   u_1 \in m_1(p_1)
 197   \}
 198   &&\text{ÄÌÑ $p_1 \in T_1$}\\
 199   \label{eq:kf-product-p2}
 200   m(p_2) &\eqdef \{ (u_1, u_2) \mid
 201   u_2 \in m_2(p_2)
 202   \}
 203   &&\text{ÄÌÑ $p_2 \in T_2$.}
 204 \end{align}
 205
 206 \subsubsection{ûËÁÌÙ ëÒÉÐËÅ, ÏÓÎÏ×ÁÎÎÙÅ ÎÁ ÍÏÎÏÉÄÁÈ}
 207
 208 \begin{definition}
 209 âÕÄÅÍ ÇÏ×ÏÒÉÔØ, ÞÔÏ \tING{× ÏÓÎÏ×Å  ÛËÁÌÙ ëÒÉÐËÅ $\kf F$
 210 ÎÁÄ~$\Sigma,T$  ÌÅÖÉÔ ÍÏÎÏÉÄ}~$\mo M$,
 211 ÅÓÌÉ ÜÔÏ ÔÁË ÄÌÑ ÉÎÄÕÃÉÒÏ×ÁÎÎÏÊ~$\kf F$
 212 ÛËÁÌÙ ëÒÉÐËÅ ÎÁÄ~$\Sigma$,
 213 \te ÅÓÌÉ  $\kf F = (Q_{\mo M}, m)$ É
 214 \begin{align}
 215   m(a) = \{ (w, wa) \mid w \in Q_{\mo M} \}
 216   &\text{ ÄÌÑ $a \in \Sigma$,}
 217 \end{align}
 218 Á ÎÁ $T$ $m\colon T \to 2^Q$\T ÐÒÏÉÚ×ÏÌØÎÏÅ ÏÔÏÂÒÁÖÅÎÉÅ.
 219
 220 ôÁËÕÀ ÛËÁÌÕ ÎÁÍ ÕÄÏÂÎÏ ÂÕÄÅÔ ÏÂÏÚÎÁÞÁÔØ $\kf F_{\mo M}(\xi)$, ÇÄÅ
 221 $\xi\colon Q_{\mo M} \times T \to \{ \False, \True \}$ ÏÐÒÅÄÅÌÑÅÔ $m$ ÎÁ $T$:
 222 $$
 223 m(p) = \{ u \mid \xi(u,p) = \True \}.
 224 $$
 225 (ïÞÅ×ÉÄÎÏ, ÓÏÏÔ×ÅÔÓÔ×ÉÅ $m \mapsto \xi$ ×ÚÁÉÍÎÏ ÏÄÎÏÚÎÁÞÎÏÅ.)
 226
 227 ôÁËÁÑ $\xi$ ÎÁÚÙ×ÁÅÔÓÑ \tING{ÏÃÅÎËÏÊ} ÂÁÚÏ×ÙÈ ÔÅÓÔÏ× $T$ ÎÁ $Q_{\mo
 228   M}$.
 229 \end{definition}
 230
 231
 232 \subsection{ôÒÁÓÓÙ}
 233 \label{sec:traces}
 234
 235 \begin{definition}\label{def:trace}
 236   ðÕÓÔØ $\kf F = \Stru{Q_{\kf F}, m_{\kf F}}$ ÛËÁÌÁ
 237   ëÒÉÐËÅ ÎÁÄ~$\Sigma$ (ÉÌÉ ÎÁÄ~$\Sigma, T$).
 238   \tING{ôÒÁÓÓÏÊ} ×~$\kf F$ ÎÁÚÙ×ÁÅÔÓÑ
 239   ËÏÎÅÞÎÁÑ ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÏÓÔØ~$\sigma$ ×ÉÄÁ:
 240   \begin{equation}
 241     \label{eq:trace}
 242     u_0 a_0 u_1 \dotsm u_{n-1} a_{n-1} u_n,
 243   \end{equation}
 244   ÇÄÅ $n \in \bbN \cup \{ 0 \}$ É
 245   \begin{align*}
 246     u_i &\in Q_{\kf F},
 247     &
 248     a_i &\in \Sigma,
 249     &
 250     \text{Á }
 251     (u_i, u_{i+1}) &\in m_{\kf F}(a_i) \text{ ÄÌÑ } 0 \leq i \leq n - 1.
 252   \end{align*}
 253
 254   \tING{íÎÏÖÅÓÔ×Ï ÔÒÁÓÓ × ÛËÁÌÅ ëÒÉÐËÅ}~$\kf F$ ÏÂÏÚÎÁÞÉÍ $\Trs(\kf F)$.
 255
 256   äÌÑ ÔÒÁÓÓÙ~$\sigma$ ×ÉÄÁ~\eqref{eq:trace}
 257   \tING{ÄÌÉÎÁ~$\Len{\sigma}$} ÒÁ×ÎÁ $n$,
 258   \begin{align*}
 259     \First(\sigma) &\eqdef u_0,
 260     \\
 261     \Last(\sigma) &\eqdef u_n,
 262     \\
 263     \Label(\sigma) &\eqdef
 264     \begin{cases}
 265       a_0 \dotsm a_{n-1}, &\\
 266       \eStr \text{ (ÐÕÓÔÁÑ ÓÔÒÏËÁ)}, &\text{ÅÓÌÉ } \Len{\sigma} = 0.
 267     \end{cases}
 268   \end{align*}
 269 \end{definition}
 270
 271 \section{íÏÄÅÌÉ É ÔÅÏÒÉÉ}
 272
 273 \todo{[ÐÅÒÅÎÅÓÔÉ ÏÂÏÚÎÁÞÅÎÉÑ $\models$ etc ÓÀÄÁ]}
 274
 275 \begin{definition}
 276   íÎÏÖÅÓÔ×Ï ÆÏÒÍÕÌ ×ÉÄÁ:
 277   \begin{equation}
 278     \label{eq:equa-formula}
 279     s = t,
 280   \end{equation}
 281   ÇÄÅ $s$ É $t$\T ÔÅÒÍÙ × ÎÅËÏÔÏÒÏÍ ÒÁÓÓÍÁÔÒÉ×ÁÅÍÏÍ ÑÚÙËÅ,
 282   ËÏÔÏÒÙÅ ×ÅÒÎÙ ÐÒÉ ÌÀÂÙÈ ÉÎÔÅÒÐÒÅÔÁÃÉÑÈ ÎÁ ÁÌÇÅÂÒÁÉÞÅÓËÉÈ ÓÔÒÕËÔÕÒÁÈ
 283   ËÌÁÓÓÁ~$\class C$\T ÜÔÏ
 284   \tING{ÜË×ÁÃÉÏÎÁÌØÎÁÑ ÔÅÏÒÉÑ} ËÌÁÓÓÁ~$\class C$.
 285
 286   ïÂÏÚÎÁÞÁÅÔÓÑ  $\EquaOf\class C$.
 287 \end{definition}
 288
 289 \begin{definition}[\cite{KA-proof-theory}]
 290   \tING{õÎÉ×ÅÒÓÁÌØÎÁÑ Horn\dÆÏÒÍÕÌÁ}\T ÜÔÏ ÆÏÒÍÕÌÁ ×ÉÄÁ
 291   \begin{equation}
 292     \label{eq:Horn-formula}
 293     s_1 = t_1 \wedge \dotsb \wedge s_k = t_k
 294     \implic s = t,
 295   \end{equation}
 296   ÇÄÅ $s_i$, $t_i$, $s$, $t$\T ÔÅÒÍÙ × ÎÅËÏÔÏÒÏÍ ÒÁÓÓÍÁÔÒÉ×ÁÅÍÏÍ ÑÚÙËÅ.
 297
 298   íÎÏÖÅÓÔ×Ï \tDJust{ÕÎÉ×ÅÒÓÁÌØÎÙÈ Horn-ÆÏÒÍÕÌ},
 299   ËÏÔÏÒÙÅ ×ÅÒÎÙ ÐÒÉ ÌÀÂÙÈ ÉÎÔÅÒÐÒÅÔÁÃÉÑÈ ÎÁ ÍÏÄÅÌÑÈ ÉÚ ËÌÁÓÓÁ $\class
 300   C$\T ÜÔÏ
 301   \tING{ÕÎÉ×ÅÒÓÁÌØÎÁÑ Horn-ÔÅÏÒÉÑ} ËÌÁÓÓÁ~$\class C$.
 302
 303   ïÂÏÚÎÁÞÁÅÔÓÑ $\HornOf\class C$.
 304
 305   íÙ ÂÕÄÅÍ ÐÏÚ×ÏÌÑÔØ ÓÅÂÅ ÚÁÐÉÓÙ×ÁÔØ ÕÎÉ×ÅÒÓÁÌØÎÙÅ Horn\dÆÏÒÍÕÌÙ ËÁË
 306   $E \implic s = t$, ÇÄÅ $E$\T ÜÔÏ ËÏÎÅÞÎÏÅ ÍÎÏÖÅÓÔ×Ï ÒÁ×ÅÎÓÔ× ×ÉÄÁ
 307   $s_i = t_i$, ÉÍÅÑ × ×ÉÄÕ ÕÎÉ×ÅÒÓÁÌØÎÕÀ Horn\dÆÏÒÍÕÌÕ:
 308   $$
 309   \bigwedge_{\psi \in E} \psi \implic s = t.
 310   $$
 311
 312   óÌÏ×Ï <<ÕÎÉ×ÅÒÓÁÌØÎÙÊ>> ÍÙ ÞÁÓÔÏ ÂÕÄÅÍ ÏÐÕÓËÁÔØ.
 313 \end{definition}
 314 \begin{remark}
 315   $\EquaOf\class C$\T ÜÔÏ ÓÕÖÅÎÉÅ $\HornOf\class C$ ÄÏ Horn-ÆÏÒÍÕÌ Ó $E = \emptyset$.
 316 \end{remark}
 317
 318 ÷ ÐÅÒ×ÕÀ ÏÞÅÒÅÄØ ÍÙ ÂÕÄÅÍ ÉÓÐÏÌØÚÏ×ÁÔØ (ÓÍ.~òÁÚÄÅÌ~\ref{sec:Equa})
 319 ÜÔÉ ÐÏÎÑÔÉÑ ÐÏ ÏÔÎÏÛÅÎÉÀ Ë ÆÏÒÍÕÌÁÍ, ÇÄÅ ÔÅÒÍÁÍÉ Ñ×ÌÑÀÔÓÑ
 320 \tND{ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ}{def:rexp} (ÉÌÉ \tND{Á×ÔÏÍÁÔÎÙÅ
 321   ×ÙÒÁÖÅÎÉÑ}{def:aexp}), Á ÍÏÄÅÌÑÍÉ ÓÌÕÖÁÔ \tND{ÁÌÇÅÂÒÙ ëÌÉÎÉ}{def:KA}
 322 ÉÌÉ \tND{ÁÌÇÅÂÒÙ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ}{def:KAT}. ôÁË ÞÔÏ, ÎÁÐÒÉÍÅÒ,
 323 ÜË×ÁÃÉÏÎÁÌØÎÁÑ ÔÅÏÒÉÑ ÎÅËÏÔÏÒÏÇÏ ËÌÁÓÓÁ ÍÏÄÅÌÅÊ,
 324 ÓÏÄÅÒÖÁÝÁÑ ÒÁ×ÅÎÓÔ×Á ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ,
 325 ÂÕÄÅÔ ×ÙÒÁÖÁÔØ ÜË×É×ÁÌÅÎÔÎÏÓÔØ ÒÅÇÕÌÑÒÎÙÈ ×ÙÒÁÖÅÎÉÊ (ÉÌÉ Á×ÔÏÍÁÔÏ×,
 326 ÉÌÉ ÅÝ£ ÂÏÌÅÅ ÓÌÏÖÎÙÈ ÁÂÓÔÒÁËÃÉÊ ÐÒÏÇÒÁÍÍ) ÐÒÉ ÚÁÄÁÎÎÙÈ
 327 ÏÓÏÂÅÎÎÏÓÔÑÈ ÉÎÔÅÒÐÒÅÔÁÃÉÊ.
 328
 329 %\todo{[ÐÏÄÒÏÂÎÅÅ ÐÒÉÍÅÒÙ?]}
 330
 331 %\todo{[Ó×ÏÂ, ÕÎÉ× ÍÏÄÅÌÉ ÓÀÄÁ?]}
 332
 333 %%% Local Variables:
 334 %%% mode: latex
 335 %%% TeX-master: "main"
 336 %%% End: