§ 36. Оценки вероятностей и условных вероятностей запросов.

Пусть M = áU, mñ – вероятностная Эрбранова модель. Рассмотрим успешный SLDF-вывод N, N₁, ..., N_k запроса N с помощью последовательности правил C₀, C₁, ..., C_k-1 некоторой программы Pr, последовательности унификаций q₀, q₁, ..., q_k-1; q = q₀q₁ ... q_k-1 и некоторого правила вычислений R.

Последовательность запросов Nq, N₁q, ..., N_k, q = q₀q₁ ... q_k-1 также будет SLDF-выводом запроса Nq с помощью последовательности правил C₀q, C₁q, ..., C_k-1q тождественных подстановок и правила вычислений R. Будем предполагать, что Nq, N₁q, ..., N_k Î Â. В данном пункте факты A ¬ представим правилами A ¬ true. Тогда m(C) = m(A / true) = m(A), для фактов C = A ¬ , A Î Â.

Определим через N_i^{^} конъюнкцию всех не подчеркнутых атомов запроса N_i. Если все атомы подчеркнуты (как в запросе N_k), то положим N_k^{^} º true. Обозначим через N_iF^{^} конъюнкцию всех подчеркнутых атомов запроса N_i. Тогда N_iF^{^} – конъюнкция всех фактов, использованных в SLDF-выводе запроса Nq.

Цель данного пункта – оценить вероятности m(Nq^{^}), m(Nq^{^} / N_kF^{^}) по SLDF-выводу запроса Nq, предполагая, что нам известны только вероятности фактов и правил.

Рассмотрим вывод запросов (1) из запроса Nq = (¬ A₁& ... &A_i& ... &A_k)q, k ³ 1 по правилу (A_i ¬ B₁, ..., B_l)q. Представим запросы (1) в виде N₁q = ( ¬ A₁, ..., A_i-1, B, A_i+1, ..., A_k)q, B = B₁, ..., B_l и Nq = ( ¬ A₁, ..., A_i, ..., A_k)q. Конъюнкция Nq^{^} является частным случаем конъюнкции N₁q^{^}, когда B = true. Оценим вероятности m(Nq^{^}), m(Nq^{^} / N₁q^{^}) в предположении, что нам известны только вероятности m(N₁q^{^}), m(A_iq), m(Bq), p = m(A_iq / Bq^{^}).

Лемма 12. Если m(N₁q^{^}) > 0 и m(Bq) > 0, то

1) m(Nq^{^}) < m(ØBq^{^}) + min{m(N₁q^{^}), m(Aq&Bq^{^})};

2) m(Nq^{^}) > m(N₁q^{^}) - (1-p)m(Bq^{^});

3) m(Nq^{^} / N₁q^{^}) < p / m(Nq^{^} / Bq^{^});

4) m(Nq^{^} / N₁q^{^}) > 1 - (1 - p) / m(Nq^{^} / Bq^{^})

Доказательство. 1) m(Nq^{^}) = m(Nq^{^}&Bq^{^}) + m(Nq^{^}&ØBq^{^}) £ m(ØBq^{^}) + m(Nq^{^}&Bq^{^}) £ m(ØBq^{^}) + min{m(N₁q^{^}), m(Aq&Bq^{^})};

3) m(Nq^{^} / N₁q^{^}) = m(Nq^{^}&Bq^{^}) / m(N₁q^{^}) £ m(Aq&Bq^{^}) / m(N₁q^{^}) = p*m(Bq^{^}) / m(N₁q^{^}) = p / m(Nq^{^} / Bq^{^});

2) m(Nq^{^}) ³ m(Nq^{^}&Bq^{^}) ³ m(Nq^{^}&Bq^{^}) - m(ØNq^{^}&ØAq^{^}&Bq^{^}). Выражение из правой части п. 2 утверждения леммы равно этому же выражению: m(N₁q^{^}) - (1-p)m(Bq^{^}) = m(N₁q^{^}) + m(Aq&Bq^{^}) - m(Bq^{^}) = m(N₁q^{^}&Aq) + m(N₁q^{^}&ØAq) + m(Aq&Bq^{^}&Nq^{^}) + m(Aq&Bq^{^}&ØNq^{^}) - m(Bq^{^}) = m(Bq^{^}&Nq^{^}&Aq) + m(Bq^{^}&Nq^{^}&ØAq) + m(Bq^{^}&Aq&Nq^{^}) + m(Bq^{^}&Aq&ØNq^{^}) - m(Bq^{^}) = m(Bq^{^}&Nq^{^}&Aq) - m(Bq^{^}&ØNq^{^}&ØAq) = m(Nq^{^}&Bq^{^}) - m(ØNq^{^}&ØAq&Bq^{^});

4. m(Nq^{^} / N₁q^{^}) = m(Nq^{^}&Bq^{^}) / m(N₁q^{^}) ³ (m(N₁q^{^}) – (1-p)m(Bq^{^})) / m(N₁q^{^}) = 1 - (1-p) / m(Nq^{^} / Bq^{^}) (см. доказательство п. 2.) ■

Следствие 4. Если m(N₁q^{^}) > 0, m(Bq^{^}) > 0 и p = 1, то:

1) m(N₁q^{^}) £ m(Nq^{^}) £ min{1, m(ØBq^{^}) + m(N₁q^{^})};

2) m(Nq^{^} / N₁q^{^}) = 1.

Доказательство. Подставим в предыдущую лемму значение p = 1. Второе из неравенств 1 следует из того, что величина min{m(N₁q^{^}), m(Aq&Bq^{^})} равна либо m(N₁q^{^}), либо m(Bq^{^}). Во втором случае m(ØBq^{^}) + m(Bq^{^}) = 1 ■

