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

[Fergus Henderson]

Lee Naish wrote:
> 
> 2) Implement a "first solution" construct.  Unfortunately this depends
> on the clause and literal selection strategy, which Mercury does not
> currently allow the programmer to fix.  You would have to fix this in
> order to make this construct declarative (as done in Trilogy).  The
> disadvantage of first solution primitives is the semantics is
> complicated.  The advantages are they are quite useful and very cheap to
> implement.  Its a very pragmatic approach.  I suspect Bart would be
> happy with it.

I think you would only need to nail down the clause (disjunct) selection
strategy (usually called the "search rule"), not the literal (conjunct)
selection strategy (usually called the "computation rule").

In fact Mercury does allow the programmer to fix both the search rule
and the computation rule.  The Mercury language reference manual documents
that implementations must support a strict sequential (left-to-right)
operational semantics.  The current Mercury implementation supports
this with the `--strict-sequential' option.  You can also get more
fine-grained control with the `--no-reorder-conj', `--no-reorder-disj',
and `--fully-strict' options.  For "first solution", you would need
only `--no-reorder-disj'.

The reason for supporting this is to ensure portability of
Mercury programs between different Mercury implementations.
However, its use is not encouraged too much, because nailing down the
search rule imposes potentially significant restrictions on the
implementation, restrictions that would for example prevent a future
Mercury implementation from taking advantage of concurrent
OR-parallelism.  The Mercury language reference manual requires that
any implementation which supports concurrent OR-parallelism also
provide a way of switching it off, but it is better to write programs
that don't depend on this.

However, even if you nail down the search rule, that is not enough
to make a higher-order `first_solution' library predicate work in Mercury.
The reason is that `first_solution' is not referentially transparent;
it does not satisfy `P = Q => first_solution(P) = first_solution(Q)',
because in Mercury, the declarative semantics of equality on higher-order
terms is such that two predicates are equal iff they have the same
set of solutions.

The "declarative" semantics for first solution which are outlined in
one of Paul Voda's papers on Trilogy have some very nasty properties.
One of these is that the declarative semantics depends on the
operational semantics.  This means that in order to reason about things
at a high level, it becomes necessary to know about and reason about
the low-level procedural details.

Another nasty property is that this effect is non-local: in order to
verify that the declarative semantics for a predicate using "first
solution" meets its specification, you need to know about the
operational semantics of the predicates it calls.  This means that for
any nondet predicate called from within "first solution", the interface
for that predicate needs to document not only its declarative semantics
(i.e. which solutions it returns), but also its procedural semantics
(i.e. the order in which they are returned).  [Incidentally, since the
Mercury standard library does not document this, that would rule out
calling any nondet procedures in the Mercury standard library.]
Furthermore, maintenance needs to ensure that any changes to the
implementation of such a nondet predicate do not change the order in
which the solutions are returned.  If maintenance does change the
order, then all the callers need to be examined.

Another unfortunate property is that to make "first solution"
referentially transparent, you would have to change the
declarative semantics of equality on higher-order terms.

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