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

[Lee Naish]

In message <199710290929.UAA19040 at mundook.cs.mu.OZ.AU>Fergus wrote:
>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).

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

Somehow I had a mental image of run/2 being cc_multi.  I think
originally in this discussion it was det, in which case Fergus is right.

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

Tricky use of if-then-else and error!

Has anyone figured out a declarative semantics for programs containing
error/1?

The reason I ask it that this example shows how it can be done (the same
style as "exists" etc).  You add an additional assertion which is that the
path containing the call to error must be false.  In this case its

all [I,O] not( some [L] (r(I, L), not ( some [M] t(L, M))))

At a guess, this is equivalent to the assertion which captures the
declarative semantics of exists given in my paper.

	lee