general.tex

   1 \section{ûËÁÌÙ ëÒÉÐËÅ É ÔÒÁÓÓÙ}\label{sec:kframes}
   2
   3 ðÕÓÔØ $\Sigma$ ËÏÎÅÞÎÙÊ ÁÌÆÁ×ÉÔ (ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ×).
   4
   5 \begin{definition}\label{def:kframe-op}
   6   \tING{ûËÁÌÁ ëÒÉÐËÅ} ÎÁÄ~$\Sigma$\T ÜÔÏ ÓÔÒÕËÔÕÒÁ $(Q, m)$, ÇÄÅ $Q$\T
   7   ÍÎÏÖÅÓÔ×Ï ÓÏÓÔÏÑÎÉÊ, Á
   8   \begin{align*}
   9     m\colon &\Sigma \to 2^{Q \times Q}.
  10   \end{align*}
  11 \end{definition}
  12
  13 \begin{application}
  14 åÓÌÉ ÍÙ ÉÍÅÅÍ ÄÅÌÏ Ó ÐÒÏÇÒÁÍÍÁÍÉ, ÓÏÓÔÁ×ÌÅÎÎÙÍÉ ÉÚ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ×,
  15 ÔÏ <<ÏÐÉÓÁÎÉÅ>> ÓÅÍÁÎÔÉËÉ ÐÒÏÇÒÁÍÍ ÍÙ ÍÏÖÅÍ ÏÓÎÏ×Ù×ÁÔØ ÎÁ <<ÏÐÉÓÁÎÉÉ>>
  16 ÓÅÍÁÎÔÉËÉ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ× É ÏÂÝÉÈ ÐÒÁ×ÉÌÁÈ ÓÅÍÁÎÔÉÞÅÓËÏÊ
  17 ËÏÍÐÏÚÉÃÉÉ. óÅÍÁÎÔÉËÕ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ×\T ÏÓÏÂÅÎÎÏÓÔÉ ÉÈ ÐÏ×ÅÄÅÎÉÑ\T
  18 ÍÙ ÍÏÖÅÍ ÐÒÅÄÓÔÁ×ÉÔØ × ×ÉÄÅ ÛËÁÌÙ ëÒÉÐËÅ. ($m$ ÐÏËÁÚÙ×ÁÅÔ ËÁË ËÁÖÄÙÊ
  19 ÏÐÅÒÁÔÏÒ ÍÏÖÅÔ ÉÚÍÅÎÉÔØ ÔÅËÕÝÅÅ <<ÓÏÓÔÏÑÎÉÅ ÐÁÍÑÔÉ ×ÙÞÉÓÌÉÔÅÌØÎÏÊ
  20 ÍÁÛÉÎÙ>>\T ÜÌÅÍÅÎÔ ÍÎÏÖÅÓÔ×Á~$Q$.)
  21 \end{application}
  22
  23 ðÕÓÔØ $\Sigma$ É $T$ ËÏÎÅÞÎÙÅ ÁÌÆÁ×ÉÔÙ (ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ× É ÂÁÚÏ×ÙÈ ÔÅÓÔÏ×).
  24
  25 \begin{definition}\label{def:kframe-op-tests}
  26   \tING{ûËÁÌÁ ëÒÉÐËÅ} ÎÁÄ~$\Sigma, T$\T ÜÔÏ ÓÔÒÕËÔÕÒÁ $(Q, m)$, ÇÄÅ $Q$\T
  27   ÍÎÏÖÅÓÔ×Ï ÓÏÓÔÏÑÎÉÊ, Á
  28   \begin{align*}
  29     m\colon &\Sigma \to 2^{Q \times Q}
  30     &
  31     m\colon &T \to 2^{Q}.
  32   \end{align*}
  33 \end{definition}
  34
  35 \begin{application}
  36 ûËÁÌÁ ëÒÉÐËÅ ÔÁËÏÇÏ ×ÉÄÁ ÍÏÖÅÔ ÓÌÕÖÉÔØ ÐÒÅÄÓÔÁ×ÌÅÎÉÅÍ ÓÅÍÁÎÔÉËÉ
  37 ÂÁÚÏ×ÙÈ ÜÌÅÍÅÎÔÏ× ÐÒÏÇÒÁÍÍ,
  38 ÅÓÌÉ ÍÙ ÉÍÅÅÍ ÄÅÌÏ Ó ÐÒÏÇÒÁÍÍÁÍÉ, ÓÏÓÔÁ×ÌÅÎÎÙÍÉ ÕÖÅ ÉÚ ÜÌÅÍÅÎÔÏ× Ä×ÕÈ
  39 ÓÏÒÔÏ×\T ÏÐÅÒÁÔÏÒÏ× É ÔÅÓÔÏ×.
  40 \end{application}
  41
  42 \begin{definition}\label{def:trace}
  43   ðÕÓÔØ $\kf F = \Stru{Q_{\kf F}, m_{\kf F}}$ ÛËÁÌÁ
  44   ëÒÉÐËÅ ÎÁÄ~$\Sigma$ (ÉÌÉ ÎÁÄ~$\Sigma, T$).
  45   \tING{ôÒÁÓÓÏÊ} ×~$\kf F$ ÎÁÚÙ×ÁÅÔÓÑ
  46   ËÏÎÅÞÎÁÑ ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÏÓÔØ~$\sigma$ ×ÉÄÁ:
  47   \begin{equation}
  48     \label{eq:trace}
  49     u_0 a_0 u_1 \dotsm u_{n-1} a_{n-1} u_n,
  50   \end{equation}
  51   ÇÄÅ $n \in \bbN \cup \{ 0 \}$ É
  52   \begin{align*}
  53     u_i &\in Q_{\kf F},
  54     &
  55     a_i &\in \Sigma,
  56     &
  57     \text{Á }
  58     (u_i, u_{i+1}) &\in m_{\kf F}(a_i) \text{ ÄÌÑ } 0 \leq i \leq n - 1.
  59   \end{align*}
  60
  61   \tING{íÎÏÖÅÓÔ×Ï ÔÒÁÓÓ × ÛËÁÌÅ ëÒÉÐËÅ}~$\kf F$ ÏÂÏÚÎÁÞÉÍ $\Trs(\kf F)$.
  62
  63   äÌÑ ÔÒÁÓÓÙ~$\sigma$ ×ÉÄÁ~\eqref{eq:trace}
  64   \tING{ÄÌÉÎÁ~$\Len{\sigma}$} ÒÁ×ÎÁ $n$,
  65   \begin{align*}
  66     \First(\sigma) &\eqdef u_0,
  67     &
  68     \Last(\sigma) &\eqdef u_n,
  69     &
  70     \Label(\sigma) &\eqdef
  71     \begin{cases}
  72       a_0 \dotsm a_{n-1}, &\\
  73       \eStr \text{(ÐÕÓÔÁÑ ÓÔÒÏËÁ)}, &\text{ÅÓÌÉ } \Len{\sigma} = 0.
  74     \end{cases}
  75   \end{align*}
  76 \end{definition}
  77
  78 \section{íÏÄÅÌÉ É ÔÅÏÒÉÉ}
  79
  80 \begin{definition}
  81   íÎÏÖÅÓÔ×Ï ÆÏÒÍÕÌ ×ÉÄÁ:
  82   $$
  83   s = t,
  84   $$
  85   ÇÄÅ $s$ É $t$\T ÔÅÒÍÙ × ÎÅËÏÔÏÒÏÍ ÒÁÓÓÍÁÔÒÉ×ÁÅÍÏÍ ÑÚÙËÅ,
  86   ËÏÔÏÒÙÅ ×ÅÒÎÙ ÐÒÉ ÌÀÂÙÈ ÉÎÔÅÒÐÒÅÔÁÃÉÑÈ ÎÁ ÁÌÇÅÂÒÁÉÞÅÓËÉÈ ÓÔÒÕËÔÕÒÁÈ
  87   ËÌÁÓÓÁ~$\class C$\T ÜÔÏ
  88   \tING{ÜË×ÁÃÉÏÎÁÌØÎÁÑ ÔÅÏÒÉÑ} ËÌÁÓÓÁ~$\class C$.
  89
  90   ïÂÏÚÎÁÞÁÅÔÓÑ  $\Equa\class C$.
  91 \end{definition}
  92
  93 \begin{definition}[\cite{KA-proof-theory}]
  94   \tING{õÎÉ×ÅÒÓÁÌØÎÁÑ Horn\dÆÏÒÍÕÌÁ}\T ÜÔÏ ÆÏÒÍÕÌÁ ×ÉÄÁ
  95   $$
  96   s_1 = t_1 \wedge \dotsb \wedge s_k = t_k
  97   \implic s = t,
  98   $$
  99   ÇÄÅ $s_i$, $t_i$, $s$, $t$\T ÔÅÒÍÙ × ÎÅËÏÔÏÒÏÍ ÒÁÓÓÍÁÔÒÉ×ÁÅÍÏÍ ÑÚÙËÅ.
 100
 101   íÎÏÖÅÓÔ×Ï \tDJust{ÕÎÉ×ÅÒÓÁÌØÎÙÈ Horn-ÆÏÒÍÕÌ},
 102   ËÏÔÏÒÙÅ ×ÅÒÎÙ ÐÒÉ ÌÀÂÙÈ ÉÎÔÅÒÐÒÅÔÁÃÉÑÈ ÎÁ ÍÏÄÅÌÑÈ ÉÚ ËÌÁÓÓÁ $\class
 103   C$\T ÜÔÏ
 104   \tING{ÕÎÉ×ÅÒÓÁÌØÎÁÑ Horn-ÔÅÏÒÉÑ} ËÌÁÓÓÁ~$\class C$.
 105
 106   ïÂÏÚÎÁÞÁÅÔÓÑ $\Horn\class C$.
 107
 108   íÙ ÂÕÄÅÍ ÐÏÚ×ÏÌÑÔØ ÓÅÂÅ ÚÁÐÉÓÙ×ÁÔØ ÕÎÉ×ÅÒÓÁÌØÎÙÅ Horn\dÆÏÒÍÕÌÙ ËÁË
 109   $E \implic s = t$, ÇÄÅ $E$\T ÜÔÏ ËÏÎÅÞÎÏÅ ÍÎÏÖÅÓÔ×Ï ÒÁ×ÅÎÓÔ× ×ÉÄÁ
 110   $s_i = t_i$.
 111
 112   óÌÏ×Ï <<ÕÎÉ×ÅÒÓÁÌØÎÙÊ>> ÍÙ ÞÁÓÔÏ ÂÕÄÅÍ ÏÐÕÓËÁÔØ.
 113 \end{definition}
 114 \begin{remark}
 115   $\Equa\class C$\T ÜÔÏ ÓÕÖÅÎÉÅ $\Horn\class C$ ÄÏ Horn-ÆÏÒÍÕÌ Ó $E = \emptyset$.
 116 \end{remark}
 117 %%% Local Variables:
 118 %%% mode: latex
 119 %%% TeX-master: "main"
 120 %%% End: