\input style
\chapter{5 две теоремы}
в ЭТОЙ ГЛАВЕ МЫ ВЫВОДИМ ДВЕ ТЕОРЕМЫ ОБ ОПЕРАТОРАХ, КОТОРЫЕ СТРОЯТСЯ 
ИЗ НАБОРОВ ОХРАНЯЕМЫХ КОМАНД. пЕРВАЯ ТЕОРЕМА КАСАЕТСЯ КОНСТРУКЦИИ 
ВЫБОРА if-fi, А ВТОРАЯ --- КОНСТРУКЦИИ ПОВТОРЕНИЯ do-od. в ЭТОМ ГЛАВЕ 
МЫ БУДЕМ РАССМАТРИВАТЬ КОНСТРУКЦИИ, ВЫВОДИМЫЕ ИЗ НАБОРА ОХРАНЯЕМЫХ 
КОМАНД
$$ 
B_1\to SL_1\wbox B_2\to SL_2  \wbox\ldots \wbox B_n\to 
SL_n 
$$

бУДЕМ ОБОЗНАЧАТЬ ЧЕРЕЗ "IF" И "DO" ОПЕРАТОРЫ, ПОЛУЧАЕМЫЕ 
ЗАКЛЮЧЕНИЕМ ЭТОГО НАБОРА ОХРАНЯЕМЫХ КОМАНД В ПАРЫ СКОБОК "if ... 
fi" И "do ... od" СООТВЕТСТВЕННО. мЫ БУДЕМ ТАКЖЕ ИСПОЛЬЗОВАТЬ 
СОКРАЩЕНИЕ
$$ 
BB=(\exists j: 1\le j \le n: B_j) 
$$

тЕОРЕМА. (оСНОВНАЯ ТЕОРЕМА ДЛЯ КОНСТРУКЦИИ ВЫБОРА) 

иСПОЛЬЗУЯ ВВЕДЕННЫЕ ТОЛЬКО ЧТО ОБОЗНАЧЕНИЯ, МЫ МОЖЕМ СФОРМУЛИРОВАТЬ 
ОСНОВНУЮ ТЕОРЕМУ ДЛЯ КОНСТРУКЦИИ ВЫБОРА: 

пУСТЬ КОНСТРУКЦИЯ ВЫБОРА IF И ПАРА ПРЕДИКАТОВ $Q$ И $R$ ТАКОВЫ, ЧТО 
$$ 
Q \Rightarrow BB  \eqno (1) 
$$ 
И
$$ (\forall j : 1\le j \le n : (Q \and B_j) \Rightarrow \wp (SL_j, R) )           
\eqno(2) 
$$ 
ОДНОВРЕМЕННО СПРАВЕДЛИВЫ ДЛЯ ВСЕХ СОСТОЯНИЙ. тОГДА
$$ 
Q \Rightarrow \wp(IF, R) \eqno (3) 
$$
СПРАВЕДЛИВО ТАКЖЕ ДЛЯ ВСЕХ СОСТОЯНИЙ. пОСКОЛЬКУ, В СИЛУ 
ОПРЕДЕЛЕНИЯ,
$$ 
\wp(IF, R) = BB \and (\forall j: 1\le j \le n: 
B_j \Rightarrow \wp(SL_j,R)) 
$$
И, СОГЛАСНО (1), ИЗ $Q$ ЛОГИЧЕСКИ СЛЕДУЕТ ПЕРВЫЙ ЧЛЕН ПРАВОЙ ЧАСТИ, 
ТО ОТНОШЕНИЕ (3) ДОКАЗЫВАЕТСЯ, ЕСЛИ НА ОСНОВАНИИ (2) МЫ МОЖЕМ 
СДЕЛАТЬ ВЫВОД, ЧТО 
$$ 
Q \Rightarrow (\forall j: 1\le j \le n: B_j \Rightarrow \wp(SL_j,R)) \eqno(4)
$$
СПРАВЕДЛИВО ДЛЯ ВСЕХ СОСТОЯНИЙ. дЛЯ ЛЮБОГО СОСТОЯНИЯ, ПРИ
КОТОРОМ $Q$ ЯВЛЯЕТСЯ ЛОЖЬЮ, ОТНОШЕНИЕ (4) ИСТИННО В СИЛУ 
ОПРЕДЕЛЕНИЯ ЛОГИЧЕСКОГО СЛЕДОВАНИЯ. дЛЯ ЛЮБОГО СОСТОЯНИЯ, ПРИ 
КОТОРОМ $Q$ ЯВЛЯЕТСЯ ИСТИНОЙ, И ДЛЯ ЛЮБОГО ЗНАЧЕНИЯ $j$ МЫ МОЖЕМ 
РАЗЛИЧАТЬ ДВА СЛУЧАЯ: ЛИБО $B_j$ ЯВЛЯЕТСЯ ЛОЖЬЮ, НО ТОГДА 
$B_j \Rightarrow \wp(SL_j, R)$ ЯВЛЯЕТСЯ ИСТИНОЙ В СИЛУ ОПРЕДЕЛЕНИЯ 
СЛЕДОВАНИЯ, ЛИБО $B_j$ ЯВЛЯЕТСЯ ИСТИНОЙ, НО ТОГДА, СОГЛАСНО (2), 
$\wp(SL_j,R)$ ЯВЛЯЕТСЯ ИСТИНОЙ, А СЛЕДОВАТЕЛЬНО, 
$B_j \Rightarrow \wp(SL_j,R)$ ТОЖЕ ЯВЛЯЕТСЯ ИСТИНОЙ. в РЕЗУЛЬТАТЕ МЫ 
ДОКАЗАЛИ ОТНОШЕНИЕ (4), А СЛЕДОВАТЕЛЬНО, И (3).

