\input style
\chapter{4 ������������� �������������� ������ 
����������������}
� ���������� ����� �� ��������� �����, ��� ����� ��������� 
����������� $S$ ���������� ������, ���� ����� �� 
"��������������� ����������", �. �. �������, ����������� ���, 
��� ������� �� ������ ����������� $R$ ��������������� 
��������� ����������� (������� �� ���������� ����� 
$\wp(S, R))$, ��������������� �� ��������� ���������, ��� 
������� ������ �������� � ������� ����������� ����������, 
������ ������� ��������� � �������� ���������, 
��������������� ����������� $R$. ⎏��� � ���, ��� �������� 
$\wp(S, R)$ ��� �������� $S$ � $R$.

���� ���� ������ �� ��������� ���������� ����������� $S$. 
������, ���������� �� ������ ������������ ����� 
����������������, ����� ��������������� ��� ����� 
�����������, ����� �����������, ������� �� ����� ���������� 
������, ���� ����� ��������������� ��������������� ���������� 
������ ���� ���������������� ������� ������ ��� ��� �������, 
��� ��� ����� ��������� ��� ������ ������ ��������� ��������, 
� ��� ���� ���� �������� ��� ���������� ����� ��������������� 
�� ��������������� ����������.

 ꀆ��� ����� ��������� �������� ����� ������� �� ������ 
������������ ����� ����������������, � ������� �� ����� 
������ ������� ��� ��� ��������� ������. � ������ ����� ���� 
���������� ����������� ��� ���������� ��������� ���������� 
������ ������ ���������. � ����� �������, ����� ��������� 
������������ ��� \emph{��������} �������������, ���� �� 
�����, ����� ��� ����� ����������� �������������, ���� �� 
�����, ����� �� ��� ��� ��� ��� ���������� �����-���� 
���������� ������. � ������ �������, ����������, ����� ����� 
��������� ������� \emph{���} � ���, ��� ������� 
��������������� ��������������� ����������, ��� ����������� 
�������������� ����������, ����� �������� ����������� 
$\wp(S, R)$ ��� ������ ������� ����������� $R$, ������� ��� 
������-���� ��������������. ��� ��������� ��������� ������, 
��� ��������������� ��� "������ ������������ ������ 
����������������" � \emph{�����} ����� ������. ꎃ�� 
��������� ���������� ����������� (��� ���������) �������� �� 
���������������� ����������, �� ������������� ������������� 
�������������� ����� ���������������� ��� ����� ������, 
������� ��������� ����� ���������, ���������� �� ���� �����, 
��������� � ������������ ��������������� ����������. � ����� 
����� ������ �� ����� ������������� ��������� ��� "���" ��� 
���������������� ��������������� ����������.

 ������� ����� ������� � �������� �������������� ����� 
���������������� � ����� �������. 쎆�� ����������������� 
(�������� ���������) ���, ��� ������� ���������� 
���������������� ���������� ������ ���� ������, �����, 
�������� ��, ������ ���� ��������� ������ �������, ����� ��� 
��������������� ����������, ����������� ���������� 1--4 �� 
���������� �����. � ����� ����, ���� ������� �� ���� ����� 
��������, �� ��� ��������, ��� �� ������������ ��������� 
����� �������, ��� ��� ��� �� ����� ������������������ ��� 
����������� � ��������������� ��������� �����������.

񐀇� ������������� ��� ������� ������ ������� 
���������������� ����������, ������� �������� ���������� 
����������.

퀗��� � �������������� ��������������, �. �, � ����������� 
$S$, �����, ��� ��� ������ ����������� $R$ �� ����� 
$\wp(S, R)=R$. ��� ����������� ����� � ����� ��� 
������������: ��� �������� �� ��� ��������� "������ 
onepa���", � � ����� ���������� ��� ����� ���������� ��, 
�������� ������� � ��� ����� ������, ��� ������������� 
��������� �����-�� ��������. ��� �� ������� ���������� ����� 
(���������� ������ �����, ��� �� "�����" ���� ��������, �� 
��� ���������, ���  �� ������ ��  �����, � ������� �� ����� 
���� ����������� ������������,  ������, "\var{����������}". 
蒀�, ��������� ��������� "\var{����������}"  ������������ 
��������� �������: 
$$
 \wp(\var{����������}, R)=R\qquad\hbox{ ��� ������ ����������� $R$ }
$$

 (ꀊ � ���, � ���� ������������ �������� "��������", 
��������� �� ������ ����� � ������. ꎃ�� ���� ����������, 
��� "�������" ����� �� ��������� ����� ���������� ��������, 
���� ��� �������  ������%
\note{  � �������� �� ��������� ���������� ������ 
"statement"  (�����������, �����������) �������� "��������", 
��������� � ���������������� �. �. 럏������, � ����� 
�������, ������� �������� ����������� � ����� �������� 
���������, ��� ����������.---{\it �. ���.} }.)

{\sl 瀌����ue.} �, ��� ������� ���������������� �������� 
�������� ������ ����� "\var{����������}" ��� ������� 
���������, ����� "�����" ����� ������������ �������� ��� 
���������, ������� ��������, ��� ���������� ������� 
��������� ��������� ��������� ������ ��������� �������� 
������� "0" ��� ������� "�����". {\sl (ꎍ�� ���������.)}

��� ��� ���������� ���� �����������, ��� �������� �� �� 
�������� ����������� ��������, ��� ��� �������� �� ��� 
���������� ����� ���� ����������������. ����� �������� 
������ ����: ��� ��������������� ����, � ������� ����� 
������� ������ ���� �����������, ������ ������������, ��� 
�������� ������� ��� ��� ������ �����������, ��� "�������� 
�ce, ��� ����" (��� "������ �� ������", �� ����� ���������� 
������������ ����� ������������ ���������, ��. ��������� 
�����).

