\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