Логическое и надежное расширение NU-Prolog и Гёделя «if-then-else»
В статье о ртути говорится следующее:
Конструкции if-then-else и отрицания в большинстве вариантов Пролога нелогичны и несостоятельны: они могут заставить систему вычислять ответы, несовместимые с программой, рассматриваемой как логическая теория. Некоторые существующие системы логического программирования, такие как NU-Prolog и Gödel, обеспечивают логическую и надежную замену этих конструкций Prolog. К сожалению, эти системы обеспечивают безопасность с помощью проверок заземления во время выполнения. Этот эффект может увеличить время выполнения программы в сколь угодно большой раз; если цели, проверяемые на обоснованность, включают большие члены, проверки могут быть непомерно дорогими.
NU-Prolog и Gödel выглядят довольно мертвыми и несвободными, но мне все равно интересно:
- Что это за логичные и разумные
if-then-elseзамены? - Есть ли у них аналоги в SWI или GNU Prologs?
- Как они работают? Как они могли работать? Добавление логического отрицания к Прологу превращает его в общий FOL, верно? Вам в основном понадобится общий доказатель теорем FOL для работы с ним?
- Отличаются ли они от if_/3 ? if_/3 необходимо расширить для использования с новыми условиями. Нужно ли делать это также в NU-Prolog и Gödel?
@TA_intern Если подумать, if_(=(...), ...) использует dif/2, что также требует проверки на заземление, не так ли? Похоже, NU-Prolog и Гёдель каким-то образом обобщили один и тот же механизм....
@MaxB: ни в одной реализации dif/2 нет проверок на заземление. Подумайте о dif ([], [_|_]) или dif (A,A), которые оба не измельчены, но уже имеют успех соответственно. неудача. И это независимо от того, используются ограничения или нет. См. этот скетч для минимальной полной реализации. Или, может быть, сначала посмотрите на iso_dif/2.
См. Indexing dif/2, в котором упоминается MU-Prolog if-then-else, а также конструктивное отрицание. (Что было бы следующим шагом после отказа от приземленности).
Мне любопытно, почему @false не дал их. См. биос для следующего, который включает такие желаемые предикаты. неверно и повторяю
@GuyCoder: «не дал это». Что вы имеете в виду под этим?
@false MaxB задает вопросы о предикатах, которые я считаю чистыми версиями предикатов, например. if_/3. Затем вы отметили dif/2, и поэтому я указывал, где есть больше таких предикатов, которые я считаю чистыми версиями предикатов, и список этих предикатов можно найти в вашей биографии. Причина, по которой мне было любопытно, почему вы не дали их, заключается в том, что то, как я вижу вопрос, и то, как вы его видите, должно быть разным, и, следовательно, есть чему поучиться.
Интересный NU-Prolog Статья, похороненная в выпуске «Ежеквартального бюллетеня компьютерного общества технического комитета IEEE по инженерии данных» за 1987-1912 гг. считается «дедуктивной системой баз данных», а не «логическим языком программирования» (но кажется, у него есть функциональные символы).
Добавление логического not в Пролог превращает его в общий FOL, верно? Это «не» по-прежнему является обычным «отрицанием как отказ» — оно просто отказывается вычислять бессмыслицу, гарантируя, что оно вызывается только для переменных, которые являются шлифованными, если они видны за пределами \+ (что превосходно). Это все еще не «сильное отрицание», так что никакого FOL. (Примечание: в настоящее время читаю "Яркую логику" Герда Вагнера... Классическая логика и, следовательно, ЛЖ, основанная на классической логике, непригодна практически для всего, кроме математики... и даже для самой математики. Так зачем на нее ориентироваться?)
@DavidTonhofer Они говорят «логическое отрицание», поэтому я не думаю, что они имеют в виду «отрицание-как-неудача».
@MaxB Я почти уверен, что они не поддерживают сильное отрицание. Для этого вам нужно Программирование наборов ответов или аналогичные очень разные системы, не основанные на разрешении SLD. Они хотят сделать так, чтобы отрицание звучало как неудача...
@GuyCoder Нагромождение «почти чистых» предикатов не является хорошим признаком того, что на этот вопрос можно ответить положительно: если достаточно лишь нескольких примитивов, зачем нам создавать столько других вручную, используя нечистые конструкции ?
Вы читали руководство Nu-Prolog?
Ответы 2
Прорывом в if-then-else может стать новая аннотация. Под аннотацией я понимаю такие вещи, как объявления режимов, декларации детерминированности и т. д. Для if then else полная декларация была бы хороша. Предположим, мы могли бы объявить предикат или встроенный p/n завершенным. Это бы означают, что он имеет свойство для основных аргументов t1,..,tn:
T |- p(t1,..,tn)
- or -
T |- ~p(t1,..,tn)
Или, короче, это был бы разрешимый предикат, если бы теория T была рекурсивно перечислима. Если мы затем вспомним, что если-то-иначе логически:
ITE(A,B,C) == (A => B) & (~A => C)
Затем мы могли бы использовать полную аннотацию следующим образом. Давайте предположим A = p(t1,..,tn). Из-за аннотации Пролог система попытается доказать А. Если это не удастся, потому что полной аннотации система Пролога может сделать вывод, что ~A преуспеет. И поэтому он может использовать ветвь else без попытки доказательства ~A.
Но интересно это уже то, что ядро ISO стандартный если-то-иначе, (A->B;C) также только доказывает Один раз. Так в чем проблема? Я думаю, проблема в том, что A может быть более сложным и не обязательно заземленным. Или даже то, что предикат p/n может быть неполным, или мы даже не знаем, завершена ли она. И во всех в этих случаях базовый стандарт ISO, тем не менее, позволяет нам использовать (A->B;C).
Проблема заземления иногда может быть решена с помощью среды выполнения. проверки заземления. Вероятно, это то, о чем говорит Меркурий:
when(ground(A), (A->B;C))
SWI-Prolog даже применяет трюк, чтобы сделать приземленность проверить дешевле, см. также дальнейшее обсуждение на Discourse:
%! trigger_ground(@Term, :Goal)
%
% Trigger Goal when Term becomes ground. The current implementation
% uses nonground/2, waiting for an atribtrary variable and re-check
% Term when this variable is bound. Previous version used
% term_variables and suspended on a term constructed from these
% variables. It is clear that either approach performs better on
% certain types of terms. The term_variables/2 based approach wins on
% large terms that are almost ground. Possibly we need a nonground
% that also returns the number of tests performed and switch to the
% term_variables/2 based approach if this becomes large.
trigger_ground(X, Goal) :-
( nonground(X, V)
-> '$suspend'(V, when, trigger_ground(X, Goal))
; call(Goal)
).
Я нашел этот обзор MU- и NU-Prologs здесь, если кому интересно:
"Как они работают?" не очень хорошо видимо