На этом шаге мы рассмотрим сопоставление и унификацию.
Рассмотрим программу с точки зрения того, как Пролог будет отыскивать все решения следующей цели:
written_by(X,Y).
Пытаясь выполнить целевое утверждение written_by(X,Y), Пролог должен проверить каждое предложение written_by в программе. Сопоставляя аргументы X и Y с аргументами каждого предложения written_by, Пролог выполняет поиск от начала программы до ее конца. Обнаружим предложение, соответствующее целевому утверждению, Пролог присваивает значения свободным переменным таким образом, что целевое утверждение и предложение становятся идентичными; говорят, что целевое утверждение унифицируется с предложением. Такая операция сопоставления называется унификацией. Рассмотрим пример pro28_1.pro:
domains
title,author=symbol
pages=integer
predicates
book(title,pages)
written_by(author, title)
long_novel(title)
clauses
written_by(fleming, "DR NO").
written_by(melville, "MOBY DICK"),.
book("MOBY DICK", 250).
book("DR NO", 310).
long_novel(Title) :-
written_by(_,Title),
book(Title,Length),
Length >300.
Поскольку X и Y являются свободными переменными в целевом утверждении, а свободная переменная может быть унифицирована с любым другим аргументом (и даже с другой свободной переменной), то целевое утверждение может быть унифицировано первым предложением written_by в программе, как показано ниже:
written_by(X,Y). written_by(fleming,"DR NO").
Пролог устанавливает соответствие, X становится связанным с fleming, a Y - с DR NO. В этот момент Пролог напечатает:
X=fleming, Y="DR NO"
Поскольку Пролог ищет все решения для заданной цели, целевое утверждение также будет унифицировано и со вторым предложением written_by:
written_by(melville,"MOBY DICK").
Пролог печатает второе решение:
X=melville, Y="MOBY DICK"
Теперь предположим, что вы задали программе целевое утверждение
written_by(X,"MOBY DICK").
Пролог произведет сопоставление с первым предложением written_by:
written_by(X,"MOBY DICK"). written_by(fleming,"DR NO").
Так как "MOBY DICK" И "DR NO" не соответствуют друг другу, попытка унификации завершается неудачно. Затем Пролог проверит следующий факт в программе:
written_by(melville,"MOBY DICK").
Этот факт действительно унифицируется, и X становится связанным с melville. Рассмотрим, как Пролог выполнит следующее целевое утверждение:
long_novel(X).
Когда Пролог пытается выполнить целевое утверждение, он проверяет, действительно ли обращение может соответствовать факту или заголовку правила. В нашем случае устанавливается соответствие с long_novel(Title).
Пролог проверяет предложение для long_novel, пытаясь завершить сопоставление унификацией аргументов. Поскольку в целевом утверждении X - свободная переменная, то она может быть унифицирована с любым другим аргументом. Title также не является связанным в заголовке предложения long_novel. Целевое утверждение соответствует заголовку правила, и унификация выполняется. Впоследствии Пролог будет пытаться согласовывать подцели с правилом.
long_novel(Title):-
written_by(_, Title),
book(Title, Length),
Length>300.
Пытаясь выполнить согласование тела правила, Пролог обратится к первой подцели в теле правила - written_by(_,Title). Поскольку авторство книги является несущественным, на месте аргумента author появляется анонимная переменная (_). Обращение written_by(_,Title) становится текущей подцелью, и Пролог ищет решение для этого обращения. Пролог ищет соответствие с данной подцелью от вершины и до конца программы.
В результате достигается унификация с первым фактом для written_by, а именно:
written_by(_,Title), written_by(fleming,"DR NO").
Переменная Title связывается с "DR NO", и к следующей подцели book(Title, Length) обращение выполняется уже с этим значением переменной.
Далее Пролог начинает очередной процесс поиски, пытаясь найти соответствие с обращением к book. Так как Title связан с "DR NO", фактическое обращение выглядит как book("DR NO",Length). Процесс поиска опять начинается с вершины программы. Заметим, что первая попытка сопоставления с предложением book("MOBY DICK",250) завершится неудачно, и Пролог перейдет ко второму предложению book в поиске соответствия. Здесь заголовок книги соответствует подцели, и Пролог связывает переменную Length с величиной 310. Теперь третье предложение в теле long_novel становится текущей подцелью:
Length > 300.
Пролог выполняет сравнение, завершающееся успешно: 310 больше, чем 300. В этот момент все подцели в теле правила выполнены, и, следовательно, обращение long_novel (X) успешно. Так как X в обращении был унифицирован с переменной Title в правиле, то значение, с которым связывается Title при подтверждении правила, возвращается и унифицируется с переменной X. Переменная Title в случае подтверждения правила имеет значение "DR NO", поэтому Пролог выведет:
X="DR NO"
B следующих шагах будет показано несколько прикладных примеров унификации. Однако прежде ознакомимся с рядом основополагающих понятий.
На следующем шаге мы рассмотрим поиск с возвратом.
