[m-dev.] call for opinions on promise_same_solutions syntax

[Zoltan Somogyi]

On 28-Feb-2006, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> Isn't the case you're describing just a special case of what I
> described?  I think it's nicer to conceive of it as a more general
> language feature, even if you only implement it for the deconstruction
> case, and give an 'unimplemented' error for other cases.  Firstly, it
> should work as well for cc_nondet as for cc_multi (though of course
> failure becomes an option).  Secondly, it makes just as much sense for
> nondet and multi as for cc_nondet and cc_multi (although of course you
> have to actually prune a real choicepoint in those cases).  And
> thirdly, why not allow this over compound goals?

An individual goal in the "premise" can be cc_nondet as well as cc_multi,
sure. The problem is what happens if you have a conjunction of two such goals,
and the second's determinism includes a can_fail component, as for example
cc_nondet does. Then, using the current rules of determinism analysis,
the first goal *cannot* be in a first solution context.

The rest of your proposal is in many ways well argued, but it doesn't solve
this problem, and this problem is *exactly* what motivated the idea of
adding a new language feature. Adding a language feature that doesn't solve
the motivating example is not a good idea.

> OK, fair enough.  But it seems more intuitive, and certainly more
> consistent with the current promise_equivalent_solutions, to list the
> variables whose alternative solutions are uninteresting, rather than
> the variables whose sets of solutions are the same regardless of the
> which solution of the other variables is chosen.

Actually, the existing promise_equivalent_solutions goal lists the second
set of variables, so you have this exactly backwards. There are arguments
in favor of listing the first set of variables, but compatibility with
the existing promise_equivalent_solutions construct is not one of them.

> says that every solution for Vars in Body1 generates the same set of
> solutions for Body2.  Operationally, it says that Mercury should
> commit to the first solution to Body1.  But it is an error for Body1
> to bind any variables not on Vars, and the variables on Vars are
> scoped to Body1 and Body2.

That's a nice idea, but as I said above doesn't address the original problem.

> with a promise that
> 
> 	forall Vars, Vars' . Body1 & Body1' ->
> 		{ Body2 | Body2 } = { Body2' | Body2' }

Sorry, I can't make head or tail of that.

Zoltan.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------