[m-dev.] semantics with any insts

[Mark Brown]

On 30-Mar-2006, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> On Wed, Mar 29, 2006 at 05:46:39PM +1100, Mark Brown wrote:
> > 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.
> 
> To me, the advantage of the declarative reading is that it makes
> sense.  Saying that X<Y has at most one solution (X and Y not ground)
> doesn't.

The s-semantics makes sense.  It's just not as abstract as the declarative
semantics.

> Another advantage is that it will remain correct with a
> different implementation of Mercury, while the operational semantics
> may change.  Similarly, developers may want to change the operational
> aspects of a solver implementation.  It would be a shame if they were
> discouraged from making such improvements because they knew that every
> module that used that type would need significant modification to
> compile.
> 
> > Remember "Algorithm = Logic + Control".  The user doesn't want to know
> > about these details for the logic part
> 
> Exactly.  Some Mercury CLP programmers may want Mercury to check the
> logical aspects of their mode and determinism declarations, but not
> want to worry about the efficiency issues.

Agreed.  That was the advantage I was referring to at the top of this mail.

And yes, we do lose some power in reasoning about our programs declaratively.
Can you think of some good examples where we really lose something useful?
I'm thinking along the following lines:

	:- func fdvar + fdvar = fdvar.
	:- mode ia + ia = oa is det.

(where fdvar represents variables from a finite domain constraint solver).
Normally this should be impure because of the partially instantiated
output, but the (declarative reading of) det entails referential
transparency so the purity is automatically okay.

> I expect in a great many
> cases, they'll just use a straight constrain-and-generate paradigm and
> really not want to bother about the operational stuff.  It's so
> straightforward in those cases, why should they?

It's straightforward until another developer changes the operational
semantics of _their_ code, which is called by the straightforward
constrain-and-generate code, and wasn't discouraged from making such
"improvements" by the prospect of having to deal with compiler error
messages.  ;-)

> 
> > but they are crucial for the control part.
> 
> OK, so give the programmer a way to assert that a particular
> operational behaviour is expected, but don't encourage programmers to
> make such assertions, since they restrict the developer of the solver.
> 
> Bottom line:  before any insts, putting mode and determinism
> declarations improved the reliability of your code, so they are to be
> encouraged.  With any insts, they really don't help correctness, they
> only ensure you understand (a little bit about) the performance
> characteristics of the program.

A little bit?  The difference between (the operational reading of) semidet
and nondet is a large part of the difference between CLP and LP, which is
the reason to have `any' insts in the first place.

To sum up my view, I think this advantage far outweighs the advantage from
my '+'/2 example.

> Moreover, they straightjacket solver
> implementors.  So they should be discouraged.

I'm really not worried about the "straightjacket" effect -- that's what
strong types, modes and determinism normally do -- but I prefer the
railroad analogy: rail is more expensive to put in place and is less
flexible than road, but makes more efficient use of resources in the long
term.

> 
> At the very least, please use better terminology.  This isn't about
> determinism at all, in the logical sense of the word.  It's just about
> backtracking.

It's about determinism in the algorithmic sense of the word.  FOLDOC defines
"deterministic" in terms of backtracking.  :-)

(But what's in a name?)

Cheers,
Mark.

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