3.3. ������� � ��������������

��� ����� ���������� � ������ 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].

����� ������� ������� � �������������� ����������.