[mercury-users] det & cc_multi question

[Ian MacLarty]

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