��� ����� ���������� � ������ EA �������� ���������� � �������, ���� ���������������� ������� � ����� ������ ���? ������ ������: �� ��� ��������� ��� ������ �������, ���������� � EA ���������� ���������� ��������� ����� "x - ������� �����":
1<x & ~(EyEz)(y<x & z<x & x=y*z).
����� ���������� �� ������ ����������� � ������ ���� ��������? ���� ���-�� ���������� ������� � ����������, ��� ��� "��������" ��-�� � ��-��, ��� ��� ���������? ��� ����� �������� �������� ������� ����������� ���������� � �������������� �������.
����� ��������, ��� ������� A(x,y) (x, y - ������������ �� ��������� ����������) �������� � ������ EA �������� a(x,y) (x,y ��������� �� ����������� ������), ���� ��� ����� ����������� ����� m, n
�) ���� ����� ����� a(m, n), �� EA |- A(m, n), - -
�) ���� a(m, n) �� ����� �����, �� EA |- ~A(m, n).
����������, ��� m, n - ����� EA, ������������ ����� m, n: 2 - ��� 1+1 � �.�. ����� �������, �������� �� ��� ���������� ������������, ����� �������� ������� A ������������� ���������� �������� a, ��, ��� ������� ��������, ��� ���������� ����������. (�� �������������� ����������� ��� ������ ����������� ����������, ���������� ������������ ����������� �����������, ����������� � �.�. ����������.)
����� ���������, ��� ������� x=y �������� � EA ������� ���������� ���������� ��������� ����������� �����. � ����� ����, ��� ����� m, n: �) ���� m=n, �� EA |- m=n (����� m, n � ���� ������ ������ ���������), �) ���� m<>n, �� EA |- ~(m=n) (���������).
��������� ���� �� �������� �����-�� �������������� ������ ��� ����������, ������� �������� � EA. ���� ������ EA �������������, �� � ��� ��������� ����� ������� � ������� - � ������ ��������� ���� ����������� - � EA ����� �������� ����� �������� (��������, ������� x=y �������� ����� ����������� ��������). ���� �� ������ EA ���������������, �� ������ ������� ����� �������� �� ����� ������ ���������, � ��������� ������ ���������� ������ ������� �����, �� � ��������� ���������� ����� �� ����� ��� ������� �����. �� ���� ������������ ����- ������� ���������� "����������" ��������� �����, �.�. ������ "������������" ����������� ���������.
����� �� ��������� �������� � EA, � ����� - ��� (���� ������������, ��� ��� ������ ���������������)? ����� ��������, ��� ������ ��������� � EA �������� ������ ���� ���������� ���������� (�� ������ ������������ - �����������) ����������. � ����� ����, ���� ������� A(x,y) �������� � EA �������� a(x,y), �� ��� ������� ������� �� ���������� a(m, n) �� ������ ����������, ������� �� ������ A(m, n), ~A(m, n) ��������� � EA (����� ��������, ��� ���� �� ��� ���������). ��������� ���� ������ EA ���������� ����������� (��.���������� 1.4). ���������� ������������ ������� EA, �� ���� ��� ������ �������� ���� ������� A(m, n), ���� ~A(m, n) (�� ������ ���� �� ���, ��������� EA - �� ������������� - ���������������). ��� � ����� ������ �� ���������� a(m, n). ����� �������, a(x,y) - ���������� ���������� ��������.
������ ������, ������������� ������ EA ��� ���, �� �� � ���������. ���, ��� ����� �������, - ��� ���������� �������� ���������� �� ������������� � ������������������ EA, ��� ��� ���������� ���������� ��������� �������� � EA. ��������� ������� �� ��� �������.
����� ��������, ��� ������� F(x,y,z) ������������ � EA ������� f(x,y) (������������ ����������� ����� � �����������), ���� ��� ���� k, m, n �����, ��� f(k, m)=n,
�) EA |- F(k, m, n),
�) EA |- (Az)(~(z=n)->~F(k, m, z)).
����� �������� �� ������ ����� �����������: ���� ������������� ������� f � ���������� f(x,y)=z, �� ������ �� �� ������� �� �������������� �������, ���������� � EA ���� ��������? ��� �������� �� ������ ������� �) ��������
�1) ���� f(k, m)<>n, �� EA|- ~F(k, m, n).
����� ������, ��� �� �) �������� �1). � ����� ����, ���� f(k, m)<>n, �� f(k,m)=q, �� EA |- ~(n=q), � �������� ������� �) EA |- ~(n=q)->~F(k, m, n), �.�. EA|- ~F(k, m, n), ��� � �����������. ������ ������� �) �� �1) �� ��� �� � ���������. ������� ����� �������, ��� ������� F, ���������� ���������� �+�), ������������ ������� f "�����", ��� �������, ������� �������� ������ ���������� �+�1). ���� � ������ �+�1) ��� ������� n, ��������� �� f(k, m), ���������� ����� ��������� �������������� ������� ~F(k, m, n), �� � ������ �+�) ��� ���� ����� n ������ ���� ���� ������ ��������������: EA |- ~(z=q)->~F(k, m, z), ��� q=f(k, m).
���� ������ EA �������������, �� � ��� ����������� ����� �������.
���������� 3.7. ���������, ��� ���� EA ���������������, �� ������ ����� ������������ �������, ������������ � EA, ������ ���� ����������.
�� ����� ��������, ��� � EA (���������� �� ������������� ������������������) ����������� ����� ���������� �������.
����� ������������ ���������� � ��������������� ������� ���������� ������� � ������������ �����.
���������� 3.8. ��������, ��� ��������� �������� ������� � EA ����� � ������ �����, ����� ��� ������������������ ������� ����������� � EA.
����������, ����� �������, ���������� �������������� � EA ������ ���������� �������, ����� ������������ ����� ���� ����������, ��� ������ ���������� �������� ������� � EA.
������� � ��������������. ������ ���������� ������� ����������� � ������ EA.
�������������� ������� � �������������� ��������� ���������� ����� ����� �������.
������� ���������� ���� �� ������ ����������� ������� ���������� �������: �������, ������������ ����������� ����� � ����������� �����, ���������� ����������, ���� ���������� ������ ��������, ����������� �� ��������. ������ ������ �������� M ������������:
�) ��������� ���������� ��������� (����������� ����� ������� �� ����������� ����������� ������, ����� m=2k, ��� k - ���������� ��� � ������):
QM = {qstart, qstop, q1 ,..., qm},
�) ��������� �����:
AM = {0, 1, a1, ..., an},
�) ���������� PM, ��������� �� ��������� ����� ������ ���� qa -> q'a'e, ��� q, q' in QM (q - "������", q' - "�����" ��������� ������), a,a' in AM (a - "������", a' - "�����" ������ � ������, ������������ �������� ������), e = -1, 0, +1 (��������, ���� ����������� �������). � ��������� �� ������ ���� ���� ������ � ����������� ������ �������.
��� ���� ���������� ������������ ������ ��������� ��������� ������:
M-------------| q |
a | ... |
� ������ ������ (����������, ��������, ����� ������ ������)
�) ������ M ��������� � ����� �� ��������� QM,
�) ������ ������ ����� (��� ���������� ������ ������) ��������� � ����� �� ��������� AM,
�) ������� ������ ���������� ��������� ������ �����. ���� � ������ t ������ M ���������� � ��������� q, ������� ���������� � ������ ������ a � � ��������� PM ���������� ������� qa -> q'a'e, �� � ������� t+1 ������ �������� � ��������� q', ������ a ��� ������� �������� a' � � ����������� �� e ������� ��������: ���� e=-1, �� �� ���� ������ �����, ���� e=0 - ��������� �� �����, ���� e=+1 - �� ���� ������ ������ (���� ������� ���������� ����� ����� ������ �����, �� e=-1 ����������� e=0).
�� ����� ��������, ��� ������ M ��������� (����� ������������) ������� f(x,y), ���� ��� ���� �������� x,y, ����������� �� ��������, � �������
a) M ��������� � ��������� qstart,
�) ������� ���������� ����� ������ �����,
�) � ������ ����� ��������� ������������������ ��������
0 1 1...1 0 1 1...1 0,
-------- --------
x ------- y
����� �������� ����� �����, ��������� �� ��������� PM, ������ �������� � ��������, � �������
�) ��� ��������� � ��������� qstop,
�) �� ����� ��������� ������������������
0 11...1 0.
------
f(x,y)
���� ��� ������� f(x,y) ������� ��������� ����� ������ M, �� ����� �������� f ����������. ��� ����������� ����������� ������������� ���� ������ ������ ������������ ������� ���������� �������.
� �������� ������� ������� ��������� ��� ������ ��������, ������� ��������� ������� f(x)=x+1. ������ ���� ��������� - ������ ����� ������ ������ �� ����, �������� ���� ��������, � ����� �������� ����� ����:
QM = {qstart, qstop, q, q'}, AM = {0,1},
PM = {qstart, 0 -> q, 0, +1;
q, 1 -> q, 1, +1;
q, 0 -> q', 1, +1;
q', 0 -> qstop, 0, 0;
q', 1 -> qstop, 0, 0}
���������� 3.9. �) �������� ��������� ��� ����� ��������, ����������� ������� x+y, x*2, x*y, 2x, [log2 x].
�) ��������� �����-���� ���� ����������������, �������� ������������� ����� ��������. ��� ���������, ������� �������� ��������� ������ � ��������� ��������� �����, � ����� "����������" ������ ��������� ��������� � ����� �� ��������� �������� �������������� ��������� �����. ����� ������������� ��������� ���������� ��������� ��� ����� ��������, ��������� ���� ����� �� ����.
��� �������������� ������� � �������������� �� ������ �������� ��������� f(x,y)=z � ���� ��������� ������� F(x,y,z) �� ����� EA. ��� ���� ����� ������������ ��, ��� ����� ����� ���������� x, y � ��������� z ������ ������������ ����� � ���� ��������������� ��������, ���������� �� ��������� PM ���������� ������ ��������.
����� ���� �� �������� �� ����������� �������, ���� �� � ����� EA ������� ����������� ���������� ��� ��� ���������� ��������. ��������� (������ ���������� ������) � ������ ������� t ����� �������� ������������������
(q, l, d0, d1, ..., ds-1),
��� q - ���������� ��������� ������ � ������ ������, l - ����� ������, ������������ �������� ������ (��������� ���������� � ����), d0, d1, ..., ds-1 - ������� � ������� � �������� 0, 1, ..., s-1. ���� C1, C2,... - ����������, ���������� ������� �������� ����� ��������, ���� �� ������ ����� � ����� EA ����� ����������� ������� ��� �������:
q(C)=q � �������� C,
l(C)=l � �������� C,
s(C)= ����� ������, ����������� � C,
di(C)=di � �������� C.
���� ��� ��� � ����� EA, �� ����� �� ��������� ��������� �������. ������� ������ ������� START � STOP. ������� START(C, x, y) ������ ����������, ��� C - ��������� ��������, � ������� �� ����� ������ ���� ���������� x, y:
q(C)=qstart & l(C)=0 & x+y+3=s(C) & d0(C)=0 &
& Ai (0<i<x+y+3 -> di(C)=1 V di(C)=0 & (i=x V i=x+y+1)).
������� STOP(C,z) ������ ����������, ��� C - �������������� ��������, � ������� ��������� �������� z:
q(C)=qstop & z<s(C) & d0(C)=0 & Ai (0<i<z+1 -> di(C)=1 V (di(C)=0 & i=z)).
�����, ������ ������� kappa in PM (��� M - ������, ����������� ������� f), ������� ��� qa -> q'a'e, �� ���������� ������� STEPkappa (C1, C2 ), ������� ����������, ��� �������� C2 ���������� �� �������� C1 � ���������� ���������� ������� kappa. ���������� ������ e=+1:
(EuEv)[q(C1)=q & l(C1)=u & s(C1)=v & du(C1)=a &
& q(C2)=q' & du(C2)=a' & l(C2)=u+1 & (Ai<=v)(i=u V (Ej)(di(C1)=j & di(C2)=j)) &
& ((u<v & s(C2)=v) V (u=v & s(C2)=v+1))].
���������� 3.10. �������� ������� ���� ������� ��� ������� e=-1, 0.
��������� ���� - ������� CHAINEM(C1, C2), ������������, ��� �������� C2 ���������� �� C1 � ������� ��������� ����� ����� �� ��������� PM. ����� ������ ������ ��� ����������� ���������� L1, L2, ����������� � �������� �������� �������� ������������������ ��������. �������������� ��� ����������� ����� ������� �������:
delta(L)= ����� �������� � ������������������ L,
gammai(L)= i-� �������� � L.
� ����� EA ����� ������� ���, �� �� ����� ���� ������������ ��� ��������������. ������� CHAINEM(C1, C2) ����� ���
(ELEw)[delta(L)=w+1 & gamma0(L)=C1 & gammaw(L)=C2 &
& (Ai<w)(EC3EC4) (gammai(L)=C3 & gammai+1(L)=C4 & STEPM(C3, C4)],
��� STEPM(C3, C4) - �������
STEPk1(C3, C4) V STEPk2(C3, C4) V ... V STEPkt(C3, C4),
� ������� k1, k2, ..., kt ���������� ��������� PM.
���� ������ M ��������� ������� f(x,y), �� ������� F(x,y,z), ������������, ��� f(x,y)=z, ����� �������� ������ ��������� �������:
(EC1EC2 )(START(C1, x, y) & CHAINEM (C1, C2) & STOP(C2, z)).
������� ��� ������, �� ���������, ������, ��������� � ����� EA. � ��� ��� ���������� ��� ��������, ��� �������������� ��������, ������� �� ������ ������, �� ������ ��� � ���������� ��� ������������������� ��������. �������, ���� �� �����, ����� ������� F(x,y,z) ������������� "�����" � ���� EA, �� ������ ������������� ��� "����������" ���������� EA.
��������� ����� qstart, qstop, 0, 1, q, q', a, a' � �.�. "�������" � EA �������� - ������ �� ��� ����� �������� ��������� ����������� ������ - �� ����� (��� ���� ����� ����������� ������ �������� ����� ����� - �������� QM , AM �������). �� ��� ������ � ����������? ����� ��� "�����" � EA, �� ����� ����� ������������ ������������ �������. ���� ���������� ��������� ������ � ������� �� ����� ��� ������������ ������������ �������, �� �������� ������������ � �������� ������������������ ����� �����. �� ������ ���������, �������������, ������������ ����� �������� ������������������ ����������� ����� ����� ����������� ������ (� ������ ������ - ����� ��� �����). ������ ������� ��� ����� ���, ����� ������� q(C), di(C) � �.�. ����� ���� ����������� ��������� EA.
�.������ ����������� ���� ������������ ��� ���� ���� ��� ���������� ��������� ������� �� ��������. ���������� ��������� ������: ����� �����, ������� ��� ������� �� 3 ���� ������� 2, ��� ������� �� 5 - ������� 3, ��� ������� �� 7 - ������� 4. ���� �������, ������� ���� ������ ����� �������:
53=3*17+2=5*10+3=7*7+4.
����������, ������, ����� ������: ����� �����, ������� ��� ������� �� �������� ����� ���� �������� �������. �������� ����� ��������� ����� u1, u2, ..., un, ��� ����������� ����� >=2. �������� ������� ��������� ����� v1, v2, ..., vn; ����� �������, 0 <= vi < ui. ���� ����� ui, uj ����� ����� ��������, �� ������� ��� ������� �� ��� ����� ��� ������ ������� ����������. ��������, ���� ui , uj - ��� ������, �� ��������������� ������� ������ ����� ���������� ��������, ����� ������ �� ����� ����� �������:
x=ui yi+vi = uj yj +vj, ui = 2ui', uj = 2uj', vi - vj = 2(ui'yi - uj'yj).
������� �������� ����������, ���� �� ���������, ����� ����� u1, u2, ..., un ���� ������� ������� �������� (�.�. ����� ������� ��� �� ��� �� ����� ����� ���������). � ����� ������ ������ ������ ����� �������, ��� ����������
��������� ������� �� ��������. ���� ���� ������� ������� ������� ����� u1, u2, ..., un (ui>=2 ��� ���� i) � ����� v1, ..., vn (0<= vi < ui ��� ���� i), �� �������� ����� p, ������� ������������ u1u2...un, ������� ��� ������� �� ui ���� ������� vi (� ��� ��� ���� i).
� � � � � � � � � � � � � �. ������� ����� p, ���
0 <= p < P = u1u2...un,
���������� "������ ��������" ��� ������� �� u1, ..., un. ��������, ��� ��� ����� ����� ����� ���� � ��� �� ������ ��������, ������ ���� �� �������� ������� �� P.
� ������� ��������� ������� �� �������� �� ����� �� ���������� ������������������ ����������� ����� v0, v1, ..., vn-1, ����������� ������ vi ��� ������� �� ������� ���������� ����� p �� ����� ui �� ������ u0, u1, ..., un-1 , ������� �� ������ ��������� ������������ �����-�� ���������� ������� ��������. ����� ����������� �� ���������. ����� ������� ������ - ����������� ui ��� �������� ������� �� i: u = yi+z. �� ��� ��������� ������������ y, z? ����� ui ������ ���� ������� ��������. ���� d ����� �������� ui � uj , �� d ����� ����� �������� ui - uj = y(i-j). ���� ������� z=y+1, �.�. ui = 1+y(1+i), �� �������� y �� ������ ���� ������ ���������� ui, uj. ��� ����� ���� ����� ������ �������� �������� |i-j|, �.�. ����� <=n-1. �� ���� � ���� �� ��� y ������� �� (n-1)!, �� � ��� ����� �� ������ ���� ������ ���������� ui , uj, �.�. ����� u0, ..., un-1 ����� ������� ��������. � ����, ����� ����, y ��������� ������, ��� u0 > v0, u1 > v1, ..., un-1 > vn-1, �� �������� ��������� ������� �� �������� �������� ����� p, ������� ��� ������� �� u0 ���� ������� v0, ��� ������� �� u1 - ������� v1, ... , ��� ������� �� un-1 - ������� vn-1.
���� ����� (x, y) �� ����� �� ������� ����� ������������������ v0, v1, ..., vn-1, �� � ���� ������ ����� �� ���������� ����� n. ���� �� ������ v0, v1, ..., vn-1 ������������ ��������� �������� ������������������ n, v0, v1, ..., vn-1, �� ��������������� ���� (x, y) ����� �� ������������� ����������� ����� v0, v1, ..., vn-1.
�������
beta(x, y, i) = ������� �� ������� x �� 1+y(1+i)
������� �������� ����-�������� ������. �� ����������, ��� ��� ������ ������ ����������� ����� v0, ..., vn-1 ����� ��������� ����� x, y �����, ���
beta(x, y, 0)=n, beta(x, y, 1)=v0,..., beta(x,y,n)=vn-1.
������� �����, ��� ����-������� ����� ����������� � ������ EA ��������� �������� B(x, y, i, j) (������������, ��� beta(x, y, i)=j):
(Ez)(x=(1+y*(1+i))*z+j & j<1+y*(1+i)).
������ ����� ���������� ������� START, STOP � �.�. ���������� ����� EA. � ���������� �� ��� ���������� - ��� ��������� ������ M, ��� ������� �� ����� ����� ���������� ������������ �������. �����, �������� - ������������������ (q, l, d0, d1, ..., ds-1) ���������� ������ ������������������� ����������� �����, ������� ����� ������������ ����� ������������ ������� a, b, ������, ���
beta(a, b, 0)=s, beta(a, b, 1)=q, beta(a, b, 2)=l, beta(a, b, i+3)=di
(��� ���� i). �������� ���� EC, ��� C - ���������� ��� ��������, ����� �������� ������ ���������� EaEb, ��� a,b - ��� ���������� ��� ����������� �����. ���������, ���������� "����������" �������������� �������:
s(C)=s, q(C)=q, l(C)=l, di(C)=di,
����� �������� �����������
beta(a, b, 0)=s, beta(a, b, 1)=q, beta(a, b, 2)=l , beta(a, b, i+3)=di.
���������� "����������" �������� �� ���������� ���� s1 < s(C) ����� �� ���������� ��������:
(Es2)(beta(a, b, 0)=s2 & s1 < s2).
���������� 3.11. ���������� ���������� EA ������� START, STOP, STEPkappa, STEPM. ���������� ����� ������ �������.
� ������� CHAINEM ��������� �����, ��� ����� ������� ���������� - ��� �������� ������������������� ��������, � ����� �������������� ������� delta(L), gammai(L). ��������� �������� �� ��������� ���������� ����� ������������ �������. ���� �������� Ci ������������ ����� ����� (ai , bi), �� ������������������ L={C0, C1, ..., Cn-1} �� ����� ������������ ��� ������������������ �����
n, a0, b0, a1, b1, ..., an-1, bn-1.
���� (a,b) - ��� ���� ������������������, �� ������� delta(L)=w ����� �������� �� beta(a, b, 0)=w, � ������� gammai(L)=C - ��
beta(a, b, 2i+1)=a' & beta(a, b, 2i+2)=b',
��� (a',b') - ��� �������� C. ������� EL, ��� L - ���������� ��� ������������������� ��������, ������� �������� ���������� EaEb.
���������� 3.12. �������� ��� ��� ������ � ������� CHAINEM � ���������� �� �����. �� �� �������� � ��� ������� F(x,y,z), ������������, ��� f(x,y)=z.
����, ��� ������ ���������� ������� f(x, y) ������ �� ������ ��������, ����������� ��, �� ����� ������� ������� F(x, y, z) � ����� EA, ������� (� ����� ����������� �� ���������) ����������, ��� f(x, y)=z. ����� ��������� �������������� ������� � ��������������, �� ������ ��������, ��� � EA ��������� �������
F(k, m, n), ~(z=n)->~F(k, m, z),
(��� �������, ��� f(k, m)=n). �� �� ����� ���� ���������� (��� �� ���������� ������� �� ������ EA �������-������ ������ ������� �������� ������� ����������� �����). �������� ���������� �� ����� �������� ����� ���������� � ����� �.����������� [1976].
����� ������� ������� � �������������� ����������.