{\sl зАМЕЧАНИЕ.} в ЧАСТНОМ СЛУЧАЕ БИНАРНОГО ВЫБОРА ($n=2$) И ПРИ 
$B_2=\non B_1$ МЫ ИМЕЕМ $BB=T$, И СЛАБЕЙШЕЕ ПРЕДУСЛОВИЕ 
ПРЕОБРАЗУЕТСЯ ТАК:
$$
\eqalign{ 
(B_1 \Rightarrow \wp(SL_1, R) ) \and (\non B_1 \Rightarrow \wp(SL_2, R)) &=\cr 
(\non B_1 \or \wp (SL_1, R) ) \and (B_1 \or \wp (SL_2, R) ) &=\cr 
(B_1 \and \wp (SL_1, R) ) \or (\non B_1 \and \wp (SL_2, R) )&\cr    
}
\eqno(5) 
$$
пОСЛЕДНЕЕ ПРЕОБРАЗОВАНИЕ ВОЗМОЖНО ПОТОМУ, ЧТО ИЗ ЧЕТЫРЕХ 
ПЕРЕКРЕСТНЫХ ПРОИЗВЕДЕНИЙ ЧЛЕН $B_1 \and \non B_1=F$ МОЖЕТ БЫТЬ 
ОТБРОШЕН, А ЧЛЕН $\wp(SL_1, R) \and \wp(SL_2, R)$ ТОЖЕ МОЖЕТ 
БЫТЬ ОТБРОШЕН ПО СЛЕДУЮЩЕЙ ПРИЧИНЕ: В ЛЮБОМ СОСТОЯНИИ, ГДЕ ОН 
ИСТИНЕН, ОБЯЗАТЕЛЬНО ЯВЛЯЕТСЯ ИСТИНОЙ КАКОЙ-ТО ОДИН ИЗ ДВУХ ЧЛЕНОВ 
ФОРМУЛЫ (5), И ПОЭТОМУ ЕГО САМОГО МОЖНО ИСКЛЮЧИТЬ ИЗ ДИЗЎЮНКЦИИ. 
фОРМУЛА (5) ИМЕЕТ ПРЯМОЕ ОТНОШЕНИЕ К ПРЕДЛОЖЕННОМУ хОАРОМ СПОСОБУ 
ОПИСАНИЯ СЕМАНТИКИ КОНСТРУКЦИИ \kwd{if}-\kwd{then}-\kwd{else} ИЗ 
ЯЗЫКА алгол 60. пОСКОЛЬКУ ЗДЕСЬ $BB=T$ ЛОГИЧЕСКИ СЛЕДУЕТ ИЗ ЧЕГО 
УГОДНО, МЫ МОЖЕМ ВЫВЕСТИ (3) ПРИ БОЛЕЕ СЛАБОМ ПРЕДПОЛОЖЕНИИ:
$$ 
((Q \and B_1) \Rightarrow \wp(SL_1,R)) \and ((Q \and \non 
B_1) \Rightarrow \wp(SL_2, R)) 
$$
{\sl (кОНЕЦ ЗАМЕЧАНИЯ.)}

