Рекурсивные определения предикатов

Для определяемых предикатов B и C отношение depend(B, C) обозначает непосредственную зависимость B от C, если в правой части определения B имеется вызов предиката C. Предикат B определяется через предикат C, def(B, C), если существуют предикаты D₁, …, D_n (n > 1) такие, что B = D₁, C = D_n и depend(D_j, D_j₊₁) (j = 1, …, n - 1).

Определение предиката B рекурсивно, если истинно отношение def(B, 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(x, A: …) определяет также зависимость между предикатами H и C, так как предикат C вызывается в правой части определения H. Косвенная зависимость предикатов может оказаться источником рекурсии. В частности, при наличии генератора CONS(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). Представим графики оператора суперпозиции (4.16), параллельного оператора (4.19) и условного оператора (4.20), используя определения логической семантики операторов:

GrS(P, Q) = Gr(B(x: z); C(z: y)) = {(x, y) | $z. (x, z) Î P & (z, y) Î Q} ; (4.33)

GrP(P, Q) = Gr(B(x: y) || C(x: z)) = {(x, y, z) | (x, y) Î P & (x, z) Î Q} ; (4.34)

GrC(P, Q) = Gr(if (b) B(x: y) elseC(x: y)) = {(b, x, y) | b & (x, y) Î P} È (4.35)

{(b, x, y) | Øb & (x, y) Î Q} .

Здесь графики P = Gr(B) и Q = Gr(C).

Определим график для рекурсивного предиката, а через график - логическую семантику. Пусть имеется рекурсивное кольцо предикатов A₁, A₂,…, A_n:

A_i(x_i: y_i) º K_i(x_i: y_i); i = 1…n; n > 0, (4.36)

где x_i и y_i - наборы переменных, K_i - оператор суперпозиции (4.16), параллельный оператор (4.19) или условный оператор (4.20). В операторах K_i могут встречаться вызовы предикатов A₁, A₂,…, A_n, а также вызовы других предикатов, не принадлежащих кольцу и определяемых вне кольца.

Обозначим графики предикатов A₁, A₂,…, A_n через G₁, G₂,…, G_n соответственно. По системе определений (4.36) строится система уравнений для графиков предикатов:

G = V(G) , (4.37)

где G = (G₁, G₂,…, G_n) - вектор графиков предикатов; V = (Gr(K₁), Gr(K₂),…, Gr(K_n)) - вектор графиков операторов. Здесь Gr(K_j)(x_j:y_j) (j = 1,…, n) рассматривается как Gr(K_j)(G₁, G₂,…, G_n); Gr(K_j) есть GrS, GrP или GrC.

Вектор G определяет множество значений вида (x₁, y₁, x₂, y₂, …, x_n, y_n) и является графиком, называемым вектор-графиком. График G_j есть j-я компонента (проекция) вектор-графика G, т. е. G_j = pr(j, G).

Отношение включения “Í”, определенное на множестве вектор-графиков, является полной решеткой [4; 5]. Минимальным элементом решетки является пустой график Æ. Для произвольных вектор-графиков H и L истинно утверждение

H Í L º "i=1..n. H_i Í L_i . (4.38)

Отношение “Í” для каждой из компонент вектор-графика является полной решеткой.

Рассмотрим цепь векторов-графиков {G^m}_m_³₀, определяемую следующим образом:

G⁰ = Æ, G^m⁺¹ = V(G^m), m ³ 0 . (4.39)

Естественно ожидать, что предел последовательности {G^m}_m_³₀ (если он существует) даст нам неподвижную точку - решение системы G = V(G). Построение неподвижной точки рассмотрим на примере следующей программы для вычисления факториала натурального числа n:

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) [16] ;

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); предикат A1 не входит в кольцо. Проследим несколько шагов построения неподвижной точки, где шаг соответствует переходу от G^m к G^m⁺¹. Вначале G⁰ = Æ, т. е. каждый из шести графиков пуст. Подставляя эти значения графиков в правые части определений, получим значения графиков на первом шаге, остающиеся пустыми, кроме G3¹, которому присваивается первая альтернатива условного оператора. Анализируя предыдущие определения, получим значение графика G3¹:0, 1, true® 1. На втором шаге изменится только значение графика G2, на третьем - G0. В итоге получаем следующую цепочку модификаций, в которой на каждом шаге мы указываем лишь изменившиеся компоненты вектора G :

