Quine's algorithm with Single Sided Unification in Prolog

Question

The new release 8.3.19 of SWI-Prolog introduces single sided unification inside new Picat style rules. This could be a welcome addition to any Prolog system. I was wondering whether we could rewrite Quine algorithm

Prolog implementation of Quine's algorithm
https://\stackoverflow.com/q/63505466/502187

Picat style rules and whether this would work? If yes and if the writing of the Quine algorithm becomes simpler, then SWI-Prolog probably did a great favor to the community by this addition.

Any take on this challenge? SWI-Prolog 8.3.19 is already available from devel.

Answer 1

Whereas normal unification aka two sided unification is in intimate relationship with the builtin (=)/2, there is a similar relationship between pattern matching aka one sided unfication and the builtin (==)/2. These bootstrappings would work:

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

If we look at the code for Quine algorithm, the take from here, we find a lot of (==)/2 uses. A job that pattern matching could directly do:

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

So we gave it a try and converted all the rules into pattern matching. The initial var/1 guard is then not anymore needed, and so are the (==)/2 not anymore needed. But we observe that we need more (=)/2 to return function values:

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

We did a little benchmark and verified 193 propositional logic test cases from Principia. We tested both normal unification and pattern matching. We also compared with a not yet compiled variant of pattern matching, an expansion that uses subsumes/2:

First the expansion via subsumes/2, that doesn't compile pattern matching:

/* 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

And now the new compiled pattern matching by 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.

I was expecting that the compiled approach shows a tick more bang and not only preservation of the performance of normal unification? But nevertheless this is a good start.

Open source:

Boole's Method from 1847, Prolog Style
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole-pl

Boole's Method from 1847, Picat Style
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole2-pl

Picat Expansion
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-picat-pl

193 propositional logic test cases from Principia
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-principia-pl

Answer 2

Another approach than using a subsumes/2 based translation for single sided unification, is to use lower level single sided unification. SWI-Prolog 8.3.19 implements that already, but the other answer with my system didn't show that.

Do we find other Prolog systems that also provide lower level implemented single sided unification? It turns out yes, for example ECLiPSe Prolog:

4.6 Matching
In ECLiPSe you can write clauses that use matching (or one-way unification) instead of head unification. Such clauses are written with the ?- functor instead of :-. Matching has the property that no variables in the caller will be bound.

ECLiPSe - A Tutorial Introduction
Page 47 (Logical Page 37)
http://eclipseclp.org/doc/tutorial.pdf

We added such an operator also to our system. The rules are now written as follows:

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

And now we are back to the usual performance:

/* 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

Noice!

Open source:

Boole's Method from 1847, ECLiPSe Style
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole3-pl