swipl-devel icon indicating copy to clipboard operation
swipl-devel copied to clipboard

Pattern matching shouldn't be bugged by occurs check

Open ghost opened this issue 4 years ago • 0 comments

Pattern matching doesn't need occurs check. The fresh clause head variables do not appear in the goal, even so after pattern matching since pattern matching doesn't change the goal.

But in SWI-Prolog concerning occurs check, (=>)/2 and the occurs check dont work well together. Because (=)/2 does still sneak into code that uses (=>)/2, to return something, SWI-Prolog will be bugged by

the occurs check. I guess there is also problem with clause head unification, that SWI-Prolog doesn't see where the occurs check is or is not needed.

/* SWI-Prolog 8.3.19 */
/* patten matching, occurs_check=false */
?- time((between(1,1000,_),test,fail;true)).
% 3,646,000 inferences, 0.766 CPU in 0.777 seconds (99% CPU, 4762122 Lips)
true.

/* patten matching, occurs_check=true */
?- time((between(1,1000,_),test,fail;true)).
% 6,547,000 inferences, 1.000 CPU in 1.002 seconds (100% CPU, 6547000 Lips)
true.

SWI-Prolog incures a considerable overhead, the ratio is 1002 / 777 = 128%. But there shouldn't be any overhead at all.

Open Source:

Negation Normal Form, Tail Recursive Picat Style matching https://gist.github.com/jburse/7705ace654af0df6f4fdd12eee80aaec#file-normswi2-pl

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

ghost avatar Feb 22 '21 12:02 ghost