䐓��� ������� ��������������� ���������� �������� � 
����������y ���������� �����������, ������� ����� �� ������� 
�� ����������� $R$. � ����� ��� ���������-���������, $T$ � 
$F$. ꎍ�������� $S$, ��� �������  $\wp(S, R)=T$ ��� ���� 
$R$, �� ����� ������������, ������ ��� ��� �������� �� ����� 
������������ ����. ��� ����������� $S$, ��� ������� 
$\wp(S,R)=F$ ��� ���� $R$, �������� ���������������� 
����������, ��������������� ���� ����������� ���������. ����� ��������� 
�� ���� �������� ���, ������� ��� "\var{��������}". 
蒀�, ��������� ��������� "\var{��������}" �������� ��������� �������:
$$
 \wp (\var{��������}, R) = F\qquad\hbox{ ��� ������ ����������� R} 
$$
���� �������� �� ����� ���� "������ �� ������" � ������ 
"�������� ���, ��� ����"; �� ������ �� �� ��� �� ��������. 
呋� �� �������� $R=T$, �. �. �� ����������� �� �������� 
��������� ������� �������������� ����������, ����� ������ 
����� ��� �������������, ���� ����� �� �������� 
���������������� ���������� ���������. 呋� ��������� 
����������� �� ����� "\var{��������}", ��� �� ������ ������� 
��������� ���������: ���� ������� �� ������� �������� 
��������� �������. (퀑 �� ������ �������� ������ (� ����� � 
������������) ��, ��� ������� �� ������ ��������� 
����������, � ������� ���������� ��� ������� ������ 
������������� ����������� ��� "\var{����������}" � 
"\var{��������}".)

򅏅�� �� ����������� ����� (��� ��� ������ ����������) 
��������������� ������ ����������������, � ������� ����� 
������� ��� �����������; ���� �� ��� ������ �� ������, � 
������ ������ ������ �������. � ������� ������������� 
����������� "񎁙���� �� ��������������� ����� ����� 60" � 
1960~�. ������� ��������� ���� ������, ������������ 
�����������������, �� �������� ���� �������� �� ���� ����� 
��� ����������� ����������� ���������� ����� ������ 
������������ ����� ���������������� � ������� �����������, 
���������� "���" (���������� �� "펐������� ����� ᝊ���"), 
� ������:
$$  
\<��������>:: = \var{����������} | \var{��������}
$$
(�������� ���: "������� �������������� ���������, ��������� 
"��������" (������ ��� ���������� �������� ������ "$<$" � 
"$>$"), ������������ ��� (��� ���������� ���� "$::=$") 
"\var{����������}" ��� (��� ���������� ������������ ����� 
"$|$") "\var{��������}". ꎋ��������! � �� ������������; 
����� ������������ ���������� ��� � �������� ������� ������ 
��������� � ���������� �����.)

� ����� ���������� ����� ���������� ���������������� 
���������� ������������ �� �����������, �. �. ��  ������ 
���� ��������� ������ ���������� � ���������� ��������� ��� 
����������� $R$ �� (���� � �� ��) "���-������ ������". 呋� 
� ��������� $R$ ��� ��������� ���������� $x$ ���������� 
��������� ���������� $(E)$, �� �� ���������� ��������� ����� 
�������������� ����� $R_{E\to X}$. 򅏅�� �� ����� 
����������� ��� �������� $x$ � $E$ ����� �����������, ����� 
��� ����� ����������� $R$ ���������� $\wp(S, R) =R_{E\to X}$; 
����� $x$ --- "������������ ����������" ������ ������������ 
���������, � $E$ ---  ��������� ���������������� ����.

{\sl 瀌������.} 򀊎� �������������� ����� ����������� 
������������� ��������� 1--4 �� ���������� �����. � �� 
������ �������� ��������������� ��� � ����������� ������  
�������� ������ � ����������� �� ������ �����, ����� �� �� 
���������� � ����� ��� � ������������ ��� �� ��� � ��������� 
��������������� ����������. {\sl(ꎍ�� ���������.)}

򀊈� �������� �������� ����� ����� ���������������� 
����������, ����� ����� �����������.  ������������ 
����������, ������� ���������� "�������� ������������"; 
����� �������� ������ ���������� ��� ����:

1) ������������ ����������, ���������� ������; 

2) ��� ����, ��� �������, ��������������� �������������� 
����������, ���� �����������;

 3) ���������, ������� ������ ���������� ������ ��������� 
���� ���������� � �����������.

呋� ���������� $x$ ������ ���� �������� ���������� $(E)$ �� 
������� ������ ������ ��������� �������� ���������
�������: 
$$  
x:=E 
$$ 
(��� ��� ���������� ���� ������������ ":=" ������� ������ ��� 
"����������"). 

񊀇����� ����� �����������, ���������
$$ 
\wp("x:=E", R) =R_{E\to X} \qquad\hbox{䋟 ������ ����������� $R$}
$$

 ������� ��� ����� ������������� ��� ������������� 
