§ 37. Вероятностные оценки запросов

Определим вероятностные оценки n(N), h(N) запросов для пространства вычислений программы Pr по правилу R. Рассмотрим SLDF-дерево некоторого запроса N пространства вычислений. Если SLDF-дерево не успешно, то оценки n(N), h(N) не определены. Для успешного SLDF-дерева рассмотрим множество {SLDF^’₁, ..., SLDF^’_m} всех успешных нормализованных SLDF’-выводов целей Nq₁, ..., Nq_m у которых конечные запросы N¹_k1, ..., N^m_km не содержат переменных. Если это множество пусто, то оценки n(N), h(N) не определены.

Вычислим оценки n₁, ..., n_m, равные правой части неравенств следствия 4.4, для вероятностей m(Nq^{^}₁) ³ n₁, ..., m(Nq^{^}_m) ³ n_m запросов Nq₁, ..., Nq_m . Вычислим также оценки h₁, ...,  h_m, равные правой части неравенств теоремы 4.2 для условных вероятностей m(Nq^{^}₁ / N¹_k1F^{^}) > h₁, ...,  m(Nq^{^}_m / N^m_kmF^{^}) > h_m запросов Nq₁, ..., Nq_m. Положим n(N) = sup{n₁, ..., n_m}, h(N) = sup{h₁, ..., h_m}. Выбор операции sup не регламентируется чисто логическими соображениями. В данном случае автор исходит из желания объединить такие понятия как логический вывод (с вероятностными оценками) и предсказание.

Если один из выводов SLDF^’₁, ..., SLDF^’_m состоит только в применении фактов, то, как следует из теоремы, он будет иметь оценку h(N) = 1. Назовем такой SLDF-вывод проверкой истинности запроса N (по аналогии с семантическим программированием [104]). Предсказанием запроса N будем называть такой SLDF-вывод запроса Nq, на котором достигается оценка h(N). Оценкой предсказания запроса N будем называть величину h(N). Если предсказание не определено, то оценка предсказания h(N) не определена.

Пусть M = áU, mñ – вероятностная Эрбранова модель, согласованная с классом G.

Определение 28. Программа Pr истинна на Эрбрановой модели N, N £ Pr тогда и только тогда, когда каждое правило истинно на N. Правило истинно на N тогда и только тогда, когда оно истинно на N при любых состояниях (при любых отображениях r : X ® U) [90].

Определение 29. Программа Pr истинна на классе моделей G тогда и только тогда, когда N £ Pr, N Î G.

Распространим вероятность m на множество формул со свободными переменными F0. Для j Î F₀\S положим где QG – множество всех подстановок основных термов вместо переменных. Для правил C = A ¬ B₁, ..., B_k k ³ 0, определим условную вероятность равенством m(C) = m(A) / m(B₁& ... &B_k), если правило не содержит переменных, и равенствами

если правило содержит переменные. Если m((B₁& ... &B_k)q) = 0 для некоторой подстановки q Î QG или m(B₁& ... &B_k) = 0 для B₁& ... &B_k Î Â, то значение m(C) не определено. При k = 0 правило C = A ¬ рассматривается как правило A ¬ true с вероятностью посылки m(true) = 1. Далее запись m(C) всегда означает, что вероятность m(C) определена. Обозначим через PR0, PR0 Ì PR множество всех правил сигнатуры S, для которых вероятность m определена.

Лемма 13. m(jq) > m(j), j Î F₀, q – некоторая подстановка ■

Лемма 14. Если программа Pr истинна на классе моделей G, то m(C) = 1, C Î Pr.

Доказательство. Пусть C = A ¬ B₁, ..., B_k; C Î Pr, k > 0;

Рассмотрим правило C = Aq ¬ (B₁, ..., B_k)q, q Î QG, и условную вероятность m(Aq / (B₁, ..., B_k)q). Каждая подстановка q Î QG однозначно определяет некоторое состояние r : X ® U. Так как программа Pr истинна на G, для любого состояния, то для любой подстановки q Î QG будем иметь G(Aq ¬ (B₁, ..., B_k)q) = G. Так как мера m согласована с классом моделей G, то из G(j₁) = G(j₂) следует m(j₁) = m(j₂) и, следовательно, m(Aq ¬ (B₁, ..., B_k)q) = 1, откуда m(Aq / (B₁, ..., B_k)q) = 1. Поэтому m(C) = 1, если m(C) определена ■