Синтез невыполнимой программы

Однако в предыдущем примере есть «подводный камень».

Возьмем ту же самую аксиоматику для синтеза программы (5.1), но резольвирование проведем по-другому.

Аксиомы:

• 1) -Jx) v Q (x, 1);
• 2) Р (х) v Q (x, -1).

Цель:

3) -i<2(x, у) v ANS (y).

Вывод:

• 4) Q (x, 1) v Q (x, -1) 1,2;
• 5) Q (x, -1) vANS (l) 3,4;
• 6) ANS (l) v ANS (-l) 3,5.

Сначала резольвируем дизъюнкты 1 и 2 по предикату Р, получаем Q (x, 1) v Q (x, -1). Потом убираем Q, резольвируя его с дизъюнктами 3 и 4. Получаем тот же ответ ANS (i) vANS (-l). Теорема доказана. Дерево, соответствующее новому доказательству, представлено на рис. 5.6.

Рис. 5.6. Другое дерево доказательства.

Эго дерево имеет немного другую структуру. Однако если к нему применить только что приведенный алгоритм извлечения программы из доказательства, то получится следующая программа (рис. 5.7).

Рис. 5.7. Невыполнимая блок-схема.

Если не верно, что ответом должен быть -1, то ответ 1. Если ответом должен быть -1, то ответ -1. Это не совсем такая программа, которую хотелось бы видеть в ответе. Таким образом, приведен конкретный пример нереализуемости, говорящий о том, что надо быть очень осторожными относительно того, может или не может нечто появиться в программе. Не все, что легко написать в программе, на самом деле реализуемо, т. е. вычислимо. В данном случае предикат Q нс реализуем, программа бессмысленна, алгоритм не сработал. Попробуем «починить» его с помощью теории примитивной резолюции.