Changeset 128 for docs/trunk/omega-test-slides

Legend:

Unmodified

Added

Removed

• docs/trunk/omega-test-slides/proofs.tex

  r127	r128
  4	4
  5	5	\usepackage{amsmath}
  6	(追記) (追記ここまで)
  7	(追記) \usepackage{listings} (追記ここまで)
  6	8
  7	9	\begin{document}
  …	…
  138	140	Once we eliminate $m,ドル one of the new bounds will be $n + 1 \leq n,ドル which is unsolveable (1ドル \leq 0$). So the whole thing is safe!
  139	141
  142	(追記) \section{Equations for REM with non-constant divisor} (追記ここまで)
  143	(追記) (追記ここまで)
  144	(追記) Consider what happens if the divisor is not known. Using the logic from the previous section, (追記ここまで)
  145	(追記) we could end up with $z|y|$ where both $z$ and $y$ are unknown. But the Omega Test is for linear equations; (追記ここまで)
  146	(追記) we cannot deal with the multiple of two unknown variables. So we can't handle this the straightforward way. (追記ここまで)
  147	(追記) (追記ここまで)
  148	(追記) For now we will consider the case where $y \geq 2$ ($y \neq 0$ for definite, because that would be division by zero, (追記ここまで)
  149	(追記) and if $y = 1$ that results in both sides of modulo division being equal), and $x \geq 1$. (追記ここまで)
  150	(追記) (追記ここまで)
  151	(追記) For $x \operatorname{REM} y,ドル we know that: (追記ここまで)
  152	(追記) (追記ここまで)
  153	(追記) \[ x \operatorname{REM} y = x - \operatorname{sign}(x)|y| \floorxy \] (追記ここまで)
  154	(追記) (追記ここまで)
  155	(追記) Since we are dealing with positive $x,ドル and remembering that $z \geq 0$ (it is the floor of the division of two positive numbers), this means: (追記ここまで)
  156	(追記) (追記ここまで)
  157	(追記) \[ x \operatorname{REM} y = x - |y| \floorxy \] (追記ここまで)
  158	(追記) (追記ここまで)
  159	(追記) We will let $a = -|y|z,ドル so that: (追記ここまで)
  160	(追記) (追記ここまで)
  161	(追記) \[ x \operatorname{REM} y = x + a \] (追記ここまで)
  162	(追記) (追記ここまで)
  163	(追記) This is a form we can work with. Although we cannot directly express that $a$ is a multiple of $|y|,ドル we can (追記ここまで)
  164	(追記) introduce some inequalities: (追記ここまで)
  165	(追記) (追記ここまで)
  166	(追記) \[ a \leq 0 \] (追記ここまで)
  167	(追記) \[ 0 \leq x + a \leq y - 1 \] (追記ここまで)
  168	(追記) (追記ここまで)
  169	(追記) The top one above being because $a$ is the negation of the multiple of two positive (or zero) integers. This on its own (追記ここまで)
  170	(追記) is not sufficient for most (any?) cases. The problem is that $y$ has no upper bound. In the Omega Test every variable must (追記ここまで)
  171	(追記) have an upper and lower bound in order to be useful. This is because if $y$ has no upper bound and its value can never be (追記ここまで)
  172	(追記) determined by equality (it is not involved in any equalities), it is not useful in constraining other variables. It may be (追記ここまで)
  173	(追記) that $x + a \leq y - 1$ as above, but without being able to determine what $y$ is or use its upper bound to constrain (追記ここまで)
  174	(追記) $x + a + 1$ (by variable elimination), all inequalities it is involved in become useless. (追記ここまで)
  175	(追記) (追記ここまで)
  176	(追記) The way we supply an upper bound for $y$ is somewhat of a trick. We know that since $a$ is a multiple of $y,ドル and $a \leq 0,ドル (追記ここまで)
  177	(追記) either $a = 0$ or $a \leq -y$. The latter equation is in effect an upper bound for $y,ドル since it rearranges to $y \leq -a$. (追記ここまで)
  178	(追記) This simple trick allows for much more reasoning, and can allow the Omega Test to solve some problems, as seen in the next section. (追記ここまで)
  179	(追記) (追記ここまで)
  180	(追記) \subsection{Example} (追記ここまで)
  181	(追記) (追記ここまで)
  182	(追記) Consider a replicated PAR: (追記ここまで)
  183	(追記) (追記ここまで)
  184	(追記) \begin{lstlisting} (追記ここまで)
  185	(追記) [n]INT as,bs: -- not valid occam (yet?) (追記ここまで)
  186	(追記) -- but mobile arrays have same effect (追記ここまで)
  187	(追記) PAR i = 0 FOR n (追記ここまで)
  188	(追記) as[(i + 1) \operatorname{REM} n] := bs[i] (追記ここまで)
  189	(追記) \end{lstlisting} (追記ここまで)
  190	(追記) (追記ここまで)
  191	(追記) The case for the indices of $bs$ is trivially solveable and is not covered here. Consider the indices of $as$; we will use (追記ここまで)
  192	(追記) $j$ as the ghost variable. Our standard inequalities for this would be as follows for the replication: (追記ここまで)
  193	(追記) (追記ここまで)
  194	(追記) \[ 0 \leq i \leq j - 1 \leq n - 2 \] (追記ここまで)
  195	(追記) (追記ここまで)
  196	(追記) The obvious equality for checking for overlap: (追記ここまで)
  197	(追記) (追記ここまで)
  198	(追記) \[i + 1 \operatorname{REM} n = j + 1 \operatorname{REM} n \] (追記ここまで)
  199	(追記) (追記ここまで)
  200	(追記) And as follows for the array index: (追記ここまで)
  201	(追記) (追記ここまで)
  202	(追記) \[0 \leq (i + 1) \operatorname{REM} n \leq n - 1 \] (追記ここまで)
  203	(追記) \[0 \leq (j + 1) \operatorname{REM} n \leq n - 1 \] (追記ここまで)
  204	(追記) (追記ここまで)
  205	(追記) As discussed earlier, we can't use this REM form directly, so we proceed as follows. We know that $n$ must be positive; otherwise (追記ここまで)
  206	(追記) the replication would not work. If $n = 1$ there is only one use of the array, so that is safe. So we know $n \geq 2$ when (追記ここまで)
  207	(追記) we are checking for parallel usage, which satisfies the previously discussed condition. We will consider the option for the array (追記ここまで)
  208	(追記) indexes (the LHS of the REM) being positive here; we do need to check the other cases, but they are trivially disproveable. We (追記ここまで)
  209	(追記) effectively add the conditions $i + 1 \geq 1$ and $j + 1 \geq 1$; these are obviously redundant given \[ 0 \leq i \leq j - 1 \]. (追記ここまで)
  210	(追記) We express REM as previously discussed, transformed the latter three equations into: (追記ここまで)
  211	(追記) (追記ここまで)
  212	(追記) \[i + 1 + a = j + 1 + b \] (追記ここまで)
  213	(追記) \[0 \leq (i + 1) + a \leq n - 1 \] (追記ここまで)
  214	(追記) \[0 \leq (j + 1) + b \leq n - 1 \] (追記ここまで)
  215	(追記) \[0 \leq (i + 1) + a \leq n - 1 \] (追記ここまで)
  216	(追記) \[0 \leq (j + 1) + a \leq n - 1 \] (追記ここまで)
  217	(追記) (追記ここまで)
  218	(追記) The reason for these duplicated equations is that one form comes from the `REM $n$' aspect, and the other comes from indexing an (追記ここまで)
  219	(追記) array of size $n$. Obviously, the duplicated/redundant inequalities will be removed. (追記ここまで)
  220	(追記) (追記ここまで)
  221	(追記) Following our earlier reasoning, we now need to consider all possible combinations of ($a = 0$ or $a leq -n$) and ($b = 0$ or $b \leq -n$). (追記ここまで)
  222	(追記) These four possibilities are considered in turn in the following sub-sections. For clarity, here are the other constraints we are working with: (追記ここまで)
  223	(追記) (追記ここまで)
  224	(追記) \[ 0 \leq i \leq j - 1 \leq n - 2 \] (追記ここまで)
  225	(追記) \[i + 1 + a = j + 1 + b \] (追記ここまで)
  226	(追記) \[0 \leq (i + 1) + a \leq n - 1 \] (追記ここまで)
  227	(追記) \[0 \leq (j + 1) + b \leq n - 1 \] (追記ここまで)
  228	(追記) (追記ここまで)
  229	(追記) \subsubsection{$a = 0,ドル$b = 0$} (追記ここまで)
  230	(追記) (追記ここまで)
  231	(追記) If we substitute in these two equalities ($a = 0,ドル$b = 0$) into just the first two equations we get: (追記ここまで)
  232	(追記) (追記ここまで)
  233	(追記) \[ 0 \leq i \leq j - 1 \leq n - 2 \] (追記ここまで)
  234	(追記) \[ i = j \] (追記ここまで)
  235	(追記) (追記ここまで)
  236	(追記) Perform the next substitution yields: (追記ここまで)
  237	(追記) (追記ここまで)
  238	(追記) \[ 0 \leq j \leq j - 1 \leq n - 2 \] (追記ここまで)
  239	(追記) (追記ここまで)
  240	(追記) Picking out the middle equation $j \leq j - 1$ (which becomes 0ドル \leq -1,ドル technically), we can see this problem is inconsistent; no solution. (追記ここまで)
  241	(追記) (追記ここまで)
  242	(追記) \subsubsection{$a = 0,ドル $b \leq -n$} (追記ここまで)
  243	(追記) (追記ここまで)
  244	(追記) We will substitute in $a = 0$ and add $b \leq -n$: (追記ここまで)
  245	(追記) (追記ここまで)
  246	(追記) \[ 0 \leq i \leq j - 1 \leq n - 2 \] (追記ここまで)
  247	(追記) \[i = j + b \] (追記ここまで)
  248	(追記) \[0 \leq i + 1 \leq n - 1 \] (追記ここまで)
  249	(追記) \[0 \leq (j + 1) + b \leq n - 1 \] (追記ここまで)
  250	(追記) \[ b \leq -n \] (追記ここまで)
  251	(追記) (追記ここまで)
  252	(追記) Substituting in $i = j + b$ we get: (追記ここまで)
  253	(追記) (追記ここまで)
  254	(追記) \[ 0 \leq j + b \leq j - 1 \leq n - 2 \] (追記ここまで)
  255	(追記) \[0 \leq j + b + 1 \leq n - 1 \] (追記ここまで)
  256	(追記) \[0 \leq (j + 1) + b \leq n - 1 \] (追記ここまで)
  257	(追記) \[ b \leq -n \] (追記ここまで)
  258	(追記) (追記ここまで)
  259	(追記) Eliminating the redundant equations and splitting them all out: (追記ここまで)
  260	(追記) (追記ここまで)
  261	(追記) \[ 0 \leq j + b \] (追記ここまで)
  262	(追記) \[ b \leq -1 \] (追記ここまで)
  263	(追記) \[ j \leq n - 1 \] (追記ここまで)
  264	(追記) \[ -1 \leq j + b \] (追記ここまで)
  265	(追記) \[ j + b \leq n - 2 \] (追記ここまで)
  266	(追記) \[ b \leq -n \] (追記ここまで)
  267	(追記) (追記ここまで)
  268	(追記) The fourth equation is obviously redundant given the top equation. We then pick out the bounds for $j$: (追記ここまで)
  269	(追記) (追記ここまで)
  270	(追記) \[ -b \leq j \] (追記ここまで)
  271	(追記) \[ j \leq n - 1 \] (追記ここまで)
  272	(追記) \[ j \leq n - 2 - b \] (追記ここまで)
  273	(追記) (追記ここまで)
  274	(追記) An exact projection. We then pair them up (eliminating $b$ from the second pair): (追記ここまで)
  275	(追記) (追記ここまで)
  276	(追記) \[-b \leq n - 1 \] (追記ここまで)
  277	(追記) \[0 \leq n - 2 \] (追記ここまで)
  278	(追記) (追記ここまで)
  279	(追記) And add the others left over: (追記ここまで)
  280	(追記) (追記ここまで)
  281	(追記) \[ b \leq -1 \] (追記ここまで)
  282	(追記) \[ b \leq -n \] (追記ここまで)
  283	(追記) (追記ここまで)
  284	(追記) We can form these into bounds for $n$: (追記ここまで)
  285	(追記) (追記ここまで)
  286	(追記) \[1 - b \leq n \] (追記ここまで)
  287	(追記) \[2 \leq n \] (追記ここまで)
  288	(追記) \[n \leq -b \] (追記ここまで)
  289	(追記) (追記ここまで)
  290	(追記) And eliminate $n$ (another exact projection): (追記ここまで)
  291	(追記) (追記ここまで)
  292	(追記) \[1 - b \leq - b \] (追記ここまで)
  293	(追記) \[2 \leq -b \] (追記ここまで)
  294	(追記) (追記ここまで)
  295	(追記) The top equation simplifies to 1ドル \leq 0,ドル which is disproveable. So no solution here either. (追記ここまで)
  296	(追記) (追記ここまで)
  297	(追記) \subsubsection{$a \leq -n,ドル $b = 0$} (追記ここまで)
  298	(追記) (追記ここまで)
  299	(追記) We substitute in $b = 0$ and add $a \leq -n$ to the list: (追記ここまで)
  300	(追記) (追記ここまで)
  301	(追記) \[ 0 \leq i \leq j - 1 \leq n - 2 \] (追記ここまで)
  302	(追記) \[i + a = j \] (追記ここまで)
  303	(追記) \[0 \leq (i + 1) + a \leq n - 1 \] (追記ここまで)
  304	(追記) \[0 \leq j + 1 \leq n - 1 \] (追記ここまで)
  305	(追記) \[a \leq -n \] (追記ここまで)
  306	(追記) (追記ここまで)
  307	(追記) We then substitute in $j = i + a$: (追記ここまで)
  308	(追記) (追記ここまで)
  309	(追記) \[ 0 \leq i \leq i + a - 1 \leq n - 2 \] (追記ここまで)
  310	(追記) \[0 \leq (i + 1) + a \leq n - 1 \] (追記ここまで)
  311	(追記) \[0 \leq i + a + 1 \leq n - 1 \] (追記ここまで)
  312	(追記) \[a \leq -n \] (追記ここまで)
  313	(追記) (追記ここまで)
  314	(追記) Eliminate redundant equations and split out: (追記ここまで)
  315	(追記) (追記ここまで)
  316	(追記) \[ 0 \leq i \] (追記ここまで)
  317	(追記) \[ 1 \leq a \] (追記ここまで)
  318	(追記) \[ i + a \leq n - 1 \] (追記ここまで)
  319	(追記) \[-1 \leq i + a \] (追記ここまで)
  320	(追記) \[ i + a \leq n - 2 \] (追記ここまで)
  321	(追記) \[ a \leq -n \] (追記ここまで)
  322	(追記) (追記ここまで)
  323	(追記) We now eliminate $i,ドル pairing up its lower bounds (0ドル,ドル $a - 1$) with its upper bounds ($n - 2 - a$): (追記ここまで)
  324	(追記) (追記ここまで)
  325	(追記) \[0 \leq n - 2 - a \] (追記ここまで)
  326	(追記) \[a - 1 \leq n - 2 - a \] (追記ここまで)
  327	(追記) (追記ここまで)
  328	(追記) Rearrange and re-add the others: (追記ここまで)
  329	(追記) (追記ここまで)
  330	(追記) \[ 1 \leq a \] (追記ここまで)
  331	(追記) \[0 \leq n - 2 - a \] (追記ここまで)
  332	(追記) \[1 \leq n \] (追記ここまで)
  333	(追記) \[ a \leq -n \] (追記ここまで)
  334	(追記) (追記ここまで)
  335	(追記) Now if we do the same for $a$ (lower: 1, upper: $n - 2,ドル$-n$): (追記ここまで)
  336	(追記) (追記ここまで)
  337	(追記) \[3 \leq n \] (追記ここまで)
  338	(追記) \[1 \leq -n \] (追記ここまで)
  339	(追記) \[1 \leq n \] (追記ここまで)
  340	(追記) (追記ここまで)
  341	(追記) The last is redundant, but the others rearrange to: (追記ここまで)
  342	(追記) (追記ここまで)
  343	(追記) \[3 \leq n \] (追記ここまで)
  344	(追記) \[n \leq -1 \] (追記ここまで)
  345	(追記) (追記ここまで)
  346	(追記) Elimination leaves 3ドル \leq -1,ドル which is clearly not satisfiable. So no solution here. (追記ここまで)
  347	(追記) (追記ここまで)
  348	(追記) \subsubsection{$a \leq -n,ドル $b \leq -n$} (追記ここまで)
  349	(追記) (追記ここまで)
  350	(追記) The last possibility! Add the inequalities: (追記ここまで)
  351	(追記) (追記ここまで)
  352	(追記) \[ 0 \leq i \leq j - 1 \leq n - 2 \] (追記ここまで)
  353	(追記) \[i + 1 + a = j + 1 + b \] (追記ここまで)
  354	(追記) \[0 \leq (i + 1) + a \leq n - 1 \] (追記ここまで)
  355	(追記) \[0 \leq (j + 1) + b \leq n - 1 \] (追記ここまで)
  356	(追記) \[a \leq -n \] (追記ここまで)
  357	(追記) \[b \leq -n \] (追記ここまで)
  358	(追記) (追記ここまで)
  359	(追記) Now substitute $i = j + b - a$: (追記ここまで)
  360	(追記) (追記ここまで)
  361	(追記) \[ 0 \leq j + b - a \leq j - 1 \leq n - 2 \] (追記ここまで)
  362	(追記) \[0 \leq (j + b - a + 1) + a \leq n - 1 \] (追記ここまで)
  363	(追記) \[0 \leq (j + 1) + b \leq n - 1 \] (追記ここまで)
  364	(追記) \[a \leq -n \] (追記ここまで)
  365	(追記) \[b \leq -n \] (追記ここまで)
  366	(追記) (追記ここまで)
  367	(追記) The middle equations are once more redundant, and we split everything out: (追記ここまで)
  368	(追記) (追記ここまで)
  369	(追記) \[ 0 \leq j + b - a \] (追記ここまで)
  370	(追記) \[b - a \leq -1 \] (追記ここまで)
  371	(追記) \[j \leq n - 1 \] (追記ここまで)
  372	(追記) \[-1 \leq j + b \] (追記ここまで)
  373	(追記) \[j + b \leq n - 2 \] (追記ここまで)
  374	(追記) \[a \leq -n \] (追記ここまで)
  375	(追記) \[b \leq -n \] (追記ここまで)
  376	(追記) (追記ここまで)
  377	(追記) Eliminate bounds on $a$ (lower: $b + 1,ドル upper: $-n,ドル $j + b$): (追記ここまで)
  378	(追記) (追記ここまで)
  379	(追記) \[b + 1 \leq j + b \] (追記ここまで)
  380	(追記) \[b + 1 \leq -n \] (追記ここまで)
  381	(追記) \[j \leq n - 1 \] (追記ここまで)
  382	(追記) \[-1 \leq j + b \] (追記ここまで)
  383	(追記) \[j + b \leq n - 2 \] (追記ここまで)
  384	(追記) \[b \leq -n \] (追記ここまで)
  385	(追記) (追記ここまで)
  386	(追記) Last equation is redundant in favour of the second. Now eliminate bounds on $n$ (lower: $j + 1,ドル$j + b - 2$ upper: $-b-1$): (追記ここまで)
  387	(追記) (追記ここまで)
  388	(追記) \[1 \leq j \] (追記ここまで)
  389	(追記) \[j + 1 \leq - b - 1 \] (追記ここまで)
  390	(追記) \[j + b - 2 \leq -b -1 \] (追記ここまで)
  391	(追記) \[-1 \leq j + b \] (追記ここまで)
  392	(追記) (追記ここまで)
  393	(追記) Simplify and eliminate redundancy: (追記ここまで)
  394	(追記) \[-1 \leq j \] (追記ここまで)
  395	(追記) \[j + b \leq -2 \] (追記ここまで)
  396	(追記) \[j + 2b \leq 1 \] (追記ここまで)
  397	(追記) \[-1 \leq j + b \] (追記ここまで)
  398	(追記) (追記ここまで)
  399	(追記) Now consider bounds on $j$ (lower: -1, $-b - 1,ドル upper: $-b - 2,ドル 1ドル - 2b$): (追記ここまで)
  400	(追記) (追記ここまで)
  401	(追記) \[ -1 \leq -b - 2 \] (追記ここまで)
  402	(追記) \[ -b - 1 \leq -b - 2 \] (追記ここまで)
  403	(追記) \[ -1 \leq 1 - 2b \] (追記ここまで)
  404	(追記) \[ b - 1 \leq 1 - 2b \] (追記ここまで)
  405	(追記) (追記ここまで)
  406	(追記) Simplify and rearrange: (追記ここまで)
  407	(追記) (追記ここまで)
  408	(追記) \[b \leq -1 \] (追記ここまで)
  409	(追記) \[0 \leq -1 \] (追記ここまで)
  410	(追記) \[2b \leq 2 \] (追記ここまで)
  411	(追記) \[3b \leq 2 \] (追記ここまで)
  412	(追記) (追記ここまで)
  413	(追記) The third equation is inconsistent. So no solution. (追記ここまで)
  414	(追記) (追記ここまで)
  415	(追記) \subsubsection{Conclusion} (追記ここまで)
  416	(追記) (追記ここまで)
  417	(追記) Having checked all four options (eventually!) it can be seen that there is no solution, hence the original equation was safe. (追記ここまで)
  418	(追記) We have proved this using the standard Omega Test, by formulating the problem correctly. (追記ここまで)
  419	(追記) (追記ここまで)
  420	(追記) TODO explore the other options (e.g. $x$ negative, maybe $y$ negative) (追記ここまで)
  421	(追記) (追記ここまで)
  422	(追記) (追記ここまで)
  140	423	\end{document}

Note: See TracChangeset for help on using the changeset viewer.