[m-dev.] semantics with any insts

[Mark Brown]

On 29-Mar-2006, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> On Wed, Mar 29, 2006 at 01:26:58PM +1000, Peter Stuckey wrote:
> > An answer in CLP (with any insts) is a set of constraints not known to 
> > be false, and determinism tells you
> > how many sets of constraints you can have.  This is the S semantics for 
> > LP/CLP.
> 
> This doesn't seem very good for Mercury, because it's very
> operational.

I agree it is an operational view.  The reference manual does take the
approach that there is a declarative reading of the main detisms (det,
semidet, nondet, multi), but there's a few things to bear in mind:

	- Those definitions were written before partially instantiated
	  data was thought about much.
	- They were certainly written before `any' insts were thought of.
	- They were not written with constraint programming in mind.

Also, on an arguably irrelevant note:

	- The current implementation of Mercury takes the operational
	  view, and doesn't respect the declarative reading.

I think we have a choice between sticking with a declarative reading and
fixing the implementation, or moving to an operational reading and fixing
the reference manual (and probably fixing the implementation a bit, too).

I can see the advantages of the declarative reading, namely that more
powerful reasoning can be done about Mercury programs.  Presumably this
is the motivation for your earlier stated view.

But there are advantages to the operational reading too.  Before I mention
them, though, I'll point out one thing: in the case where there is no
non-ground final insts (which in practice mostly means no `any' insts, but
there are occasional uses of the `unused' mode), the two readings
correspond exactly.  In other words, if you aren't doing constraint
programming then the determinisms give you the same effective power to
reason about your program with.

> For example, is this predicate deterministic:
> 
> 	p(X) :- X =< 4, X >= 2.
> 
> Your semantics distinguishes between {{2=<X, X=<4}} and
> {{X=2},{X=3},{X=4}} as two possible semantics for this; the first one
> is det while the second one was multi.

Precisely, assuming the argument has mode `oa' (otherwise they would be
semidet and nondet, respectively).

Observe that the former corresponds to constraint-and-generate, while
the latter corresponds to generate-and-test.  The distiction between
these is, of course, extremely important to constraint programmers.
And the distinction is operational only -- declaratively they are
indistinguishable.

> So the user of a solver type
> has to know too much about changable implementation details.

Remember "Algorithm = Logic + Control".  The user doesn't want to know
about these details for the logic part, but they are crucial for the
control part.  As an example, the constraint programs I've been writing
can (mostly) be divided into parts that are semidet, and parts that are
nondet.  It is very useful to have this distiction made explicit and
verified by the compiler.  It will be even more useful when implementing
hybrid FD + LP applications (*).

So the question is: should the determinism system help with the logic
or the control?

As I said above, when not doing constraint programming the operational
view and the declarative view are pretty much equally useful for helping
with the logic.  So the point is moot in that case.

When doing constraint programming, however, the usefulness of the
operational view for the control part seems to me to far outweigh
the usefulness of the declarative view for the logic part.  So in my
opinion the operational view is the one we should go with.

Cheers,
Mark.

(*) I can elaborate on these points, if anyone wants.

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