Программирование на языке Пролог | страница 40
и войдет в прямоугольник родители (мэри,анна,фред) снизу для того, чтобы попытаться передоказать данное целевое утверждение (см. рис. 2.5).
Рис. 2.5.
Отступая дальше, стрелка достигнет места, где было выбрано утверждение, соответствующее целевому утверждению отец. В первую очередь освобождаются все переменные, которые были конкретизированы в результате использования данного утверждения. Это означает, что переменная F вновь становится неконкретизированной. Затем Пролог просматривает базу данных, начиная с утверждения, следующего за первым утверждением с предикатом отец (здесь находится маркер), пытаясь найти альтернативное утверждение. Если предположить, что мэри имеет только одного отца, то этот процесс успехом не завершится. Поэтому стрелка продолжит отступление. Она покинет прямоугольник отец(мэри, F) (это целевое утверждение недоказуемо) и вернется в прямоугольник мать(мэри,анна) (для того, чтобы попытаться передоказать данное целевое утверждение) (см. рис. 2.6).
Рис. 2.6.
Отступление стрелки будет продолжаться до успешного доказательства соответствующего целевого утверждения.
Эти примеры иллюстрируют общую схему повторного рассмотрения целевых утверждений в процессе возврата. Когда некоторое целевое утверждение недоказуемо, стрелка возвращается из соответствующего прямоугольника в прямоугольник с предшествующим целевым утверждением. Стрелка отступает до тех пор, пока не встретится маркер. Все переменные, которые были конкретизированы в результате предыдущего выбора сопоставимого утверждения, становятся неконкретизированными. Затем Пролог возобновляет поиск в базе данных сопоставимого утверждения, начиная с маркера. Если сопоставимое утверждение будет найдено, новое место помечается маркером, создаются прямоугольники для целевых подутверждений и стрелка опять начинает движение вниз. В противном случае стрелка продолжает отступать вверх в поисках другого маркера.
2.6.3. Установление соответствия
Правила, определяющие, подходит ли некоторое утверждение для согласования с целевым утверждением, выглядят следующим образом. Отметим, что при выборе утверждения все переменные сначала неконкретизированы.
• Неконкретизированная переменная соответствует любому объекту. Этот объект становится значением переменной.
• Целое число или атом соответствуют только самим себе.
• Между структурами можно установить соответствие, только если они имеют одинаковый функтор, одинаковое число параметров и соответствующие параметры соответствуют друг другу.