[mercury-users] Re: can one_solution/2 and unsorted_solutions/2 be det?

[Lee Naish]

In message <199710281257.XAA00507 at mundook.cs.mu.OZ.AU>Fergus wrote:
>above-mentioned compile/2 predicate.  The most obvious way of writing
>this in Mercury is as follows:
>
>	:- pred compile(program::in, objectcode::out) is cc_multi.
>
>	:- pred compute_answer(program::in, answer::out) is det.
>	compute_answer(Program, Answer) :-
>		compile(Program, ObjectCode),
>		run(ObjectCode, Answer).
>
>This doesn't quite work, because compile/2 is `cc_multi', whereas
>compute_answer/2 was declared `det'.  But the solution is quite
>straight-forward:
>
>	:- pred compute_answer(program::in, answer::out) is det.
>	compute_answer(Program, Answer) :-
>		Answer = promise_one_solution(compute_answer_cc_multi(Program))
>.
>
>	:- pred compute_answer_cc_multi(program::in, answer::out) is cc_multi.
>	compute_answer_cc_multi(Program, Answer) :-
>		compile(Program, ObjectCode),
>		run(ObjectCode, Answer).

promise_one_solution seems very similar to my proposed "only" construct,
which has well defined declarative semantics.

>(Although this solution is straight-forward, it is not quite ideal;
>as Peter Schachte mentioned, the ideal way of solving this would be
>by adding some sort of declaration, e.g.

Another problem is that the pruning is only done (I think) after run,
not immediately after compile, possibly doubling the space requirements
of the program.  In general, if a program makes N nondeterministic
choices, the space usage can grow by a factor of N.  I proposed a
declarative construct ("exists") which can avoid this.

	lee