from [mercury-users] Re: Question regarding determinism

[David Glen JEFFERY]

Hi all,

Thought I'd move this one to mercury-developers... this thread might get
pretty technical.

On 19-Aug-1998, Thomas Charles CONWAY <conway at cs.mu.OZ.AU> wrote:
> Waugh, Sam, you write:
> 
> > This is defined as semidet, because I want it to fail under
> > certain conditions.  In this case the code marks an assumption
> > about an existing object; but that only makes sense if the
> > object exists.
> > 
> > Now the type is along the lines of:
> > 
> > :- type moddat == list(elements).
> > :- type elements ---> o(string, string); a(string).
> > 
> > where o is definition of the object and it's class and a is a
> > statement about a defined object.
> > 
> > My initial implementation was:
> > 
> > moddat__add_assumption(Obj, Model, [a(Obj)|Model) :-
> > 	list__member(o(Obj,_), Model).
> > 
> > which runs into problems as list__member with a non-ground term
> > is nondet.  How can I make this semidet?  I don't care what class
> > the object is, as along as it exists.
> 
> A quantifier is the right thing, but to get it right you need to
> know that the compiler flattens unifications, so your code becomes
> something like (I've used more sensible variable names than the
> compiler uses for its automatically introduced variables):
> 
> moddat__add_assumption(Obj, Model, Result) :-
> 	list__member(Element, Model),	% <---
> 	Element = o(Tmp, _),		% <---
> 	Tmp = Obj,			% <---
> 	Thing = a(Obj),
> 	Result = [Thing|Model].
> 
> Now, the determinism problem is because call to member is nondeterministic,
> and is not within a scope with no output bindings. What we need to do is
> restrict the scope of element by putting the three marked lines above in
> a restricted scope:
> 
> moddat__add_assumption(Obj, Model, Result) :-
> 	some Element (
> 		list__member(Element, Model),
> 		Element = o(Tmp, _),
> 		Tmp = Obj
> 	),
> 	Thing = a(Obj),
> 	Result = [Thing|Model].
> 
> This we can now simplify till we get almost your original code:
> 
> moddat__add_assumption(Obj, Model, [a(Obj)|Model]) :-
> 	some [] (
> 		list__member(o(Obj, _), Model)
> 	).

Yuck! IMHO, the compiler is not handling implied modes correctly.

Surely this:
moddat__add_assumption(Obj, Model, [a(Obj)|Model) :-
	list__member(o(Obj,_), Model).

and this:
moddat__add_assumption(Obj, Model, [a(Obj)|Model]) :-
	some [] (
		list__member(o(Obj, _), Model)
	).

are the same thing, given that the call to list__member/2 has no output vars!

I think that the introduction of variables for the implicit unifications of an
implied mode need to be a little more careful in preserving quantification.

Thoughts?


love and cuddles,
dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) |  Marge: Did you just call everyone "chicken"?
PhD student,                    |  Homer: Noooo.  I swear on this Bible!
Department of Computer Science  |  Marge: That's not a Bible; that's a book of
University of Melbourne         |         carpet samples!
Australia                       |  Homer: Ooooh... Fuzzy.