Правильность исполнения логических программ

Пусть: С - стратегия управления, Г(гамма) - вычисление.

Тогда (P(множество процедур), G(цель), C(стратегия управления)) – это есть исполнение.

Определение 14. Г производимо из (P, G) при управлении С <=> тройка (P, G, C) порождает каждое целевое утверждение из Г за конечное число шагов.

Определение 15. Вычисляемое решение (tΘ) производимо из (P, G) при управлении С <=> (tΘ) вычислимо за конечное время: (P |=с gs(tΘ)).

Замечание. Не каждая производимое вычисление Г дает производимое решение.

Пример Грина. Исполнить программу.

P1: g(Y):- p(Y), q(Y).

P2: p(a).

P3: q(a).

P4: q(f(x)):-q(f(f(x))).

G:?g(Y).

{Левая ветка – стандартная стратегия управления, правая – нет.}

Вычисления Г1, Г2, Г3 – производимы.

Г1, Г2 порождают производимое решение Y=a.

Г3 – бесконечно.

Если бы первоначально была выбрана стратегия 3, то логически полностью правильная программа (P, G) не смогла бы породить решения.

Пример Грина показывает, почему при исследовании разрешимости программы недостаточно требовать ее исполнения.

Теоретические исследования правильности исполнения программ используют понятия частичной правильности и полноты (P, G, C) относительно S.

Г3 можно рассматривать как процесс синтеза программы, допускающий воздействие f на объект х (данные).

Т.о. Г3 порождает зацикленную программу.

Определение16. (P, G, C) частично правильно относительно S<=>

("Θ) ((P |=_c gs(tΘ)) => (S |= gs(tΘ)) производимость специфицируемость

Определение 17. (P, G, C) полно относительно S <=> ("Θ) ((S |= gs(tΘ)) => (P |=_с gs(tΘ)))

(tΘ производимо из Р с помощью С).

Определение 18. (P, G, C) полностью правильно относительно S <=> ("Θ) ((S |= gs(tΘ)) <=> (P |=_с gs(tΘ)))

Теорема 4. Достаточное условие правильности (P, G, C).

Если (P, G) частично правильна относительно S то (P, G, C) частично правильно относительно S.

□:

Т.к. (P, G) частично правильная относительно S, то по определению ("Θ) ((P |= gs(tΘ)) => (S |= gs(tΘ))).

Стратегия C основана на резолюции, система вывода корректная => производимое решение является вычисляемым, т.е. ("Θ) ((P |=_c gs(tΘ)) => (P |= gs(tΘ))).

В силу транзитивности получаем ("Θ) ((P |=_с gs(tΘ)) => (S |= gs(tΘ))).■.

Теорема 5. Если (P, G) полна относительно S, (P, G) определяет конечное пространство вычислений, стратегия С – исчерпывающая,

То (P, G, C) полно относительно S.

□:

Т.к. (P, G) полна относительно S, то по определению ("Θ) ((S |= gs(tΘ)) => (P|= gs(tΘ))).

Т.к. пространство вычислений конечно, Стратегия исследует все вычисления

=> все вычисляемые решения будут производимыми

т.е. ("Θ) ((P |= gs(tΘ)) => (P |=_с gs(tΘ))).

В силу транзитивности получаем

("Θ) ((S |= gs(tΘ)) => (P |=_с gs(tΘ))).■.

Теорема 6. Если (P, G) полностью правильна относительно S, (P, G) определяет конечное пространство вычислений, стратегия С – обеспечивает исчерпывающее управление,

То (P, G, C) полностью правильно относительно S.

Комментарий. Т.к. мало формальных представлений сформулированных условий, на практике удобнее пользоваться теоремой 7.

Теорема 7. Если S |= Р, Р полностью правильно относительно S,

(P,G) определяет конечное пространство вычислений, С – исчерпывающее управление

То (P, G, C) полностью правильно относительно S.