[m-dev.] more correctness problems

[Peter Stuckey]

On 30/03/2006, at 4:55 PM, Ralph Becket wrote:

> schachte at csse.unimelb.edu.au, Thursday, 30 March 2006:
>> Hi all,
>>
>> I've been considering the problem of solvers goals that
>> (operationally) succeed even when the constraint store is
>> unsatisfiable.  I've argued before that due to this, problems arise
>> from existential quantification.  Peter argued that the only problem
>> is negation (I hope I'm being fair here).  On reflection, I think
>> both are problems.  Consider this code:
>>
>> 	p(X) :- q(X,Y).
>>
>> 	q(X,Y) :- X>4, Y>4, Y<4.
>>
>> Suppose operationally, the solver for X promises that (>)/2 fails when
>> the domain for either of its arguments is empty, while the solver for
>> Y does not (assume they're different types).  Now the code for p/1 may
>> actually be wrong, because when Y goes out of scope (is existentially
>> quantified away), nothing forces the solver to actually test that
>> there does exist a satisfying Y.
>
> I believe my promise_consistent scope addresses this problem.
>
>> Certainly
>>
>> 	exists Y . Y>4, Y<4
>>
>> is false, but Mercury implements existential quantification by just
>> dropping the variable.  If the solver doesn't keep a central store, Y
>> will just get garbage collected, so the inconsistency will never be
>> discovered.
>
> Both the solvers and the trail will remember Y, so Y will not be  
> garbage
> collected.

Indeed the answer is not (true) but
	exists Y. Y > 4, Y < 4

Hence the answer is correct.
What Peter points out that just keeping seeing when a body with anys
leads to a head with no anys doesnt stop you missing that some solver
needs its complete method run, if we quantify away all the variables
for one solver but not another.

I think it does fit with Rafes scheme since the interpretation is this
	for any goal with an any variable in it
		success = unknown
whereas for any goal without an any variable
		success = true.
So my argument agrees with Rafe. Track this info and you can see when
you have to be careful with negation.


>> Even if it does have a central store, when would it ever
>> get around to checking that Y has a solution?  Note, though, that if
>> the arguments in the call to q/2 were exchanged, there would be no
>> problem there, because the unsolvable variable would still be alive.
>> So the problem is specific to the variables quantified away.
>>
>> This suggests solvers should be able to define a semidet method that
>> gets invoked when a solver variable goes out of scope (is quantified
>> away), indicating that it's now or never to check that the variable
>> has solutions.  The Mercury compiler would generate calls to this
>> method automatically where the variable goes out of scope.
>
> I think this would shaft search performance in virtually all solver
> applications and make solver types highly unattractive.  This is why I
> suggested promise_consistent instead.

Well the solver may be able to do variable elimination in which case  
its OK.
Or perhaps we could use it to mark a global saying the solver has
existentially quantified variables.
But I agree forcing it to search at this point will
	(a) break determinism (everything will be nondet becuase of this call)
	(b) kill performance.

>> This would
>> also allow solvers that do keep a central store of constraints to
>> remove dead variables, knowing they'll never be seen again.
>
> That's not quite true, as these things will still exist on the trail
> (untrailing will cause solvers to "forget" variables).
>
>> Probably
>> the method should take a list of variables, so the solver gets all the
>> variables to be killed off at the same time, allowing it to plan its
>> actions.
>>
>> Note that this problem is different from the problem of negations
>> involving any insts.  There the concern is that a negated goal should
>> not further constrain a non-ground variable.  I don't imagine there
>> are many goals involving any inst variables that don't constrain those
>> variables, so I don't expect there would be many cases where a negated
>> context mentioning an any inst variable is sound.  They really should
>> be impure.
>
> There are many sound cases where you end up with a solver variable in
> the condition of an if-then-else.  For example, list.length(Xs) (Xs is  
> a
> list of solver vars) or any_map.search(AnyMap, Key, X) (AnyMap contains
> solver vars, but Keys are ground).  Currently the compiler *does*  
> require
> such situations to be treated as impure.  It has been suggested (and I
> think it's a good idea) that such things should instead only be allowed
> in a scope that states explicitly the nature of the problem (e.g.,
> something like promise_solver_type_in_negation_is_sound, but hopefully
> less wordy).
>
> -- Ralph
> ----------------------------------------------------------------------- 
> ---
> mercury-developers mailing list
> Post messages to:       mercury-developers at cs.mu.oz.au
> Administrative Queries: owner-mercury-developers at cs.mu.oz.au
> Subscriptions:          mercury-developers-request at cs.mu.oz.au
> ----------------------------------------------------------------------- 
> ---
>
>
------------------------------------------------------------------------ 
--------------------------
Peter Stuckey					
Professor of Comp Sci and Soft Eng
Network Information Processing Program NICTA	
University of Melbourne
www.cs.mu.oz.au/~pjs

National ICT Australia Limited
Locked Bag 9013
Alexandria NSW 1435
Tel. +61 3 8344 1341
Fax. +61 3 9348 1184
Email. peter.stuckey at nicta.com.au
Web. www.nicta.com.au
 
The imagination driving Australia's ICT future.
 
To receive the latest NICTA information register at  
http://nicta.com.au/registration.cfm
 

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------