����������� ��������� ������������ ��� ����� ������������ 
���������� $x$ � ������ ��������� $E$ ���������������� ����. 
퀑��������, �� ������ �����������, ������������� ���, �� 
����� ��������� ��� ���������� ���������, ����� �� ������� 
���:
$$ 
\eqalign{
&\<��������> ::=\var{����������}|\var{��������}|\<�������� ������������> 
\cr
&\<�������� ������������> ::=\<����������> := \<���������> \cr
}
$$
������ ��������� ������� ������� ������ ���: "������� 
�������������� ���������, ��������� "�������� ������������", 
������������ ��� ������� �������������� ���������, ��������� 
"����������", �� ������� ������� ������� ���� ������������ 
"$:=$", � ����� ������� �������������� ���������, ��������� 
"���������".
�� ��� ��� ���������� �����������, �������������� �������� 
��������� � ���, ��� ���� ���������� ��������� ��������� 
������������ � ����� ���� ������������ ���� ����������� 
��������� ��������� ������������ --- ���� ��� � ��� ����! 
���������� ������������ ��������� � ����� ������ 
������������� ����������� "$a$" � "$b$". 򎃄�
$$ 
\wp("a:=7", a=7)= \{7=7\} 
$$
�, ��������� ���������� ��������� � ������ ����� �������� 
������� ��� ���� �������� $a$ � $b$, �. �. ��� ���� ����� 
������������ ���������, �� ����� ��������� �������� ��� ���:
$$ 
\wp("a:=7", a=7)=T 
$$
荀�� ������, ������ ��������� ��������� �����������, ��� 
������������ "$a:=7$" ��������� ���������� "$a=7$". ����������
$$ 
\wp("a:=7", a=6) = \{7=6\} 
$$
�, ��������� ��� ���������� ��������� �������� ����� ��� ���� 
�������� $a$ � $b$, �� ��������
$$
 \wp( "a:=7", a=6)=F 
$$

��� ��������, ��� �� ���������� �������� ���������� ���������, ��� 
�������� �� ����� �� �������������, ��� ������������ "$a:=7$" 
��������� ���������� "$a=6$". (��� ��������� � ����������� � ����� 
���������� �����������, ��� ��� ��������� ��������� ��������� 
�������� ���������� "$a=7$", �  �������������, �������� �������� 
"$a\not=7$".) 䀋��,
$$ 
\wp ("a:=7", b=b0)=\{b=b0\}
$$
�. �. ���� �� ����� �������������, ��� ����� ������������ "$a:=7$" 
���������� b ����� ��������� �������� $b0$, �� �����, ����� $b$ ����� 
��� �������� ��� � ��������� ���������. 䐓���� �������, ��� 
����������, �� ����������� "$a$", �� ����������, ��� ��������� �� 
��������, ������� ����� ������; ������������ "$a:=7$" ���������� � 
������������ ��������� �����, ��������������� �������� ��������� 
�������, ����������� ��� $a$  ���, ��� �������������� �������� 
���������� ��������� "$a=7$".

⌅��� ���� ����� ����� � �������� ��������� $E$ ���������,  �� 
����� �� ����� �����-�� ������� �� ����������  ���������. ��� 
�������������� ���������� ���������:
$$ 
\eqalign{
&\wp("a:=2*b+1", a=13)=\{2*b+1=13\}=\{b=6\} \cr
&\wp ("a: =a +1", a>10)=\{a+1>10\}=\{a>9\} \cr
&\wp("a:=a-b", a>b) = \{a-b>b\}=\{a>2*b\} \cr
}
$$

⎇������ ��������� ����������, ���� �� ��������� ��������� $E$ ���� 
�������� ������������ �������� ������������ ���������, �. �. ����� 
��������, ������� ���������� ������� ��� ���������� ���������, �� 
��������� � ������� �����������, �� �������� � ��������� ����������� 
������. 呋� �� ����� ������������� � ��� ��������, �� ��� ����� 
�������� ���� ����������� ��������� ��������� ��������������� � 
��������
$$ 
\wp ("x:=E", R) = \{D(E) \cand R_{E \to X}\} 
$$
焅�� �������� $D(E)$ �������� "� ������� ����������� $E$"; 
���������� ��������� "$B1 \cand B2$" (��� ���������� "�������� 
����������") ����� �� �� ��������, ��� � "$B1\and B2$", ���� ��� 
�������� ����������, �� ������ ����� �� ����������� ��� ����� 
�������� "����", ���� $B1$ �������� "�����"; ���������  ����������� 
��� ����������� �� ����, ��������� �� ������� $B2$. ��� ������� 
$D(E)$ �� �������������� ���� ���� ������, ��� ���=$T$, ���� ������, 
��� �� ������� �� �������������, ��� �������� ������������ ������� 
�� ����� ������� � ��������� ����������, ��  ������������� ������� 
����������� ��������� $E$.

呒��������� ���������� ��������� ������������ �������� 
����������� ���������� �������������� ��� ���������� 
"������������� ������������". � ���� ������ �������� 
������������� ������ ��� ���������� \emph{���������}����������. 
����� �������������� ������������ 
������������ ������� ��������� ����������), ���������� 
������ (��� ���������� ����������� ��������), ����� �� ����� 
������������ � ����� �� ����������� ������� ��������� (����� 
����������� ��������) ������ �� ����� ������������. 蒀�, 
����������� ������
$$ 
x1,x2:=E1, E2 \qquad x1,x2, x3:=E1, E2, E� 
$$
瀌����, ��� $i$-�  ���������� �� ������ ����� ����� ������ 
���� �������� �� $i$-e ��������� �� ������ ������ �����, ��� 
���, ��������, ��� �������� $x1$, $x2$, $E1$ � $E2$ ��������
$$ 
x1, x2:=E1,E2 
$$ 
������������ ������������ ��������� 
$$ 
x2,x1:=E2,E1 
$$
���������� ������������ ��������� ��� ����������, ����� 
��� ���������� $x$ � $y$ ���������� ������ ���������� � 
������� ���������
$$ 
x, y:=y, x 
$$
� ���� ������ ��� �������� ��������� �� ����� ����������. 
녃����� ���������� �������������� ������������ � 
����������� � ��� ������� �������� ��������� ������������ 
������ �������� ��������� ������������ ����� ����������. 
瀌����, ��� ���� ������ ���������� ������� ��������, �� 
���������� ��������� ���������� ������ ���������������. 

葒����� �������� ��� �������� ���� ���������, ��������� ��� 
��������� ����� ��� ��������� ������������, ��������� 
�������:
$$ 
\eqalign{
\<�������� ������������>::=&\<����������>:=\<���������> | \cr
 &\<����������>,  \<�������� ������������>, \<���������> \cr
}
$$
��� ��� ���������� "����������� �����������", ��������� ���� 
�� �������������� ���� ��� �������������� �������, ��������� 
"�������� ������������" (� ������ ������ �����), �������� � 
�������� ������ �� ����� ����������� �����
��� �� �������������� �������, ��������� "�������� ������������", 
�. �. �� ����� �������������� �������, ������� �� ����������! � 
������ ������ ����� ����������� ����������� �������� ��������, �� 
����� ����� ������������� �������� �� ����� ��������� � ���, ���, 
�� ������� ���� � �������������� ����� ������, � ���� ��� ������ 
�������������. 퀏�����, ���������, �������� ������ ������������,
$$ 
x2:=E1 
$$
�������� �������� ��������� ������������, �� �������
$$ 
x1,x2:=E1, E2 
$$
��������� ������ ���� 
$$ x1, \<�������� ������������>, E2 
$$
� �������������, �������� ������ ������������, ����� �������� 
���������� ������������. ��� � ������������� ����� ������ ��� 
�������������, ������ ��� ����������, ��� $E2$ ������������� � 
$x1$ ������ ����, ����� ��������������� � $x2$.

� ��������� � ��������������� ������, ���������� ������ 
"����������" � "��������", ��� ���� � ���������� ������������ 
�������� ����������� ����� �������: ��� ��� ����� �� �� �� ���� 
������� ������� ��� ����� ��������� �������� �������������� 
������� "�������� ������������". � �� ��� �� ���� ������������ 
��� ����� �����; ��� ����� ����������� ������� ����� ���������� 
���������, ����� ������� �����������. 䋟 ���������� ������������ 
������� ����������� �� ���������� ������, ������� ����� 
���������� ������� ���:
$$
\displaylines{
\<�����������>::=\<������� �����������>| \hfill\cr
\hfill\<���������� ���������� ������� ����: {\<�����������>} >\cr
}
$$ 

䋟 ���� ����� ��� ����� ����� �������� ���� �����-������ ������, 
���������� ���������� ���� �������: � ����� ������������ ������ 
������� "������� �����������", ����� ���� � ���� ������, �, ����� 
����, �� ������ �����, ��� ������� "���������� ����������". 
₅������ ������ ��������� ����� ����� � �������� ������� 
�����������; ���������� ����� ���� ����� ��������� ������ 
�������� ���������� ���������� ������ ����� ����������� �� 
�������� �����������. 펂�� ����������� � ���� ������� ����� 
��������� � ���� ����� ��� ����� ��������  ���������� �������. 

�� ����, ��� ������ ��� ��������� ����������� ������, �� ����� 
������������� ��� ����� ���������. �-������, ��
����� ������� ��� "������������ �����", ����������� ��� �������� 
� ������� ��� ������� ������� ��� ���������� (��� �������� �� �� 
���� ��� ��� ���������).  ����� ������� ����������� ������ 
�������� �����������; �� ����� �����oro ��������, ����� ������� 
��� ���������� �� ����� ������. � ����� ����� ������ ����� ��� 
�����������, ���������� ����������� ����������, ������������. 苈 
�� �� ������������� ����������� ��� "��������� ������", 
������������ ���, ��� �� ����� ������, ������ ��� �������� 
������������ ����������.  ���� �� ������������ ����� ��� 
"�����" ������������ �����, ��� ������� ����������� � ������ 
������ �� ����� ��������. ⒎��� ������ ������ ������� � ��, ��� 
�� �������� ��� "�����������". ꎌ������� ������  ����������, ��� 
�������� ������ ������� �� ������� ������.

�� ���� ����� ��������� �������� � ����� ���������� 
������������, �������� �������, ��� �� �������, ���������� �� 
����������������� ����������. 򎗍�� ������, ���� ������ ��� 
����������� $S1$ � $S2$, ��� ��������������� ���������� ��������, 
����� �� �� ����������� ���� ������� ������ ������ 
��������������� ���������� �� ���� ��������? 呋� ��, �� �� ����� 
������� �������������� ��������������� ���������� ��������� 
������� ���������� �������, ������������ ����������� ������� �� 
������ $S1$ � $S2$. 

�� �� ���������� �������� ��������� ����� ������� �� ���� 
�������� �������� ��� ���������� "�������������� ����������", �. 
�. �������������� �������� ����� ������� � �������� ��������� ��� 
������. 񎑒����� ������, ��������������� ������ ��������������� 
����������, ������� ���������� ����� "S1; S2", � �� ����������
$$ 
\wp("S1; S2", R) =\wp(S1, \wp(S2, R)) 
$$
��� ��� ������� ����� ������������� ��� ������������� ����������� 
����� � �������.

{\sl 瀌����ue.} � ���� �����, ��� ��������������� ���������� 
��� $S1$ � $S2$ �������� ���������� 1--4 �� ���������� �����, 
����� ���������, ��� � ������������ ���� ��������������� 
���������� ��� "$S1; S2$" ����� �������� ����� �������� 
����������. 퀏�����, ��������� ��� $S1$ � $S2$ ���������� ����� 
������������ ����:
$$ 
\wp(S1, F)=F\quad\hbox{ � }\quad\wp(S2, F)=F 
$$
�� ���������, ���������� $F$ ������ $R$ � ������� ����������� ��� 
$$
\eqalign{
 \wp("S1; S2", F)&=\wp(S1, \wp(S2, F))\cr
&=\wp(S1, F) \cr
&=F \cr
}
$$

�������� ��������������� � �������� ���������� ���������, ��� 
��������� ��� �������� ���� �����������. {\sl (ꎍ�� ���������.)}

�� ��� ��� ���������� ���� �����������, ��������  � ���, ��� 
���� ���������� ��������� ��������� ����� � ������� ������������ 
���� ����������� ������������� � ��� (���� ��� � ��� ����!), 
�. �. ��� ��������� ����������� "$S1;S2$"  ����� ���� ����������� 
�� ������� "������� ��������� ����������� $S1$ � �o ��������� �� 
������ ��������� $S2$".  � ����� ����, � ����� ����������� 
$\wp ("S1; S2", R)$ ��  ������������ $R$-����������� ��� 
��������� ����������� --- ��� ����������� � ��������������� 
���������� ��� $S2$, � ���� ���������� ��, ��� ����� ������ 
����������� "$S1; S2$" ����� ����������� � ���������� ������ 
$S2$. 񎎒����������� ��������� ����������� ��� $S2$, �. �. 
$\wp(S2, R)$, �������������� ��� ����������� � ��������������� 
���������� ��� $S1$; ��� ����� �� ���� ������������� ��������� 
��������� ��� $S2$ � �������� ���������� ��� $S1$. ��� ������ 
��� � ������, ���� ������ $S1$ ��������������� ������������ �� 
������� ������� $S2$.

����� �������������� � ����, ���������� ������. �� "$S1; S2$" 
������������ �����
$$ 
"a:=a+b;  b:=a*b" 
$$
� ����� ����� ������������ �������� ��������� �������� $R(a, b)$; 
� ����� ������
$$ 
\eqalign{
\wp (S2, R (a, b) ) &=\wp ("b:= a * b", R (a, b))\cr
&=R(a. c*b) \cr
}
$$ 
�
$$ 
\eqalign{
\wp("S1; S2", R(a, b))&=\wp(S1,\wp(S2, R(a, b)))\cr
&=\wp(S1,R(a, a*b))\cr
&=\wp( "a:= a + b ", R ( a, a * b))\cr
&=R(a+b, (a+b)*b)\cr
}
$$
�.� �� ����� ������������� ���������� ��������� $R$ ����� 
��������� ���������� $a$ � $b$ ��� �������, ��� ������������� �� 
�� ��������� ����������� ����� $a+b$ � $(a+b)*b$ ��������������.

� �������, ��������� �������������� ���������� �������� 
��������� ���������������, �� �� ����� ��������, ����� �� �� 
��������� "S1; S2; S3" ��� "[S1; S2]; S3" ��� �� ��� 
"S1;[S2;S3]". 荀�� ������, �� ����� ������ ����� ���������� 
����� � ������� ��� ������ ����������; ������� �� ��������� 
������� ����������������, ����� �� ���������� ����������� 
������ ���� "$S_1$; $S_2$; $S_3$; \dots ; $S_n$", � �� ����� 
��� ��������� ��������� ���, ����� ��� ����� ������������ 
���������� ������. 

{\bf 󏐀������.}
������, ��� ����������� 
$$ 
"x1:=E1; x2:=E2"\hbox{ � }"x2:=E2; x1:=E1" 
$$
������������ ������������, ���� ���������� $x1$ �� 
����������� � ��������� $E2$, � ���������� $x2$ �� 
����������� � ��������� $E1$. � ����� ����, � ����� ������ 
��� ��� ����������� ������������ ������������ �������������� 
������������ "$x1, x2:=E1, E2$". (��� ��������������� 
�������� ����� �� ���������� � ������ �������������� 
������������; �� ���������� ��������� ��� �������� 
������������ ���������������� ������, ���ee ����, ��� 
������������� ������������ ���������� ���������, ��� ��� 
��������� $E1$ � $E2$ ����� ����������� ������������, � ��� 
��������� �������������� ������������ ������� ��� ��������� 
��������� ����������. ��� ����, ���� �����, ����� 
���������� �����������, ��� ����������� "$x1, x2:=E1, E2$" �� 
�������� ������������ ������������� �� ����������� 
"$x1:=E1; x2:=E2$", �� ����������� "$x2:=E2; x1:=E1$".) (ꎍ�� 
����������.)

� �������� ����� � ������� �� ����� ������ ������ 
��������������� ���������; � ������� ����� � ������� �� 
������ ����������� ������ ��������� � ���� ���������� �� $n$, 
$(n>0)$ ����������: "$S_1$; $S_2$; $S_3$; \dots; 
$S_n$". 呋� ��������� ������������� ���������������, 
���������� ������ ��������� ������ �������� ��������� 
������������������ ���������� $n$ ����������, ������� 
$S_1$, ����� $S_2$ � ��� ����� �� $S_n$ ������������. 
��� �� ������ ������� ���� �� ����� �������, ����������� 
�������� 傊����, �� �����, ��� ������ ����� ��������� ����� 
������� ����� "������ ����": ������ ���� ����� �������� �� 
������������������ �����������, ��� ������ ����������� ����� 
��� ���� "$x:=x-y$", ���� "$y:=y-x$", �� ������ ����������� 
���� ����������� �� ������� � ���� �� ����� ����� ����� 
���������� �� ���� � ����; �� ������� �� ���������� ��������� 
�����, �� ������� �� ���������� ��������� �������. 呋� ����� 
� ������� �������� ������������ ����� ��������� ��� 
����������� ������ ������ �� �������� ������, �� �� �� � 
��������� ����� ��������, � ������� ��� ���������� ������ 
����� �����.

� ����� � ������� �������� ������������ ��������� � ����� 
������������ ��������� ����������, ������������ 
���������������, ��� ������� ���������� ������ ����� �� 
������������ ����������� $S_i\; (i>1)$, �������� ���������� 
���������� ������ (�����������������) �������������� 
�����������. ����� �������� ������ ��� ��������, ���������� 
���������� ����������� ������� ��� ��� ���� (���) ����������� 
� ����������� �� �������� ��������� �������. 䋟 ����� �� 
������ --- � ��� ����� --- ������� "���������� �������", 
��������� ������� �������� ��������� �������:
$$
\eqalign{
\<���������� ���������>&::=\<���������� ���������>\to\cr
&\<��������>\cr
\<���������� �������>&::=\<���������� ���������> \{;\cr
&\<��������>\}\cr
}
$$
��� �������� ������ "$\{$" � "$\}$" ������� ������ ���: 
"conp���������� ����� ������ (���� �����, �����) ����������� 
����������� ������".

(䐓��� ������� ���������� ���������� ������� ����� ��������� 
���:
$$
\eqalign{
\<������ ����������>&::=\<��������> \{;\<��������>\}\cr 
\<���������� �������>&::=\<���������� ���������>\to\cr
&\<������ ����������>\cr
}
$$
��� �� ��������, ������� �� ������ ��� ������ 
������������, � ����������� ���������, � ������� �������� 
������� ����������� ���������).

� ���� ��������� ���������� ���������, �������������� 
�������, ���������� "���������������". 脅� ������� � ���, 
��� ��������� �� �������� ������ ���������� ����� ����������� 
���� ��� ��� �������, ��� ���������� ��������� ���������� 
�������� ���������������� ��������������.  ����������� 
��������� ��� �������� ���������� ������  ���������� ��� ��� 
�������������� ���������������, ����� ��� �������� ��������� 
�� ������������� ��� (���� ������������� �������� 
������������ ��������) �����������.

葒������� �������� �������������� �������� ����������� 
��������������� �������� ��� ���������� ���������� ������� 
��� ������; ��� �������, ����������, �� �������� �����������, 
��������� ��� ��� ���� �������� --- � ����� ������ ��������� 
�� ���������� --- �� ���� ��� ������ ����� ������������� 
"�������". 茅��� ������� ���������� ������� �� 
��������������� ��� ��������: �������� �������������
�����������, ����� ��������� ��� �������, � ���������� 
������� ����� �������������� � �������� ������������� ����� 
��� ���������. 呋� �������� ������, �� ��������� ��� 
��������� ������� ����������� ��������� �� ������ ���������� 
������.

 �� ���������� ������������ ������������ ������ ���������� 
������ �������������� ������ ������������. ��������, ��� 
��� ��������� ��������� �����������, �����, ����� ��� 
�������, ��� ��������� ��������� ������������� $Q$, �������� 
��������� ������������� $R$. �������� �����, ��� ��� �� 
������� ����� ������ ������ ����������, ������� �������� �� 
��� ������ � ����� �������. (呋� �� ����� ������  ���������� 
�����������, �� �� ������ ��� �� � ������������ � �� �������� 
�� ����������� � ���������� ��������.) ��� ��� ����� 
�������� ����� ��������� ������� ����������, ������ �� 
������� ����� ��������� ������ ������ ��� ���oero 
������������ ��������� ��������� ���������. � ������� �� ���� 
������� ���������� �� ����� ������������ � �������� 
�������������� ���������� ���������, ��������������� �� 
������������, ��� �������� ���� ������ ��������, � ���� � ��� 
������� ������ ����������� ����� ���������������, �����, ��� 
�� ���������� $Q$ ������ ��������� ������� ���������� 
�������� ���� �� ������ ��������������, �� ��� ������� 
���������� ���������, ���������������� $Q$, �� ����������� 
������������, ������� ��������� ������� � ���������, 
��������������� ������� $R$, ������ ���� ������������ ������ 
���� �� ���������� ������, ��� �������������� ���� ��������� 
�������� "������". 
����� �������� ���, ��������� �������
$$ 
\<����� ���������� ������>::=\<���������� �������> \{\wbox 
\<���������� �������>\} 
$$ 
%\ wbox --- white box vs black border: []
��� ������ "\wbox" ��������� � ���� ����������� ���������, � 
��������� �� �������������. � �� �������� ������������ 
��������� �� ������ ���������� ������ ������� � ���, ����� 
�������� ����� ����� � ���� ������ "\kwd{if} \dots \kwd{fi}", ��� ���� ��� 
��������� ��� �������������� ���������, ��������� "��������", 
����������� ��������� ������:
$$ 
 \<��������>::=\kwd{if}\<����� ���������� ������> \kwd{fi} 
