\input style
\chapter{6 о проектировании правильно завершаемых конструкций}

оСНОВНАЯ ТЕОРЕМА ДЛЯ КОНСТРУКЦИИ ПОВТОРЕНИЯ  ПРИМЕНИТЕЛЬНО К 
УСЛОВИЮ $P$, СОХРАНЯЕМОМУ ИНВАРИАНТНО ИСТИННЫМ, УТВЕРЖДАЕТ, ЧТО
$$ 
(P \and \wp (DO, T) ) \Rightarrow (DO, P \and \non BB) 
$$

зДЕСЬ ЧЛЕН $\wp(DO, T)$ ПРЕДСТАВЛЯЕТ СОБОЙ СЛАБЕЙШЕЕ ПРЕДУСЛОВИЕ, 
ТАКОЕ, ЧТО КОНСТРУКЦИЯ ПОВТОРЕНИЯ ЗАВВЕРШИТСЯ. еСЛИ ЗАДАНА 
ПРОИЗВОЛЬНАЯ КОНСТРУКЦИЯ DO, ТО В ОБЩЕМ СЛУЧАЕ ОЧЕНЬ ТРУДНО (А 
МОЖЕТ БЫТЬ, НЕВОЗМОЖНО) ОПРЕДЕЛИТЬ $\wp (DO, T)$. пОЭТОМУ Я 
ПРЕДЛАГАЮ ПРОЕКТИРОВАТЬ НАШИ КОНСТРУКЦИИ ПОВТОРЕНИЯ, ПОСТОЯННО 
ПОМНЯ О ТРЕБОВАНИИ ЗАВЕРШИМОСТИ, Т. Е. ПРЕДЛАГАЮ ИСКАТЬ 
ПОДХОДЯЩЕЕ ДОКАЗАТЕЛЬСТВО ЗАВЕРШИМОСТИ И СТРОИТЬ ПРОГРАММУ ТАКИМ 
СПОСОБОМ, ЧТОБЫ ОНА УДОВЛЕТВОРЯЛА ПРЕДПОЛОЖЕНИЯМ, НА КОТОРЫХ 
ОСНОВЫВАЕТСЯ ЭТО ДОКАЗАТЕЛЬСТВО. 

пРЕДПОЛОЖИМ ОПЯТЬ, ЧТО $P$ --- ОТНОШЕНИЕ, КОТОРОЕ СОХРАНЯЕТСЯ 
ИНВАРИАНТНО ИСТИННЫМ, Т.Е.
$$ 
(P \and BB) \Rightarrow \wp(IF, P)\qquad\hbox{ ДЛЯ ВСЕХ СОСТОЯНИЙ }
$$
пУСТЬ $t$ --- КОНЕЧНАЯ ЦЕЛОЧИСЛЕННАЯ ФУНКЦИЯ ОТ ТЕКУЩЕГО 
СОСТОЯНИЯ, ТАКАЯ, ЧТО
$$
 (P \and BB) \Rightarrow (t>0) \qquad\hbox{ДЛЯ ВСЕХ СОСТОЯНИЙ }
$$
И, КРОМЕ ТОГО, ДЛЯ ЛЮБОГО ЗНАЧЕНИЯ $t_0$ И ДЛЯ ВСЕХ 
$$
 (P \and BB \and t\le t_0+1) \Rightarrow \wp(IF, t\le t_0) \eqno (3) 
$$
тОГДА МЫ ДОКАЖЕМ, ЧТО 
$$ 
P \Rightarrow \wp(DO, T)\qquad\hbox{ ДЛЯ ВСЕХ СОСТОЯНИЙ }\eqno(4) 
$$
сОПОСТАВИВ ЭТОТ ФАКТ С ОСНОВНОЙ ТЕОРЕМОЙ ДЛЯ ПОВТОРЕНИЯ, МЫ МОЖЕМ 
ЗАКЛЮЧИТЬ, ЧТО ИМЕЕМ ДЛЯ ВСЕХ СОСТОЯНИЙ
$$ 
P \Rightarrow \wp(DO, P \and \non BB)\eqno(5)
$$

мЫ ПОКАЖЕМ ЭТО, ДОКАЗАВ СНАЧАЛА МЕТОДОМ МАТЕМАТИЧЕСКОЙ ИНДУКЦИИ, 
ЧТО
$$ 
(P \and t\le k) \Rightarrow H_k(T)\qquad\hbox{ДЛЯ ВСЕХ 
СОСТОЯНИЙ}\eqno(6) 
$$
СПРАВЕДЛИВО ПРИ ВСЕХ $k\ge 0$. нАЧНЕМ С ОБОСНОВАНИЯ ИСТИННОСТИ 
(6) ПРИ $k=0$. пОСКОЛЬКУ $н_0(т)=\non вв$, НАМ ТРЕБУЕТСЯ 
ПОКАЗАТЬ, ЧТО
$$ 
(P \and t \le 0) \Rightarrow \non BB \qquad\hbox{ДЛЯ ВСЕХ СОСТОЯНИЙ}
\eqno (7) 
$$
оДНАКО 7 --- ЭТО ПРОСТО ДРУГАЯ ФОРМА ЗАПИСИ ВЫРАЖЕНИЯ (2): ОБА 
ОНИ РАВНЫ ВЫРАЖЕНИЮ
$$ 
\non P \or \non BB \or (t>0) 
$$ 
И ПОЭТОМУ (6) СПРАВЕДЛИВО ПРИ $k=0$. 

пРЕДПОЛОЖИМ ТЕПЕРЬ, ЧТО (6) СПРАВЕДЛИВО ПРИ $k=K$; ТОГДА
$$ 
\eqalign{ 
(P \and BB \and t\le K+l) & \Rightarrow \wp(IF, P \and t \le K)\cr 
& \Rightarrow \wp(IF,H_K(T));\cr 
} (P \and \non BB \and t\le K+1) \Rightarrow \non BB=H_0(T) 
$$
и ЭТИ ДВА ЛОГИЧЕСКИХ СЛЕДОВАНИЯ МОЖНО ОБRЕДИНИТЬ (ИЗ $A \Rightarrow B$ И 
$B \Rightarrow D$  МЫ МОЖЕМ ЗАКЛЮЧИТЬ, ЧТО СПРАВЕДЛИВО $(A \or B \Rightarrow C \or 
D)$):
$$ 
(P \and t\le K+1) \Rightarrow \wp(IF,H_K(T)) \or H_0(т)=H_{K+1}(T) 
$$
И ТЕМ САМЫМ ИСТИННОСТЬ (6) ДОКАЗАНА ДЛЯ ВСЕХ $k\ge 0$. пОСКОЛЬКУ 
$t$ --- ОГРАНИЧЕННАЯ ФУНКЦИЯ, МЫ ИМЕЕМ
$$ 
(\exists k: k\ge 0 : t\le k) 
$$ 
И
$$ 
\eqalign{ 
P& \Rightarrow (\exists k: k\ge 0 : P \and t\le k)\cr  
& \Rightarrow (\exists k:k\ge 0: H_k(T))\cr  
&=\wp(DO, T)\cr 
}
$$
И ТЕМ САМЫМ ДОКАЗАНО (4).

иНТУИТИВНО ТЕОРЕМА СОВЕРШЕННО ЯСНА. с ОДНОЙ СТОРОНЫ, $P$ 
ОСТАНЕТСЯ ИСТИНОЙ, А СЛЕДОВАТЕЛЬНО, $t\ge 0$ ТОЖЕ ОСТАНЕТСЯ 
ИСТИНОЙ; С ДРУГОЙ СТОРОНЫ, ИЗ ОТНОШЕНИЯ (3) СЛЕДУЕТ, ЧТО КАЖДАЯ 
ВЫБОРКА ОХРАНЯЕМОЙ КОМАНДЫ ПРИВЕДЕТ К ЭФФЕКТИВНОМУ УМЕНЬШЕНИЮ $t$  
ПО КРАЙНЕЙ МЕРЕ НА 1. нЕОГРАНИЧЕННОЕ КОЛИЧЕСТВО ВЫБОРОК 
ОХРАНЯЕМЫХ КОМАНД УМЕНЬШИЛО БЫ ЗНАЧЕНИЕ $t$ НИЖЕ ЛЮБОГО ПРЕДЕЛА, 
ЧТО ПРИВЕЛО БЫ К ПРОТИВОРЕЧИЮ. 

пРИМЕНИМОСТЬ ЭТОЙ ТЕОРЕМЫ ОСНОВЫВАЕТСЯ НА ВЫПОЛНЕНИИ УСЛОВИЙ (2) 
И (3). оТНОШЕНИЕ (2) ЯВЛЯЕТСЯ ДОСТАТОЧНО ПРОСТЫМ, ОТНОШЕНИЕ (3) 
ВЫГЛЯДИТ БОЛЕЕ ЗАПУТАННЫМ. нАША ОСНОВНАЯ ТЕОРЕМА ДЛЯ КОНСТРУКЦИИ 
ПОВТОРЕНИЯ ПРИ 
$$ 
\eqalign{ 
Q&= (P \and BB \and t\le t_0+1)\cr 
R&=(t\le t_0)\cr 
}
$$
(ПРИСУТСТВИЕ СВОБОДНОЙ ПЕРЕМЕННОЙ $t_0$ В ОБОИХ ПРЕДИКАТАХ 
ЯВЛЯЕТСЯ ПРИЧИНОЙ ТОГО, ЧТО МЫ ГОВОРИЛИ О "ПАРЕ ПРЕДИКАТОВ") 
ПОЗВОЛЯЕТ НАМ ЗАКЛЮЧИТЬ, ЧТО УСЛОВИЕ (3) СПРАВЕДЛИВО, ЕСЛИ
$$ 
(\forall j: 1\le j \le n: (P \and B_j \and t\le 
t_0+1) \Rightarrow \wp(SL_j, t\le t_0)) 
$$

иНАЧЕ ГОВОРЯ, НАМ НУЖНО ДОКАЗАТЬ ДЛЯ ВСЯКОЙ ОХРАНЯЕМОЙ КОМАНДЫ, 
ЧТО ВЫБОРКА ПРИВЕДЕТ К ЭФФЕКТИВНОМУ yМЕНЬШЕНИЮ $t$. пОМНЯ О ТОМ, 
ЧТО $t$ ЯВЛЯЕТСЯ ФУНКЦИЕЙ ОТ ТЕКУЩЕГО СОСТОЯНИЯ, МЫ МОЖЕМ 
РАССМОТРЕТЬ
$$ 
\wp(SL_j, t\le t_0) \eqno (8)
$$
эТО ПРЕДИКАТ, ВКЛЮЧАЮЩИЙ, ПОМИМО КООРДИНАТНЫХ ПЕРЕМЕННЫХ 
ПРОСТРАНСТВА СОСТОЯНИЙ, ТАКЖЕ И СВОБОДНУЮ ПЕРЕМЕННУЮ $t_0$. дО 
СИХ ПОР МЫ РАССМАТРИВАЛИ ТАКОЙ ПРЕДИКАТ КАК ПРЕДИКАТ, 
ХАРАКТЕРИЗУЮЩИЙ НЕКОЕ ПОДМНОЖЕСТВО СОСТОЯНИЙ. оДНАКО ДЛЯ ЛЮБОГО 
ЗАДАННОГО СОСТОЯНИЯ МЫ МОЖЕМ ТАКЖЕ РАССМАТРИВАТЬ ПРЕДИКАТ КАК 
УСЛОВИЕ, НАЛАГАЕМОЕ НА $t_0$. пУСТЬ $t_0=t_{min}$ 
ПРЕДСТАВЛЯЕТ СОБОЙ МИНИМАЛЬНОЕ РЕШЕНИЕ УРАВНЕНИЯ (8) ОТНОСИТЕЛЬНО 
$t_0$, ТОГДА МЫ МОЖЕМ ИНТЕРПРЕТИРОВАТЬ ЗНАЧЕНИЕ $t_{min}$ КАК 
НАИМЕНЬШУЮ ВЕРХНЮЮ ГРАНИЦУ ДЛЯ КОНЕЧНОГО ЗНАЧЕНИЯ $t$. еСЛИ 
ВСПОМНИТЬ, ЧТО, ПОДОБНО ФУНКЦИИ $t$, $t_{min}$ ТАКЖЕ ЯВЛЯЕТСЯ 
ФУНКЦИЕЙ ОТ ТЕКУЩЕГО СОСТОЯНИЯ, ТО МОЖНО ИНТЕРПРЕТИРОВАТЬ 
ПРЕДИКАТ
$$ 
t_{min}\le t-1 
$$
КАК СЛАБЕЙШЕЕ ПРЕДУСЛОВИЕ, ПРИ КОТОРОМ ГАРАНТИРУЕТСЯ, ЧТО 
ВЫПОЛНЕНИЕ $SL_j$, уМЕНЬШИТ ЗНАЧЕНИЕ $t$ ПО КРАЙНЕЙ МЕРЕ НА 1.

