Cтраница 2
История синтеза логических программ практически совпадает с историей их верификации, изложенной в конце предыдущей главы. Как мы уже видели, оба этих направления можно рассматривать в одних и тех же рамках, основываясь на выводе процедур, посредством которого устанавливается логическая связь программ с их спецификациями. [16]
При таком подходе логические программы с NAF преобразуются в абдуктивную структуру, в которой могут быть определены ограничения целостности более общего вида, чем просто отрицания. [17]
Различные виды семантики логических программ разрешают различные множества гипотез. Все виды семантики, которые будут рассмотрены, могут быть сформулированы в терминах следующего отношения атаки между множествами негативных литер, не содержащих переменных. [18]
Для выяснения смысла логических программ необходимо каждой программе приписать некоторое значение, вычисляемое программой. Возможны три подхода к определению семантики логических программ: декларативная семантика, процедурная ( или операционная) семантика и вычислительная семантика. [19]
В самом общем виде логическая программа представляет собой собрание сведений о предметной области решаемой задачи, записанных на языке, приближенным к естественному языку человеческого общения. Обращаясь к программе с запросами, пользователь может получать все возможные ответы, логически вытекающие из той совокупности знаний, которыми располагает логическая программа. Чем полнее и детальнее будет описание области знаний, к которой относится решаемая задача, тем точнее будут ответы на поставленные вопросы. Диалог программы с пользователем теперь становится похожим на обычную беседу учителя с послушным и аккуратным учеником: учитель наделяет ученика знаниями, а ученик, опираясь на эти знания, безошибочно решает задачи и отвечает на вопросы. Поэтому в логическом программировании для решения поставленной задачи нужно всего лишь как можно точнее и детальнее описать, что именно требуется решить. Если решение задачи существует, то в этом случае компьютер самостоятельно догадается, как достичь искомого решения. Логическое программирование открывает новые возможности использования компьютера. Теперь мы можем общаться с ним как с интеллектуальным, хотя и несколько своеобразным, собеседником, который берет на себя значительную часть работы, связанную с организацией вычислений программы. Поэтому основное внимание программиста может быть сосредоточено на самой задаче как таковой, на формировании тех знаний, которые могут оказаться полезными при ее решении. [20]
Краткий обзор видов семантики логических программ выполнен по работе [9.1], с. Семантика устойчивых моделей была впервые определена в работе [9.5] Гельфондом и Лифшицем. В работе [9.9] обосновывается необходимость введения второго отрицания для выполнения вывода здравого смысла. [21]
Они вводят понятие завершения логической программы с помощью определений производных предикатов в виде логических эквивалентностей, а не логических импликаций. После этого семантика логической программы может определяться как множество всех следствий ( положительных или отрицательных) из этого завершения. Он может быть формализован в виде SLDNF-резолюции - специального расширения SLD-резолюции. [22]
Рассматриваемое понятие частичной правильности логических программ по своей сути подобно тому, которое используется в доказательстве правильности традиционных программ. И в том и другом контексте частичная правильность сама по себе не требует, чтобы каждое решение действительно вычислялось в результате исполнения программы; требуется только то, что уж если решение вычисляется, то оно должно удовлетворять задаваемому спецификацией отношению между входом и выходом. [23]
В литературе по верификации логических программ имеется некоторая терминологическая путаница, что может вызвать недоразумение у тех, кто не знаком с происходившими в процессе развития этой теории изменениями в определениях. В подходе Кларка и Тернлунда принимается стандартное понятие частичной правильности, однако, пытаясь достичь согласованности с понятиями из области доказательства правильности традиционных программ, в качестве дополнительного требования для определения полной правильности они выбирают завершаемость. [24]
Представим себе тогда, что логическая программа составлена из трех предложений SI, S2 и S3, и она подается на вход системы резолютивного вывода, реализованной на ЭВМ. [25]
Чтобы расширить это определение для логических программ со вторым отрицанием - i общего вида, мы дополнительно преобразуем все такие литеры с отрицаниями в новые атомы. [26]
В приводимых ниже иллюстрациях синтеза логических программ мы принимаем в качестве стандартного метода синтеза вывод процедур: каждая процедура программы логически выводится из заданной полной, непротиворечивой, очевидно правильной спецификации, целиком записанной на языке логики первого порядка. Управление процессом построения вывода основывается на соображениях алгоритмической полезности предпринимаемых шагов, которая оценивается неформально. [27]
Поиски эффективной методологии для построения логических программ первоначально мотивировались проводившимися в начале 70 - х годов более общими разработками в области структурного программирования для традиционных формализмов. [28]
Программа 4 иллюстрирует типичные особенности итеративных логических программ, а именно использование в них специальных параметров для помещения информации, которая в эквивалентной рекурсивной программе была бы закодирована в стеке латентных вызовов. [29]
Процедурная интерпретация придает операционный характер логическим программам. Суть ее заключается в том, чтобы рассматривать целевые утверждения как множества вызовов процедур, каждый из которых обрабатывается посредством обращения к соответствующей процедуре. В этом отношении процедурная интерпретация очень похожа на процедурные семантики многих традиционных языков программирования. Она позволяет, в частности, смотреть на исполнение логических программ с алгоритмической точки зрения, а не только с точки зрения логического вывода. Понятие процедурной интерпретации является, возможно, наиболее важным достижением в вычислительной логике, которое позволило рассматривать логику как язык программирования. [30]