Unexpected rule fired.

[chansey97]

Hi,

For the following program

%% test.pl 
:- use_module(library(chr)).
:- chr_constraint c/2.

c(K,_I), c(K,_J) <=> writeln('rule 1 fired').
c(_I,K), c(_J,K) <=> writeln('rule 2 fired').

?- consult(["test.pl"]).
true.

?- c(X,Y).
rule 2 fired
c($VAR(X),$VAR(Y)).

Although the 2nd rule has two heads and I only added one constraint (c(X,Y)), the rule still fired.

This issue can be reproduced in Stable release - SWI-Prolog 8.4.1-1 for Microsoft Windows (64 bit), and Daily builds - swipl-w64-2022-01-31.exe (version 8.5.6-26-gee0b3fea1).

N.B. swish has no the same problem, but the constraint are not preserved, see https://swish.swi-prolog.org/p/unexpected_rule_fired.pl

Thanks.

[JanWielemaker]

Might be better to ask on the Discourse forum. I can barely belief such elementary code can show a bug. It is probably more misunderstanding of CHR. I'm not an expert on this.

[fnogatz]

Hi @chansey97. This is probably due to some confusion about how CHR works on the terms in a rule's head. When checking if a given constraint matches a rule's head, it performs a matching instead of Prolog's traditional unification. The matching is like a one-way unification (as also stated in the Wikipedia article). That's why even a small program like the following does not what one might expect at first sight:

:- use_module(library(chr)).
:- chr_constraint p/2.
p(1,1) ==> writeln('rule 0 fired').
% ?- p(X,Y) will just put this constraint to the constraint store, without any unification

Therefore, there are two rules of thumb:

• Do not expect a constraint's variable to bind while matching.
• Check guard bindings yourself.

Depending on what you want to achieve, you could modify you program to reflect CHR's way of unification and thinking. However, after all, I'm not sure if that's something you really want to achieve: firing a rule that has two constraints in the head by just a single constraint. This really sounds like something that should be modelled differently.

[JanWielemaker]

This issue has been mentioned on SWI-Prolog. There might be relevant details there:

https://swi-prolog.discourse.group/t/a-strange-behavior-of-chr-package/4964/1

[chansey97]

@JanWielemaker

OK. I have repost it on Discourse.

Thanks.

@fnogatz

Yes, CHR is like a one-way unification. However, even from this perspective, it is still hard to explain this strange behavior.

For your example, it is no problem and works as I expected:

?- p(X,Y).
p($VAR(X),$VAR(Y)).

As you said that p(X,Y) be put in the constraint store. Then I can wake it by unification:

?- p(X,Y), X=Y, X=1.
rule 0 fired
X = Y, Y = 1,
p(1,1).

It reflects the constraint logic programming. That is good.

For my example, I also hope c(X,Y) be put in the constraint store.

The expected behavior is

?- c(X,Y).
c($VAR(X),$VAR(Y)).

The "rule 2 fired" should not be printed, because there is only one constraint. It could matches the 1st constraint at head, but no partner constraint in the store.

Thanks.

[fnogatz]

Ah, I thought you were arguing that rule 1 should fire instead. I would suggest we stick to the Discourse discussion first and close the issue here as long as we have not clearly identified it as a bug?

[chansey97]

@fnogatz I have seen your comment in the discourse forum. It looks like a bug (after 7.3) as you said? So still leave it open for a while? Thank you for tracking this issue.