Язык исчисления вычислимых предикатов (прод.) Конструктор предиката Конструктор массива Программа на языке CCP Предикаты в качестве параметров предикатов Правила построения заместителей Рекурсивные определения предикатов Пример программы Лемма согласованности предикатов рекурсивного кольца Теорема о согласованности предикатов программы Лекция 4 Предикатное программирование

Структура программы на языке CCP Программа набор определений предикатов Определение A K предикат A, оператор K параллельный оператор, оператор суперпозиции, условный оператор Вызов предиката (d 1, d 2, …, d n : e 1, e 2, …, e m )(3.1) φ имя предиката или переменной предикатного типа, n 0, m > 0, d 1, d 2, …, d n имена переменных аргументы вызова, e 1, e 2, …, e m результаты вызова Вычисление предиката Вызов φ(d: e), где d = d 1, d 2, …, d n, e = e 1, e 2, …, e m – наборы переменных n = 0 – вызов предикта соответствует константе Значение φ(d) φ(d: b), где b переменная логического типа Определение предиката A(x: y) K(x: y)(3.2) A имя предиката; набор x аргументы предиката, набор y результаты предиката, K(x: y) – оператор. Предикат – определяемый, базисный, значение переменной. Тип данных определяет набор базисных предикатов со значениями типа Система типов определяет совокупность всех базисных предикатов

Логическая семантика: LS(S k ) = L k LS( (d: e)) (d, e) LS(A(x: y) K(x: y)) A(x, y) LS(K(x: y)) Операционная семантика: метапрограмма Метаязык. Память – набор секций. Секция памяти – набор переменных и их значений: аргументы, результаты, локалы. s[a] – значение переменной с именем a в секции s s[x] – набор значений для набора имен x в секции s s[a] := v – оператор присваивания значения v переменной a в секции s s[x] := w – групповое присваивание набора значений w набору переменных x в секции s s = newSect(A) – создание в памяти новой секции s для определения предиката с именем A runCall(s, (d: e)) – исполнение вызова (d: e) runStat(s, K(x: y)) – исполнение оператора K(x: y) правой части Значение переменной предикатного типа – (имя предиката, набор значений части аргументов) Например, (A, z ~ ), для A(z, t: y) K(z, t: y), где t непусто.

