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

[Ralph Becket]

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.

> OK, consider the following procedure.
> 
> 	:- pred p is semidet.
> 	p :- 1 >= list.length(std_util.solutions(
> 		(pred(X::out) is nondet :- Term = f(c), q(X)))).
> 
> 	... 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?

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

> But your definition of cf/1 does not satisfy those laws of logic, and
> so applying the optimization for cf/1 would be unsound.

I disagree.  You have to do something to a constrained float to obtain a
normal float and *that* might be a non-deterministic operation.  But
there's nothing particularly special about the ground representation of
constrained float that may or may not represent a unique, ground, normal
float.

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

Cheers,
-- Ralph

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