Алгоритм Куайна с односторонним объединением в Прологе

В то время как обычное объединение, известное как двустороннее объединение, находится в тесной взаимосвязи со встроенным (=) / 2, существует аналогичная взаимосвязь между сопоставлением с образцом, также известным как одностороннее указание, и встроенным (==) / 2. Эти начальной загрузки будут работать:

=(X,X) :- true.
==(X,X) => true.

Если мы посмотрим на код алгоритма Куайна, взятый здесь, мы найдем много (==) / 2 использует. Работа, которую может выполнить сопоставление с образцом:

simp(A, A) :- var(A), !.
simp(A+B, B) :- A == 0, !.
simp(A+B, A) :- B == 0, !.
Etc..

Итак, мы попробовали и преобразовали все правила в сопоставление с образцом. Тогда начальная защита var / 1 больше не нужна, как и (==) / 2 больше не нужны. Но мы замечаем, что нам нужно больше (=) / 2 для возврата значений функции:

simp(0+B, X) => X = B.
simp(A+0, X) => X = A.
Etc..

Мы провели небольшой тест и проверили 193 тестовых примера логики высказываний из Principia. Мы протестировали как обычную унификацию, так и сопоставление с образцом. Мы также сравнили с еще не скомпилированным вариантом сопоставления с образцом, расширением, которое использует subsumes / 2:

Сначала расширение с помощью subsumes / 2, которая не компилирует сопоставление с образцом:

/* Jekejeke Prolog 1.5.0 */
/* normal unification */
?- time((between(1,380,_), test, fail; true)).
% Up 996 ms, GC 6 ms, Threads 984 ms (Current 02/14/21 11:30:28)
Yes

/* pattern matching */
?- time((between(1,380,_), test, fail; true)).
% Up 3,525 ms, GC 24 ms, Threads 3,500 ms (Current 02/14/21 11:42:50)
Yes

А теперь новое скомпилированное сопоставление с образцом с помощью SWI-Prolog:

/* SWI-Prolog 8.3.19 */
/* normal unification */
?- time((between(1,380,_), test, fail; true)).
% 4,940,000 inferences, 0.547 CPU in 0.534 seconds (102% CPU, 9033143 Lips)
true.

/* pattern matching */
?- time((between(1,380,_), test, fail; true)).
% 4,940,000 inferences, 0.531 CPU in 0.531 seconds (100% CPU, 9298824 Lips)
true.

Я ожидал, что скомпилированный подход покажет галочку побольше а не только сохранение работоспособности нормальной унификации? Но тем не менее это хорошее начало.

Открытый источник:

Метод Буля из 1847 года, стиль Пролога
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole-pl

Метод Буля из 1847 года, стиль Пика
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole2-pl

Расширение Picat
http://%20https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-picat-pl

193 тестовых примера логики высказываний из Principia
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-principia-pl

Другой подход, чем использование перевода на основе Subumes / 2 для односторонней унификации, заключается в использовании односторонней унификации более низкого уровня. SWI-Prolog 8.3.19 уже реализует это, но другой ответ с моей системой этого не показал.

Находим ли мы другие системы Prolog, которые также обеспечивают одностороннюю унификацию на более низком уровне? Получается да, например ECLiPSe Prolog:

4.6 Сопоставление
В ECLiPSe вы можете писать предложения, которые используют сопоставление (или одностороннее объединение) вместо объединения заголовков. Такие предложения записываются с функтором? - вместо: -. Сопоставление имеет свойство, заключающееся в том, что никакие переменные в вызывающей программе не будут связаны.

ECLiPSe - Введение в учебное пособие
Стр. 47 (Логическая страница 37)
http://eclipseclp.org/doc/tutorial.pdf

Мы также добавили такой оператор в нашу систему. Теперь правила записаны следующим образом:

simp(0+B, X) ?- !, X = B.
simp(A+0, X) ?- !, X = A.
Etc..

А теперь вернемся к обычному исполнению:

/* Jekejeke Prolog 1.5.0 */
?- time((between(1,380,_), test, fail; true)).
% Up 1,067 ms, GC 11 ms, Threads 1,032 ms (Current 02/14/21 21:43:56)
Yes

Шум!

Открытый источник:

Метод Буля из 1847 года, стиль ECLiPSe
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole3-pl