Re: Getting different results than Schrijvers

I’m sure you are right, but I’m afraid I am unable to parse your message.

As far as I understand, the point here is that   X \= Y  is not supposed to unify anything: it’s simply a check whether the two are unifiable.  The check for unifiability should be done „in parentheses”, „out of line”. or whatever expression you want to use:  just converting the inequality to   \+ X = Y   and firing off a normal unification leads, as you say, to something that is illegal.  In my opinion it’s not the user’s fault: it’s the implementor’s.

— Feliks


On Apr 5, 2014, at 18:37, [email protected] wrote:

> It really can't. Allowing unification there violates the basic theory of CHR.  The problem is that binding variables activates constraints, but we are in the middle of deciding whether to activate a constraint so doing so would be inconsistent.  Also not activating would be wrong.
> The choices are 
> a) prevent it, at a small performance cost (swi default)
> b) tell people not to do it, and hope (yap default)
> 
> 
>> On Apr 4, 2014, at 3:13 PM, Feliks Kluzniak <[email protected]> wrote:
>> 
>> 
>>> The other one is a case of bad code.
>>> 
>>> neq(X,Y) <=> X \= Y | true.
>>> 
>>> This breaks one of the requirements of CHR: variables cannot be bound in
>>> the guard.  Since X \= Y is \+ X = Y, the runtime is screwing up because
>>> there is an attempt to unify. 
>> 
>> Most interesting!
>> 
>> But shouldn’t this be treated as an error in the implementation?  One can view it as a good example of a leaking interface.  People are sure to trip over this time and time again.
>> 
>> — Feliks
>> _______________________________________________
>> SWI-Prolog mailing list
>> [email protected]
>> https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog