\input style
\chapter{7 �������������� �������� �������}
������ ��������� ���� ���������, � ������� e�� ���� ����� ��������� 
傊����. ����, ��� � ����� ������� ��������� �� ��������� ��� 
���������� ��� � ����
\prg
x, y:=X, Y;
\.{do} x\not=y \to \.{if} x>y \to x:=x-y
 \wbox y>x \to y:=y-x
\.{od};
\var{��������}(x)
\grp
��� �������������� ����������� ���������� �����������, ��� 
����������� ������ �� �������� � ������. 䐓��� �������� ���������, 
��� ���� �������� ����� ������������ ����� ������ ��������� 
�������:
\prg
x,y:=X, Y;
\.{do} x>y \to x:=x-y
 \wbox y>x \to y:=y-x
\.{od};
\var{��������}(x)
\grp

������ ������ ������ ���� �� ����� ������� �  ���������� 
��������� ������ �������� 傊���� ��� ��������� ����������� ������ 
�������� ���� ������������� ����� $X$ � $Y$. ꎃ�� �� ������������ 
� ������ ���� ���������, �  �������� ������ �������� ��� �������.

��� ������� � ���, ����� �������� ��������� ����������� 
���������� ������ ��������� ������, ��������� ��� ��������. 
�-��������, �� ����� �� ������������ ������� ��������� ����� $X$; 
��� ������� ��������� �� ������ �������� ����� ���������, ����� 
������� ������� �� 1 � �������� ����������� � $X$ � �������� 
����������� ��������. (呋� $X=1$, �� ���������� � ���������� 
�������� ��������. 瀒�� �� ����� �� ������������ ����� ����������� 
������� ��������� $Y$. � ���� ���� ������ �� ����� �� ������������ 
������� �����, �������������� � ��� �����.  ������������ ����� 
������� \emph{�����} ��������� ����� $X$ � $Y$ � ����������� 
�������� ��������, ��� ��� �������� ������� 1. 񋅄���������, �� 
���� ������� ������� �� ����� ������� (��������� ��� ���� 
��������!) ������������ �������, � �� ��� ��  \emph{����������} 
����� ���������.

荎��� ������� ���������� �����������, �������� ������������� ����, 
�������� ������ �� ����, ��� �� ����� �������. 񓙅������, ������, 
� ������ ������, ������� ����� �����������, ���� �� ����� (��� 
����� ������) �������� �������, ���������� ����������. 쎆�� 
���������, ��� �� ����� ��� ����� �������, ��� ��� � ������������ 
���������� ��� �������, ����� �� ����� ���������� ��������� �����, 
��������� ��� ��������.

� �����e ����������� ������ �������� �� ��������, ��������, ���, 
��������� �������� ����� $-x$ �� �� �����, ��� � ���  ������ ����� 
$x$, $\���(x, y)$ ��������� ����� ��� ������������� ���������� � �� 
��������, ���� �� �������� ���� ����������. � ��������� � �����, 
����� ���� �� ���������� ����� ����; ����� �������� �������� 
����������� �������� ��������� (� ������� ��� �� ������� �������� 
������� ��� �������!), �� ��������� ������ �������� $(\not=0)$ 
�������� �������� �������� ���������, ������� ����� ��������� 
�������� ��� �� �������� � ��������. 蒀�, �� �������� � 
����������, ��� $\���(x,y)$ ��������� ��� ������ ���� $(x,y)$, 
�����, ��� $(x, y)\not=(0, 0)$. 䀋��, � ���� ��������� ������� 
"�����" ���������� ����� �������� �������� ������������ �������� 
����� ���� ����������. 噅 ���� ��������� ���������� ������ 
�������� ��� ��������� � ���, ��� ���������� ����� �������� ���� 
���������� �� ����������, ���� �� �������� ���� �� ���� ���������� 
�� ������ ��� ���������. ������ ��� ��� ����������, �� ����� 
��������: ��� $(x,y)\not=(0,0)$
$$ 
\leqalignno{ 
\���(x, y) &=  ���(y, x). & (�) \cr 
\���(x, y)&=  ���(-x, y). & (�) \cr 
\���(x, y) &=���(x+y, y) = ���(x-y, y)\hbox{  � �. �.} & (�) \cr 
\���(x, y) &=abs(x),\hbox{ ���� $x=y$}. & (�) \cr 
} 
$$

�������� ��� �������� �����������, ��� ����� �������� ���������� 
������������� ���� �������� � ������� $\���$. 䎑������� �� ��? � 
������, ��� ������ ��� ��������� �������� ���������� ����� �������� 
����� $x$ � $y$ �����  $\���$ ��� ������ ����, � ��������� �������� 
�������� ��� ��������������� ����� $x$. � � ���� ��� 
��������������� ������� ���������, ������� ��� ������ ������������ 
����������
$$ 
P= (\���(X,Y)=\���(x,y)) 
$$
(��� ����� ����������� ����� ������������ "$x, y:= X, Y$"), ����� 
���� �� "�������������" ���� �������� $(x,y)$ ����� �������, ����� 
� ������������ � (�), (�) ��� (�) ��������� $P$ ���������� 
������������. 呋� �� ����� op�a�������� ���� ������� ���������� 
���, ����� ���������� ���������, ���������������� $x=y$, ��, 
�������� (�), �� ������� ������� �����, ���� ���������� �������� 
$x$.

������ ���� �������� ���� ������� � ���, ����� ���������� ��� 
�������������� $P$ ���������� $x=y$, �� ����� �� �������� � 
�������� ��������� ��������� ������� �������
$$ 
t=\abs(x-y). 
$$

����� ��������� ��� ������ (������ ���������� ����!), �� ��������, 
��� ���� ��������� �������� $x$ � $y$  ���������������, �� ������ 
������ �������� ���������  �������������� ��������: ���� 
������������ $x:=E$ ���������� �� $x<0$, �� ������������ $x:=-E$ 
������� �� ������� �� � ��������� �������� ��������� �������� $t$ 
(������, ��� $y\ge 0$). ���� �� ��������� ���� ��������� $P$, 
������� ������ ����������� ������������: 
$$ 
P=(P1 \and P2) 
$$ 
��� 
$$  
P1=(\��� (X, Y)=\��� (x, y)) 
$$ 
� 
$$ 
P2=(x\ge 0 \and y\ge 0) 
$$
��� ��������, ��� �� ������������ �� ������� ������������� �������� 
$x:=-x$ � $y:=-y$, �.�. ��������������, ���������� �� �������� (�). 
퀌 �������� ��������
$$ 
\eqalign{ 
\hbox{�� (a):}\; x,y&:=y,x\cr 
\hbox{�� (�):}\;\;\;\;    x&:=x+y \;  y:=y+x\cr                                               
x&:=x-y   \; y:=y-x\cr
x&:=y-x  \;  y:=x-y\cr 
} 
$$

ᓄ�� ���������� ��� �� ������� � ������ �  ������������ 
$x, y :=y, x$:
$$ 
\wp("x, y: = y, x", \abs(x-y) \le t_0) = (\abs(y-x)\le t_0) 
$$ 
�������
$$ 
t_{min} (x, y) = \abs (y-x) 
$$
������������� 
$$ 
\wdec ("x, y:= y, x", \abs (x-y) ) 
= (\abs (y-x) \le \abs(x-y)-1)=F 
$$

� ����� --- ��� ���, ��� �� ������� �� ��� ����������� ������,---�� 
�������� (���, ���� ������, ����������) � ������� ���ero 
����������, ��� ������������� �������� $x,y:=y,x$ �� ������������ 
��������, ��� ��� ��� �� ����� �������� � ��������� ������������ 
���������� ��������� ���� �������  $t$.

񋅄����� ������������ �������� $x:=x+y$, � �� �������, ����� 
�������� ���������� �� ���������� ����:
$$ 
\displaylines{ 
\wp("x:=x+y", \abs(x-y)\le t_0)=(\abs(x)\le t_0)\cr 
t_{min} (x, y)=\abs(x)=x\cr 
} 
$$
(�� �������������� �����������, ���������������� $P$) 
$$
\eqalign{ 
\wdec("x:=x+y", \abs(x-y)) &= (t_{min}(x, y) \le t(x, y)-1)\cr 
&= (x\le \abs(x-y)-1)\cr 
&= (x+1\le \abs(x-y))\cr 
&= (x+1\le x-y \or x+1 \le y-x)\cr 
} 
$$

������ �� $P$ ������� ��������� ������� ����� � � ���� �� 
$P \Rightarrow \wp("x:=x+y", P)$, �� ��������� ������ ��������������
$$ 
(P \and B_j) \Rightarrow (\wp (SL_j, P) \and \wdec (SL_j, t )) 
$$
��������������� ��������� ������, � �� ����� ���� ������, � ����� 
(�� ����������� ���������) ���� ������ ���������� �������: 
$$ 
x+1\le y-x \to x:=x+y 
$$
� 
$$
 y+1\le x-y \to y :=y+x 
$$
���������� �� ������� (���������� ����������� ��������������� � 
�������� ���������� ���������� ��������)
$$ 
1\le y \and 3 * y \le 2* x-1\to x:=x-y 
$$ 
� 
$$ 
1\le x \and 3 * x \le2 * y-1\to y:=y-x
$$
� 
$$ 
 x+1\le y-x \to x:=y-x 
$$ 
�
$$
y+1\le x-y \to y:=x-y
$$

������������ � ���, ���� �� ��������, �� ��������� ������ � 
��������� ����������, ��� ��������, ���������� � ����� ���������� 
�����, ��� �� ������� ������ ���� ������: �� $P \and \non BB$ �� 
�������, ��� $x=y$. (퀏�����, ��� $(x, y) = (5,7)$ �������� ���� 
��������������� ����������� �������.) 쎐��� ����������, 
����������, � ���, ��� ���� ����� ����� �� ������ ������������ 
����� ���� �� ���������� ��������� � �������� ���������, ��� 
������� $\abs(x-y)$ ��������� �����������. ���� ��� ����� 
�������� ������ �����������.

䋟 ������ �������, ��� �� �������� ��������� ������� ������� $P2$: 
$$ 
P2=(x>0 \and y>0) 
$$
��� ��� ��������� �������� $x$ � $y$ ������������� ������ �������, 
�, ����� ����, ��� �������� ������ � ��������� ������� ���� 
��������, ��������� ��� �������� ����� ���������� ������ ��� 
��������� � ���������, ��� $x=y$, �.�. ����� ��� ���������� 
�������� ���������. � ��� ������ ����� �����������; �������� 
����������� ������ ���� ������� � ��������� ����� ������� $t$, � � 
��������� ����� ����� ������� $t$, ������� ������ ���������� ����� 
� ���� �������������� $P$. ������ �������� ��������
$$ 
t=x+y 
$$
� ��������, ��� ��� �������������� ���������������
$$ 
\wdec ("x, y:=y, x", x+y) =F 
$$
� ������� ������������� ������������ �����������. 

� ������� ��� ������������ $x:= x+y$
$$ 
\wdec("x:=x+y", x+y) = (y< 0) 
$$
葒������� ����� ��������� ����������� ����������� ������������� 
��������� $P$, � �������������, ����� ������������ (������ � 
������������� $y:=y+x$)  ����� �����������.

��� ��� ���������� ������������ $x:=x-y$ �� ������� 
$$ 
\wdec("x:=x-y", x+y) = (y>0) 
$$
�. �. �������, �������, ��������� ������� �� ������� $P$ ( 
���������� ���� ���� �����). 

������� ��������, �� ������� 
$$ 
\wp("x:=x-y", P) = (\���(X, Y)=\���(x-y, y) \and x-y > 0 \and y>0) 
$$
ꐀ���� ����� ����� ���������, ������ ��� ��� ������� �� $P$, � � 
��� �������� ������� ����: ����, �� �������
\prg 
x>y\to x:=x-y 
\grp 
�
\prg
y>�\to y:=y-x 
\grp
� �� ���� �� ����� �� ���������� ������������, ��� ���, ����� 
�������� ����� ��������������� ���������� �������, ����������� 
�������� ���� ��������� $x=y$. 呋� �� ���������, �� ������ ������ 
� ��������� ��������:
\prg
 x>y-x \and y>x\to x:=y-x 
\grp
 �
\prg
 y>x-y \and x>y\to y:= x-y 
\grp
�� �� ����, ��� ����� �������� �� ����������.

{\bf 󏐀������.}

1. 葑������� ��� ��� �� $P$ ����� $t=\max(x, y)$.

2. 葑������� ��� ��� �� $P$ ����� $t=x+2*y$.

3. 䎊�����, ��� ��� $X>0$ � $Y>0$ ��������� ���������, ����������� 
��� �������� �����������,
\prg
x, y, u, v:=X, Y, Y, X;
\.{do} x>y\to x, v:=x-y, v+u
 \wbox y>x \to y, u:= y-x, u+v
\.{od};
\var{��������}((x+y)/2); \var{��������}((u+v)/2)
\grp
�������� ���������� ����� �������� ����� � � �, � ������ �� ��� �� 
���������� ����� �������. (ꎍ�� ����������.)

퀊����, ���� ��� ��������� �������� ����������� ��� ���� $(X,Y)$, 
������� �� ������������� ������������� $X>0 \and Y>0$, �� 
���������� ������������: ���� $(X,Y)=(0, 0)$, �� ��������� 
������������ ������� ���������, � ���� ���� �� ���������� 
�������������, �� ������ �������� � ����������� ������. ����� ����� 
��������, �������
\prg
\.{if} X>0 \and Y>0 \to x,y:=X,Y;
   \.{do} x>y\to x:=x-y\wbox y>x\to y:=y-x \.{od}; \var{��������}(x) 
\.{fi}
\grp

⊋���� ������ ���� ������� � ����������� ������, �� ���� �������� 
�������, ��� ������� ��������� ������ ���� ��������� ���������. � 
����� ���� ��� ������ ���������� � �������� ��������������� 
��������, ���������� ��� �������� ���������, ��� ������� ������� 
��� ��� ������� ����������� �������� � ������������ ������.
\bye
