Bug in determinism analysis

[Fergus Henderson]

On 05-Dec-1997, Warwick HARVEY <warwick at cs.mu.oz.au> wrote:
> There seems to be a bug in determinism analysis with respect to function
> calls in the first argument of the head of predicates.

Hmm.  The issue here is that switch detection stops at the first call.
So if you rewrite your code

> add_list(_, [], []).
> add_list(0 - X, [Y|Ys], Zs) :-
> 	Zs = [X + Y | Zs0],
> 	add_list(X, Ys, Zs0).

as
	add_list(_, [], []).
	add_list(NegX, [Y|Ys], Zs) :-
		NegX = 0 - X,
		Zs = [X + Y | Zs0],
		add_list(X, Ys, Zs0).

then determinism analysis will work fine.

I suppose it would be possible to change switch detection so that
it stops at the first *predicate* call.  However, this might lead
to some anomalies.  Consider the following example.  If you compile
with `--strict-sequential', how should it behave?

	main --> ( { p(0, [1]) } -> print("yes\n") ; print("no\n") ).

	:- pred p(int::in, list(T)::in) is semidet.
	p(loop, []).
	p(_, [_|_]).

	:- func loop = int.
	loop = loop.

Currently the semantics say that with `--strict-sequential', everything
is left-to-right, except as required by the modes.  So this example is
required to loop.  But if we change switch detection so that it
continues past function calls, then this program would not loop;
thus we would also need to change the language's operational semantics
to take into account reordering required by switch detection.

It *might* be worth complicating the operational semantics in this way;
but I'd like to see some compelling examples first.

I suppose the major problem is that the error message doesn't explain
the problem.  We could fix this, I guess, but it would be a fair bit
of work.

Comments?

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