Re: Getting different results than Schrijvers

Thanks for the explanation!

— Feliks

On Apr 5, 2014, at 23:27, Alan Baljeu <[email protected]> wrote:

> At one time, \= was a nice simple predicate, and it could have simply checked the terms to see if they were compatible.  Now, the only way to be sure is to actually attempt unification, and go see if the bindings that result violate any constraints such as from CLP(FD) - or any other system that may have been built using attributed variables.  This is useful behaviour, and absolutely necessary.
> 
> CHR implements an algorithm such as 
> 	when(nonvar(X), <<check if there are any constraints on X and process rules>>).
> 
> It goes out to match rule heads to constraints.  This includes guard, whose sole purpose is to delve into the terms so we can match on something more narrow than equality of parameters.  Checking a rule against a new binding is supposed to be an atomic operation.  But if you unify something, that causes recursion back through the when clause.
> 
> Given the above factors, I claim there is no possible solution: CHR cannot allow unification, and \= cannot operate without unification.  I consider the choice in SWI of converting the attempt to failure a reasonable choice.  Perhaps a run-time error would be more appropriate because quite simply A \= B in the guard CANNOT be supported.
>  
> Alan Baljeu
> From: Feliks Kluzniak <[email protected]>
> To: [email protected] 
> Cc: Michael Richter <[email protected]>; swipl list <[email protected]> 
> Sent: Saturday, April 5, 2014 4:58:23 PM
> Subject: Re: [SWIPL] 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
> 
> 

-------------- next part --------------
HTML attachment scrubbed and removed