Tricky CHR behaviour

Hello, I have a CHR as follows:

:- use_module(library(chr)).
:- chr_constraint try/1.

try(X), try(Y) <=> X == Y | writeln(succeed).

then I declared a constraint, but got an unexpected result:

?- try(A).
succeed
try(A).

The unexpected succeed seems to be because Prolog matches try(A) to both try(X) and try(Y). But does this make sense?

Thanks in advance! :slightly_smiling_face:

See A strange behavior of CHR package

However, if you only have grounded constraints, then you should be okay. try(X) by itself doesn’t make sense (at least to me) as a constraint.

Thanks Ian!
From the post your shared, it is a pretty old issue.
Hope this will be fixed, sooner rather than later…

CHR is not in active development. It is open source and could be fixed, but i dont know any experts on the internals are around to do so. Seems like something i would have to tackle if i got back into chr, but its not presently my focus.

I was scratching my head why this could be unexpected. I haven’t touched CLIPS for a while but I’m quite confident that it behaves the same. I’m 99% sure that this is the same behavior Soufflé uses too. It also aligns with my understading of RETE rule engines.

For me the dissection is as follows:

?- try(A). % Add fact to the store

try(X), % Is there a fact try(X) => YES - try(_999).
try(Y)  % Is there a fact try(Y) => YES - try(_999).
<=>
X == Y  % Does X == Y? => YES, because _999 is _999.
| writeln(succeed).

To those unfamiliar with RETE - there are 3 phases of rule resolutions:

  1. Match (find entities in rule)
  2. Resolve (check rules)
  3. Act (fire actual rules)

In Match phase there is no store modification (this happens in Act phase) nor conflict resolution (which is Resolve phase). Match phase is completely isolated from store and guards.

An example to consider, as well:

number(4), number(X) <=> X < 5 | writeln(succeed).
?- number(4).

And finally: If match phase would be sequential it would be impossible to parallelize queries. For naive constructs it doesn’t matter but in production each part of match query can and probably should be ran in parallel, so there’s no “knowledge” between the threads/systems which entity was “yanked” from the store.

For me this is completely intutive, though I spent considerate time with CHR systems (even designed a rule based parser in CLIPS: Crazy Parser Idea), and RETE rule engine design.

Thanks @xlii, that explains a lot!

Now that I understand the mechanism and can adjust the expectation of how it behaves. However, the actual problem remains unsolved. Essentially the CHR guard needed here is to compare any two separate try/1 facts, iff there are at least two separate try/1 facts. I guess this may be a pretty common scenario when we input the CHR facts one by one into the store. But with my limited skill, I don’t know how to implement that.

Any workaround? Much appreciated!

In addition to the last message, I’ve found something interesting.

We can get a different result, if we disable the printout of CHR store:

:- use_module(library(chr)).
:- chr_constraint try/1.

:- set_prolog_flag(chr_toplevel_show_store, false).

try(X), try(Y) <=> X == Y | writeln(succeed).

Then it works as I want it to.

?- try(A).
true.

Pretty amazing…

Keep in mind, you don’t have a duplicate facts, i.e. there’s no:

cat(black).
cat(black).

only

cat(black).

So you need to be explicit that these facts are, in fact, separate, so:

cat(A, Color), cat(B, Color) <=> A #= B | cat_pair(A,B,Color).

Give facts identifier of some sort.

In this case you have:

?- cat(spooky, black).
% Nothing runs, because the only match is cat(spooky, black), cat(spooky,black)
% and spooky ==  spooky.
?- cat(cookie, black).
% 3 pairs found: (spooky,spooky), (cookie,cookie), (cookie, spooky)
% 
% Why not (spooky, cookie) and (cookie, spooky)? - RETE engine Matches are unordered

% cat(spooky,black), cat(spooky, black) NO MATCH
% cat(cookie,black), cat(cookie, black) NO MATCH
% cat(cookie,black), cat(spooky, black) MATCH -> ACT

This might be actually confusing.
I’m not sure what’s the phase of the printout (empty store wouldn’t make any printout, I suspect this is after-fact before-rule). Would have to check the docs.

Other explanation would be that non-concrete fact cannot be removed from store, because at that moment it could be that:

store:  try(_9999)
act:    remove(try(_1111))
result: [try(_9999)] sub try(_1111) => [try(_9999)]

I propose checking this with manual printout of store - should tell more than a flag.

Thanks @xlii , assigning each fact a unique identifier is a solid solution!

CHR will have a rule like a(X) \ a(X) <=> true to eliminate duplicates. If that fired when you only have a single a(4), it would be bad.

Efficiency note: it doesn’t matter for toy problems, but at scale, with optimizations on, the optimizations including hashing on integers. So using _vars is convenient but if you’re tagging your terms for uniqueness a ground identifier is better.