[mercury-users] Getting 'any' insts to ground
lee at cs.mu.oz.au
Tue Nov 11 12:44:36 AEDT 1997
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.
I suspect many novice Mercury programmers would not realise that calling
is_ground inside promise_one_solution is telling a lie - they would
think that its a legitimate way of getting the mode checker to stop
producing those stupid error messages.
There is a fine line between logical and nonlogical code/languages once
you introduce pruning. In Goedel its possible to implement a version of
is_var which works *if* you have a fixed clause selection rule. Since
Goedel doesn't guarantee this, you can argue that its theoretically
impossible write a correct version of is_var (of course in practice you
can write one which works, since the only existing Goedel implementation
does used a fixed selection rule).
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"), but it is desirable to have
debugging support for the cases where promises are broken (since this is
one source of bugs).
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. However, I think its important that there
are ways of automatically checking that no promise is broken, for a
particular input to the program.
More information about the users