[m-dev.] semantics with any insts

[Mark Brown]

On 03-Apr-2006, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> On Mon, Apr 03, 2006 at 11:37:55AM +1000, Ralph Becket wrote:
> > Peter Schachte, Monday,  3 April 2006:
> > >Maybe today a solver writer implements a primitive
> > > constraint by backtracking over possible solutions because it's easy,
> > > and tomorrow does something clever to avoid backtracking.
> > 
> > That sort of implementation detail *should* remain hidden, regardless of
> > whether detisms are given a declarative or operational reading.  Maybe
> > I've misunderstood; can you give an example of what you have in mind?
> 
> Say I'm implementing a cbool type.  I implement the common connectives
> as "semidet" preds, but I get lazy handling xor for some reason, and
> just implement it to backtrack over (true,false) and (false,true), so
> I (correctly) declare it nondet.  Then several users complain that
> it's too inefficient,

The usefulness of the operational reading is that the `nondet' _tells_
the callers that the implementation is too inefficient!  The declarative
reading will provide no help whatsoever in this case.

> so I make it do the correct bookkeeping so I
> don't have to backtrack over solutions, but I'm still too lazy to 
> check that the goal is satisfiable, so I change the declaration to
> "det."  Then after more cajoling, I finally do the right thing and
> change the declaration to "semidet."  But then I get more complaints,
> this time because the data structures grow too large, so I modify the
> code to check if this is happening, and backtrack over the
> alternatives when that happens, so I have to change it back to nondet.
> And every time I change it, all the users scurry back to their code
> and change the determinisms of most of their predicates, cursing that
> this drudgery is the kind of things computers are supposed to be good
> at.

If they don't like having to deal with this themselves they can use
`--infer-all', or a language that doesn't have prescriptive modes.

Can you give an example of where the declarative reading would really
benefit?  The only one I've seen so far is the one I supplied myself.
In fact, can you define what the declarative reading actually is?  The
existing definition in the reference manual talks about "inputs" and
"outputs", but with the xor example both arguments are partly input and
partly output.

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