$$
򀊈� �������, �� �������� ����������� ���������� ��������� 
���������� ������ � ����� �����������. � ����� ����������� 
���� ������, ������� ���������� ����� ������� ���� 
�����������, ��������� �������. ⛁������� ���� ��
���������� ������, ��� �������������� �������� ��������, � 
����������� �� ������ ����������.

��� ��� �� �������� � ��������� ����������� �������� 
��������� ����� ����� �����������, ������� ������� ��� 
���������.                                    

\medskip
\item{1.} �����������, ��� ��� �������������� ����������; 
���� ��� �� ���, �. �. ���������� ������-�� �������������� 
����� �������� � ������ ��� ����������� ����������, �� 
�����������, ��� � ��� ����������� �� ������ ��������� 
��������� ���� ������.

\item{2.} ⎎��� ������, ���� ����������� �������� � 
��������������������� ��� ��� ��������� ����������, ��� 
������� ������� �������� ����� ��� ������ ��������������, 
��������� �������� ��������������, ����� �� ��������������� 
������� ���������� ����� ����� ���������� ��� �������. 
H������ ��������������������� �� ���������, ���� ��� 
�������������� ������� ��������� ���� �����.

\item{3.} 呋� ��������� ��������� ������, ��� �� ���� ��  
��������������� �� �������� �������, �� �� ����������� � 
��������� ����������, ��� �������� �� �������� �� ���� ��  
���������, � �������������, � ��� ����������� � �����. 瀏��� 
��� ����� ��������� ��������� �������� � ������.
\medskip

{\sl 瀌������.} 呋� �� ��������� ����� � ������ ����� 
���������� ������, �� �������� "\kwd{if}-\kwd{fi}" ������������ 
������������ ������ �������� ��������� "��������". {\sl(ꎍ�� 
���������.)}

(� ��������� ���������� ����������� ���������� ����������� 
��� ����������� \kwd{if}-\kwd{fi} �� ����������� �������, ����� ��� 
�������������� �������� ��������� ������������� ���������. 
呋� ��� �� ���, �� ����� ���������� ��������� � 
�������������� ������� $\cand$ ��� �������������� ����������, 
����� ��������� ��������� ������������ �������  ����������� 
���� ���������������.) 
������ ����� "\kwd{IF}" ��������  
\footnote{1} {SL- ������������ ��� Statement List --- ������ 
����������. ---{\sl �. �����.} }
$$ 
 \kwd{if} B_1 \to SL_1 \wbox B_2\to SL_2 \wbox \dots \wbox 
B_n \to SL_n 
 \kwd{fi} 
$$
򎃄� ��� ������ ����������� $R$ 
$$ 
\wp(IF, R) = (\exists j : 1\le j \le n: B_j) \and (\forall 
j : 1\le j \le n : B_j \Rightarrow wp(SL_j,R)) 
$$ % A � E --- ��� \forall � \exist?

��� ������� ������� ������ ���: $\wp(IF, R)$ �������� ������� 
��� ������ ����� ����� � ������������ ���������, ���
���� �� ���� �������� $j$ �� ������� $1\le j \le n$, �����, 
��� $B_j$ �������� �������, � ���, ����� ����, ��� ���� $j$ 
�� ������� $1\le j \le n$, �����, ��� $B_j$ --- ������, 
�������� $wp(SL_j, R)$ ����� �������� �������. 葏������ 
������ "\dots", ��� �� ��� ������ ��� �������� ������ 
��������� IF, �� ����� ���������� ���� ����� �����������:
$$ 
\eqalign{
\wp (IF, R) =&(B_1 \or B_2 \or \ldots \or B_n) \and \cr                   
&(B_1 \Rightarrow \wp(SL_1, R)) \and \cr                   
&(B_2 \Rightarrow \wp(SL_2, R)) \and \ldots \and \cr                   
&(B_n \Rightarrow \wp(SL_n, R) )\cr 
}
$$

