[mercury-users] Determinism question

[Mark Brown]

Hi Peter,

I believe I can explain what is going on here.  I'm not sure how we should
go about fixing the problem, though.  In fact, given that determinism
inference can never be perfect, I'm not sure we should try to "fix" it at
all.

On 06-Jan-2006, Peter Hawkins <hawkinsp at cs.stanford.edu> wrote:
> In the following code, why can the determinism checker verify that the 
> first mode of foo is semidet, but not the first mode of bar?
> 
> As far as I can see both satisfy the requirement of section 6.4 of the 
> reference manual:
> -----
> If you just want to see if a nondeterministic goal is satisfiable or 
> not, without needing to know what variable bindings it produces, then 
> there is no problem - determinism analysis considers |nondet| and 
> |multi| goals with no non-local output variables to be |semidet| and 
> |det| respectively.
> ----

You need to consider what is meant by "goal".  Goals such as individual
calls and entire conjunctions are checked to see if they satisfy this
property.  It is possible to have a sequence of conjuncts which
individually do not satisfy this property, but do when conjoined.  If
they are the only goals in the conjunction then fine -- it will be
inferred semidet or det -- but if there are other conjuncts then the
conjunction as a whole may not satisfy this property.

>    % ndindex0
>    % Like list.index0, but can be used non-deterministically as well
> :- pred ndindex0(list(T), int, T).
> :- mode ndindex0(in, in, out) is semidet.
> :- mode ndindex0(in, out, out) is nondet.

...

> :- pred foo(list(int), int).
> :- mode foo(in, in) is semidet.
> :- mode foo(in, out) is nondet.
> foo(List, Val) :-
>    ndindex0(List, _, Val).

For the first mode of foo/2, the call to ndindex0 is an implied mode.  This
means it gets expanded to something like the following conjunction:

	ndindex(List, _, Vnew),		% nondet
	Vnew = Val

List and Val are inputs, according to the mode of foo/2, and Vnew is local,
therefore this conjunction is inferred to be semidet rather than nondet.

> 
> :- pred bar(list(int), int, int).
> :- mode bar(in, in, out) is semidet.
> :- mode bar(in, out, out) is nondet.
> bar(List, Val, Val2) :-
>    ndindex0(List, _, Val),
>    Val2 = Val + 1.

Here the body gets expanded to somthing like:

	ndindex(List, _, Vnew),
	Vnew = Val,
	Val2 = Val + 1

Again, List and Val are inputs and Vnew is local.  But in this case the
conjunction has a non-local output, Val2, so it can't be inferred to be
semidet.

> I've worked around the problem with some impure code, but I'd like to 
> know what's going on here.

You can probably also work around it by expanding the implied mode yourself,
and explicitly existentially quantifying the introduced variable.  Like this:

bar(List, Val, Val2) :-
	some [Val0] (
		ndindex(List, _, Val0),
		Val0 = Val
	),
	Val2 = Val + 1.

The "some" goal will be able to be inferred semidet.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------