Управление выбором значения переменной Prolog

Question

Вдохновленный an earlier question Я попытался реализовать что-то, что бы перечислить возможности для булевого выражения. Однако у меня возникают проблемы с выбором переменных. Вот мой ожидаемый результат:

?- eval(X^Y, R). 
R = 0^0; 
R = 0^1; 
R = 1^0; 
R = 1^1; 
no. 

Вот мой код:

:- op(200, yfx, ^). 

split(V, R) :- var(V), R = 0. 
split(V, R) :- var(V), R = 1. 
split(X^Y, XP^YP) :- split(X, XP), split(Y, YP). 

Это уже не делать то, что я хочу, даже для этого простого случая:

?- split(Y, R). 
R = 0 ; 
R = 1 ; 
Y = _G269^_G270, 
R = 0^0 ; 
Y = _G269^_G270, 
R = 0^1 ; 
Y = _G269^ (_G275^_G276), 
R = 0^ (0^0) ; 
Y = _G269^ (_G275^_G276), 
R = 0^ (0^1) ; 
Y = _G269^ (_G275^ (_G281^_G282)), 
R = 0^ (0^ (0^0)) . 

Итак, я могу видеть проблема в том, что на пути через split(Y, YP) Пролог исчерпал первые два предложения, так что он снова заканчивается в split(X^Y, ...), объединяя мой Y с X'^Y', по существу. Я просто не уверен, что мне нужно сделать, чтобы закрыть этот путь, за исключением того, что у меня есть структура ^/2.

Мне также хотелось бы, чтобы это работало с вложенными структурами, поэтому я не могу просто исключить рекурсивную обработку ветвей.

Редактировать: без операторов

Если op/3 беспокоит Вас, рассмотреть эту формулировку:

eval(and(X,Y), R). 
R = and(0,0); 
R = and(0,1); 
R = and(1,0); 
R = and(1,1); 
no. 

Это будет код в этом случае:

split(V, R) :- var(V), R = 0. 
split(V, R) :- var(V), R = 1. 
split(and(X,Y), and(XP,YP)) :- split(X, XP), split(Y, YP). 

Медведь в я бы все еще хотел, чтобы он работал с рекурсивными формулировками, такими как and(and(X,Y),and(Y,Z)) и т. д.

Answer 1

Главная проблема: Defaulty представление

Основная проблема в данном случае является представление defaulty используется для представления логических выражений.

Под «defaulty» Я имею в виду, что вы не можете четко различать случаи по шаблону   сопоставления: В вашем случае, переменная V может обозначать либо

• один из пропозициональных констант 0 и   1, или
• составное выражение формы A^B.

Из-за этот недостаток, вы не можете чисто выразить ограничение в форме «переменной X стоит только для одного из двух пропозициональных констант» в вашей программе.

---

Выход: Чистое представление

Декларативного выхода заключается в использовании чистого представлениявместо.

Например, предположим, что мы произвольно использовать v/1 различать переменные, которые только обозначают пропозициональные константы, то мы имеем:

• v(X) для обозначения пропозициональной переменной X
• A^B обозначать выражение в соединение ,

Очевидно, что так как основные функторы и арностей различны (v/1 против (^)/2), мы можем различать случаи по шаблону соответствие в одиночку.

С помощью этого нового представления, ваш фрагмент кода становится:

 
split(v(V), V) :- V = 0. 
split(v(V), V) :- V = 1. 
split(X^Y, XP^YP) :- 
     split(X, XP), 
     split(Y, YP). 

Пример запроса:

 
?- split(v(X)^v(Y), R). 
X = Y, Y = 0, 
R = 0^0 ; 
X = 0, 
Y = 1, 
R = 0^1 ; 
X = 1, 
Y = 0, 
R = 1^0 ; 
X = Y, Y = 1, 
R = 1^1. 

Обратите внимание, что это еще работает в всех направлениях, а также в наиболее общий случай:

 
?- split(Expr, R). 
Expr = v(0), 
R = 0 ; 
Expr = v(1), 
R = 1 ; 
Expr = v(0)^v(0), 
R = 0^0 ; 
Expr = v(0)^v(1), 
R = 0^1 ; 
etc. 

Как правило, как только вы должны использовать в своем коде экстра-логический предикат, такой как var/1, мало надежды сохранить его логическую чистоту и монотонность. Цель чистых представлений для сохранения этих свойств.

Иногда, например, невозможно использовать представления по умолчанию, потому что вы хотите облегчить ввод для пользователей  . В таких случаях старайтесь быстро преобразовать их в чистые, прежде чем начинать фактические рассуждения.

Answer 2

В какой-то момент я написал очень маленькую программу, которая кажется более или менее то, что вы ищете. Надеюсь, я не совсем неправильно понимаю ваш вопрос. Вы можете проверить this SWISH program на всю программу. Есть несколько отличий, например, использование f и t вместо 0 и 1 или использование and и or вместо ^ и v. Однако основная идея такая же, как ваша (я думаю).