������ ���� ������ �� ������������ ������� �����. 
򐅁�������, ����� �������� ���� �� ������ �������������� 
�������� �������, ���������� ���� ������ � ������, ����� 
�������� ��� ���� ��������������� �����. ꐎ�� ����, �� 
������� ��� ������� ���������� ���������, ���������������� 
$\wp(IF,R)$, ����� ����������� $B_j \Rightarrow wp(SL_j, R)$ ��� 
���� $j$. 䋟 ��� �������� $j$, ��� ������� $�_j$  --- 
����, ��� ���������� ������� ���������� �� �������� 
$wp(SL_j, R)$, �. �. ��� ����� �������� $j$, ����������, 
�����������, ��� ����� ������ $SL_j$.  ����� ���������� 
��� ����������� � ���, ��� ��� ������� �� ������� $SL_j$ � 
������ ��������� ��������� �������������� $B_j$.  ��� 
��������� $j$, ��� ������� $B_j$ --- ������, ������ 
���������� ����� ���� ������� ������ � ��� ������, ����� 
$wp(SL_j,R)$ ����� �������� �������. ������ ���� 
���������� ����������� ������� ���������� ���������� ��� ���� 
��������� $j$, �� ���������� �� ����� ���� ����� ������� 
������, ����� ����� ��� ���� �������������� �������� �������. 
ꎍ�������� \kwd{if}-\kwd{fi} ������������ ����� ������ ���� �� 
���� ��������� �������� ���������� ��������� �� ������ 
���������� ������. � ����������� \kwd{if}-\kwd{fi} ���������, ��� 
������� ��� �������������� ����� ������ ��������, ����� � 
������. � ����� ������ ����� �� ���������, ����� ���������, 
��� ������� ��� �� ������ �������������� � �������� 
���������, ��������� � ����������� ����������; ��������� � 
���� �������� �� ����������� ������� ������ ����������, 
������ �����������, ��� ��� ���� ��������� ������������� 
��������������� � ������ ����������. ��� ��� ���������� �� 
���������� ����������, ����� ��� �� ������ �������������� � 
�������� ���������, ����������� ���, ��� ������ �� 
����������� �����������, ���� ���� �� ���� �������������� 
�������� �������. 蒀�, ����� ������� ����������� ��� 
��������������. 呋�  ��� �� ������ ��������� �������� 
��������������, �� ������ �����������; ���� �� ������� 
�������������� � ��������� ����������, �� ���� �� 
��������������� ������� ���������� �����������, � ����� ��� 
���������� ���������� ����� �������� ����� �������� ���� 
���������������. ��� ������ ����������� ������������ ����� 
���������� ������ ���������� ������ � ���� ������ "\kwd{do} .. \kwd{od}".

􎐌������ ����������� ���������� ����������� ���  
����������� \kwd{do}-\kwd{od} �������� ����� �������, ��� ��� 
����������� \kwd{if}-\kwd{fi}; ���� � ���, ��� ������ ���������� ����� 
������. � ������� �������� ��� ���������� �����������, � 
����� �������� ���. ������ ����� "DO" ��������
$$ 
 \kwd{do} B_1\to SL_1\wbox  B_2\to SL_2 \wbox \ldots \wbox 
B_n \to SL_n \kwd{od} 
$$
� ����� "IF" ��������, ���������� ����� ���������� ���� �� 
������ ���������� ������ � ���� ������ "\kwd{if} ... \kwd{fi}". 呋�  
������� $H_k(R)$ �������� � ���� 
$$ 
H_0(R)=R \and \non (\exists j: 1\le j \le n : B_j) 
$$
� ��� $k>0$
$$ 
H_k(R)=\wp(IF, H_{k-1} (R)) \or H_0(R) 
$$ 
��
$$ 
\wp(DO,R) = (\exists k: k\ge 0 : H_k(R)) 
$$

焅�� ���������� �� �������� $H_k(R)$ ���������  �������: 
��� ��������� �����������, �����, ��� ����������� \kwd{do}-\kwd{od}
�������� ���� ������ ����� �� ����� ��� $k$ ������� 
���������� ������, ������ ������� ��������� � �������� 
���������, ��������������� ����������� $R$.

 $k=0$ ���������, ����� ����������� \kwd{do}-\kwd{od} ��������� 
������, �� ��������� ������� �����-���� ���������� �������, 
�. �. �� ����������� ������������� ������-���� �������������� 
� �������� ���������, ��� � �������� ������ ���������� 
������������.  ���� ��������� ���������� $R$ ��������� 
������� �������� ����������� �������� ��� �������� ���������� 
$R$, ��� � �������� ������ ���������� ������������.

 $k>0$ ��� ����� ��������� ��� ������: ���� �� ���� �� 
��������������� �� ����� ��������� ��������, �� ����� ������ 
����������� ������� $R$, � ��� �������� ��� �� ������� 
����������� ����������; ���� ���� �� ���� �������������� 
�������� �������, � ����� ������� ����������� ���, ��� ��� 
����������� ������� ��������� "IF" (� ��������� ���������, 
������� �� ����� �������� � ������������ ������ ���������� 
���������� �������� �������� ���������������). ��� ����� 
������ ����������, ��� ������� ������������� ������� ����� 
���������� �������, ��� ���������� �������� ��������� � 
���������, �����, ����� ������������� �� �����
��� $(k-1)$ ���������� ������� ��� ���������� ���������� 
������ � �������� ���������, ��������������� $R$. � 
������������ � ����� ������������, ����� ������������ ��� 
����� ��������� "IF" ������ $H_{k-1}(R)$.

񎃋���� ��������� ������, ������������ $\wp(DO, R)$, ������ 
������������ ����� �������� $k$, ����� ������������� �� ����� 
��� $k$ ������� ��� ����������� ���������� ������ � �������� 
���������, ��������������� ����������� $R$.

{\sl 瀌������.} 呋� �� ��������� ����� � ������ ����� 
ox�������� ������, �� � ���� ���������� �������� "\kwd{do} \kwd{od}" 
������������ ������������ ������ �������� ��������� 
"����������". {\sl (ꎍ�� ���������.)}

\bye