Следствие 5. Если m(N₁q^{^}) > 0 и правило является фактом (A ¬ true)q, то:

1) m(Nq^{^}) £ min{m(N₁q^{^}), m(Aq)};

2) m(Nq^{^}) ³ m(N₁q^{^}) + m(Aq) - 1;

3) m(Nq^{^} / N₁q^{^}) £ m(Aq) / m(N₁q^{^});

4) m(Nq^{^} / N₁q^{^}) ³ 1 - (1 - m(Aq)) / m(N₁q^{^}).

Доказательство. Следует из предыдущей леммы и равенств p = m(Aq), m(Nq^{^}) = m(N₁q^{^}) ■

Следствие 6. Если m(Bq^{^}) > 0, то:

1) m(Nq^{^}&Bq^{^}) £ min{m(N₁q^{^}), m(Aq&Bq^{^})};

2) m(Nq^{^}&Bq^{^}) ³ m(N₁q^{^}) - (1-p)m(Bq^{^}).

Доказательство. Следует из доказательств пп. 1, 2 леммы ■

Рассмотрим SLDF-вывод Nq, N₁q, ..., N_k запроса Nq посредством последовательности правил C_iq = (A ¬ Bⁱ₁, ..., Bⁱ_li)q, i = 0, 1, ...,  k-1 и пустых унификаций. Положим Bⁱq = (Bⁱ₁& ... &Bⁱ_li)q, p_i = m(C_iq).

Теорема 11. Если m(Bⁱq) > 0, i = 0, 1, ..., k-1, то:

m(Nq^{^}&A⁰q&A¹q& ... &A^k-1q) ³ 1 - m(Bⁱq)

Доказательство. Используем оценку 2 следствия, примененную к последнему шагу вывода от N_k-1q^{^} к N_k. Получим m(N_k-1q^{^}&B^k-1q) ³ m(N_k^{^}) - (1 - p_k-1)m(B^k-1q), где m(N_k^{^}) = m(true) = 1, так как все атомы выделены. Рассмотрим вывод запроса N_k-1q^{^}&B^k-1q из запроса N_k-2q^{^}&B^k-1q посредством правила C_k-2q. Снова применим оценку 2 следствия. Получим: m(N_k-2q^{^}&B^k-1q&B^k-2q) ³ m(N_k-1^{^}&B^k-1q) - (1-p_k-2)m(B^k-2q). Рассмотрим вывод запроса N_k-2q^{^}&B^k-1q&B^k-2q из запроса N_k-3q^{^}&B^k-1q&B^k-2q посредством правила C_k-3q и т. д. Получим m(Nq^{^}&B⁰q&B¹q&…&B^k-1q) ³ m(N₁q^{^}&B¹q&…&B^k-1q) - (1 - p₀)m(B⁰q). Подставляя левые части неравенств в их правые части, получаем оценку

m(Nq^{^}&B⁰q&B¹q& … &B^k-1q) ³ 1 - m(Bⁱq).

Покажем, что если из конъюнкции m(Nq^{^}&B⁰q&B¹q& … &B^k-1q) удалить все константы true, то получим конъюнкцию m(Nq^{^}&A⁰q&A¹q&…&A^k-1q). Заметим, что каждый атом конъюнкции Bⁱq (true – не атом) в процессе вывода обязательно унифицируется с левой частью одного из правил. Следовательно, каждый атом конъюнкции B⁰q&B¹q& … &B^k-1q содержится в конъюнкции A⁰q&A¹q&…&A^k-1q. С другой стороны, каждый атом Aⁱq, i = 0, 1, ..., k-1 содержится либо в Nq^{^}, либо в правой части одного из правил C_iq, i = 0, 1, ..., k-1 ■

Следствие 7. Если m(Bⁱq) > 0, i = 0, 1, ..., k-1, то:

m(Nq^{^}) ³ 1 - m(Bⁱq).

Доказательство. Следует из m(Nq^{^}) > m(Nq^{^}&A⁰q& ... &A^k-1q) и теоремы 4.1 ■

Для каждого успешного SLDF-вывода Nq = N₀q, N₁q, ..., N_k существует успешный SLDF’-вывод Nq = N₀q, N^’₁q, ..., N^’_iq, ..., N_k, в котором факты применяются последними и до запроса N^’_iq применяются правила C_j с длиной l_j ³ 1; j = 0, ..., i-1. Тогда запрос N^’_iq будет иметь вид ¬ A₁, ..., A_m, а запрос N_k – вид ¬ A₁, ..., A_m. Такой SLDF^’ - вывод будем называть нормализованным.

Теорема 12. Если m(B^jq) > 0, j = 0,1, ..., i-1, и m(N_kF^{^}) > 0, то

m(Nq^{^} / N_kF^{^}) ³ 1 - m(B^jq) / m(N_kF^{^}),

где p_j – условные вероятности, а B^jq – условия правил C_j, j = 1, ..., i-1.

Доказательство: Проводится аналогично доказательству предыдущей теоремы, но для нормализованного вывода и начинается с запроса i. Первое неравенство имеет вид m(N_i-1q^ &B^i-1q) ³ m(N_iq^) - (1-p_i-1)m(B^i-1q), где m(N_iq^{^}) = m(N_kF^{^}). Далее, рассуждая как в теореме 4.1, получаем неравенство m(Nq^{^}&B⁰q& … &B^i-1q) ³ m(N_kF^{^}) - m(B^jq). Так как m(Nq^{^}& B⁰q& … &B^i-1q) £ m(Nq^{^}&N_kF^{^}), то m(Nq^{^} / N_kF^{^}) = m(Nq^{^}&N_kF^{^}) / m(N_kF^{^}) ³ (m(N_kF^{^}) - m(B^jq)) / m(N_kF^{^}) ■