Если я удалить некоторые из ненужных вещей, для демонстрации, то это будет программа:

:- op(100, fy, ?). 
:- op(500, yfx, and). 
:- op(500, yfx, or). 

table(F, T) :- 
     term_variables(F, Vs), 
     bagof(R-Vs, bl(F, R), T). 

bl(?X, R) :- 
     v(X, R). 
bl(X and Y, R) :- 
     bl(X, R0), 
     and_bl(R0, Y, R). 
bl(X or Y, R) :- 
     bl(X, R0), 
     or_bl(R0, Y, R). 

v(f, f). 
v(t, t). 

and_bl(f, _, f). 
and_bl(t, Y, R) :- bl(Y, R). 

or_bl(f, Y, R) :- bl(Y, R). 
or_bl(t, _, t). 

Главное здесь в том, что у меня есть чистое отношение, мой v/2, который просто утверждает, что значение от true - true, а значение false - false. Затем я использую взаимно-рекурсивное определение для фактической оценки булевых выражений, которое в конечном итоге заканчивается на v/2.

Я решил «пометить» логические переменные самостоятельно, поэтому вместо X вам нужно будет написать ?X. Если я правильно помню, в то время, когда я понял, мне нужен способ явно сказать, есть ли в выражении логическая переменная, или все выражение остается «неизвестным». Другими словами, это: ?X либо t или f и это: Expr может быть ?X или not ?X или ?X and ?Y или ?X or ?Y или not (?X and ?Y), и так далее.

Маркировка переменной с ?X - это то, что позволяет избежать «представления по умолчанию» - what @mat explained. Важно отметить, что без явной маркировки я не вижу способа рассказать обособленные логические переменные из булевых выражений.

Вот как вы можете использовать его:

?- bl(?t and ?X, R). 
X = R, R = f ; 
X = R, R = t. 

?- bl(?t or ?X, R). 
R = t. 

?- bl(?A or (?B and ?C), R). 
A = B, B = R, R = f ; 
A = C, C = R, R = f, 
B = t ; 
A = f, 
B = C, C = R, R = t ; 
A = R, R = t. 

?- table(?A or (?B and ?A), R). 
R = [f-[f, f], f-[f, t], t-[t, _7734]]. 

Answer 3

Есть уже два хороших ответов, один чистый и короче один с помощью term_variables/2. Я все еще хотел бы адресовать деталь:

Итак, я вижу, что проблема здесь, которая является то, что на пути через split(Y, YP) Пролог исчерпал первые два пункта, так что ветра в split(X^Y, ...) снова, объединяя мой Y с X'^Y', по существу. Я просто не уверен, что мне нужно сделать, чтобы закрыть этот путь, за исключением того, что у меня есть структура ^/2.

Если вы не хотите выполнять объединение головы с X^Y, если первый аргумент является переменной, вытащите унификацию из головы. Ничто не заставляет вас поставить здесь термин X^Y! То, что вы хотите сделать, - это рассмотреть только последнее предложение, если предыдущие два предложения не применялись. Предыдущие два положения охраняли var/1, так что вы можете защитить последнюю с nonvar/1:

split(V, R) :- var(V), R = 0. 
split(V, R) :- var(V), R = 1. 
split(Term, SplitTerm) :- 
    nonvar(Term), 
    Term = X^Y, 
    split(X, XP), 
    split(Y, YP), 
    SplitTerm = XP^YP. 

С этим ваши примеры работы по назначению:

?- split(Y, R). 
R = 0 ; 
R = 1 ; 
false. 

?- split(X^Y, R). 
R = 0^0 ; 
R = 0^1 ; 
R = 1^0 ; 
R = 1^1 ; 
false. 

Edit: Как циновка указано в комментарии, используя тесты, такие как var/1, могут помочь вам в любых неприятностях.

Одна из проблем заключается в том, что вы должны тщательно проверить различные уровни инстанцирования: пример запроса мата split(1, R) не соответствует указанному выше коду (он должен преуспеть с R = 1). Это связано с тем, что 1 попадает в корпус nonvar, но не объединяется с _^_. Если мы идем таким образом, мы должны различать не только случаи, но и var, ground и nonvar -but-not-ground. Это становится немного грязным.

Другая проблема заключается в запросе split(V, R), V = 1, который декларативно эквивалентен запросу выше, но успешно выполняется дважды, в том числе с решением R = V. Это связано с тем, что это определение split/2 (намеренно) избегало введения совместного использования его аргументов. Хотим ли мы, чтобы этот обмен или нет, зависит от спецификации.

Я не буду пытаться дать полностью надежное решение с помощью тестов на экземпляр, поскольку мой вопрос не в том, что это лучший способ пойти.