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

Fergus Henderson fjh at cs.mu.OZ.AU
Mon Feb 16 10:43:29 AEDT 2004

On 16-Feb-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Fergus Henderson, Friday, 13 February 2004:
> > On 13-Feb-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> > > it seems reasonable to me to say that the following
> > > programs are equivalent under their respective interpretations:
> > >
> > > [example deleted]
> > 
> > Your example is reasonable.  But in that example, you only are only
> > considering one constraint store, the one that contains the final
> > (ground) answers.  The problems that I see come because the constraint
> > store is mutable, or because some terms represent non-ground values,
> > neither of which was present in your example.
> As far as the constraint store is concerned, surely that's just a
> mechanism for representing posted constraints?  It doesn't matter how
> many constraint stores there are.
> I think I see where you're going with the second point: non-ground
> solver values can potentially take on any number of possible ground
> values.  However, solutions/1 takes a predicate that produces inst
> ground values, not inst any values.  So it seems to me that there's a
> mode error in your example at least.

Nope -- the parameter of the predicate passed to solutions/1
gets ground by the call to q/1, whose mode should be
`:- mode q(out)' is nondet.  So there is no mode error.

There was however a typo in my example: s/X/Term/g
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)))).

> > 	... assume suitable definitions of f/1, c/0, and q/1 ...
> >
> > The laws of logic mean that there can only be at most one value of Term
> > for which Term = cf(x), which means that the list of solutions can have
> > length at most one, so a Mercury implementation is permitted to replace
> > the body of p/0 with `true'.
> I take it that q/1 is semidet or det in this case?

No, q/1 is nondet.

> Your argument here, if I understand, is that if f(c) denotes some
> non-ground solver type value then there may be an arbitrary number of
> ground term bindings for Term that would unify successfully.

Not exactly.  There may be an arbitrary number of ground term bindings
for Term which would NOT unify successfully with each other
(but which will each unify with Term).

> But that's
> exactly the case with non-canonical types.  If I rewrite `Term = f(c)'
> as `Term = set_represented_by_unsorted_list([1])', say, (defining
> set_.../1 as a data constructor for a non-canonical type) then the same
> "problem" arises.

No, it doesn't because in that case although e.g. both
`set_represented_by_unsorted_list([1,1])' and
`set_represented_by_unsorted_list([1,1,1])' will unify with Term,
they will also unify with each other.

In the case of `Term = cf(0)', `cfloat(1.0)' and `cfloat(2.0)'
will each individually unify with Term, but not with each other.
That's the difference.

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


Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
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

More information about the developers mailing list