[m-dev.] Thinking about mode analysis and uniqueness

[Ralph Becket]

Following feedback from Peter:

Ralph Becket, Monday,  6 January 2003:
> 
> X < Y	X is possibly used in the construction bound to Y.  < is a
> 	partial order.

Consider

	(	Y = a; X = f(Y)		% 1
	;	X = b; Y = g(X)		% 2
	)

Arm 1 gives Y < X, hence the disjunction as a whole gives Y < X.
Arm 2 gives X < Y, hence the disjunction as a whole gives X < Y.
Hence the disjunction as a whole gives both X < Y and Y < X.
This is fine; it just means that < cannot be a partial order.
Our constraints on < are therefore that it is transitive and
irreflexive:

	(X < Y, Y < Z) => X < Z

	not X < X

I also omitted the the following rules:

	(X < Y, Y ~ Z) => X < Z
	(X ~ Y, Y < Z) => X < Z

> Sharing:
>
> X is possibly shared if two of its possible aliases (which may include X
> itself) are possibly used in the constructions for two other variables
> which are not themselves possibly aliased:
>
> 	(some [Y, Z, A, B] (X ~ Y, X ~ Z, Y < A, Z < B, not A ~ B))  =>	sX

This rule can be simplified and needs refinment: it's only live
references that contribute to sharing:

	(some [Y, A, B] (X ~ Y, X < A, lA, Y < B, lB, not A ~ B)) => sX

> Variable Death
> 
> 	If at any point we have uX and for all Y s.t. X ~ Y we have that
> 	Y does not appear anywhere in the subsequent computation, then
> 	we infer that X is dead, hence dX.

This is not quite right the correct rule is

	(
		local_variable(X),
		all [Y] ( X ~ Y => no_further_occurrences(Y) ),
		all [Y] ( X < Y => dY                        )
	) =>
		dX

We must also have the correctness constraint that the final inst of any
head variables must match (in the obvious sense) the final inst given
for that head variable in the mode declaration.

- Ralph
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------