Можно ли написать непоследовательную программу на Прологе, используя только чистый Пролог, вырезать и `false`?

Question

Меня заинтересовала эта теория:

Можно ли написать несовместимую программу на Прологе, то есть программу, которая отвечает как false , так и true в зависимости от как он запрашивается, используя только чистый Пролог, вырезку и false?

Например, можно запросить p(1), и процессор Prolog выдаст false. Но когда кто-то запрашивает p(X), процессор Prolog выдаст набор ответов 1, 2, 3.

Этого можно легко достичь с помощью «предикатов проверки вычислительного состояния», например var/1 (на самом деле лучше называть fresh/1) + el cut:

p(X) :- nonvar(X),!,member(X,[2,3]).
p(X) :- member(X,[1,2,3]).

Затем

?- p(1).
false.

?- p(X).
X = 1 ;
X = 2 ;
X = 3.

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

Итак. может быть выполнено без этих "предикатов проверки вычислительного состояния"? вычислительное состояние ":

p(X,StateIn,StateOut).

, которое можно использовать для объяснения поведения var/1 и друзей. Тогда программа Prolog будет "чистой", если она вызывает только предикаты, которые не обращаются и не изменяют этот State. Что ж, по крайней мере, это хороший способ посмотреть на то, что происходит. Думаю.

Answer 1

Вот очень простой:

f(X,X) :- !, false.
f(0,1).

Затем:

| ?- f(0,1).

yes
| ?- f(X,1).

no
| ?- f(0,Y).

no

Итак, Prolog утверждает, что нет решений для запросов с переменными, хотя f(0,1) истинно и будет быть решением обоих.

Answer 2

Вот одна попытка. Основная идея c состоит в том, что X - это переменная, если она может быть объединена с как a, так и b. Но, конечно, мы не можем записать это как X = a, X = b. Итак, нам нужен «унифицируемый» тест, который будет успешным без привязки переменных, таких как =/2.

Во-первых, нам нужно определить отрицание самим, поскольку оно нечисто:

my_not(Goal) :-
    call(Goal),
    !,
    false.
my_not(_Goal).

Это всего лишь приемлемо, если ваше понятие чистого Пролога включает call/1. Предположим, что это так: -)

Теперь мы можем проверить унифицируемость, используя =/2 и шаблон «not not», чтобы сохранить успех при отмене привязок:

unifiable(X, Y) :-
    my_not(my_not(X = Y)).

Теперь мы есть инструменты для определения var / nonvar проверок:

my_var(X) :-
    unifiable(X, a),
    unifiable(X, b).

my_nonvar(X) :-
    not(my_var(X)).

Давайте проверим это:

?- my_var(X).
true.

?- my_var(1).
false.

?- my_var(a).
false.

?- my_var(f(X)).
false.

?- my_nonvar(X).
false.

?- my_nonvar(1).
true.

?- my_nonvar(a).
true.

?- my_nonvar(f(X)).
true.

Остальное - ваше определение:

p(X) :-
    my_nonvar(X),
    !,
    member(X, [2, 3]).
p(X) :-
    member(X, [1, 2, 3]).

Что дает:

?- p(X).
X = 1 ;
X = 2 ;
X = 3.

?- p(1).
false.

Изменить: Использование call/1 не обязательно, и интересно написать решение без него:

not_unifiable(X, Y) :-
    X = Y,
    !,
    false.
not_unifiable(_X, _Y).

unifiable(X, Y) :-
    not_unifiable(X, Y),
    !,
    false.
unifiable(_X, _Y).

Посмотрите на эти вторые предложения каждого из этих предикатов. Они одинаковые! При декларативном прочтении этих пунктов любые два термина не могут быть унифицированы , но также любые два термина не могут быть унифицированы ! Конечно, вы не можете декларативно читать эти статьи из-за сокращения. Но я нахожу это особенно поразительным как иллюстрацию того, насколько катастрофически загрязнен разрез.