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

[Fergus Henderson]

Don Smith wrote:

> Declarative languages are like stern, strict codes of ethics.

I quote this part first, because this is perhaps the key issue.
I don't have time right now to respond to this in the depth which it deserves.
However, I want to make one thing absolutely clear: in the context of
declarative programming languages as I see them, and as reflected in
the design of Mercury, purity is a practical issue, *not* a moral issue.

The reason for designing a declarative language based on pure logic
is to make programming easier, not to make it harder.
Our hypothesis is that by keeping the semantics simple, and
preserving the relationship with predicate calculus, we will
have a language that is easy to understand, easy to reason about,
and which enables us to harness and make practical use of the many
theoretical advantages of logic programming (e.g. parallelization,
automatic proofs of termination, etc., etc.)

The designers of Mercury are very pragmatic people, we want to build
real systems, and we want our language to assist in that task, not
to make it harder.

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

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

> Should the programmer be forced to make do without this (allegedly
> non-logical) "feature"? 

Well, that depends.  If the feature is going to break the relationship
between programs and logic, make programs difficult to reason about,
and make it impossible for compilers to take advantage of the laws
of logic to optimize, transform, and parallelize programs, and
particularly if the alternatives are not terribly burdensome,
then yes, the programmer should use the alternatives.

> Or should the language theorists try harder to 
> find a respectable semantics for it?

I don't think exhorting language theorists to "try harder" is going to
resolve the issue.  I personally have put a lot of work into finding a
respectable semantics for committed choice nondeterminism.  By my own
criteria, I think I have succeeded.  But if you think Mercury's approach
isn't a success, then by all means show us the programs for which Mercury's 
approach fails.

> For the case of destructive
> assignment, modern declarative languages allow the feature only within
> single threaded code (using unique modes, monads, etc);  this too is 
> painful sometimes.

Mercury (versions >= 0.7.2) has support for backtrackable trailed
destructive update, so you can use destructive update in nondeterministic
code too.

> > For example, there might be two logically equivalent predicates (with 
> > different predicate names) for which the solutions are computed in a 
> > different order, yet the semantics says that the chosen solution must be 
> > the same in both cases.
> 
> Orgun and Wadge claim that they avoid this pitfall by making choice
> predicates first-order rather than second order.

Well, I still haven't read that paper, but I think I can take a guess
at why they say that: second-order choice predicates would be undecidable;
first-order choice predicates are merely inefficient.  By restricting
things to the first-order case, they avoid the problem of undecidability,
but this still doesn't solve the efficiency problem.

> 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.  A Mercury
compiler might not always return the answers to a goal in the same
order (e.g. answers might be returned in arbitrary order each time, due
to concurrent OR-parallelism).  So the choice function would need to
table its results in order to ensure that they remained consistent.
That would be OK in some circumstances, but in many cases the overhead
of tabling would be too high.  Furthermore, the storage for the table
entries could never be deallocated, so the result would be a memory
leak.

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