Разрешимость логических программ. Спецификация программ
Разрешимость ЛП и значение ЛП – тесно связанные понятия.
Пусть Р – множество процедур, G- задача: ?g1(t), …, gn(t).
Тогда парой (P, G) обозначим программу.
Определение 6. (P, G) разрешима <=> ($Θ) (P |= g1(tΘ), …, gn(tΘ)).
Разрешимость пары (P, G) можно установить либо исполнением программы (P,G), либо анализом спецификаций этой программы.
Определение 7. Спецификация программы (P, G) – это любое множество определений, которое точно задает каждое отношение программы.
Пример. Специфицируем отношение подмножества (X, Y), т.е. X – подмножество Y.
S1: подмножество(X, Y) <=> ("U) (U Î Y если U Î X).
Обозначим S = { S1, …, Sn}, P = { P1, …, Pm, G}.
Доказательство корректности P относительно S и является проверкой правильности программы (верификацией).
Верификация сводится к доказательству того,
1. что вычисленные решения являются правильными,
2. все правильные решения получены данными программы.
Полагаем:
что G представляет только одну цель, только один вызов,
что S непротиворечиво, написано на языке логики предикатов 1 порядка.
Обозначим:
gs – основное специфицируемое отношение,
Rs – множество решений tΘ, которые удовлетворяют соотношению S |= gs(tΘ).
Это интервал целевого утверждения относительно S: Rs = { tΘ | S |= gs(tΘ) }
(если t содержит термы-переменные, то gs(t) выделит некоторую часть отношения gs).
Определение 8. Решение tΘ называется специфицируемым, если tΘ Î Rs.
Верификация программы (P, G) должна выяснить, является ли tΘ вычисляемым.
Введем интервал (вычисляемое отношение) R = { tΘ | P |= gs(tΘ) } для определения таких решений, которые порождаются tΘ.
Тогда tΘ – вычисляемое решение задачи G, если tΘ Î R.
Замечания.
1. Если кортеж tΘ не содержит переменных, то tΘ Î R.
2. Если интервал Rs пуст, то программа не должна иметь решения, то программа неразрешима.
Определение 9. Если программа (P, G) полностью правильная, то:
1. Вычисляемое программой решение правильно относительно S. (частичная правильность)
2. Каждое решение, приписываемое спецификацией S предложению G должно быть вычисляемым программой (P, G). (полнота)
Определение 10. Программа частично правильна <==> выполняется 1 из условий:
1. ("Θ) ( (tΘ Î R) => (tΘ Î Rs)).
2. R Í Rs.
3. ("Θ) ( (P |= gs(tΘ)) => (S |= gs(tΘ)) ).
Т.е. совсем не требуется, чтобы tΘ вычислялось, а требуется, чтобы вычисляемое решение было специфицируемым.
Замечания.
1. Неразрешимые программы являются частично правильными.
2. Программа, не вычисляющая никакого решения, не может вычислить и правильного решения.
Определение 11. Программа (P, G) полна для G относительно S <==> выполняется 1 из условий:
1. ("Θ) ( (tΘ Î Rs) => (tΘ Î R)).
2. Rs Í R.
3. ("Θ) ( (S |= gs(tΘ)) => (P |= gs(tΘ)) ).
Т.е. процедур из P достаточно, чтобы вычислить все решения из Rs.
Некоторые множества Р являются полными вне зависимости от G. Их называют полными относительно S.
Определение 12. P полно относительно S <=> ("T) ( (S |= gs(T)) => (P |= gs(T)) ) где Т не обязательно имеет вид tΘ.
Определение 13. Программа (P, G) является полностью правильной относительно S <==> выполняется 1 из условий:
1. ("Θ) ( (tΘ Î Rs) <=> (tΘ Î R)).
2. Rs = R.
3. ("Θ) ( (S |= gs(tΘ)) <=> (P |= gs(tΘ)) ).
Т.е. вычисляемое и специфицируемое решения совпадают.
Замечание. Если (P, G) не является полностью правильной, то:
1. Либо она вычисляет некоторое неправильное решение, т.к. Р неправильно описывает проблемную область.
2. Либо не может вычислить некоторое правильное решение, т.к. не хватает информации о проблемной области.
Задача. Написать БД, позволяющую осуществить поиск ответов на вопросы:
1. Является ли человек Х студентом?
2. Человек Х успевает?
3. Получает ли человек Х стипендию?
Решение.
1. Возможные спецификации:
S1: студент(Х) <=> (X Î студ).
S2: успевающий(Х) <=> (X Î усп).
S3: получает-стипендию(Х) <=> (X Î студ, X Î усп).
S4: ?студент(x) <=> (x Î студ) => T1=true.
S5: ?успевающий(x) <=> (x Î усп) => T2=true.
S6: ?получает-стипендию(x) <=> (T1=true, T2=true) => T3=true.
S7: студ = { иванов, петров, сидоров }.
S8: усп = { иванов, петров, сидоров }.
Rs = { X=иванов, X=петров, X=сидоров }.
2. Программа (P, G):
P1: студент(иванов).
P2: студент(петров).
P3: студент(сидоров).
P4: успевающий(петров).
P5: успевающий(сидоров).
P6: получает-стипендию(Х) :- студент(Х), успевающий(Х).
R = { X=петров, X=сидоров }.
Вывод программа частично правильна.
Чтобы сделать ее полностью правильной, необходимо добавить предложение
P7: успевающий(иванов).
Замечание. Сформулированные критерии называются минимальными (правильность зависит от G).
Пример. Программа становится неправильной лишь при замене G (P сохраняется).
Р1: сумма(Т, 0, Т).
Р2: сумма(Y, 2, 3).
Р3: сумма(Т, 1, Z) :- сумма(Т, 0, Y), сумма(Y,2, Z).
G: ? сумма(2, 1, Х).
1. Cпецификации:
S1: сумма(T1, T2, T3) <=> T3=T1+T2.
S2: ? сумма(2, 1, X) <=> (X=2+1, X=3).
Rs = { X=3 }.
2. Вычислим решение, составляющее R с помощью стандартной стратегии управления:
S0: Ø сумма(2, 1, Х).
Р1: сумма(Т, 0, Т).
-----------------------------------------
Θ = Æ.
S0: Ø сумма(2, 1, Х).
Р2: сумма(Y, 2, 3).
-----------------------------------------
Θ = Æ.
S0: Ø сумма(2, 1, Х).
Р3: сумма(Т, 1, Z).
-----------------------------------------
Θ = { T:=2, Z:=X }.
S1: Ø сумма(2, 0, Y).
Р1: сумма(2, 0, 2).
-----------------------------------------
Θ = { T:=2, Z:=X, Y:=2 }.
S2: Ø сумма(2, 2, X).
Р2: сумма(2, 2, 3).
-----------------------------------------
S3: ð.
R = { X=3 }.
Изменим целевое утверждение. Обратимся к программе с вопросом:
G: ? сумма(1, 1, Х).
S2': сумма(1, 1, X) <=> (X=1+1, X=2).
Программа вычисляет решение R’s = { X=2 }
Очевидно, что Rs <> R’s.
Поэтому программа не является правильной для данного G.
Объяснение. Использованные критерии правильности являются необходимыми условиями.
Они не накладывают ограничений на отдельные процедуры. Процедура Р2 бессмысленна (она не верна "Y<>1). По этой причине на практике пользуются достаточными условиями правильности программ.
Теорема 1. Если S |= P, то (P, G) частично правильная относительно S.
□:
tΘ – произвольно вычисляемое решение для целей. Поэтому
S |= P } P |= gs(tΘ) => S |= gs(tΘ) (в силу транзитивности).
tΘ
Таким образом, выполняется ("Θ) ( (P |= gs(tΘ)) => (S |= gs(tΘ)) ).
Следовательно, по определению, (P, G) частично правильная.
■.
Теорема 2. Если Р полно относительно S, то Р полно для цели G относительно S.
□:
В силу того, что Р полно относительно S:
("t) ( (S |= gs(t)) => (P |= gs(t)) )
в силу произвольности t следует, что какую бы подстановку мы не взяли, можно работать с решением:
($Θ) ( (S |= gs(tΘ)) => (P |= gs(tΘ)) ).
Следовательно, Р полно для G относительно S по определению.
■.
Теорема 3. Если S |= P и Р полно относительно S то (P, G) полностью правильная относительно S.
□:
Т.к. S |= P то (P, G) частично правильная относительно S. (теорема 1)
Т.к. Р полно относительно S то (Р, G) полна для цели G относительно S. (теорема 2)■.
Замечания.
1. Условие S |= P не зависит от G. Смысл условия: Р полностью описывает S. На практике неполнота Р может быть оправдана необходимостью вычислений неполного пространства решений программы (Р, G) или негибкостью языка представления процедур Р.
2. Если (Р, G) полна относительно S, то из ($Θ) (S |= gs(tΘ)) следует, что (Р, G) разрешима. Обратное неверно.
3. Если (Р, G) частично правильна, ("Θ) (S |= Øgs(tΘ)), то (Р, G) – неразрешима. Обратное неверно.