[HAL-dev] Re: [m-dev.] Solver types in Mercury - meeting notes and comments

[Zoltan Somogyi]

On 16-Feb-2004, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> So the correct example is
> 
>  	:- pred p is semidet.
>  	p :- 1 >= list.length(std_util.solutions(
>  		(pred(Term::out) is nondet :- Term = f(c), q(Term)))).

I don't see how that could be replaced with true with or without solver
types being involved.

I think one disconnect between you two is that in this context, asking
"what is the declarative semantics" is a in a sense the wrong question.
We are providing facilities for building solvers, and it is up to the
*programmer of the solver* to ensure that the implementation of the
solver faithfully implements a declarative semantics. I think the best
we can do are:

- decide on what parts of the program have declarative semantics implemented by
  Mercury, and what parts have their declarative semantics implemented by a
  solver,

- document exactly what properties we require from the solver implementation
  (including properties of the implemented declarative semantics), and

- provide tools for solver programmers.

One problem we haven't adddressed so far, but will need to, is detecting
and handling floundering.

> > Are you in this afternoon?  I think this discussion would work better in
> > person with a whiteboard!
> 
> Sure.

That would be a good idea.

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