[mercury-users] det & cc_multi question

[Vladimir Gubarkov]

Thanks, Ian for your explanation

Now I indeed see the difference.[?]


On Mon, May 17, 2010 at 4:20 AM, Ian MacLarty
<maclarty at csse.unimelb.edu.au>wrote:

> On Sun, May 16, 2010 at 11:46 PM, Vladimir Gubarkov <xonixx at gmail.com>
> wrote:
> > Hi Dear sirs
> >
> > let's look at code
> >
> >
> > :- module tst2.
> >
> > :- interface.
> >
> > :- import_module io.
> >
> > :- pred main(io, io).
> > :- mode main(di, uo) is det.
> >
> > :- implementation.
> >
> >
> > :- import_module solutions, list, int.
> >
> > main -->
> >     {
> >      promise_equivalent_solutions [L] unsorted_solutions((pred(E::out) is
> > nondet :-
> >                                  member(E, 1..20),
> >                                   E mod 3 = 0
> >                                  ), L)
> >     },
> >     print(L).
> >
> >
> > Note, that without "promise_equivalent_solutions [L]" it gives
> >
> >
> > $ mmc tst2
> > tst2.m:008: In `main'(di, uo):
> > tst2.m:008:   error: determinism declaration not satisfied.
> > tst2.m:008:   Declared `det', inferred `multi'.
> > tst2.m:017:   call to `solutions.unsorted_solutions'((pred(out) is
> nondet),
> > tst2.m:017:   out) can succeed more than once.
> > tst2.m:017: Error: call to predicate `solutions.unsorted_solutions'/2
> with
> > tst2.m:017:   determinism `cc_multi' occurs in a context which requires
> all
> > tst2.m:017:   solutions.
> >
> >
> > while compiling.
> >
> > I've read some documentation on cc_multi, and I seem to understand the
> > meaning of cc_multi. It's used when we defining predicate as being multi,
> > but using it in place where we nead only 1 solution (actually, anyone..
> this
> > is determined by compiler what solution to return taking in mind
> > optimization concerns). What I can't understand is why should I
> explicitely
> > convert it to det with "promise_equivalent_solutions [L]". Why compiler
> is
> > not smart enough to make this automatically?
>
> In general det is not the same as cc_multi, which is why the compiler
> doesn't infer them the same automatically.  det means that there is
> exactly one solution to the procedure when it's inputs are bound.
> cc_multi means that there are one or more solutions, but we only want
> to pick one of them.
>
> Consider the following example:
>
> :- pred q is semidet.
> q :-
>    p(X),
>    X > 2.
>
> :- pred p(int::out) is multi.
> p(1).
> p(2).
> p(3).
>
> When you evaluate q it succeeds.  Now say we changed the determinism
> of p to cc_multi and used promise_equivalent_solutions to cast it to
> det in the body of q:
>
> :- pred q is semidet.
> q :-
>    promise_equivalent_solutions [X] p(X),
>    X > 2.
>
> :- pred p(int::out) is cc_multi.
> p(1).
> p(2).
> p(3).
>
> Now q fails, even though the program logic (the declarative semantics)
> hasn't changed.
>
> By requiring you to add the promise_equivalent_solutions the compiler
> is forcing you to think about whether the solutions to p really are
> equivalent.  In this case they aren't and the
> promise_equivalent_solutions is a bug.
>
> I hope that helps.
>
> Ian.
>
> --------------------------------------------------------------------------
> mercury-users mailing list
> Post messages to:       mercury-users at csse.unimelb.edu.au
> Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
> Subscriptions:          mercury-users-request at csse.unimelb.edu.au
> --------------------------------------------------------------------------
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mercurylang.org/archives/users/attachments/20100517/ccf3254e/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 330.gif
Type: image/gif
Size: 96 bytes
Desc: not available
URL: <http://lists.mercurylang.org/archives/users/attachments/20100517/ccf3254e/attachment.gif>