\input style
\chapter{5 dve teoremy}
v |TOJ GLAVE MY VYVODIM DVE TEOREMY OB OPERATORAH, KOTORYE STROYATSYA 
IZ NABOROV OHRANYAEMYH KOMAND. pERVAYA TEOREMA KASAETSYA KONSTRUKCII 
VYBORA if-fi, A VTORAYA --- KONSTRUKCII POVTORENIYA do-od. v |TOM GLAVE 
MY BUDEM RASSMATRIVATX KONSTRUKCII, VYVODIMYE IZ NABORA OHRANYAEMYH 
KOMAND
$$ 
B_1\to SL_1\wbox B_2\to SL_2  \wbox\ldots \wbox B_n\to 
SL_n 
$$

bUDEM OBOZNACHATX CHEREZ "IF" I "DO" OPERATORY, POLUCHAEMYE 
ZAKLYUCHENIEM |TOGO NABORA OHRANYAEMYH KOMAND V PARY SKOBOK "if ... 
fi" I "do ... od" SOOTVETSTVENNO. mY BUDEM TAKZHE ISPOLXZOVATX 
SOKRASHCHENIE
$$ 
BB=(\exists j: 1\le j \le n: B_j) 
$$

tEOREMA. (oSNOVNAYA TEOREMA DLYA KONSTRUKCII VYBORA) 

iSPOLXZUYA VVEDENNYE TOLXKO CHTO OBOZNACHENIYA, MY MOZHEM SFORMULIROVATX 
OSNOVNUYU TEOREMU DLYA KONSTRUKCII VYBORA: 

pUSTX KONSTRUKCIYA VYBORA IF I PARA PREDIKATOV $Q$ I $R$ TAKOVY, CHTO 
$$ 
Q \Rightarrow BB  \eqno (1) 
$$ 
I
$$ (\forall j : 1\le j \le n : (Q \and B_j) \Rightarrow \wp (SL_j, R) )           
\eqno(2) 
$$ 
ODNOVREMENNO SPRAVEDLIVY DLYA VSEH SOSTOYANIJ. tOGDA
$$ 
Q \Rightarrow \wp(IF, R) \eqno (3) 
$$
SPRAVEDLIVO TAKZHE DLYA VSEH SOSTOYANIJ. pOSKOLXKU, V SILU 
OPREDELENIYA,
$$ 
\wp(IF, R) = BB \and (\forall j: 1\le j \le n: 
B_j \Rightarrow \wp(SL_j,R)) 
$$
I, SOGLASNO (1), IZ $Q$ LOGICHESKI SLEDUET PERVYJ CHLEN PRAVOJ CHASTI, 
TO OTNOSHENIE (3) DOKAZYVAETSYA, ESLI NA OSNOVANII (2) MY MOZHEM 
SDELATX VYVOD, CHTO 
$$ 
Q \Rightarrow (\forall j: 1\le j \le n: B_j \Rightarrow \wp(SL_j,R)) \eqno(4)
$$
SPRAVEDLIVO DLYA VSEH SOSTOYANIJ. dLYA LYUBOGO SOSTOYANIYA, PRI
KOTOROM $Q$ YAVLYAETSYA LOZHXYU, OTNOSHENIE (4) ISTINNO V SILU 
OPREDELENIYA LOGICHESKOGO SLEDOVANIYA. dLYA LYUBOGO SOSTOYANIYA, PRI 
KOTOROM $Q$ YAVLYAETSYA ISTINOJ, I DLYA LYUBOGO ZNACHENIYA $j$ MY MOZHEM 
RAZLICHATX DVA SLUCHAYA: LIBO $B_j$ YAVLYAETSYA LOZHXYU, NO TOGDA 
$B_j \Rightarrow \wp(SL_j, R)$ YAVLYAETSYA ISTINOJ V SILU OPREDELENIYA 
SLEDOVANIYA, LIBO $B_j$ YAVLYAETSYA ISTINOJ, NO TOGDA, SOGLASNO (2), 
$\wp(SL_j,R)$ YAVLYAETSYA ISTINOJ, A SLEDOVATELXNO, 
$B_j \Rightarrow \wp(SL_j,R)$ TOZHE YAVLYAETSYA ISTINOJ. v REZULXTATE MY 
DOKAZALI OTNOSHENIE (4), A SLEDOVATELXNO, I (3).

