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

[Fergus Henderson]

Lee Naish, you wrote:
> 
> In message <199711101256.XAA15090 at mundook.cs.mu.OZ.AU>Fergus wrote:
> >	:- pred is_ground(var(T), maybe(T)).
> >	:- mode is_ground(in(any), out) is cc_multi.
> >
> >Operationally, is_ground(Var, Result) returns Result = no
> >if Var is non-ground, and Result = yes(Value) if Var is ground;
> 
> If this is guartanteed to be the case then isn't it possible to use
> something like promise_one_solution to write a correct non-logical 
> version which is det/semidet?  Of course you have to tell a little
> white lie: is_ground has one solution.
> 
> I think its important that at least the documentation and predicate
> naming makes it reasonably obvious that this kind of thing is BAD.

Yes, indeed.  If you lie to the compiler, then one day the compiler
will get its revenge.

> In Mercury there are options to fix the selection rule, which makes
> things more dangerous, but the mode system forces us to use cc_ modes
> and keeps things logical.  The logic is lost when the promise in
> promise_one_solution is broken.  I think it fine to have predicates such
> as promise_one_solution (though this name is poor -  six possible
> interpretations are "there is at least/exactly/at most one solution according
> to the declarative/procedural semantics"),

Do you have any suggestions for a better name?

The veteran Prolog hackers probably already consider `promise_one_solution'
to be too verbose.  In fact, even `once' is too verbose for many --
they prefer `!'.

> but it is desirable to have
> debugging support for the cases where promises are broken (since this is
> one source of bugs).

Desirable, yes; but often not feasible, I fear.

> Ideally there should be some debugging/paranoid version/mode for such
> predicates which allows promises to be checked.  For example,
> promise_one_solution called with a nondet procedure could find all
> 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.  This
> might be a bit tricky to arrange - we would need non-cc versions of
> each cc procedure in general.

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.

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.

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