lframes-rem.tex

   1 \subparagraph{úÁÍÅÞÁÎÉÑ.}
   2 \todo{[ $\frCo$ ÐÏÈÏÖÅ ÎÁ $\gsCo$ ÄÌÑ
   3 \tD{ÎÁÓÙÝÅÎÎÙÈ ÓÔÒÏË}
   4 (ÓÍ. ïÐÒ.~\ref{def:gsCo}) ÔÅÍ, ÞÔÏ × ÒÅÚÕÌØÔÁÔÅ ÏÐÅÒÁÃÉÉ
   5 ÎÅÓÕÝÉÅ ÉÎÆÏÒÍÁÃÉÀ ÞÁÓÔÉ ÓÔÁ×ÑÔÓÑ ÄÒÕÇ ÚÁ ÄÒÕÇÏÍ. -- ÄÌÑ ÍÏÎÏÉÄÏ× Ó
   6 ÓÏËÒÁÝÅÎÉÅÍ]}
   7
   8
   9 áÌØÔÅÒÎÁÔÉ×ÎÙÅ ÏÐÒÅÄÅÌÅÎÉÑ \tDJust{ÛËÁÌ ëÒÉÐËÅ Ó ÐÒÅÄÅÌÁÍÉ, ÏÓÎÏ×ÁÎÎÙÈ
  10   ÎÁ}~$\mo M$:
  11
  12 \begin{definition*}[×ÁÒÉÁÎÔ ÄÌÑ ïÐÒ.~\ref{def:lframe} (ÎÅÜË×É×ÁÌÅÎÔÎÙÊ!)]
  13 \emph{ûËÁÌÏÊ ëÒÉÐËÅ Ó ÐÒÅÄÅÌÁÍÉ, ÏÓÎÏ×ÁÎÎÏÊ ÎÁ ÍÏÎÏÉÄÅ $\mo M$}
  14 ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ ÔÒÏÊËÕ $(u, v, \kf F)$, ÔÁËÕÀ, ÞÔÏ $u, v \in Q_{\mo
  15   M}$, $\kf F = ([u,v], m)$\T ÛËÁÌÁ ëÒÉÐËÅ, Õ ËÏÔÏÒÏÊ
  16 \begin{align}
  17   m(a) = \{ (w, wa) \mid w \in [u,v], \text{ É ÔÁËÖÅ } wa \in [u,v] \}
  18   \text{ ÄÌÑ $a \in \Sigma$}
  19   &
  20   \text{ÎÁ $T$ $m\colon T \to 2^{[u,v]}$\T ÐÒÏÉÚ×ÏÌØÎÏÅ ÏÔÏÂÒÁÖÅÎÉÅ,}
  21 \end{align}
  22 ÇÄÅ $[u,v]$\T \tD{ÏÔÒÅÚÏË}{def:segment} × $(Q, \coLe)$, $\coLe$\T ÐÏÒÑÄÏË,
  23 ÉÎÄÕÃÉÒÏ×ÁÎÎÙÊ ÎÁ ÜÌÅÍÅÎÔÁÈ ÍÏÎÏÉÄÁ~$\mo M$ ÏÐÅÒÁÃÉÅÊ $\cdot$ (ÓÍ.\
  24 ïÐÒ.~\ref{def:monoid-order}).
  25 \end{definition*}
  26 åÓÌÉ ÐÒÉÎÑÔØ ÔÁËÏÅ ÏÐÒÅÄÅÌÅÎÉÅ, ÔÏ
  27 ÎÁÄÏ ÕÄÅÌÉÔØ ÏÓÏÂÏÅ ×ÎÉÍÁÎÉÅ ÏÐÒÅÄÅÌÅÎÉÀ
  28 $\frCo$, ÐÏÔÏÍÕ ÞÔÏ ÎÅ ÄÌÑ ×ÓÅÈ ÍÏÎÏÉÄÏ× $[ u, v] \cup [v, w] = [ u,
  29 w]$.
  30
  31 åÝ£ ÏÄÎÏ ÏÐÒÅÄÅÌÅÎÉÅ ÍÏÇÌÏ ÂÙ ÉÓÐÏÌØÚÏ×ÁÔØ ÛËÁÌÙ ëÒÉÐËÅ Ó <<ÞÁÓÔÉÞÎÏ
  32 ÏÐÒÅÄÅÌ£ÎÎÙÍÉ>> $\xi$. úÄÅÓØ ÏÓÏÂÏÅ ×ÎÉÍÁÎÉÅ
  33 ÎÁÄÏ ÂÙÌÏ ÂÙ ÕÄÅÌÉÔØ ÏÐÒÅÄÅÌÅÎÉÀ ÏÐÅÒÁÃÉÉ $+$ × ÓÔÒÏÑÝÅÊÓÑ ÁÌÇÅÂÒÅ
  34 ëÌÉÎÉ É ÔÏÍÕ, ÞÔÏ ÓÞÉÔÁÔØ ÉÄÅÎÔÉÞÎÙÍÉ ÜÌÅÍÅÎÔÁÍÉ ÜÔÏÊ ÁÌÇÅÂÒÙ
  35 (ÏÂßÅÄÉÎÅÎÉÅ ÒÁÚÎÙÈ ÎÁÂÏÒÏ×  ÔÁËÉÈ ÜÌÅÍÅÎÔÏ× Ó ÞÁÓÔÉÞÎÏ ÏÐÒÅÄÅÌ£ÎÎÙÍÉ
  36 <<ÏÃÅÎËÁÍÉ>> ÍÏÖÅÔ ÄÁÔØ <<ÜË×É×ÁÌÅÎÔÎÙÅ ÒÅÚÕÌØÔÁÔÙ>>).
  37 \todo{[ÐÒÉÍÅÒ]}
  38
  39
  40 \begin{equation}
  41   \label{eq:frCo}
  42   (u_1, v_1, \ka F_1) \frCo (u_2, v_2, \ka F_2)
  43   \eqdef
  44   \begin{cases}
  45     (u_1, v_2, \ka F_1)
  46     & \text{ ÅÓÌÉ $v_1 = u_2$ É $\kf F_1 = \kf F_2$,}\\
  47     \text{ÎÅÏÐÒÅÄÅÌÅÎÏ}
  48     & \text{ÉÎÁÞÅ.}
  49   \end{cases}
  50 \end{equation}
  51
  52 ÷ÏÚÍÏÖÎÏ, ÂÏÌØÛÅ ÏÔ×ÅÞÁÅÔ ÉÎÔÕÉÃÉÉ ÒÁÓÓÍÏÔÒÅÎÉÅ \KAT, ÂÕÌÅ×ÏÊ
  53 ÐÏÄÁÌÇÅÂÒÏÊ~$B$
  54 ËÏÔÏÒÏÊ Ñ×ÌÑÅÔÓÑ ÎÅ ×ÓÅ $2^{\ILFrames(\Sigma, T, \mo M)}$,
  55 Á ÌÉÛØ ÍÎÏÖÅÓÔ×Á ×ÉÄÁ
  56 $$
  57 \bt C(\bt s) = \{ (\xi, 1_{\mo M}) \mid
  58 \xi(1_{\mo M}, p) =
  59 \begin{cases}
  60   \False & \text{ ÅÓÌÉ } \neg(\bt s \implic p)\\
  61   \True & \text{ ÅÓÌÉ } \bt s \implic p
  62 \end{cases}
  63 \},
  64 $$
  65 ÇÄÅ $\bt s$\T ÜÌÅÍÅÎÔ Ó×ÏÂÏÄÎÏÊ ÂÕÌÅ×ÏÊ ÁÌÇÅÂÒÙ, ÐÏÒÏÖÄ£ÎÎÏÊ $T$.
  66 ïÎÏ ÚÁÍËÎÕÔÏ ÏÔÎÏÓÉÔÅÌØÎÏ ÂÕÌÅ×ÙÈ ÏÐÅÒÁÃÉÊ É ÌÕÞÛÅ ÓÏÏÔ×ÅÔÓÔ×ÕÅÔ $B$\T
  67 ÂÕÌÅ×ÏÊ ÐÏÄÁÌÇÅÂÒÅ ÁÌÇÅÂÒÙ
  68 ÍÎÏÖÅÓÔ× ÎÁÓÙÝÅÎÎÙÈ ÓÔÒÏË (ÓÍ.~õÔ×.~\ref{prop:all-gs-KAT})
  69 É $\Reg_{\Sigma,T}$.
  70 ($\bt C(\place)$\T ×ÚÁÉÍÎÏ ÏÄÎÏÚÎÁÞÎÏÅ ÓÏÏÔ×ÅÔÓÔ×ÉÅ ÍÅÖÄÕ ÔÁËÉÍÉ
  71 ÍÎÏÖÅÓÔ×ÁÍÉ É Ó×ÏÂÏÄÎÏÊ ÂÕÌÅ×ÏÊ ÁÌÇÅÂÒÏÊ, ÐÏÒÏÖÄ£ÎÎÏÊ $T$. ÷ ÎÁÛÅÍ
  72 ÏÓÎÏ×ÎÏÍ ×ÁÒÉÁÎÔÅ ÏÐÒÅÄÅÌÅÎÉÑ $B$ ÂÙÌÏ ÐÏ ÓÕÔÉ Ó×ÏÂÏÄÎÏÊ ÂÕÌÅ×ÏÊ
  73 ÁÌÇÅÂÒÏÊ, ÐÏÒÏÖÄ£ÎÎÏÊ $T \times Q_{\mo M}$, ÞÔÏ ÄÌÑ ÎÁÛÉÈ ÃÅÌÅÊ ÂÅÓÐÏÌÅÚÎÏ.)
  74
  75 \begin{question}
  76   á ÄÌÑ ÐÒÏÉÚ×ÏÌØÎÏÇÏ ÍÏÎÏÉÄÁ, Á ÎÅ ÍÏÎÏÉÄÁ Ó ÓÏËÒÁÝÅÎÉÅÍ ÞÔÏ-ÔÏ ÉÚ
  77   ÜÔÏÇÏ ×ÏÚÍÏÖÎÏ?
  78
  79   é ÚÁÞÅÍ ÜÔÏ ÍÏÖÅÔ ÂÙÔØ ÎÕÖÎÏ?
  80   ëÏÇÄÁ × ÎÁÛÉÈ ÚÁÄÁÞÁÈ ÁÎÁÌÉÚÁ ÐÒÏÇÒÁÍÍ ÍÏÇÕÔ ×ÏÚÎÉËÎÕÔØ ÍÏÎÏÉÄÙ ÂÅÚ ÓÏËÒÁÝÅÎÉÑ?
  81 \end{question}
  82
  83 ôÏ, ÞÔÏ Õ ÎÁÓ ÍÏÎÏÉÄ Ó ÓÏËÒÁÝÅÎÉÅÍ, ÇÁÒÁÎÔÉÒÕÅÔ ÎÁÍ, Ë ÐÒÉÍÅÒÕ, ÔÏ,
  84 ÞÔÏ
  85 $F(a_1 \dotsm a_n) \frCo \{ (\xi_2, u_2) \}$ ÎÉËÏÇÄÁ ÎÅ ÒÁ×ÅÎ
  86 $\emptyset$. (õÓÌÏ×ÉÅ $\xi_1(u_1 w) = \xi_2(w)$ ÉÚ~\eqref{eq:frCo}
  87 ÐÒÅÄßÑ×ÌÑÅÔ <<ÎÅÚÁ×ÉÓÉÍÙÅ>> ÔÒÅÂÏ×ÁÎÉÑ ÎÁ $\xi_2$.)
  88
  89 \begin{answer}
  90 \todo{[!!!]}
  91
  92 \begin{definition}\label{def:lframe}
  93 \tING{ûËÁÌÏÊ ëÒÉÐËÅ Ó ÐÒÅÄÅÌÁÍÉ, ÏÓÎÏ×ÁÎÎÏÊ ÎÁ ÍÏÎÏÉÄÅ $\mo M$}
  94 ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ ÔÒÏÊËÕ $(u, v, \xi)$, ÔÁËÕÀ, ÞÔÏ $u, v \in Q_{\mo
  95   M}$, $\xi\colon Q_{\mo M} \times T \to \{ 0, 1\}$.
  96
  97 $\LFrames(\Sigma, T, \mo M)$\T ÍÎÏÖÅÓÔ×Ï ×ÓÅÈ \tDJust{ÛËÁÌ ëÒÉÐËÅ Ó
  98   ÐÒÅÄÅÌÁÍÉ, ÏÓÎÏ×ÁÎÎÙÈ ÎÁ}~$\mo M$.
  99 \end{definition}
 100
 101 ðÏÓÔÒÏÉÍ ÎÁ ÏÓÎÏ×Å~$\LFrames(\Sigma, T, \mo M)$ ÓÔÒÕËÔÕÒÕ \KAT.
 102
 103 óÎÁÞÁÌÁ ÏÐÒÅÄÅÌÉÍ ÞÁÓÔÉÞÎÏ ÏÐÒÅÄÅÌ£ÎÎÕÀ
 104 ÏÐÅÒÁÃÉÀ \tING{ÎÁÌÏÖÅÎÉÑ} Ä×ÕÈ ÛËÁÌ ëÒÉÐËÅ Ó
 105 ÐÒÅÄÅÌÁÍÉ:
 106 \begin{equation}
 107   \label{eq:frCo}
 108   (u_1, v_1, \xi_1) \frCo (u_2, v_2, \xi_2)
 109   \eqdef
 110   \begin{cases}
 111     (u_1, v_2, \xi_1)
 112     & \text{ ÅÓÌÉ }
 113     \left\{
 114     \begin{aligned}
 115       v_1 &= u_2\\
 116       \xi_1(v_1 w) &= \xi_2(w)
 117       &\text{ ÄÌÑ ×ÓÅÈ $w \in \mo M$,}
 118     \end{aligned}
 119     \right.
 120     \\
 121     \text{ÎÅÏÐÒÅÄÅÌÅÎÏ}
 122     & \text{ÉÎÁÞÅ.}
 123   \end{cases}
 124 \end{equation}
 125
 126 \end{answer}
 127
 128
 129 %%% Local Variables:
 130 %%% mode: latex
 131 %%% TeX-master: "main"
 132 %%% End: