27.10.10 Лекция 5Предикатное программирование
Пусть рекурсивный предикат D(z: u) принадлежит кольцу (3.36), т.е. D = Aj для некоторого j. Логическая семантика предиката D определяется следующим образом: LS(D(z: u)) ≅ (z, u)∈pr(j, ∪m≥0Gm) (3.40) Систему (3.36) определений кольца предикатов запишем в векторном виде: A ≡ K(A), где A = (A1, A2,…, An), K = (K1, K2,…, Kn). Определим цепь векторов предикатов {Am}m≥0: A0 ≡ Ф, Am+1 ≡ K(Am), m ≥ 0, (3.41) где Ф ≅ (F, F, …, F) ⎯ вектор тотально ложных предикатов. Цепь {Am}m≥0 соответствует цепи (3.39) вектор-графиков {Gm}m≥0, поскольку Gm = (Gr(Am1), Gr(Am2),…, Gr(Amn)). G0 = ∅, Gm+1 = V(Gm), m ≥ 0 (3.39) Ai(xi: yi) ≡ Ki(xi: yi); i = 1…n; n > 0, (3.36) Рекурсивное кольцо предикатов представим в виде: A ≡ K(A1, A2,…, An, E1, E2,…, Es) (3.42) E1, E2,…, Es, s > 0, ⎯ предикаты, используемые в правых частях определений (3.36), но не принадлежащих данному кольцу. Лемма 3.16. Пусть предикаты E1, E2,…, Es, используемые в системе (3.42), обладают свойством согласованности. Тогда рекурсивные предикаты A1, A2,…, An кольца (3.42) обладают свойством согласованности.