Логическая эквивалентность в Прологе

Question

Я получил два выражения, чтобы перечислить все списки бит с помощью Пролога:

bit(0). 
bit(1). 

bitlist1([]). 
bitlist1([B|Bs]) :- 
    bit(B), 
    bitlist1(Bs). 

bitlist2([]). 
bitlist2([B|Bs]) :- 
    bitlist2(Bs), 
    bit(B). 

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

Как я использую SWI-Пролог Я получил следующие результаты:

?- bitlist1(Bs). 
Bs = [] ; 
Bs = [0] ; 
Bs = [0, 0] ; 
Bs = [0, 0, 0] ; 
Bs = [0, 0, 0, 0] ; 
Bs = [0, 0, 0, 0, 0] ; 
Bs = [0, 0, 0, 0, 0, 0] ; 
Bs = [0, 0, 0, 0, 0, 0, 0] ; 
Bs = [0, 0, 0, 0, 0, 0, 0, 0] ; 
Bs = [0, 0, 0, 0, 0, 0, 0, 0, 0] ; 
Bs = [0, 0, 0, 0, 0, 0, 0, 0, 0|...] ; 
... 

?- bitlist2(Bs). 
Bs = [] ; 
Bs = [0] ; 
Bs = [1] ; 
Bs = [0, 0] ; 
Bs = [1, 0] ; 
Bs = [0, 1] ; 
Bs = [1, 1] ; 
Bs = [0, 0, 0] ; 
Bs = [1, 0, 0] ; 
Bs = [0, 1, 0] ; 
Bs = [1, 1, 0] ; 
Bs = [0, 0, 1] ; 
Bs = [1, 0, 1] ; 
Bs = [0, 1, 1] ; 
Bs = [1, 1, 1] ; 
Bs = [0, 0, 0, 0] ; 
... 

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

bitlist2 перечисляет все комбинации 0 и 1 каждой длины, а затем продолжает список бит с длиной более высокой длины.

Таким образом, они логически эквивалентны imo, только порядок вывода списков бит отличается.

Может быть, кто-нибудь может подтвердить мою догадку или объяснить, почему два выражения не логически эквивалентны? Было бы замечательно.

Answer 1

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

Ваш первый предикат, например, будет на самом деле never закончился из 0. Нет «послесловий», или «послесловия в дереве поиска, безусловно, никогда не будут посещены. Это, конечно, если вы использовать его для генерации ответов;. использовать его для проверки не обнаруживает такое поведение

Answer 2

В чистой логике порядок операций не имеет значения, поскольку все является функцией идемпотента. Так что, пока у вас нет разрезов или побочных эффектов, A, B и B, A эквивалентны.

Answer 3

Приводя Vannoord

Проблема ли два выражения логически эквивалентны неразрешима для любого `интересной» логики

.

Затем, из-за неполноты поиска Пролога, вы должны несколько ограничить свои критерии доказательств. Я бы сказал, что эквивалентность возникает из-за того, что

для любого заданного N невозможно найти длину (L, N), битlist1 (L), битlist2 (L), которые терпят неудачу. Действительно

2 ?- length(L,N), bitlist1(L), bitlist2(L). 
L = [], 
N = 0 ; 
L = [0], 
N = 1 ; 
L = [1], 
N = 1 ; 
L = [0, 0], 
N = 2 ; 
L = [0, 1], 
N = 2 ; 
L = [1, 0], 
N = 2 ; 
L = [1, 1], 
... 

Answer 4

На логическом уровне, оба предиката эквивалентны, так как «» в правиле интерпретируется как логическое соединения, которое является коммутативной (самый простой способ проверить это, глядя на таблицы истинности для A & B -> C и B & A -> C, а также секвенциальное исчисление или какое-либо другое исчисление исчислений делает работу).

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

?- bitlist1([a|Xs]). 
false. 

?- bitlist2([a|Xs]). 
^CAction (h for help) ? abort 
% Execution Aborted 

Причина заключается в том, что Пролог пытается доказать голы один за другим. В случае bitlist1 первая цель - бит (B), где пролог может сразу решить, что бит (a) не выполняется. В случае bitlist2 пролог сначала пытается доказать bitlist2 (Bs) и рекурсивно делает это для хвоста списка Bs, что приводит к бесконечной рекурсии. Поэтому, даже если оба предиката логически эквивалентны, они ведут себя по-разному.

Для вашей проблемы, глядя на решениях, вы могли бы попытаться перечислить списки в увеличении длины:

?- length(X,_), bitlist1(X). 
X = [] ; 
X = [0] ; 
X = [1] ; 
X = [0, 0] ; 
X = [0, 1] ; 
X = [1, 0] ; 
X = [1, 1] ; 
X = [0, 0, 0] ; 
X = [0, 0, 1] ; 
X = [0, 1, 0] . 

?- length(X,_), bitlist2(X). 
X = [] ; 
X = [0] ; 
X = [1] ; 
X = [0, 0] ; 
X = [1, 0] ; 
X = [0, 1] ; 
X = [1, 1] ; 
X = [0, 0, 0] ; 
X = [1, 0, 0] ; 
X = [0, 1, 0] . 

длина предикат дает соотношение между списком и его длиной. Теперь мы полагаемся на то, что длина (X, _) создает списки свободных переменных возрастающей длины. Затем битовый список цели (1/2) будет вызываться в списке фиксированного размера, а пролог найдет все решения такого размера перед откатом и попробовал следующий более крупный список.

Пожалуйста, обратите внимание, что этот трюк только упорядочивает решения, но не меняет окончание в целом:

?- X=[a|Xs], length(X,_), bitlist2(X). 
^CAction (h for help) ? abort 
% Execution Aborted 

Это до сих пор не удается, потому что Пролог должен проверить все списки X не начать с, но проверка только после рекурсивной цели.