{\sl zAMECHANIE.} v CHASTNOM SLUCHAE BINARNOGO VYBORA ($n=2$) I PRI 
$B_2=\non B_1$ MY IMEEM $BB=T$, I SLABEJSHEE PREDUSLOVIE 
PREOBRAZUETSYA TAK:
$$
\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) 
$$
pOSLEDNEE PREOBRAZOVANIE VOZMOZHNO POTOMU, CHTO IZ CHETYREH 
PEREKRESTNYH PROIZVEDENIJ CHLEN $B_1 \and \non B_1=F$ MOZHET BYTX 
OTBROSHEN, A CHLEN $\wp(SL_1, R) \and \wp(SL_2, R)$ TOZHE MOZHET 
BYTX OTBROSHEN PO SLEDUYUSHCHEJ PRICHINE: V LYUBOM SOSTOYANII, GDE ON 
ISTINEN, OBYAZATELXNO YAVLYAETSYA ISTINOJ KAKOJ-TO ODIN IZ DVUH CHLENOV 
FORMULY (5), I PO|TOMU EGO SAMOGO MOZHNO ISKLYUCHITX IZ DIZ®YUNKCII. 
fORMULA (5) IMEET PRYAMOE OTNOSHENIE K PREDLOZHENNOMU hOAROM SPOSOBU 
OPISANIYA SEMANTIKI KONSTRUKCII \kwd{if}-\kwd{then}-\kwd{else} IZ 
YAZYKA algol 60. pOSKOLXKU ZDESX $BB=T$ LOGICHESKI SLEDUET IZ CHEGO 
UGODNO, MY MOZHEM VYVESTI (3) PRI BOLEE SLABOM PREDPOLOZHENII:
$$ 
((Q \and B_1) \Rightarrow \wp(SL_1,R)) \and ((Q \and \non 
B_1) \Rightarrow \wp(SL_2, R)) 
$$
{\sl (kONEC ZAMECHANIYA.)}

tEOREMa DLYA KONSTRUKCII VYBORA PREDSTAVLYAET OSOBUYU VAZHNOSTX V 
SLUCHAE, KOGDA PARA PREDIKATOV $Q$ I $R$ MOZHET BYTX ZAPISANA V VIDE 
$$ 
\eqalign{
R&=P \cr 
Q&=P \and BB \cr 
}
$$
v |TOM SLUCHAE PREDPOSYLKA (1) VYPOLNYAETSYA AVTOMATICHESKI, A 
POSKOLXKU $(BB \and B_j) = B_j$, PREDPOSYLKA (2) SVODITSYA K 
VIDU
$$ 
(\forall j: 1\le j\le n: (P \and B_j) \Rightarrow \wp(SL_j, P)) \eqno (6) 
$$
IZ CHEGO MY MOZHEM VYVESTI, SOGLASNO (3), 
$$ 
(P \and BB) \Rightarrow \wp(IF, P) \qquad\hbox{ DLYA VSEH SOSTOYANIJ } \eqno (7) 
$$

eTO OTNOSHENIE POSLUZHIT PREDPOSYLKOJ DLYA NASHEJ SLEDUYUSHCHEJ TEOREMY.

{\bf tEOREMA.} (oSNOVNAYA TEOREMA DLYA KONSTRUKCII POVTORENIENIYA.) 

pUSTX NABOR OHRANYAEMYH KOMAND S POSTROENNOJ DLYA NEGO KONSTRUKCIEJ 
VYBORA IF I PREDIKAT $P$  TAKOVY, CHTO
$$ 
(P \and BB) \Rightarrow \wp(IF, P) \eqno(7) 
$$
SPRAVEDLIVO DLYA VSEH SOSTOYANIJ. tOGDA DLYA SOOTVETSTVUYUSHCHEJ 
KONSTRUKCII POVTORENIYA DO MOZHNO VYVESTI, CHTO
$$ 
(P \and \wp (DO, t) ) \Rightarrow \wp (DO, P \and \non BB) \eqno(8) 
$$
DLYA VSEH SOSTOYANIJ.

eTU TEOREMU, KOTORAYA IZVESTNA TAKZHE POD NAZVANIEM "OSNOVNAYA  
TEOREMA INVARIANTNOSTI DLYA CIKLOV", NA INTUITIVNOM UROVNE NE TRUDNO 
PONYATX. pREDPOSYLKA (7) GOVORIT NAM, CHTO ESLI PREDIKAT $P$ 
PERVONACHALXNO ISTINEN I ODNA IZ OHRANYAEMYH KOMAND VYBIRAETSYA DLYA 
VYPOLNENIYA, TO POSLE EE VYPOLNENIYA $P$ SOHRANIT SVOYU ISTINNOSTX. 
iNACHE GOVORYA, PREDOHRANITELI GARANTIRUYUT, CHTO VYPOLNENIE 
SOOTVETSTVUYUSHCHIH SPISKOV OPERATOROV NE NARUSHIT ISTINNOSTI $P$, ESLI 
NACHALXNOE ZNACHENIE $P$ BYLO ISTINNYM. sLEDOVATELXNO, VNE 
ZAVISIMOSTI OT TOGO, KAK CHASTO PROIZVODITSYA VYBORKA OHRANYAEMOJ 
KOMANDY IZ IMEYUSHCHEGOSYA NABORA, PREDIKAT $P$ BUDET SPRAVEDLIV PRI 
LYUBOJ NOVOJ PROVERKE PREDOHRANITELEJ. pOSLE ZAVERSHENIYA VSEJ 
KONSTRUKCII  POVTORENIYA, KOGDA NI ODIN IZ PREDOHRANITELEJ NE 
YAVLYAETSYA  ISTINOJ, MY TEM SAMYM ZAKONCHIM RABOTU V KONECHNOM 
SOSTOYANII, UDOVLETVORYAYUSHCHEM $P \and \non BB$. vOPROS V TOM, 
ZAVERSHITSYA LI RABOTA PRAVILXNO. dA, ESLI USLOVIE $\wp(DO, T)$ 
SPRAVEDLIVO I VNACHALE; POSKOLXKU LYUBOE SOSTOYANIE UDOVLETVORYAET $T$, 
TO $\wp(DO, T)$ PO OPREDELENIYU YAVLYAETSYA SLABEJSHIM PREDUSLOVIEM DLYA 
NACHALXNOGO SOSTOYANIYA, TAKOGO, CHTO ZAPUSK OPERATORA DO PRIVEDET K 
PRAVILXNO ZAVERSHAEMOJ RABOTE.

