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

[Fergus Henderson]

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

Actually pruning will still be done inside `compile' even if run/2 is
cc_multi.

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

Sure.

The declarative semantics for error/1 are just `error(X) <=> error(X)'.
Since this is a tautology, the declarative semantics for error/1 are
vacuous.  Note that this is different to say var/1, which does not have
any consistent declarative semantics; error/1 _does_ have a declarative
semantics, just not a very informative one.

To prove that the definition of q/2 conforms to its specification, i.e.
that the declarative semantics of the clauses for q/2 are sound with
respect to its intended interpretation, you need to prove that the
semantics of those clauses are independent of the semantics of error/1
(presuming error/1 is not part of the specification).

To prove that q/2 will not fail at runtime, you need to prove that
it won't call error/1.  You need to reason using the operational
semantics to prove this.

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

This is not the semantics of error/1 in Mercury.
Those semantics would give you a quite different construct.

With the semantics defined in the same style as for "exists", the
compiler would be allowed to *assume* that the assertion is correct, and
generate code accordingly.  With error/1, the compiler is not allowed
to assume that the assertion is correct.  Instead, it is allowed to
check it at runtime and if the assertion is not satisfied, to give up
trying to solve this query.

In other words, with "exists" (as with promise_one_solution), the
programmer is making an assertion, and if the assertion is wrong, the
program is inconsistent, and so the behaviour is undefined.  With
error/1, the worst that can go wrong is that the implementation may
be incomplete (it may report an error message, rather than giving an
answer to the top-level query).

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