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

[Fergus Henderson]

Lee Naish wrote:
> 
> [Fergus wrote:]
> >	:- 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.

Yes, indeed.  The semantics are basically the same.
The difference is just that promise_one_solution is a
higher-order predicate which you can put in the library,
not a new quantifier construct that needs to be part
of the language.

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

That's not a problem in Mercury.  Because `compile' is declared `cc_multi',
the pruning will be done inside `compile'.

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

This can be done in Mercury using promise_one_solution/1 and other
existing constructs.  Consider the example in your paper:
	
	q(I, O) :-
		( r(I, L) =-> exists [O] t(L, O)
		; s(I, L), t(L, O)
		).

In Mercury this can be written as

	:- mode q(in, out) is cc_nondet.
	q(I, O) :-
		( r(I, L), (if t(L, M) then O = M else error("t/2 failed"))
		; s(I, L), t(L, O)
		).

The compiler will push the pruning as far into the body
of the procedure as possible, so in this case, it is equivalent to
putting a cut after the call to `r', rather than putting one
after the disjunction.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.