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

[Fergus Henderson]

Bart Demoen, you wrote:
> 
> (my code is Prolog rather than Mercury, because it doesn't matter)
> 
> Don and I seem in favour of a predicate like once/1 that could have
> been implemented in Prolog as
> 
> 	once(Goal) :- Goal, !.

Why are you in favour of such a predicate?
Please show us a program in which it would be useful.

> but doesn't need to be. I would be perfectly happy if its semantics
> were rather like in
> 
> 	once(Goal) :-
> 		findall(Goal,Goal,ListOfGoal),
> 		random(N),
> 		nth_element(N,ListOfGoal,Goal).
> 
> and at each invocation - even with the same goal - returns a different
> solution. I would be happy with this semantics but not with its
> implementation.

What is the declarative semantics of `random(N)'?

> Now there is no garantee that for
> 
> 	a :- once(member(X,[1,2])), once(member(Y,[1,2])), X = Y.
> 
> 	?- a.
> 
> succeeds. It doesn't scare me a bit: I can already write it purely;
> once/1 is just that kind of a predicate.

No, you can't write it purely.  The semantics you give above for
once/1 are not pure, because random/1 is not pure.
(Nor is findall, for that matter.)

(Actually you _can_ make random/1 and findall/1 pure in Mercury,
but only by giving them committed choice determinisms,
and if you do that, then once/1 would have determinism `cc_multi'
not `det', which would defeat the purpose -- if you only use
once/1 in single-solution contexts, then Mercury will insert
pruning automatically, so there is no need to write once/1 explicitly.)

> Another aspect of the once/1 I like, cannot be simulated in Mercury:
> 
> 	a(X) :- once(member(X,[1,2])) ; once(member(X,[1,2])).
> 
> also with the random definition of once/1, the query ?- a(X).
> returns the same solution twice (modulo elimination of duplicate
> solutions :-) because random/1 returns the same random number in
> alternative branches.

Why do you like this aspect of once/1?

The once/1 procedure that you have defined cannot be reasoned about
using the declarative semantics.  You can only reason about it using
the operational semantics.  The operational semantics of Prolog is
complicated -- backtracking can be difficult to reason about.
If you want to give up the declarative semantics, you had better
have a good reason.  But I don't see _why_ you would want to
write examples like the a/1 above.

> I picked up once (sic) more the pruneslides.dvi that Lee recommended.
> There is a striking sentence on page 18 with different uses of once/1:
> 
> 	compile(I,O) - you want any solution (this may affect
> 	  completeness if used other than at the top level)
> 
> 
> One person's top level is another person's goal ...
>
> In real life, I very often want any solution (of a restricted set
> though) and [...] it is mostly not at my top level.

Perhaps your complaint is based on lack of knowledge about how to use
Mercury.  Mercury does allow you to use `cc_multi' predicates at places
other than the top level.  For example, suppose you have a procedure
`compute_answer' that computes an answer by invoking the
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).

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

	:- pragma promise_one_solution(compute_answer/2).

rather than by modifying the code for compute_answer/2.
Still, that is basically a minor matter of syntax.)

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