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

[Ralph Becket]

Second attempt.

Properties of variables at some point in a computation:

bX	X is definitely bound to some (fully ground) value.

fX	X is definitely free.

sX	X is possibly shared (i.e. X may have been used in more than one
	construction).  Possible sharing may be asserted or inferred
	(see Sharing, below.)

uX	X is definitely unique (i.e. X has been used in at most one
	construction that is itself definitely unique).

dX	X is definitely dead (i.e. X may not be used again.)

lX	X is definitely alive.

X ~ Y	X and Y are possibly aliased.  ~ is an equivalence relation.

X < Y	X is possibly used in the construction bound to Y.  < is a
	partial order.

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 is a little subtle.  The constraint on A and B is most clearly
stated as possibly_different(A, B); now
	possibly_different(A, B)   <=> not definitely_the_same(A, B)
and 	definitely_the_same(A, B)   => possibly_the_same(A, B)
so	not possibly_the_same(A, B) => not definitely_the_same(A, B)
hence	not possibly_the_same(A, B) => possibly_different(A, B)
and possibly_the_same is synonymous with ~.

Definitions:

	fX <=> not bX.
	uX <=> not sX.
	lX <=> not dX.

Inference:

	(sX, X ~ Y) => sY
	(dX, X ~ Y) => dY

	(X < Y, sY) => sX
	(dX, X < Y) => dY

Goals:

I will use the notation Precondition | Goal | Postcondition
or just Goal | Postcondition where Precondition is not of interest
or just Precondition | Goal where Postcondition is not of interest.

We treat goals as operators on states of variables and write P(S) to
denote the state resulting from successfully executing P starting in
state S.

The Postcondition lists those properties that are explicitly affected
by successfully executing the goal.  All others that do not follow are
unaffected (so we don't have to write endless frame axioms.)

Aliasing, X = Y

	lX, fX, lY, bY  |  X = Y  |  bX, X ~ Y

Test for equality, X = Y

	lX, bX, lY, bY  |  X = Y  |

Construction, X = f(Y, ...)

	lX, fX, lY, bY, ...  |  X = f(Y, ...)  |  bX, Y < X

Deconstruction, X = f(Y, ...)

	lX, bX, lY, fY, ...  |  X = f(Y, ...)  |  bY, Y < X, ...

	We may also have postcondition uY for some uY depending upon the
	inst of X at this point.

Test for equality with functor, X = f(Y, ...)

	lX, bX, lY, bY, ...  |  X = f(Y, ...)  |

Procedure calls, p(X, Y, ...)

	The pre- and postconditions for each call will depend upon the
	procedure used.

	The precondition will require that all arguments be live.

	Argument mode X	| Precondition	| Postcondition
	----------------+---------------+--------------
	free >> free	| fX		|
	free >> bound	| fX		| bX, sX
	free >> unique	| fX		| bX, uX
	bound >> bound	| bX		| sX
	unique >> bound	| bX, uX	| sX
	unique >> unique| bX, uX	|
	unique >> dead	| bX, uX	| dX

	It is an error for the postcondition of p(X, Y, ...) to
	include (X ~ Y, uX, uY) (unless we also have (dX, dY) in the
	postcondition.)

	This constraint forbids Peter's example where

		:- mode p(di, uo, uo).

		p(X, Y, Z) :- Y = X, Y = Z.

Conjunction, (P, Q), starting with state S

	If PrecondP | P then S must entail PrecondP.
	If PrecondQ | Q then P(S) must entail PrecondQ.
	The resulting state is Q(P(S)).

Disjunction, (P ; Q), starting with state S

	If PrecondP | P then S must entail PrecondP.
	If PrecondQ | Q then S must entail PrecondQ.
	If X is a nonlocal and P | bX then we must also have Q | bX
	and vice versa.
	For any nonlocals X and Y we must have
		if P | dX    then (P ; Q) | dX    (and similarly for Q),
		if P | sX    then (P ; Q) | sX    (and similarly for Q),
		if P | X < Y then (P ; Q) | s < Y (and similarly for Q),
		if P | X ~ Y then (P ; Q) | s ~ Y (and similarly for Q).

Negation, not P

	Handled as ( if P then false else true ).

Conditional goals, ( if P then Q else R ), starting with state S

	If X is a nonlocal then we may not have P | bX.

	Otherwise handled as (P, Q ; R).

Initial state

	The initial properties of each argument variable are taken from
	the argument mode (with initally free variables also being
	unique) and local variables are initially free and unique.

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.

Reuse criterion

	A variable X's cell may be destructively updated (reused) if we
	have (uX, dX).

I'll hold off posting thoughts on efficient implementation until I see
what holes people can find in the above.

Cheers,

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