У Клоксин - ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ

И наконец, небольшое замечание о возможных различиях между процедурой сопоставления, используемой в Прологе, и процедурой унификации, используемой в методе резолюций. Большинство Пролог-систем допускают обращение с вопросами, подобными следующему:

равны(X,X).

?- равны(foo(Y),Y).

Это возможно по той причине, что в Прологе разрешается сопоставлять некоторый терм с его собственным подтермом. В этом примере foo(Y)сопоставляется с Y, который сам является частью этого терма. В результате этого Yстановится равным foo(Y)что в свою очередь равно foo(foo(Y))(учитывая значение Y), что равно foo(foo(foo(Y)))и так далее. Так что в результате Yобозначает некоторую бесконечную структуру. Заметим, что хотя Пролог-системы могут допускать использование подобных конструкций, большинство из них будут не в состоянии напечатать окончательный результат сопоставления. В соответствии с формальным определением унификации, подобного вида «бесконечные термы» никогда не должны появляться. Так что, Пролог выполняет эту процедуру неправильно в сравнении с тем, как это делается при доказательстве теорем методом резолюций. Для того чтобы сделать процедуру корректной, необходимо добавить проверку условия, заключающегося в том, что переменная не может быть конкретизирована некоторым значением, содержащим эту переменную. Такая проверка, проверка на вхождение, не представляла бы труда для ее реализации, но значительно замедляла бы выполнение программы на Прологе. Так как число программ, в которых может встретиться такая конструкция, невелико, то в большинстве реализаций такая проверка просто не делается.

В нескольких последних разделах было показано, как используются в Прологе идеи доказательства теорем. Можно видеть, что наши программы довольно похожи на гипотезы о проблемной области, а вопросы очень похожи на теоремы, которые нам хотелось бы доказать. Таким образом, программирование на Прологе имеет мало общего с процессом выдачи машине указаний о том, что и когда следует делать. Оно скорее состоит в передаче машине информации, которая предполагается истинной, и обращении к ней с вопросами о возможных следствиях из этой информации. Идея о том, что программирование должно выглядеть именно так, привлекательна и она привела многих специалистов к исследованию концепции логического программирования, то есть программирования на языке логики, как практической альтернативы обычному. Такой подход резко отличается от использования традиционных языков программирования подобных Фортрану или Лиспу, при программировании на которых необходимо как можно более подробно описать что и когда должна делать вычислительная машина. Преимущества логического программирования должны проявиться в том, что программы станут более понятными. Они не будут содержать затрудняющие понимание детали относительно того как решать задачу, а скорее будут напоминать описание того, что собой представляет результат решения. Кроме этого, если программа выглядит как описание (спецификация) того, что предполагается получить, то и относительно проще проверить (вручную или, возможно, используя какие-то автоматические средства), делает ли она в действительности то, что требуется. Подводя итог, можно сказать: преимущества языка логического программирования были бы следствием того, что программы обладают как декларативной семантикой, так и процедурной. Мы бы знали что программа вычисляет, а не как она это делает. Мы не будем здесь рассматривать логическое программирование вообще. Интересующемуся этим вопросом читателю рекомендуем обратиться к книге Ко-walski R. Logic for Problem Solving, North Holland, 1979.

Давайте рассмотрим Пролог как кандидата на место языка логического программирования и посмотрим, насколько хорошо он для этого подходит. Прежде всего, ясно, что некоторые программы на Прологе действительно представляют описание проблемной области на языке логики. Запись:

мать(Х,Y):- родитель(Х,Y), женщина(Y).

можно рассматривать как описание того, что значит быть матерью (это значит быть женщиной и быть одним из родителей). Это утверждение выражает высказывание, которое, как мы предполагаем, должно быть истинным, и, кроме того, указывает, как показать, что кто-то является матерью. Аналогично, утверждения;

присоединить([], X, X).

присоединить([А|В],С[А|D]):- присоединить (B,C,D).

говорят о том, что собой представляет добавление одного списка в начало другого списка. Если пустой список помещается в начало некоторого списка X, то результатом будет X. С другой стороны, если непустой список присоединяется в начало некоторого списка, то головой списка-результата будет голова присоединяемого списка. Кроме того, хвостом списка-результата будет список, получаемый в результате присоединения хвоста первого списка ко второму списку. Можно считать, что эти утверждения описывают отношение присоединить, так же как и (возможно) то, как в действительности присоединить один список к другому.

Это все верно лишь для некоторых программ на Прологе. А какое возможное логическое значение можно приписать утверждениям подобным следующим?

memberl(X, List):- var(List),!,fail.

memberl(X,[X|_]).

memberl(X,[_|List]):- memberl(X,List).

print(0):-!.

print(N):- write(N), N1 is N-1, print(N1).

noun(N):- name(N,Name1), append(Name2, [ll5],Namel), name(RootN,Name2), noun(RootN).

implies(Assum,Concl):-asserta(Assum), call(Concl), retract(Concl).

Эта проблема имеет место для всех «встроенных» предикатов, используемых в программах на Прологе. Предикат подобный Var(List)ничего не говорит о принадлежности элемента списку, а проверяет состояние переменной (является ли указанная переменная неконкретизированной), возникающее в процессе доказательства. Аналогично, «отсечение» говорит кое-что о доказательстве высказывания (выбор каких альтернатив можно игнорировать), а не о самом этом высказывании. Два указанных «предиката» можно рассматривать как способ выражения управляющей информации о том, как должно выполняться доказательство. Точно так же, предикаты подобные write(N)не имеют каких-либо интересных логических свойств, но заранее предполагают, что в ходе доказательства будет достигнуто определенное состояние ( Nконкретизируется) и начинают обмен информацией с программистом, сидящим за терминалом. Целевое утверждение name(N, Name1)говорит кое-что о внутренней структуре объекта, который в исчислении предикатов был бы неделимым символом. В Прологе можно преобразовывать символы в строки литер, структуры в списки и в утверждения. Эти операции нарушают замкнутость высказываний исчисления предикатов. В последнем примере, использование предиката assertaозначает, что правило, о котором идет речь, добавляет что-то к множеству аксиом. В логике каждое правило или факт сохраняет истинность независимо от того, существуют ли какие либо другие факты или правила. В данном случае мы имеем дело с правилом, которое грубо нарушает этот принцип. Кроме того, если мы используем это правило, то окажемся в ситуации, когда на разных этапах доказательства имеется различное множество аксиом. Наконец, то что в одном из правил предполагается использовать терм Conclв качестве целевого утверждения, означает, что допускается, чтобы переменная обозначала высказывание, встречающееся в некоторой аксиоме. Такая конструкция не относится к числу тех, которые могут быть выражены на языке исчисления предикатов, но напоминает возможности, которые могут быть представлены логикой более высокого порядка.