Целевое утверждение

Cтраница 3

Следует отметить пользу, которую приносит употребление первого вызова в целевом утверждении: он избавляет нас от необходимости указывать имя сумма ( А В) в различных других местах этого целевого утверждения. [31]

Интерпретатор осуществляет построение логического вывода путем последовательного применения правила резолюции к текущему целевому утверждению и к некоторой логической формуле, выбираемой из хранящейся в памяти программы. Если интерпретатору удается вывести пустую формулу, то процесс вывода заканчивается, и на выходе в качестве результата выдаются те значения переменных, которые были определены подстановками в результате последовательных унификаций. [32]

Система вывода параллельно решает две или более подцелей, находящихся в целевом утверждении. Здесь появляются довольно сложные проблемы. Так, в вышеприведенном целевом утверждении две подцели Р ( х ] и Q ( x) имеют общую переменную х, и система вывода должна гарантировать, что при параллельном разрешении этих подцелей переменная х будет связана с одним и тем же значением. В ином случае возникает противоречие, которое необходимо разрешить. [33]

Дерево вычислений для задачи об упорядоченном списке. [34]

Полное пространство вычислений можно изобразить в виде дерева вычислений, корнем которого является исходное целевое утверждение, а ветви, выходящие из корня, представляют все различные вычисления. Простоты ради на этом рисунке в термах, служащих именами списков, опущена константа NIL. Всего имеется восемь завершенных вычислений, и каждое из них успешное. Они соответствуют восьми различным путям решения указанной задачи при отсутствии ограничений на выбор вызова. Самая левая ветвь, выделенная на рисунке жирными ребрами, представляет единственное вычисление в подпространстве, определяемом стандартным правилом выбора вызова. В других вычислениях обрабатываются просто разнообразные перестановки этой последовательности вызовов, что соответствует различным правилам выбора. Например, правило, согласно которому всегда выбирается последний ( самый правый) вызов из текущего целевого утверждения, ограничивало бы исполнение программы подпространством, представляемым самой правой ветвью дерева. [35]

Согласно стандартному правилу вычислений, на каждом шаге всегда выбирается первый вызов из целевого утверждения. При этом подразумевается, что, когда вызов заменяется на тело вызванной им процедуры, текстуальный порядок вызовов из ее тела не меняется. [36]

Заметим, что если этот интервал пуст, то в соответствии со спецификацией S целевое утверждение G не должно иметь решений. В общем случае решения, разумеется, существуют; чтобы подчеркнуть соответствие решений спецификации S, каждое такое решение tS назовем специфицируемым решением G. Является ли оно также решением, вычисляемым программой, - совсем другой вопрос, и именно на этот вопрос должна дать ответ верификация программы. [37]

Более детальная характеризация корректности и полноты SLD-резолюции получается путем включения в рассмотрение как решений целевого утверждения ( подстановок, дающих ответ), вычисляемых посредством вывода пустого дизъюнкта П, так и правила вычислений, используемого для их нахождения. Правило вычислений - это любое фиксированное правило, однозначно определяющее, какие из вызовов, содержащихся в текущем целевом утверждении, отрезаются на каждом шаге SLD-резолюции. [38]

Так как на каждом шаге вычисления вызывается некоторая процедура, и в результате этого в целевое утверждение вводятся ( в общем случае) новые вызовы ( из тела процедуры), исполнение программы можно рассматривать как повторяющийся процесс входа в процедуру и выхода из процедуры. Вход в процедуру происходит в тот момент, когда телом процедуры заменяется обращавшийся к ней вызов. Выход из процедуры происходит в тот момент, когда оказываются решенными все вызовы из ее тела. Строго говоря, здесь был описан лишь успешный выход из процедуры; с понятием неудачного выхода мы встретимся несколько позже. [39]

При стандартном способе исполнения программы для активации всегда выбирается первый ( самый левый) вызов из целевого утверждения. [40]

Этот процесс можно представить с помощью ИЛИ - дерева ( дерева поиска), вершины которого составляют целевые утверждения. Потомки вершины - альтернативные целевые утверждения, выводимые из целевого утверждения данной вершины. Концевые вершины дерева соответствуют неразрешимым либо пустым целевым утверждениям, которые представляют решения. Композиция подстановок, используемых на пути от корневой вершины к пустой, примененная к переменным исходного целевого утверждения, дает требуемый результат. [41]

Затем ПРОЛОГ освобождает переменные X и Y от ранее полученных значений, совершает откат, пытаясь выполнить целевое утверждение С ( Х, Y) иным способом. [42]

В процессе исполнения входной программы из нее последовательно выбираются вызовы ( начиная с первого вызова RI из целевого утверждения G) с целью их решения. [43]

Непосредственными потомками корня дерева являются литералы ( вызовы) или подцели PI ( % 1 п) исходного целевого утверждения - Pi... Подцель Pi ( i - 1 п), к которой применяется процедура Pi - Si... Вт, получает в качестве потомков подцели Si... Унификатор U далее применяется к каждой из вершин дерева. [44]

Доказательство цели-отсечения всегда заканчивается успешно, и после этого не могут быть передоказаны цели, стоящие в целевом утверждении до отсечения, включая головную цель. [45]

Страницы: 1 2 3 4