Корректность программы


Как было показано ранее, каждая программа имеет вполне определенное значение. Это значение само по себе не может быть корректным или некорректным

Однако значение программы может совпадать или не совпадать с тем, к чему стремился программист. Таким образом, обсуждение корректности требует рассмотрения подразумеваемого значения программы. Наши предыдущие рассмотрения корректности и полноты всегда соотносились с некоторым подразумеваемым значением.

Подразумеваемое значение программы Р – это некоторое множество основных целей. С помощью подразумеваемого значения мы выделяем те цели, для вычисления которых программа и была создана. Программа P корректнаотносительно подразумеваемого значения М, если М(Р) содержится в М. Программа Р полна относительно подразумеваемого значения М, если М содержится в М(Р). Таким образом, программа корректна и полна относительно подразумеваемого значения, если эти два значения полностью совпадают.

Другим важным вопросом, относящимся к логическим программам, является вопрос об остановке программы. Назовем областью любое; множество целей (не обязательно основных), замкнутое относительно построения примеров. То есть для любой области D, если А входит в D и А' – пример А, то А’ тоже входит в D.

Областью остановки, программы Р называется такая область D, что каждое вычисление программы Р с каждой целью из D заканчивается.

Обычно полезные программы должны иметь область остановки, охватывающую подразумеваемое значение. Однако поскольку вычислительная модель логических программ не зависит от порядка, в котором редуцируются цели в резольвенте, то большинство интересных логических программ имеют бессодержательную область остановки. Эта ситуация улучшится при рассмотрении языка Пролог. Ограничения, налагаемые на вычислительную модель Пролога, позволяют создавать нетривиальные программы с требуемыми областями остановки.

Рассмотрим программу 3.1 определяющую натуральныe числа. Программа останавливается для любой цели, принадлежащей базису Эрбрана. Однако в области {natural_number(X)} программа не останавливается. Это связано с возможностью незавершающегося вычисления, показанного на рис. 5.1.

При анализе любой логической программы полезно найти области, в которых программа останавливается. Для рекурсивных программ это обычно сделать не просто. Нам нужно ввести описание рекурсивных типов данных, пригодное для исследования проблемы остановки.

Напомним, что тип – это множество термов. Тип называется полным, если данное множество замкнуто относительню построения примеров.

 

natural_number (X) X=s(Xl)

natural_number(Xl) Xl=s(X2)

natural_number(X2) X2=s(X3)

Рис. 5.1. Незавершающееся вычисление.

 

Каждому полному типу Т мы сопоставим неполный тип IT, состоящий из термов, имеющих примеры, входящие в Т, и имеющих примеры, не входящие в Т.

Продемонстрируем применение этих понятий на примере определения областей остановки рекурсивных программ, использующих рекурсивные типы. Приведем примеры определений полного и неполного типов для натуральных чисел и списков. Константа 0 и любой терм вида s(0) являются (полным) натуральным числом. Неполным натуральным числом является или переменная X, или терм вида s(X). Программа 3.2, задающая отношение£, останавливается в области, состоящей из целей, у которых первый или второй аргумент (или оба) являются полным натуральным числом.

Список является полным, если любой пример данного списка удовлетворяет программе 3.11. Список неполный, если имеются примеры, удовлетворяющие программе 3.11, и примеры, не удовлетворяющие этой программе. Список [а, b, c], например, является полным списком (доказывается на рис. 3.3), в то время как переменная Х – неполный список. Два менее тривиальных примера: [а, X, с] – полный список, хотя и не основной, a [a. B | Xs] неполный.

1. Областью остановки программы, задающей append, является множество целей, у которых первый или третий аргумент (или оба) являются полными списками.