[HAL-dev] Re: [m-dev.] Solver types in Mercury - meeting notes and comments
Ralph Becket
rafe at cs.mu.OZ.AU
Mon Feb 16 08:47:05 AEDT 2004
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
--------------------------------------------------------------------------
More information about the developers
mailing list