[mercury-users] Getting 'any' insts to ground

[Lee Naish]

In message <199711110303.OAA21245 at mundook.cs.mu.OZ.AU>Fergus wrote:
>Lee Naish, you wrote:
>> as promise_one_solution (though this name is poor
>
>Do you have any suggestions for a better name?

I suggest a semidet procedure only_solution and a det procedure
one_and_only_solution.  The "_solution" could be dropped from both if
you want things more concise.  Only_solution could have a det mode(s)
if its argument has a mode which guarantees at least one solution.
One_and_only_solution can be implemented using only_solution and error.

To me at least, reading "only_solution" my immediately thought is if
there really are more solutions.  I think this is a good thing (my
second thought would be that the programmer is claiming there are no
other solutions).  Documentation should clearly distinguish between
declarative and procedural semantics for cc procedures.

Other names could be based on the following words:

sole (gives me a stronger impression that it exists cf "only" - you could
	use sole_solution instead of one_and_only_solution)
single (less informative - could mean "a single" rather than "the
	single"; note that "sole" doesn't have this problem, at least
	not as much)
one (seems less informative to me - like "single")
unique (could be confused with unique modes; otherwise it would be good)

>> solutions and check there is the right number.  The "right" thing to do
>> for promise_one_solution calling a cc_nondet procedure would be to have
>> a nondet version of the procedure and call that instead, as above.

>For many predicates, such as for example is_ground/2, it is not
>feasible to provide non-cc versions.  The non-cc version of is_ground/2
>would have to have an infinite number of solutions.  So there is no
>possibility of checking all cases.

Yes, you would want to combine the generation of solutions and the
checking for the right number (as soon as you got two different
solutions you could complain).

>One possibility would be to allow (require?) the programmer to supply
>a proof of the assertion; this proof could be checked by a theorem
>prover.

Requiring it would be too restrictive.  There is a big difference
between having a formal proof online in the right syntax and just knowing
a theorem eg, looking it up in some handy reference book (such as The
Complete Works of Fermat:-).

	lee