[m-dev.] semantics with any insts

[Ian MacLarty]

On 3/29/06, Mark Brown <mark at cs.mu.oz.au> wrote:
> 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.
>

I agree that determinism declarations are more useful if viewed operationally.

Maybe the determinism category names should be reviewed.  Instead of
having the existing determinism categories such as 'det', 'semidet',
'multi', etc, we should have mode attributes 'can_fail',
'leaves_choicepoint', 'prune_choicepoints' and possibly others.  By
default every procedure succeeds exactly once (same as the 'det'
category), however if you add 'can_fail', then it's determinism is the
same as the current 'semidet' category.  If you add
'leaves_choicepoints', then the determinism is the same as 'multi' or
'nondet', depending on the presence of 'can_fail'. If you add
'prune_choicepoints', then you get the committed choice determinism
categories.  We'd probably also need 'always_aborts' and
'always_fails' mode attributes.

With such a system it is much clearer that the determinism declaration
is an operational property.  To me the word "deterministic" is saying
something about the declarative semantics, since it suggests there is
exactly one solution for a given input. Perhaps "determinism
declaration" is even the wrong term.

For CLP, as an alternative to the promise_consistent scope, we might
add an 'always_fails_if_inconsistent(T)' mode attribute where T is a
solver type.  This mode attribute says that the procedure will always
fail if the constraint store for the given solver type become
inconsistent by executing the procedure.

In the user level code there should be at least one call to a
procedure with this mode attribute in each conjunction that would
otherwise require a promise_consistent scope (this can be verified by
the compiler).  This moves the promise burden from the user to the
constraint solver implementor.

Another possible use of mode attributes would be to declare what
exceptions a procedure might throw, though that's not very relevant to
this discussion.

Anyway it's just an idea I thought I'd throw in.

Ian.

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