Picat style test case

General
1

Dear All,

I offer a test case to compete with subsumes_term/2 based realization of Picat style rules. I am not against subsumes_term/2 based ideas, but to be convinced, would of course like to see some hard facts, means benchmarking results.

The alternative I see for subsumes_term/2 based ideas is my var/1 indexing. Here is a real world example from a theorem prover:

norm(A, R) :- var(A), !, R = pos(A).
norm((A;B), R) :- !, norm(A, C), norm(B, D), R = or(C,D).
norm((A,B), R) :- !, norm(A, C), norm(B, D), R = and(C,D).
norm((A-:B), R) :- !, norm((-A;B), R).
norm(all(A,B), R) :- !, norm(B, C), R = all(A,C).
norm(exist(A,B), R) :- !, norm(B, C), R = exist(A,C).
norm(-A, R) :- var(A), !, R = neg(A).
norm(- (A;B), R) :- !, norm(-A, C), norm(-B, D), R = and(C,D).
norm(- (A,B), R) :- !, norm(-A, C), norm(-B, D), R = or(C,D).
norm(- (A-:B), R) :- !, norm((A,-B), R).
norm(- all(A,B), R) :- !, norm(-B, C), R = exist(A,C).
norm(- exist(A,B), R) :- !, norm(-B, C), R = all(A,C).
norm(- -A, R) :- !, norm(A, R).
norm(-A, R) :- !, R = neg(A).
norm(A, pos(A)).

One can rewrite it Picat style, and one will possibly find that it needs a few var/1 rules less. But will it also perform? I am happy to see some results. The interesting thing is that var/1 indexing can decide a whole set of subsumes_term/2 tests at once, so this is really a challenge.

Best Regards

Open source:

Maslov Calculus over Herbrandisized Formulas
Prolog flag occurs_check
https://gist.github.com/jburse/ed6eb3316ba1d19309e3711c89dcce3f#file-fitting2-pl

2

It ends with

 ?- time((between(1,100,_), test, fail; true)).

but there is no predicate test/0.

5

Just the code in translated form. The time difference is not measurable but indeed the profiler says this predicate only uses 2% of the time. I do like this version of the code better :slight_smile: Note that eventually we can also gain a little more performance as the clause indexing doesn’t have to check whether this is the only clause as it will commit anyway.

norm((A;B), R) => norm(A, C), norm(B, D), R = or(C,D).
norm((A,B), R) => norm(A, C), norm(B, D), R = and(C,D).
norm((A-:B), R) => norm((-A;B), R).
norm(all(A,B), R) => norm(B, C), R = all(A,C).
norm(exist(A,B), R) => norm(B, C), R = exist(A,C).
norm(- (A;B), R) => norm(-A, C), norm(-B, D), R = and(C,D).
norm(- (A,B), R) => norm(-A, C), norm(-B, D), R = or(C,D).
norm(- (A-:B), R) => norm((A,-B), R).
norm(- all(A,B), R) => norm(-B, C), R = exist(A,C).
norm(- exist(A,B), R) => norm(-B, C), R = all(A,C).
norm(- -A, R) => norm(A, R).
norm(-A, R) => R = neg(A).
norm(A, R) => R = pos(A).
7

I don’t care much. SWI-Prolog is not Picat. It just got a feature from Picat that I consider a good move. Even that is merely inspired by Picat.