fORMALXNOE DOKAZATELXSTVO OSNOVNOJ TEOREMY DLYA KONSTRUKCII 
POVTORENIYA OSNOVYVAETSYA NA FORMALXNOM OPISANII SEMANTIKI |TOJ 
KONSTRUKCII (SM. PREDYDUSHCHUYU GLAVU), IZ KOTOROGO MY VYVODIM
$$ 
\eqalignno{
H_0(T)&=\non BB & (9) \cr 
\hbox{PRI $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{PRI $k>0$}: H_k(P \and \non BB)&=\wp(IF,H_{k-1} (P \and \non 
BB)) \or P \and \non BB &(12)\cr 
}
$$

nACHNEM S TOGO, CHTO DOKAZHEM POSREDSTVOM MATEMATICHESKOJ INDUKCII, 
CHTO PREDPOSYLKA (7) GARANTIRUET SPRAVEDLIVOSTX
$$
 (P \and H_k(T)) \Rightarrow H_k(P \and \non BB) \eqno  (13) 
$$
DLYA VSEH SOSTOYANIJ.

v SILU OTNOSHENIJ (9) I (11) OTNOSHENIE (13) SPRAVEDLIVO PRI $k=0$. 
mY POKAZHEM, CHTO OTNOSHENIE (13) MOZHET BYTX DOKAZANO PRI 
$k=K\;(K>0)$ NA OSNOVANII PREDPOLOZHENIYA, CHTO (13) SPRAVEDLIVO PRI 
$k=K-1$.
$$ 
\eqalign{ 
P \and H_k(t)&=r \and \wp(IF, n_{K-1}t)) \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 
} 
$$
rAVENSTVO V PERVOJ STROKE SLEDUET IZ (10), RAVENSTVO VO VTOROJ 
STROKE SLEDUET IZ TOGO, CHTO VSEGDA $\wp(IF, R) \Rightarrow BB$, LOGICHESKOE 
SLEDOVANIE V TRETXEJ STROKE VYTEKAET IZ (7), RAVENSTVO V 
CHETVERTOJ STROKE OSNOVYVAETSYA NA SVOJSTVE 3 PREOBRAZOVATELEJ 
PREDIKATOV, SLEDOVANIE V PYATOJ STROKE VYTEKAET IZ SVOJSTVA 2 
PREOBRAZOVATELEJ PREDIKATOV I IZ INDUKTIVNOGO  PREDPOLOZHENIYA (13) 
DLYA $k=K-1$, I POSLEDNYAYA STROKA SLEDUET IZ (12). iTAK, MY 
DOKAZALI (13) DLYA $k=K$, A SLEDOVATELXNO, DLYA VSEH ZNACHENIJ $k 
\ge 0$. 

nAKONEC, DLYA LYUBOJ TOCHKI V PROSTRANSTVE SOSTOYANIJ MY IMEEM, V 
SILU (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 
} 
$$
I TEM SAMYM DOKAZANA OSNOVNAYA  TEOREMA  (8) DLYA KONSTRUKCII 
POVTORENIYA. cENNOSTX OSNOVNOJ TEOREMY DLYA KONSTRUKCII POVTORENIYA 
OSNOVYVAETSYA NA TOM, CHTO NI V PREDPOSYLKE, NI V EE SLEDSTVII NE 
UPOMINAETSYA FAKTICHESKOE CHISLO VYBOROK OHRANYAEMOJ KOMANDY. pO|TOMU 
ONA PRIMENIMA DAZHE V TEH SLUCHAYAH, KOGDA |TO CHISLO NE OPREDELYAETSYA 
NACHALXNYM SOSTOYANIEM.

\bye