оБОЗНАЧИМ ЭТО ПРЕДУСЛОВИЕ, ГДЕ --- МЫ ПОВТОРЯЕМ ---АРГУМЕНТ 
ЯВЛЯЕТСЯ ЦЕЛОЧИСЛЕННОЙ ФУНКЦИЕЙ ОТ ТЕКУЩЕГО СОСТОЯНИЯ, ЧЕРЕЗ

$$ 
\wdec(SL_j, t) 
$$
пРИ ЭТОМ ИНВАРИАНТНОСТЬ $P$ И ЭФФЕКТИВНОЕ УМЕНЬШЕНИЕ $t$ 
ГАРАНТИРУЮТСЯ, ЕСЛИ МЫ ИМЕЕМ ПРИ ВСЕХ ЗНАЧЕНИЯХ $j$
$$ 
(P \and B_j) \Rightarrow (\wp(SL_j, P)  \and \wdec (SL_j,t) ) 
$$

оБЫЧНО ПРАКТИЧЕСКИЙ СПОСОБ ОТЫСКАНИЯ ПОДХОДЯЩЕГО ПРЕДОХРАНИТЕЛЯ 
$B_j$ СОСТОИТ В СЛЕДУЮЩЕМ. уРАВНЕНИЕ (9) ОТНОСИТСЯ К ТИПУ
$$ 
(P \and Q) \Rightarrow R 
$$
ГДЕ (ПРАКТИЧЕСКИ ВЫЧИСЛИМОЕ!) ЗНАЧЕНИЕ $Q$ НУЖНО НАЙТИ ДЛЯ 
ЗАДАННЫХ ЗНАЧЕНИЙ $P$ И $R$. мЫ ЗАМЕЧАЕМ, ЧТО

\medskip
\item{1.} $Q=R$ ЯВЛЯЕТСЯ РЕШЕНИЕМ.
\item{2.} $Q=(Q1 \and Q2)$ ЯВЛЯЕТСЯ РЕШЕНИЕМ И $р \Rightarrow Q2$, ТО $Q1$ 
ТОЖЕ ЯВЛЯЕТСЯ РЕШЕНИЕМ.
\item{3.} еСЛИ $Q=(Q1 \or Q2)$ ЯВЛЯЕТСЯ РЕШЕНИЕМ И $р \Rightarrow \non Q2$, 
(ИЛИ, ЧТО СВОДИТСЯ К ТОМУ ЖЕ САМОМУ, $(P \and Q2) = F)$, ТО $Q1$ 
ТОЖЕ ЯВЛЯЕТСЯ РЕШЕНИЕМ.
\item{4.} еСЛИ $Q$ ЯВЛЯЕТСЯ РЕШЕНИЕМ И $Q1 \Rightarrow Q$, ТО $Q1$ ТОЖЕ 
ЯВЛЯЕТСЯ РЕШЕНИЕМ.
\medskip