G3¹: 0, 1, true® 1;

G2²: 0, 0, 1® 1;

G0³: 0® 1;

G5⁴: 1, 0® 1 - параметр n1 = 0 как результат подстановки G0³;

G4⁵: 1, 1® 1;

G3⁶: 0, 1, true® 1; G3⁶: 1, 1, false® 1;

G2⁷: 0, 0, 1® 1; G2⁷: 1, 0, 1® 1;

G0⁸: 0® 1; G0⁸: 1® 1; и т. д.

Лемма 4.12. Пусть {H^m}_m_³₀ - возрастающая цепь вектор-графиков. Тогда для наименьшей верхней грани цепи (см. разд. 3.1) справедливо равенство

È_m_³₀H^m = (È_m_³₀H₁^m, …, È_m_³₀H_n^m) .

Лемма 4.13. Пусть {H^m}_m_³₀ - возрастающая цепь вектор-графиков и H^~ = È_m_³₀H^m. Пусть w Î H^~, где w - набор вида (x₁, y₁, x₂, y₂, …, x_n, y_n). Тогда $k "m³k. w Î H^m.

Доказательство от противного. Допустим, что для всех k набор w не принадлежит вектор-графику H^k. Определим вектор-график H^#, совпадающий с H^~ всюду, за исключением набора w, который ему не принадлежит. Предикат H^# является верхней гранью последовательности {H^m}_m_³₀, причем H^# Í H^~ и H^# ¹ H^~, а тогда грань H^~ не является минимальной, что приводит к противоречию. □

Замечание. Лемма верна и для возрастающей цепи обычных графиков {H_j^m}_m_³₀.

Лемма 4.14. Вектор-функция V, составленная из непрерывных функций V_i (i = 1, …, n), является непрерывной. Понятие непрерывности функций определено в разд. 3.1.

Доказательство. Пусть {H^m}_m_³₀ - возрастающая цепь вектор-графиков. В соответствии с леммой 4.12 имеет место цепочка равенств:

È_m_³₀V(H^m) = È_m_³₀(V₁(H^m), …, V_n(H^m)) = (È_m_³₀V₁(H^m), …, È_m_³₀V_n(H^m)) = = (V₁(È_m_³₀H^m), …, V_n(È_m_³₀H^m)) = V(È_m_³₀H^m). □

Лемма 4.15. Функции GrS, GrP и GrC (4.33-4.35), определяющие соответственно графики оператора суперпозиции, параллельного оператора и условного оператора, непрерывны относительно вхождений графиков P и Q.

Доказательство. Докажем непрерывность функции GrS(P, Q) для оператора суперпозиции. Пусть {H^m}_m_³₀ - возрастающая цепь вектор-графиков. Здесь H вырождается в набор (P, Q). Необходимо доказать, что GrS(È_m_³₀(P, Q)^m) = È_m_³₀ GrS((P, Q)^m). Это эквивалентно GrS(È_m_³₀P^m, È_m_³₀Q^m) = È_m_³₀ GrS(P^m, Q^m) при условии, что {P^m}_m_³₀ и {Q^m}_m_³₀ - возрастающие цепи графиков предикатов. Итак, требуется доказать:

{(x, y) | $z. (x, z) Î È_m_³₀P^m & (z, y) Î È_m_³₀Q^m} = È_m_³₀{(x, y)|$z. (x, z) Î P^m & (z, y) Î Q^m}.

Пусть (x, y) принадлежит множеству в левой части. Тогда для некоторого z₀ истинны (x, z₀) Î È_m_³₀P^m и (z₀, y) Î È_m_³₀Q^m. В соответствии с леммой 4.13 существует такое k, что (x, z₀) Î P^k и (z₀, y) Î Q^k. Далее, очевидно, (x, y) принадлежит правой части равенства.

Нетрудно показать, что {(x, y)|$z. (x, z) Î P^m & (z, y) Î Q^m}_m_³₀ - возрастающая цепь графиков. Допустим, (x, y) принадлежит наименьшей верхней грани этой цепи, т. е. правой части равенства. Принадлежность (x, y) множеству в правой части доказывается применением леммы 4.13.

Доказательство непрерывности функций GrP и GrC проводится аналогично.□

График GrC(P, Q) условного оператора if (b) B(x: y) elseC(x: y) не является непрерывным относительно вхождения переменной b [17]. Поэтому вхождение b не может быть источником рекурсии. Ограничение: допустим, значение переменной b является результатом вызова E(…: b…). Предикат, правой частью которого является условный оператор, и предикат E не могут входить в одно и то же рекурсивное кольцо.

Допустим, система (4.36) определений кольца предикатов не использует сложные формы рекурсии и удовлетворяет отмеченному ограничению. Из лемм 4.14 и 4.15 следует, что вектор-график операторов V в системе уравнений G = V(G) для графиков кольца предикатов является непрерывным. В соответствии с теоремой Клини о неподвижной точке (см. разд. 3.1 и [4, 7]) решение системы G = V(G) есть G = lfp(V) = È_m_³₀G^m, где G⁰ = Æ, G^m⁺¹ = V(G^m), m ³ 0 (т. е. цепь (40)), lfp(V) - наименьшая неподвижная точка (least fixed point) вектор-графика операторов V.

Пусть рекурсивный предикат D(z:u) принадлежит кольцу (4.36), т. е. D = A_j для некоторого j. Логическая семантика предиката D определяется следующим образом:

LS(D(z:u)) @ (z,u) Î pr(j, È_m_³₀G^m) . (4.40)

Систему (4.36) определений кольца предикатов запишем в векторном виде: A º K(A), где A = (A₁, A₂,…, A_n); K = (K₁, K₂,…, K_n). Определим цепь векторов предикатов {A^m}_m_³₀:

A⁰ º Ф, A^m⁺¹ º K(A^m), m ³ 0, (4.41)

где Ф @ (F, F, …, F) - вектор тотально ложных предикатов. Цепь {A^m}_m_³₀ соответствует цепи (4.39) вектор-графиков {G^m}_m_³₀, поскольку G^m = (Gr(A^m₁), Gr(A^m₂),…, Gr(A^m_n)).

Рассмотрим подробнее структуру рекурсивного кольца предикатов. Пусть предикат D принадлежит кольцу и имеет определение, в правой части которого вызываются предикаты B и C. Тогда один из предикатов (или оба) принадлежат кольцу. В противном случае предикат D не будет принадлежать кольцу. В соответствии с определением последовательности {A^m}_m_³₀ и цепи (4.39) D⁰ = F. Далее, D¹ = F, если D имеет определение в виде оператора суперпозиции или параллельного оператора, поскольку конъюнкция двух вызовов предикатов, из которых один ложный, дает ложный предикат. Если D имеет определение в виде условного оператора, а вызываемые предикаты B и C оба принадлежат кольцу, то также имеем D¹ = F. Если во всех условных операторах, используемых в определениях предикатов кольца, оба вызываемых предиката принадлежат кольцу, то решением системы (4.36) является набор тождественно ложных предикатов. Поэтому в дальнейшем будем считать, что в системе (4.36) имеется по крайней мере один предикат с определением в виде условного оператора, причем в правой части один вызываемый предикат принадлежит кольцу, а другой - нет.

Рекурсивное кольцо предикатов (4.36) представим в виде

A º K(A₁, A₂,…, A_n, E₁, E₂,…, E_s) . (4.42)

Здесь E₁, E₂,…, E_s, s > 0, - предикаты, используемые в правых частях определений (4.36), но не принадлежащих данному кольцу.

Лемма 4.16. Предположим, что предикаты E₁, E₂,…, E_s, используемые в системе (4.42), обладают свойством согласованности. Тогда рекурсивные предикаты A₁, A₂,…, A_n кольца (4.42) обладают свойством согласованности.

Доказательство. Пусть D(u:v) - рекурсивный предикат кольца, т. е. D = A_j для некоторого j. Докажем истинность Cons(D). Зафиксируем значения наборов u и v.

Допустим, D(u:v) истинно, и докажем, что исполнение вызова D(u:v) на выбранных значениях набора u завершается вычислением значений набора v. В соответствии с (4.40) (u,v) Î pr(j, G). Существует w Î G такой, что (u,v) = pr(j, w). По лемме 4.13 существует k такой, что w Î G^k. Доказательство реализуется индукцией по k. Рассмотрим случай k = 1, т. е. w Î G¹. Единственная возможность: правая часть определения D имеет вид условного оператора if (b) B(u:v) elseC(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 < k, то исполнение предиката P на наборе t завершается набором q. Рассмотрим случай, когда правая часть определения D имеет вид оператора суперпозиции B(u:z); C(z:v). Истинность D(u:v) определяет истинность $z. B(u:z) & C(z:v). Допустим, предикат B принадлежит кольцу и B = A_i. Тогда для некоторого z₀ истинно (u,z₀) Î pr(i, G^k^-1), иначе в соответствии с определением (4.33) для GrS получим: (u,v) Ï pr(j, G^k), что приводит к противоречию. В соответствии с индукционным предположением, исполнение B(u:z₀) завершается получением набора z₀. Нетрудно доказать истинность C(z₀,v). Далее, если предикат C принадлежит кольцу, то аналогичным образом, набор (z₀,v) должен входить в G^k^-1 для предиката C и, по индуктивному предположению, исполнение вызова C(z₀,v) завершается вычислением набора v. Как следствие, исполнение D(u:v) завершается набором v, что доказывает первую часть истинности Cons(D). Если предикат B или C не принадлежит кольцу, т. е. находится среди E₁, E₂,…, E_s, то используется свойство согласованности этих предикатов. Доказательство для случаев, когда предикат D определяется в виде параллельного или условного оператора, является более простым.

Допустим, что для фиксированных значений u исполнение вызова D(u:v) завершается выбранными значениями набора v. Докажем истинность D(u:v). Совокупность исполняемых вызовов предикатов имеет форму дерева вызовов. Вершина дерева - вызов предиката с конкретными значениями аргументов и результатов вызова. Начальной вершиной является вызов D(u:v). Листья дерева - вызовы предикатов E₁, E₂,…, E_s. Два вызова связаны дугой, если второй вызов исполняется в теле определения предиката для первого вызова. Доказательство проводится индукцией по высоте k дерева. Пусть высота k = 1. Это возможно лишь в случае, когда правая часть определения D имеет вид условного оператора if (b) B(u:v) elseC(u:v), а предикат (B или C), соответствующий исполняемому вызову, является одним из E₁, E₂,…, 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₁. Если B является одним из E₁, E₂,…, E_s, то вызов B(u:z₁) является истинным. Допустим, B принадлежит кольцу. Вызов B(u:z₁) определяет поддерево в дереве вызовов с высотой m = k - 1. В соответствии с индукционным предположением, вызов B(u:z₁) является истинным. Аналогично доказывается истинность вызова C(z₁:v). Как следствие, истинна формула $z. B(u:z) & C(z:v), что определяет истинность D(u:v). Доказательство для случаев, когда предикат D определяется в виде параллельного или условного оператора, проводится аналогично. □

Теорема 4.1. Допустим, что при наличии в программе вызова вида ConsArray(x, B: A) предикат B определяет однозначную всюду определенную функцию. Допустим, что для всякого другого базисного предиката j языка CCP реализуется свойство согласованности Cons(j). Пусть имеется программа на языке CCP, и ее исполнение реализуется вызовом предиката D(u:v). Тогда истинно Cons(D).

Доказательство. Сначала доказательство проводится для программы, в которой нет переменных предикатного типа.

Рассмотрим случай, когда программа не содержит рекурсивно определяемых предикатов. Пусть предикат D имеет определение в виде оператора суперпозиции (4.16), параллельного оператора (4.19) или условного оператора (4.20). В соответствии с леммами 4.3, 4.4 и 4.5 достаточно установить свойство согласованности для предикатов B и C, вызываемых в правой части определения. Если эти предикаты базисные, то для них это свойство является условием теоремы. Если один из них определяемый, то его полное замкнутое определение представляется частью программы меньшего размера, что позволяет применить доказательство по индукции.

Допустим, программа на языке CCP содержит несколько рекурсивных колец предикатов. Пусть кольцо a определяется системой (4.42). Кольцо a зависит от кольца b, если один из предикатов E₁, E₂,…, E_s принадлежит другому кольцу b. Рекурсивные кольца образуют граф. Вершинами являются кольца, а дугами - отношения зависимости колец. Допустим, что имеется цикл в графе колец. Нетрудно доказать, что предикаты разных колец, находящихся на цикле, должны принадлежать одному кольцу. Следовательно, граф не имеет циклов и является деревом.

Докажем свойство согласованности для предикатов произвольного рекурсивного кольца a, определяемого системой (4.42). Рассмотрим различные пути от a до листьев дерева колец. Пусть k - максимальная длина пути по этому набору путей. Доказательство проводится индукцией k. При k = 0 предикаты E₁, E₂,…, E_s не являются рекурсивно определяемыми и, следовательно, обладают свойством согласованности. По лемме 4.16 предикаты кольца обладают свойством согласованности. Предположим, что свойство согласованности доказано для колец с длиной пути m = k - 1, и докажем его для кольца a. Рассмотрим предикат E_j (j = 1, …, s). Пусть E_j принадлежит рекурсивному кольцу b. Из кольца a имеется дуга в кольцо b. Поэтому максимальная длина пути для b по крайней мере на единицу меньше, чем k. По индуктивному предположению предикаты кольца b обладают свойством согласованности. Таким образом, предикаты E₁, E₂,…, E_s обладают свойством согласованности. Свойство согласованности предикатов кольца a следует из леммы 4.16.

Рассмотрим общий случай, когда программа П может содержать переменные предикатного типа. Обозначим через SUBS(П) набор предикатов, являющийся объединением множеств заместителей для всех переменных предикатного типа в программе П. Для набора предикатов M из П обозначим через П[M] минимальную программу, являющуюся частью П и содержащую определения предикатов набора M. Пусть П₀ = П, П_j₊₁ = П_j[SUBS(П_j)], j = 0, 1, 2, …. Докажем, что при некотором k программа П_k ¹ Æ, а П_k₊₁ = Æ. Допустим обратное, т. е. существует такое k, что П_k ¹ Æ и П_k₊₁ = П_k. Пусть П_k построено на базе заместителей B₁, B₂,…, B_n; n > 0. Тогда П_k содержит вызовы генераторов CONS(x, B₁:A₁), …, CONS(x, B_n:A_n). Допустим, CONS(x, B₁:A₁) встречается в программе П_k[{B₁}]. В этой программе должен встречаться вызов C(…), где C - переменная предикатного типа и значение C получено от A₁ через параметры вызовов; если это не так, то генератор становится ненужным и может быть исключен из программы. Поскольку вызов C(…) доступен при исполнении тела предиката B₁, то получаем рекурсивный вызов B₁ через вызов C(…)- это сложная форма рекурсии, которая запрещена. Поэтому CONS(x, B₁:A₁) не может встречаться в программе П_k[{B₁}]. Пусть он встречается в П_k[{B₂}]. Тогда из тела предиката B₂ через некоторый косвенный вызов C(…) вызывается предикат B₁. Если CONS(x, B₂:A₂) встречается в П_k[{B₁}], то получим сложную форму рекурсии. Поэтому генератор CONS(x, B₂:A₂) может быть доступен только из третьего предиката, например, B₃. Продолжая анализ для предикатов B₃ и далее, получим цепочку предикатов, которая неизбежно замкнется, что приведет к сложной форме рекурсии. Получили противоречие.

Итак, П_k ¹ Æ и П_k₊₁ = Æ. Программа П_k не содержит переменных предикатного типа. Для этого случая теорема доказана. Тогда предикаты B₁, B₂,…, B_n, входящие в SUBS(П_k_-1), обладают свойством согласованности. В соответствии с леммой 4.11 любой вызов вида C(…) в программе П_k_-1, где C - переменная предикатного типа, обладает свойством согласованности. Доказательство теоремы, представленное выше, может быть повторено для программы П_k_-1, поскольку согласно принятым ограничениям вызов вида C(…) не может участвовать в рекурсии. Доказательство теоремы для произвольной программы П_i, i = k - 1, …, 0, проводится по индукции. □