s[C] = (A, z ~ ) предикат A является заместителем переменной C предикатного типа. subs(C) множество заместителей переменной C. A subs(C) H(x: y) есть вызов предиката или оператор. RUN(H, x, y) существует исполнение H(x: y) для значений набора x, завершающееся значениями набора y. Свойство согласованности Cons(H) x y (LS(H(x: y)) y RUN(H, x, y) (4.11) Предикат A обладает свойством согласованности Cons(A) если любой его вызов обладает свойством согласованности

Оператор суперпозиции A(x: y) B(x: z); C(z: y)(3.16) LS(B(x: z); C(z: y)) z. (B(x, z) & C(z, y))(3.17) Процедура runStat(s, K(x: y)) абстрактного процессора: runCall(s, B(x: z)); (3.18) runCall(s, C(z: y)) z набор локальных переменных секции s Лемма 3.3 Cons(B) & Cons(C) Cons(H), где H обозначает B(x: z); C(z: y). Доказательство. Пусть истинно Cons(B) и Cons(C). Докажем истинность Cons(H). Зафиксируем значения x и y. Пусть истинна H(x: y), т.е. истинна правая часть (3.17). Для некоторого z будут истинны B(x: z) и C(z: y). Из Cons(B) и Cons(C) следует, что исполнение B(x: z) завершается получением набора z, а исполнение C(z: y) вычислением набора y. Поэтому исполнение операторов (3.18), а значит и H(x: y), завершается вычислением y. Это доказывает первую часть истинности Cons(H).

Параллельный оператор A(x: y, z) B(x: y) || C(x: z)(3.19) x, y и z произвольные непересекающиеся наборы переменных, причем x может быть пустым. Если B или C есть имя переменной предикатного типа, то это имя входит в набор x. Логическая семантика параллельного оператора: LS(B(x: y) || C(x: z)) B(x, y) & C(x, z) Процедура runStat(s, K(x: y)) абстрактного процессора: runCall(s, B(x: y)) || runCall(s, C(x: z)) Лемма 3.4. Cons(B) & Cons(C) Cons(H), где H обозначает B(x: y) || C(x: z).

Условный оператор A(b, x: y) if (b) B(x: y) else C(x: y) (3.20) LS(if (b) B(x: y) else C(x: y)) (b B(x, y)) ( b C(x, y)) (3.21) Процедура runStat(s, K(x: y)) абстрактного процессора: if (s[b]) runCall(s, B(x: y)) else runCall(s, C(x: y)) (3.22) Лемма 3.5. Cons(B) & Cons(C) Cons(H), где H(b, x: y) обозначает if (b) B(x: y) else C(x: y). Доказательство. Пусть истинно Cons(B) и Cons(C). Докажем истинность Cons(H). Зафиксируем значения b, x и y. Пусть истинна H(b, x: y). Тогда в соответствии с (3.21) истинны формулы b B(x, y) и b C(x, y). Рассмотрим случай, когда значение b истинно. Тогда истинна формула B(x, y). Из Cons(B) следует, что исполнение вызова B(x: y) завершается получением набора y. Поэтому исполнение оператора (3.22), а значит и H(b, x: y), завершается вычислением y. Это доказывает первую часть свойства Cons(H) для истинного значения b. Доказательство в случае ложного значения b проводится аналогично.

3. Язык исчисления вычислимых предикатов (продолжение 2)

Конструктор предиката Базисный предикат ConsPred(x, B: A), x набор переменных, B имя предиката, A имя переменной предикатного типа. B не ConsPred и не ConsArray LS(ConsPred(x, B: A)) y z. (LS(A(y: z)) LS(B(x, y: z))) (3.23) Процедура runCall(s, ConsPred(x, B: A)) абстрактного процессора: s[A] := pVal(B, s[x]) (3.24) pVal(B, x ~ ) = (C, (t ~, x ~ )) (3.25) где s[B] = (C, t ~ ) для переменной B; C=B и t ~ = для имени предиката B Пусть q[A]=(D, p). Операционная семантика A(y: z) : runCall(q, A(y: z)) runCall(q, D(p, y: z)). Лемма 3.6. Cons(B) Cons(ConsPred). Доказательство. LS(A(y: z)) LS(B(x, y: z)) LS(C(t ~, x, y: z)) RUN(C(t ~, x, y: z)) RUN(B( x, y: z)) RUN(A(y: z))

Лемма 3.7. Пусть имеется вызов ConsPred(x, B: A), причем Cons(B) истинно. Тогда истинно Cons(A). Доказательство.

Конструктор массива Базисный предикат ConsArray(x, B: A), x набор переменных, B имя предиката, A имя переменной предикатного типа. B не ConsPred и не ConsArray LS(ConsArray(x, B: A)) y z. (LS(A(y: z)) LS(B(x, y: z))) (3.27) Кодирование массива A(y: z) A ~ [y] = z (3.28) Процедура runCall(s, ConsArray(x, B: A)) абстрактного процессора: s[A] = newArray(Y, Z); // Y, Z - списки типов y, z (3.29) forAll y Y do runCall(s, B(x, y: s[A][y])) end S(y: z) F(y). Тогда forAll y Y do S(y: z) end y Y. F(y) (3.30) Лемма 3.8. Cons(A). Доказательство непосредственно следует из соотношения (3.28). Лемма 3.9. Допустим, предикат B(x, y: z) определяет однозначную всюду определенную функцию по x и y, т.е. истинно условие: x y Y !z B(x, y: z) (3.31) Тогда Cons(B) Cons(ConsArray)

Доказательство. Пусть истинно Cons(B). Зафиксируем x. В соответствии с (3.30) после исполнение оператора forAll из (3.29) будет истинной формула: y Y. B(x, y: A ~ [y]). Пусть z тот единственный набор, для которого истинно B(x, y: z) в соотношении (3.31). Тогда A ~ [y] = z. Из (3.28) следует истинность A(y: z). В итоге, после исполнения тела forAll будет истинно y Y. B(x, y: z) & A(y: z). Поскольку z единственно для B(x, y: z) и A(y: z), то будет истинным y Y. B(x, y: z) A(y: z). Дальнейшее доказательство очевидно. Допустим, в секции s исполняется вызов предиката A(u: v), где A является переменной предикатного типа, а значением A является массив. Секция s содержит переменную A и наборы u и v. Исполнение вызова A(u: v) реализуется следующим оператором: s[v] := s[A] [u] Для исполнения вызова A(u: v) принято обозначение runCall(s, A(u: v)).

Определение предиката. В правой части оператор суперпозиции, параллельный оператор или условный оператор. Первичные конструкции вызовы предикатов. Имя предиката: имя базисного предиката; имя предиката, имеющего определение в программе; аргумент предиката имя переменной предикатного типа; в правой части определения предиката встречается данный вызов; имя переменной предикатного типа, являющейся результатом вызова ConsPred или ConsArray, находящегося в правой части того же определения, что и данный вызов. Программа замкнутый набор определений предикатов вызываемые предикаты либо базисные, либо имеют определение в программе. Программа на языке CCP

Исполнение программы: исполнение вызова A(z: u) s = newSect(z, u); (3.32) input(s[z]); runCall(s, A(z: u)); output(s[u]) Предикаты в качестве параметров предикатов Генератор CONS(x, B: A) CONS есть ConsPred или ConsArray Лемма Имеется вызов A(z: u), где A переменная предикатного типа. Тогда: ( B subs(A). CONS(B)) CONS(A). Доказательство следует из лемм 3.7, 3.8.

depend(B, C) непосредственная зависимость B от C в правой части определения B имеется вызов предиката C. def(B, C) B определяется через предикат C существуют предикаты D 1, D 2, …, D n (n > 0) такие, что B = D 1, C = D n и depend(D j, D j+1 ) (j = 1, …, n-1). Определение предиката B рекурсивно def(B, B) rec(B) = {C | def(B, C) & def(C, B)} рекурсивное кольцо Лемма C rec(B) rec(B) = rec(C). B косвенно зависит от C в правой части определения B имеется вызов предиката H(x, A: …) и C subs(A); H также зависит от C ConsPred(x, B: A). Сложная форма рекурсии для предиката B: A вызывается в правой части определения B ! Сложные формы рекурсии запрещены Рекурсивные определения предикатов

График предиката B(x: y) есть Gr(B) = {(x, y) | LS(B(x: y))}. Как следствие, LS(B(x: y)) (x, y) Gr(B). Представим графики оператора суперпозиции (3.16), параллельного оператора (3.19) и условного оператора (3.20), используя определения логической семантики операторов: GrS(P, Q) = Gr(B(x: z); C(z: y)) = {(x, y) | z. (x, z) P & (z, y) Q} (3.33) GrP(P, Q) = Gr(B(x: y)||C(x: z)) = {(x, y, z) | (x, y) P & (x, z) Q} (3.34) GrC(P, Q) = Gr(if (b) B(x: y) else C(x: y)) = (3.35) {(b, x, y) | b & (x, y) P} {(b, x, y) | b & (x, y) Q} Здесь графики P = Gr(B) и Q = Gr(C).

Рекурсивное кольцо предикатов A 1, A 2,…, A n : A i (x i : y i ) K i (x i : y i ); i = 1…n; n > 0, (3.36) где x i и y i наборы переменных, K i оператор суперпозиции, параллельный оператор или условный оператор. В операторах K i могут встречаться вызовы предикатов A 1, A 2,…, A n, а также вызовы других предикатов, не принадлежащих кольцу и определяемых вне кольца. G 1, G 2,…, G n графики предикатов A 1, A 2,…, A n. По системе (3.36) строится система уравнений для графиков предикатов: G = V(G), (3.37) где G = (G 1, G 2,…, G n ) вектор графиков предикатов, V = (Gr(K 1 ), Gr(K 2 ),…, Gr(K n )) вектор графиков операторов. Здесь Gr(K j )(x j : y j ) (j = 1,…, n) рассматривается как Gr(K j )(G 1, G 2,…, G n ); Gr(K j ) есть GrS, GrP или GrC. G вектор-график. G j = pr(j, G).

Отношение на множестве вектор-графиков, является полной решеткой. Минимальный элемент пустой график. Для произвольных вектор-графиков H и L истинно утверждение: H L i=1..n. H i L i (3.38) Отношение для каждой из компонент вектор-графика является полной решеткой. Рассмотрим цепь векторов-графиков {G m } m 0 : G 0 =, G m+1 = V(G m ), m 0 (3.39) Factorial(n: f) if (n = 0) f = 1 else f = n Factorial(n - 1) A0(n: f) A1( : c0, c1); A2(n, c0, c1: f) A1( : c0, c1) ConsIntZero( : c0) || ConsIntOne( : c1) A2(n, c0, c1: f) =(n, c0: b); A3(n, c1, b: f) A3(n, c1, b: f) if (b) =(c1: f) else A4(n, c1: f) A4(n, c1: f) -(n, c1: n1); A5(n, n1: f) A5(n, n1: f) A0(n1: f1); (n, f1: f) G = (G0, G2, G3, G4, G5 ).

A0(n: f) A1( : c0, c1); A2(n, c0, c1: f) A1( : c0, c1) ConsIntZero( : c0) || ConsIntOne( : c1) A2(n, c0, c1: f) =(n, c0: b); A3(n, c1, b: f) A3(n, c1, b: f) if (b) =(c1: f) else A4(n, c1: f) A4(n, c1: f) -(n, c1: n1); A5(n, n1: f) A5(n, n1: f) A0(n1: f1); (n, f1: f) G 0 =, G m+1 = V(G m ), m 0 (3.39) G3 1 : 0, 1, true 1 G2 2 : 0, 0, 1 1 G0 3 : 0 1 G5 4 : 1, 0 1 n1 = 0 как результат подстановки G0 4 ; G4 5 : 1, 1 1 G3 6 : 0, 1, true 1; G3 6 : 1, 1, false 1; G2 7 : 0, 0, 1 1; G2 7 : 1, 0, 1 1; G0 8 : 0 1; G0 8 : 1 1; и т.д.

Лемма Пусть {H m } m 0 возрастающая цепь вектор- графиков. Тогда : m 0 H m = ( m 0 H 1 m, …, m 0 H n m ). Лемма Пусть {H m } m 0 возрастающая цепь вектор- графиков и H ~ = m 0 H m. Пусть w H ~, где w набор вида (x 1, y 1, x 2, y 2, …, x n, y n ). Тогда k m k. w H m. Доказательство от противного. Допустим, что k набор w не принадлежит вектор-графику H k. Определим вектор- график H #, совпадающий с H ~ всюду, за исключением набора w, который ему не принадлежит. Предикат H # является верхней гранью последовательности {H m } m 0, причем H # H ~ и H # H ~, а тогда грань H ~ не является минимальной, что приводит к противоречию. Замечание. Лемма верна и для возрастающей цепи обычных графиков {H j m } m 0. Лемма Вектор-функция V, составленная из непрерывных функций V i (i = 1…n) непрерывна. Доказательство. Пусть {H m } m 0 возрастающая цепь вектор- графиков. В соответствии с леммой 3.12: m 0 V(H m ) = m 0 (V 1 (H m ), …, V n (H m )) = = ( m 0 V 1 (H m ), …, m 0 V n (H m ))= = (V 1 ( m 0 H m ), …, V n ( m 0 H m )) = V( m 0 H m ).

Лемма Функции GrS, GrP и GrC ( ) графиков оператора суперпозиции, параллельного оператора и условного оператора, непрерывны относительно вхождений графиков P и Q. Доказательство. Докажем непрерывность функции GrS(P, Q) для оператора суперпозиции. Пусть {H m } m 0 возрастающая цепь вектор-графиков. Здесь H вырождается в набор (P, Q). Необходимо доказать, что GrS( m 0 (P, Q) m ) = m 0 GrS((P, Q) m ). Это эквивалентно GrS( m 0 P m, m 0 Q m ) = m 0 GrS(P m, Q m ) при условии, что {P m } m 0 и {Q m } m 0 возрастающие цепи графиков предикатов. Итак, требуется доказать: {(x, y) | z. (x, z) m 0 P m & (z, y) m 0 Q m } = = m 0 {(x, y)| z. (x, z) P m & (z, y) Q m } Пусть (x, y) принадлежит множеству в левой части. Тогда для некоторого z 0 истинны (x, z 0 ) m 0 P m и (z 0, y) m 0 Q m. В соответствии с леммой 3.13 существует такое k, что (x, z 0 ) P k и (z 0, y) Q k. Далее, очевидно, (x, y) принадлежит правой части равенства. Нетрудно показать, что {(x, y)| z. (x, z) P m & (z, y) Q m } m 0 возрастающая цепь графиков. Допустим, (x, y) принадлежит наименьшей верхней грани этой цепи, т.е. правой части равенства. Принадлежность (x, y) множеству в правой части доказывается применением леммы Непрерывность функций GrP и GrC доказывается аналогично.

График GrC(P, Q) условного оператора if (b) B(x: y) else C(x: y) не является непрерывным относительно вхождения переменной b (не является даже монотонным). Поэтому вхождение b не может быть источником рекурсии. Ограничение: Допустим, значение переменной b является результатом вызова E(…: b…). Предикат, правой частью которого является условный оператор, и предикат E не могут входить в одно и то же рекурсивное кольцо. Допустим, система (3.36) определений кольца предикатов не использует сложные формы рекурсии и удовлетворяет отмеченному ограничению. Из лемм 3.14 и 3.15 следует, что вектор-график операторов V в системе уравнений G = V(G) для графиков кольца предикатов является непрерывным. В соответствии с теоремой Клини о неподвижной точке решение системы G = V(G) есть G = lfp(V) = m 0 G m, где G 0 =, G m+1 = V(G m ), m 0, lfp(V) наименьшая неподвижная точка (least fixed point) вектор-графика операторов V.

Пусть рекурсивный предикат D(z: u) принадлежит кольцу (3.36), т.е. D = A j для некоторого j. Логическая семантика предиката D определяется следующим образом: LS(D(z: u)) (z, u) pr(j, m 0 G m ) (3.40) Систему (3.36) определений кольца предикатов запишем в векторном виде: A K(A), где A = (A 1, A 2,…, A n ), K = (K 1, K 2,…, K n ). Определим цепь векторов предикатов {A m } m 0 : A 0 Ф, A m+1 K(A m ), m 0, (3.41) где Ф (F, F, …, F) вектор тотально ложных предикатов. Цепь {A m } m 0 соответствует цепи (3.39) вектор-графиков {G m } m 0, поскольку G m = (Gr(A m 1 ), Gr(A m 2 ),…, Gr(A m n )). G 0 =, G m+1 = V(G m ), m 0 (3.39) A i (x i : y i ) K i (x i : y i ); i = 1…n; n > 0, (3.36)

Структура рекурсивного кольца предикатов Пусть предикат D принадлежит кольцу и имеет определение, в правой части которого вызываются предикаты B и C. Тогда один из предикатов (или оба) принадлежат кольцу. В противном случае предикат D не будет принадлежать кольцу. В соответствии с определением D 0 = F, где F тотально ложный предикат. Далее, D 1 = F, если D имеет определение в виде оператора суперпозиции или параллельного оператора, поскольку конъюнкция двух вызовов предикатов, из которых один ложный, дает ложный предикат. Если D имеет определение в виде условного оператора, а вызываемые предикаты B и C оба принадлежат кольцу, то также имеем D 1 = F. Если во всех условных операторах, используемых в определениях предикатов кольца, оба вызываемых предиката принадлежат кольцу, то решением системы A = K(A) является набор тождественно ложных предикатов. Поэтому в дальнейшем будем считать, что в системе A = K(A) имеется по крайней мере один предикат с определением в виде условного оператора, причем в правой части один вызываемый предикат принадлежит кольцу, а другой нет.

Рекурсивное кольцо предикатов представим в виде: A K(A 1, A 2,…, A n, E 1, E 2,…, E s ) (3.42) E 1, E 2,…, E s, s > 0, предикаты, используемые в правых частях определений (3.36), но не принадлежащих данному кольцу. Лемма Пусть предикаты E 1, E 2,…, E s, используемые в системе (3.42), обладают свойством согласованности. Тогда рекурсивные предикаты A 1, A 2,…, A n кольца (3.42) обладают свойством согласованности. Доказательство. Пусть D(u: v) рекурсивный предикат кольца, т.е. D = A j для некоторого j. Докажем истинность Cons(D). Зафиксируем u и v. Допустим, D(u: v) истинно и докажем, что исполнение вызова D(u: v) на выбранных значениях набора u завершается вычислением значений набора v. В соответствии с LS (3.40) (u, v) pr(j, G). Существует w G такой, что (u, v) = pr(j, w). По лемме 3.13 существует k такой, что w G k. Доказательство реализуется индукцией по k. Рассмотрим случай k = 1, т.е. w G 1. Единственная возможность: правая часть D имеет вид условного оператора if (b) B(u: v) else C(u: v), причем значение b выбирает предикат B или C, не принадлежащий кольцу; в противном случае D(u: v) будет ложным. Поскольку выбранный предикат (B или C) обладает свойством согласованности, то его исполнение (а значит и исполнение D) завершается вычислением набора u, что завершает доказательство для k = 1.

Индукционное предположение для k>1: если предикат кольца P(t: q) истинен для t и q, а (t, q) поднабор некоторого w1 G m при m

Допустим, что для фиксированных значений u исполнение вызова D(u: v) завершается значениями набора v. Докажем истинность D(u: v). Совокупность исполняемых вызовов предикатов имеет форму дерева вызовов. Вершина дерева вызов предиката с конкретными значениями аргументов и результатов вызова. Начальной вершиной является вызов D(u: v). Листьями дерева являются вызовы предикатов E 1, E 2,…, E s. Два вызова связаны дугой, если второй вызов исполняется в теле определения предиката для первого вызова. Доказательство индукцией по высоте k дерева. Пусть высота k = 1. Это возможно, когда правая часть D есть if (b) B(u: v) else C(u: v), а предикат (B или C) является одним из E 1, E 2,…, E s. Из согласованности этих предикатов следует истинность исполняемого вызова, а значит, и истинность D(u: v). Будем использовать следующее индукционное предположение: если вызов P(t: q) является вершиной дерева вызовов, высота m поддерева, определяемого вызовом P(t: q), меньше k и исполнение вызова на наборе t завершается вычислением набора q, то P(t: q) истинно. Рассмотрим случай, когда определения D есть B(u: z); C(z: v). Допустим, что исполнение вызова B(u: z) (при исполнении D(u: v)) завершилось вычислением набора z 1. Если B является одним из E 1, E 2,…, E s, то вызов B(u: z 1 ) является истинным. Допустим, B принадлежит кольцу. Вызов B(u: z 1 ) определяет поддерево в дереве вызовов с высотой m = k - 1. В соответствии с индукционным предположением, вызов B(u: z 1 ) является истинным. Аналогично доказывается истинность вызова C(z 1 : v). Как следствие, истинна формула z. B(u: z) & C(z: v), что определяет истинность D(u: v). Доказательство для случаев, когда предикат D определяется в виде параллельного или условного оператора, проводится аналогично.

Теорема 3.1. При наличии в программе вызова вида ConsArray(x, B: A) предикат B определяет однозначную всюду определенную функцию. Допустим, что для всякого другого базисного предиката языка CCP реализуется свойство согласованности Cons( ). Пусть имеется программа на языке CCP, и ее исполнение реализуется вызовом предиката D(u: v). Тогда истинно Cons(D). Доказательство. Сначала доказательство проводится для программы, в которой нет переменных предикатного типа. Рассмотрим случай, когда программа не содержит рекурсивно определяемых предикатов. Пусть предикат D имеет определение в виде оператора суперпозиции (3.16), параллельного оператора (3.19) или условного оператора (3.20). В соответствии с леммами 3.3, 3.4 и 3.5 достаточно установить свойство согласованности для предикатов B и C, вызываемых в правой части определения. Если эти предикаты базисные, то для них это свойство является условием теоремы. Если один из них определяемый, то его полное замкнутое определение представляется частью программы меньшего размера, что позволяет применить доказательство по индукции.

Допустим, программа на языке CCP содержит несколько рекурсивных колец предикатов. Пусть кольцо определяется системой (3.42). Кольцо зависит от кольца, если один из предикатов E 1, E 2,…, E s принадлежит другому кольцу. Рекурсивные кольца образуют граф. Вершинами являются кольца, а дугами отношения зависимости колец. Допустим, что имеется цикл в графе колец. Тогда предикаты разных колец, находящихся на цикле, должны принадлежать одному кольцу. Следовательно, граф не имеет циклов и является деревом. Докажем свойство согласованности для предикатов произвольного рекурсивного кольца, определяемого системой (3.42). Рассмотрим различные пути от до листьев дерева колец. Пусть k максимальная длина пути по этому набору путей. Доказательство проводится индукцией k. При k = 0 предикаты E 1, E 2,…, E s не являются рекурсивно определяемыми и, следовательно, обладают свойством согласованности. По лемме 3.16 предикаты кольца обладают свойством согласованности. Предположим, что свойство согласованности доказано для колец с длиной пути m = k - 1, и докажем его для кольца. Рассмотрим предикат E j (j=1,…,s). Пусть E j принадлежит рекурсивному кольцу. Из кольца имеется дуга в кольцо. Поэтому максимальная длина пути для по крайней мере на единицу меньше, чем k. По индуктивному предположению предикаты кольца обладают свойством согласованности. Таким образом, предикаты E 1, E 2,…, E s обладают свойством согласованности. Свойство согласованности предикатов кольца следует из леммы 3.16.

Рассмотрим общий случай, когда программа П может содержать переменные предикатного типа. Обозначим через SUBS(П) набор предикатов, являющийся объединением множеств заместителей для всех переменных предикатного типа в программе П. Пусть П[M] минимальная программа, являющаяся частью П и содержащая определения предикатов набора M. Пусть П 0 = П, П j+1 = П j [SUBS(П j )], j = 0, 1, 2, …. Докажем, что при некотором k программа П k, а П k+1 =. Допустим обратное, т.е. существует такое k, что П k и П k+1 = П k. Пусть П k построено на базе заместителей B 1, B 2,…, B n ; n > 0. Тогда П k содержит вызовы генераторов Cons(x, B 1 : A 1 ), …, Cons(x, B n : A n ). Допустим, Cons(x, B 1 : A 1 ) встречается в программе П k [{B 1 }]. В П k [{B 1 }] должен встречаться вызов C(…), где C переменная предикатного типа и значение C получено от A 1 через параметры вызовов; иначе генератор становится ненужным и может быть исключен из программы. Поскольку вызов C(…) доступен при исполнении тела предиката B 1, то получаем рекурсивный вызов B 1 через вызов C(…) это сложная форма рекурсии, которая запрещена. Поэтому Cons(x, B 1 : A 1 ) не может встречаться в программе П k [{B 1 }]. Пусть он встречается в П k [{B 2 }]. Тогда из тела предиката B 2 через некоторый косвенный вызов C(…) вызывается предикат B 1. Если Cons(x, B 2 : A 2 ) встречается в П k [{B 1 }], то получим сложную форму рекурсии. Поэтому генератор Cons(x, B 2 : A 2 ) может быть доступен только из третьего предиката, например, B 3. Продолжая анализ для B 3 и далее, получим цепочку предикатов, которая неизбежно замкнется, что приведет к сложной форме рекурсии. Противоречие.

Итак, П k и П k+1 =. Программа П k не содержит переменных предикатного типа. Для этого случая теорема доказана. Тогда предикаты B 1, B 2,…, B n, входящие в SUBS(П k-1 ), обладают свойством согласованности. В соответствии с леммой 3.11 любой вызов вида C(…) в программе П k-1, где C переменная предикатного типа, обладает свойством согласованности. Доказательство теоремы, представленное выше, может быть повторено для программы П k-1. Доказательство теоремы для произвольной программы П i, i = k-1, …, 0, проводится по индукции. Лемма Имеется вызов A(z: u), где A переменная предикатного типа. Тогда: ( B subs(A). Cons(B)) Cons(A).