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

[Lee Naish]

Fergus wrote:
>Don Smith wrote:
>> Fergus wrote:
>> 
>> >This is exactly the problem which Mercury's support for committed choice
>> >nondeterminism was designed to solve.  
>> 
>> But it doesn't solve the problem in general, because cc_multi (cc_nondet)
>> predicates are not usable in all contexts where the feature is useful.
>> The programmer is forced to restructure the program so that the cc_multi
>> (cc_nondet) code is at the top level --- not within the scope of other
>> nondeterministic code.   For my program, it was most natural to call
>> unsorted_solutions/2 deep inside nondeterministic code.
>
>I'd like to see your program.

Me too.  A key question is what is the logic behind the assertion that
the nondeterminism in the outer computation is necessary but the
(logical) nondeterminism of unsorted_solutions/2 is unnecessary and
hence can be pruned?

>I suspect that while you may need to use user-defined equality predicates,
>there should not be any need to restructure it.

I have the same suspicion: ie, the logic is the non-standard equality
theory saying that different permutations of the answer are equivalent.
However, is probably additional logic behind the code which uses the
solutions.

The following paper discusses various pruning operators.  Those 
interested in this thread may wish to take a look.  There are a few
wheels being reinvented.

@TechReport{prune,
        Author = { Naish, Lee },
        Title = { Pruning in logic programming },
        Number = { 95/16 },
        Institution = { Department of Computer Science, University of
                Melbourne },
        Address = { Melbourne, Australia },
        pages = 15,
        Month = jun,
        Year = 1995,
        abstractURL = "http://www.cs.mu.oz.au/~lee/papers/prune/",
        comment   =     {Based on an advanced tutorial presented at the
               International Conference on Logic Programming, June
                1995}
}

>> Perhaps another way
>> to avoid it is to add an extra, distinguishing tag argument (e.g., a 
>> string representing the static syntactic call with arguments) to calls 
>> to choice predicates.
>
>This is more promising.
>
>I can still see some serious potential difficulties, though.

It simply doesn't work.  To get referential transparency you need to be
able to replace equals by equals.  This is not replacing syntactic
equals by equals (replacing "1+1" by "1+1" doesn't get you very far!) -
its replacing *semantic* equals by equals (eg, replacing "1+1" by "0").
Its not possible for a dumb machine, or even some smart humans, to
figure out what symbols in my programs/e-mail messages mean addition
(modulo 2).

	lee