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

[Lee Naish]

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

Not true, as I pointed out in

@inproceedings{naish:solns:85,
        author =        {Naish, Lee},
        title  =        {All solutions predicates in {Prolog}},
        booktitle =     {Proceedings of the Second IEEE Symposium on
                                Logic Programming},
        address =       {Boston, Massachusetts},
        year   =        {July 1985},
        pages  =        {73--77},
        comment = {Technical report 84/4, Department of Computer Science,
                University of Melbourne}
}

You can implement var/1 in IC-Prolog due to this fact.

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

Last time I was involved in discussion of these, `--no-reorder-conj' did
not guarantee no reordering (it just prevented unnecessary reordering).
I suggested the meaning should be changed.  Was this done?  Does
`--strict-sequential' really guarantee no reordering (ie, will the
compiler produce an error message if left to right ordering is not "well
moded")?

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

Hmm, I hadn't thought of that.  In a more Prologish language you can
give a schema to define the semantics of (declarative) all solutions
predicates.  You can't do this if you have "real" higher order.

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

As I said, the semantics are complicated, downright nasty even.
Nevertheless, programmers do use such reasoning.  I suspect Fergus has
used such reasoning in game playing programs he has written.  I
certainly have.

	lee