тЕОРЕМa ДЛЯ КОНСТРУКЦИИ ВЫБОРА ПРЕДСТАВЛЯЕТ ОСОБУЮ ВАЖНОСТЬ В 
СЛУЧАЕ, КОГДА ПАРА ПРЕДИКАТОВ $Q$ И $R$ МОЖЕТ БЫТЬ ЗАПИСАНА В ВИДЕ 
$$ 
\eqalign{
R&=P \cr 
Q&=P \and BB \cr 
}
$$
в ЭТОМ СЛУЧАЕ ПРЕДПОСЫЛКА (1) ВЫПОЛНЯЕТСЯ АВТОМАТИЧЕСКИ, А 
ПОСКОЛЬКУ $(BB \and B_j) = B_j$, ПРЕДПОСЫЛКА (2) СВОДИТСЯ К 
ВИДУ
$$ 
(\forall j: 1\le j\le n: (P \and B_j) \Rightarrow \wp(SL_j, P)) \eqno (6) 
$$
ИЗ ЧЕГО МЫ МОЖЕМ ВЫВЕСТИ, СОГЛАСНО (3), 
$$ 
(P \and BB) \Rightarrow \wp(IF, P) \qquad\hbox{ ДЛЯ ВСЕХ СОСТОЯНИЙ } \eqno (7) 
$$

эТО ОТНОШЕНИЕ ПОСЛУЖИТ ПРЕДПОСЫЛКОЙ ДЛЯ НАШЕЙ СЛЕДУЮЩЕЙ ТЕОРЕМЫ.

{\bf тЕОРЕМА.} (оСНОВНАЯ ТЕОРЕМА ДЛЯ КОНСТРУКЦИИ ПОВТОРЕНИЕНИЯ.) 

пУСТЬ НАБОР ОХРАНЯЕМЫХ КОМАНД С ПОСТРОЕННОЙ ДЛЯ НЕГО КОНСТРУКЦИЕЙ 
ВЫБОРА IF И ПРЕДИКАТ $P$  ТАКОВЫ, ЧТО
$$ 
(P \and BB) \Rightarrow \wp(IF, P) \eqno(7) 
$$
СПРАВЕДЛИВО ДЛЯ ВСЕХ СОСТОЯНИЙ. тОГДА ДЛЯ СООТВЕТСТВУЮЩЕЙ 
КОНСТРУКЦИИ ПОВТОРЕНИЯ DO МОЖНО ВЫВЕСТИ, ЧТО
$$ 
(P \and \wp (DO, т) ) \Rightarrow \wp (DO, P \and \non BB) \eqno(8) 
$$
ДЛЯ ВСЕХ СОСТОЯНИЙ.