{\sl зАМЕЧАНИЕ 1.} еСЛИ, ДЕЙСТВУЯ ТАКИМ ОБРАЗОМ, МЫ ПРИХОДИМ К 
КАНДИДАТУРЕ $Q$ ДЛЯ $B_j$, ТАКОЙ, ЧТО $р \Rightarrow \non Q$, ТО ЭТА 
КАНДИДАТУРА МОЖЕТ БЫТЬ ДАЛЕЕ УПРОЩЕНА (В СООТВЕТСТВИИ С 
ПРЕДЫДУЩИМ НАБЛЮДЕНИЕМ 3, ПОСКОЛЬКУ ПРИ ЛЮБОМ $Q$ МЫ ИМЕЕМ 
$Q=(\var{ЛОЖЬ} \or Q))$ К ВИДУ $Q=\var{ЛОЖЬ}$; ЭТО ОЗНАЧАЕТ, ЧТО 
РАССМАТРИВАЕМАЯ ОХРАНЯЕМАЯ КОМАНДА ВВЕДЕНА НЕУДАЧНО: ЕЕ МОЖНО 
ИСКЛЮЧИТЬ ИЗ НАБОРА, ПОТОМУ ЧТО ОНА НИКОГДА НЕ БУДЕТ ВЫБИРАТЬСЯ. 
{\sl(кОНЕЦ ЗАМЕЧАНИЯ 1.)}

{\sl зАМЕЧАНИЕ 2.} чАСТО НА ПРАКТИКЕ РАСЩЕПЛЯЮТ УРАВНЕНИЕ (9) НА 
ДВА УРАВНЕНИЯ:
$$ 
\eqalignno{ 
(P \and B_j)& \Rightarrow \wp(SL_j, P ) &  (9А)\cr
(P \and B_j)& \Rightarrow \wdec(SL_j, t) & (9Б)\cr
}
$$
И РАССМАТРИВАЮТ ИХ ПО ОТДЕЛЬНОСТИ. тЕМ САМЫМ РАЗДЕЛЯЮТСЯ ДВЕ 
ЗАДАЧИ: $(9А)$ ОТНОСИТСЯ К ТОМУ, ЧТО ОСТАЕТСЯ ИНВАРИАНТНЫМ, ТОГДА 
КАК $(9Б)$ ОТНОСИТСЯ К ТОМУ, ЧТО ОБЕСПЕЧИВАЕТ ПРОДВИЖЕНИЕ ВПЕРЕД. 
еСЛИ, ИМЕЯ ДЕЛО С УРАВНЕНИЕМ $(9А)$, МЫ ПРИХОДИМ К РЕШЕНИЮ 
$B_j$, ТАКОМУ, ЧТО $р \Rightarrow в_j$, ТО ТОГДА ОЧЕВИДНО, ЧТО ЭТО 
УСЛОВИЕ НЕ БУДЕТ УДОВЛЕТВОРЯТЬ УРАВНЕНИЮ $(9Б)$, ПОСКОЛЬКУ ПРИ 
ТАКОМ $B_j$ ИНВАРИАНТНОСТЬ $р$ ПРИВЕЛА БЫ К 
НЕДЕТЕРМИНИРОВАННОСТИ {\sl(кОНЕЦ ЗАМЕЧАНИЯ 2.)}


тАКИМ ОБРАЗОМ, МЫ МОЖЕМ ПОСТРОИТЬ КОНСТРУКЦИЮ DO, ТАКУЮ, ЧТО
$$ 
P \Rightarrow \wp(DO, р \and \non BB) 
$$
нАШИ УСЛОВИЯ $B_j$ ДОЛЖНЫ БЫТЬ ДОСТАТОЧНО СИЛЬНЫМИ, ЧТОБЫ 
УДОВЛЕТВОРЯЛИСЬ СЛЕДОВАНИЯ (9); В РЕЗУЛЬТАТЕ ЭТОГО НОВОЕ 
ГАРАНТИРУЕМОЕ ПОСТУСЛОВИЕ $P \and \non BB$  МОЖЕТ ОКАЗАТЬСЯ 
СЛИШКОМ СЛАБЫМ И НЕ ОБЕСПЕЧИТЬ НАМ ЖЕЛАЕМОГО ПОСТУСЛОВИЯ $R$. в 
ТАКОМ СЛУЧАЕ МЫ ВСЕ-ТАКИ НЕ РЕШИЛИ НАШУ ПРОБЛЕМУ И НАМ СЛЕДУЕТ 
РАССМОТРЕТЬ ДРУГИЕ ВОЗМОЖНОСТИ.

\bye