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

[Peter Schachte]

On Tue, Feb 28, 2006 at 03:38:04PM +1100, Zoltan Somogyi wrote:
> On 28-Feb-2006, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> > Let me see if I understand this right.  You've got some (possibly
> > compound) nondet goal p(X) and another (possibly compound) nondet goal
> > q(X,Y),
> 
> No, for several reasons. First, the motivating p(X) for this whole exercise
> is the deconstruction of a value of a type with user-defined equality.
> That means it is not nondet; it is cc_multi, and no multi version is available
> or can be made available. Second, I am arguing that p(X) cannot be compound,
> and that if we do allow p(X) to syntactically be a conjunction of calls or
> unifications, then that is just a shorthand for there being a separate 'p'
> for each conjunct.

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?

> > If that's the general case, how about just generalizing
> > promise_equivalent_solutions?  You could say that
> > 
> > 	promise_equivalent_solutions Vars Body
> 
> The dealbreaker on that one is that *human readers* of the code would
> *also* have to analyze the code to determine the place of the commit.
> The point of the proposals is to use explicit syntax to mark the scope.

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.

So here's another proposal:

	promise_equivalent_solutions Vars Body1 in Body2

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.

The semantics should be:

	exists Vars . Body1 & Body2

with a promise that

	forall Vars, Vars' . Body1 & Body1' ->
		{ Body2 | Body2 } = { Body2' | Body2' }

where priming is just a renaming toggle (ie, it just gives fresh names
consistently to all variables appearing in the primed atom or variable
list) and = here is just means term equivalence.

-- 
Peter Schachte              You are a sad, strange little man, and you have
schachte at cs.mu.OZ.AU        my pity.
www.cs.mu.oz.au/~schachte/      -- Buzz Lightyear 
Phone: +61 3 8344 1338      
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------