эТУ ТЕОРЕМУ, КОТОРАЯ ИЗВЕСТНА ТАКЖЕ ПОД НАЗВАНИЕМ "ОСНОВНАЯ  
ТЕОРЕМА ИНВАРИАНТНОСТИ ДЛЯ ЦИКЛОВ", НА ИНТУИТИВНОМ УРОВНЕ НЕ ТРУДНО 
ПОНЯТЬ. пРЕДПОСЫЛКА (7) ГОВОРИТ НАМ, ЧТО ЕСЛИ ПРЕДИКАТ $P$ 
ПЕРВОНАЧАЛЬНО ИСТИНЕН И ОДНА ИЗ ОХРАНЯЕМЫХ КОМАНД ВЫБИРАЕТСЯ ДЛЯ 
ВЫПОЛНЕНИЯ, ТО ПОСЛЕ ЕЕ ВЫПОЛНЕНИЯ $P$ СОХРАНИТ СВОЮ ИСТИННОСТЬ. 
иНАЧЕ ГОВОРЯ, ПРЕДОХРАНИТЕЛИ ГАРАНТИРУЮТ, ЧТО ВЫПОЛНЕНИЕ 
СООТВЕТСТВУЮЩИХ СПИСКОВ ОПЕРАТОРОВ НЕ НАРУШИТ ИСТИННОСТИ $P$, ЕСЛИ 
НАЧАЛЬНОЕ ЗНАЧЕНИЕ $P$ БЫЛО ИСТИННЫМ. сЛЕДОВАТЕЛЬНО, ВНЕ 
ЗАВИСИМОСТИ ОТ ТОГО, КАК ЧАСТО ПРОИЗВОДИТСЯ ВЫБОРКА ОХРАНЯЕМОЙ 
КОМАНДЫ ИЗ ИМЕЮЩЕГОСЯ НАБОРА, ПРЕДИКАТ $P$ БУДЕТ СПРАВЕДЛИВ ПРИ 
ЛЮБОЙ НОВОЙ ПРОВЕРКЕ ПРЕДОХРАНИТЕЛЕЙ. пОСЛЕ ЗАВЕРШЕНИЯ ВСЕЙ 
КОНСТРУКЦИИ  ПОВТОРЕНИЯ, КОГДА НИ ОДИН ИЗ ПРЕДОХРАНИТЕЛЕЙ НЕ 
ЯВЛЯЕТСЯ  ИСТИНОЙ, МЫ ТЕМ САМЫМ ЗАКОНЧИМ РАБОТУ В КОНЕЧНОМ 
СОСТОЯНИИ, УДОВЛЕТВОРЯЮЩЕМ $P \and \non BB$. вОПРОС В ТОМ, 
ЗАВЕРШИТСЯ ЛИ РАБОТА ПРАВИЛЬНО. дА, ЕСЛИ УСЛОВИЕ $\wp(DO, T)$ 
СПРАВЕДЛИВО И ВНАЧАЛЕ; ПОСКОЛЬКУ ЛЮБОЕ СОСТОЯНИЕ УДОВЛЕТВОРЯЕТ $T$, 
ТО $\wp(DO, T)$ ПО ОПРЕДЕЛЕНИЮ ЯВЛЯЕТСЯ СЛАБЕЙШИМ ПРЕДУСЛОВИЕМ ДЛЯ 
НАЧАЛЬНОГО СОСТОЯНИЯ, ТАКОГО, ЧТО ЗАПУСК ОПЕРАТОРА DO ПРИВЕДЕТ К 
ПРАВИЛЬНО ЗАВЕРШАЕМОЙ РАБОТЕ.

фОРМАЛЬНОЕ ДОКАЗАТЕЛЬСТВО ОСНОВНОЙ ТЕОРЕМЫ ДЛЯ КОНСТРУКЦИИ 
ПОВТОРЕНИЯ ОСНОВЫВАЕТСЯ НА ФОРМАЛЬНОМ ОПИСАНИИ СЕМАНТИКИ ЭТОЙ 
КОНСТРУКЦИИ (СМ. ПРЕДЫДУЩУЮ ГЛАВУ), ИЗ КОТОРОГО МЫ ВЫВОДИМ
$$ 
\eqalignno{
H_0(T)&=\non BB & (9) \cr 
\hbox{ПРИ $k>0$}: H_k(T)&=\wp(IF,H_{k-1}(T)) \or \non BB & (10)\cr 
H_0(P \and \non BB)&=P \and \non BB &(11)\cr 
\hbox{ПРИ $k>0$}: H_k(P \and \non BB)&=\wp(IF,H_{k-1} (P \and \non 
BB)) \or P \and \non BB &(12)\cr 
}
$$

нАЧНЕМ С ТОГО, ЧТО ДОКАЖЕМ ПОСРЕДСТВОМ МАТЕМАТИЧЕСКОЙ ИНДУКЦИИ, 
ЧТО ПРЕДПОСЫЛКА (7) ГАРАНТИРУЕТ СПРАВЕДЛИВОСТЬ
$$
 (P \and H_k(T)) \Rightarrow H_k(P \and \non BB) \eqno  (13) 
$$
ДЛЯ ВСЕХ СОСТОЯНИЙ.

в СИЛУ ОТНОШЕНИЙ (9) И (11) ОТНОШЕНИЕ (13) СПРАВЕДЛИВО ПРИ $k=0$. 
мЫ ПОКАЖЕМ, ЧТО ОТНОШЕНИЕ (13) МОЖЕТ БЫТЬ ДОКАЗАНО ПРИ 
$k=K\;(K>0)$ НА ОСНОВАНИИ ПРЕДПОЛОЖЕНИЯ, ЧТО (13) СПРАВЕДЛИВО ПРИ 
$k=K-1$.
$$ 
\eqalign{ 
P \and H_k(т)&=р \and \wp(IF, н_{K-1}т)) \or P \and \non 
BB\cr &=P \and BB \and \wp(IF, H_{K-1}(T)) \or P \and \non BB\cr 
& \Rightarrow \wp(IF, P) and wp(IF, H_{K-1}(T)) \or P \and \non BB\cr 
&=\wp(IF, P) and H_{K-1}(T)) or P and non BB\cr
& \Rightarrow wp(IF, H_{K-1} (P and non BB)) or P and non BB\cr 
&=H_K (P and non BB)\cr 
} 
$$
рАВЕНСТВО В ПЕРВОЙ СТРОКЕ СЛЕДУЕТ ИЗ (10), РАВЕНСТВО ВО ВТОРОЙ 
СТРОКЕ СЛЕДУЕТ ИЗ ТОГО, ЧТО ВСЕГДА $\wp(IF, R) \Rightarrow BB$, ЛОГИЧЕСКОЕ 
СЛЕДОВАНИЕ В ТРЕТЬЕЙ СТРОКЕ ВЫТЕКАЕТ ИЗ (7), РАВЕНСТВО В 
ЧЕТВЕРТОЙ СТРОКЕ ОСНОВЫВАЕТСЯ НА СВОЙСТВЕ 3 ПРЕОБРАЗОВАТЕЛЕЙ 
ПРЕДИКАТОВ, СЛЕДОВАНИЕ В ПЯТОЙ СТРОКЕ ВЫТЕКАЕТ ИЗ СВОЙСТВА 2 
ПРЕОБРАЗОВАТЕЛЕЙ ПРЕДИКАТОВ И ИЗ ИНДУКТИВНОГО  ПРЕДПОЛОЖЕНИЯ (13) 
ДЛЯ $k=K-1$, И ПОСЛЕДНЯЯ СТРОКА СЛЕДУЕТ ИЗ (12). иТАК, МЫ 
ДОКАЗАЛИ (13) ДЛЯ $k=K$, А СЛЕДОВАТЕЛЬНО, ДЛЯ ВСЕХ ЗНАЧЕНИЙ $k 
\ge 0$. 

нАКОНЕЦ, ДЛЯ ЛЮБОЙ ТОЧКИ В ПРОСТРАНСТВЕ СОСТОЯНИЙ МЫ ИМЕЕМ, В 
СИЛУ (13),
$$ 
\eqalign{ 
P \and \wp(DO, T) &= (\exists k: k\ge 0: P and H_k(T))\cr 
& \Rightarrow (\exists k: k\ge 0 : H_k (P \and \non BB))\cr 
&=\wp(DO, P \and \non BB)\cr 
} 
$$
И ТЕМ САМЫМ ДОКАЗАНА ОСНОВНАЯ  ТЕОРЕМА  (8) ДЛЯ КОНСТРУКЦИИ 
ПОВТОРЕНИЯ. цЕННОСТЬ ОСНОВНОЙ ТЕОРЕМЫ ДЛЯ КОНСТРУКЦИИ ПОВТОРЕНИЯ 
ОСНОВЫВАЕТСЯ НА ТОМ, ЧТО НИ В ПРЕДПОСЫЛКЕ, НИ В ЕЕ СЛЕДСТВИИ НЕ 
УПОМИНАЕТСЯ ФАКТИЧЕСКОЕ ЧИСЛО ВЫБОРОК ОХРАНЯЕМОЙ КОМАНДЫ. пОЭТОМУ 
ОНА ПРИМЕНИМА ДАЖЕ В ТЕХ СЛУЧАЯХ, КОГДА ЭТО ЧИСЛО НЕ ОПРЕДЕЛЯЕТСЯ 
НАЧАЛЬНЫМ СОСТОЯНИЕМ.

\bye