[mercury-users] single solution predicates and deductive DBs

[Fergus Henderson]

On 15-Jul-1998, Don Smith <dsmith at cs.waikato.ac.nz> wrote:
> 
> A while ago we discussed single-solution predicates on this list.     
> Below are some references about work in the deductive database 
> community on the similar topic of "choice operators."
>
> In short, if you're looking for a respectable semantics for single
> solution predicates, you can find one in these works.  One basic idea
> is that in a program with negation there are often multiple, minimal 
> models.   The semantics for a single-solution predicate is to
> asymmetrically choose one of those models.

This basically comes down to the same thing as one of your previous
suggestions on this topic, the use of Hilbert-style choice functions. 
If there is a single model, then every call with the same inputs must
return the same outputs.  We could use those semantics, but there are
some potential problems with actually implementing them.

One problem is that it would require us to fix the order of computation,
which we don't want to do.

Another problem is that it won't work for higher order predicates,
at least not unless we change the semantics of equality for higher
order terms, which we don't want to do.  Similarly, it would not
work for predicates that take input arguments of a type with a
user-defined equality.

It would be possible to implement without fixing the order of computation
by tabling the answers (indeed the latest development version of Mercury
does support tabling) but that would have significant efficiency costs,
and could cause space leaks, and so you generally don't want to do that.
In addition, this work-around would not be possible in the case of
higher order predicates, and would be theoretically possible but
practically infeasible in the case of types with a user-defined
equality.

And practically, I think the current approach of using committed choice
nondeterminism will work fine anyway.  All we need is better support
for promising that a goal only has one solution, in cases where it really
does, but the compiler can't figure that out -- currently you can
do it using a higher-order library predicate, but a pragma or language
builtin would be more convenient.

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