чае соответствие устанавливается сразу же:
В данном слу чае соответствие устанавливается сразу же: "wor" соответствует переменной s, a "Hello world" — переменной t. Это определяет подстановку выражений (в данном случае констант) для переменных; подстановка применяется ко всем переменным в формуле:
"wor" с "Hello world" c= ("Hello world" = tl || t2) л ("wor" с tl)
Теперь мы должны показать, что:
("Hello world" = t1|| t2) л ("wor" с tl)
является истинным, и это ведет к новому соответствию образцов, а именно попытке установить соответствие "Hello world" с tl || t2. Здесь, конечно, может быть много соответствий, что приведет к поиску. Например, машина вывода может допускать, чтобы tl указывало на "Не", a t2 указывало на "Но world"; эти подстановки затем проводятся во всем вычислении.
Знак «: — » обозначает импликацию, а переменные должны начинаться с прописных букв. Когда задана цель:
?- substring ("wor", "Hello world").
вычисление пытается унифицировать ее с головой формулы; если это удается сделать, цель заменяется последовательностью элементарных формул (также называемых целями):
?- concat ("Hello world", T1,12), substring ("wor", T1).
Цель, которая получается в результате, может состоять из боле? чем одной элементарной формулы; машина вывода должна теперь выбрать одну из них, чтобы продолжить поиск решения. По правилу вычисления языка Prolog машина вывода всегда выбирает крайнюю левую элементарную формулу. В данном примере правило вычисления требует, чтобы concat было выбрано перед рекурсивным вызовом substring.
Головы нескольких формул могут соответствовать выбранной элементарной формуле, и машина вывода должна выбрать одну из них, чтобы попытаться сделать унификацию. Правило поиска в языке Prolog определяет, что формулы выбираются в том порядке, в котором они появляются в тексте программы.
