Как было показано ранее, каждая программа имеет вполне определенное значение. Это значение само по себе не может быть корректным или некорректным
Однако значение программы может совпадать или не совпадать с тем, к чему стремился программист. Таким образом, обсуждение корректности требует рассмотрения подразумеваемого значения программы. Наши предыдущие рассмотрения корректности и полноты всегда соотносились с некоторым подразумеваемым значением.
Подразумеваемое значение программы Р – этонекоторое множество основных целей. С помощью подразумеваемого значения мы выделяем те цели, для вычисления которых программа и была создана. Программа 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, является множество целей, у которых первый или третий аргумент (или оба) являются полными списками.