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

[Ralph Becket]

I've been thinking about mode analysis for nested uniqueness and wanted
to put my thoughts up for discussion.

I am only considering the case where variables are either free or fully
bound; I am not interested in partial instantiation.

To start with I will just consider conjunctions of non-negated atomic
goals.

Each variable in the goal may have one or more of the following
properties:

	bound(X)	X is bound to some term.

	X < Y		X was used in the construction of the term to
			which Y is bound; < is areflexive, asymmetric
			and transitive.

	X ~ Y		X is an alias of Y; ~ is symmetric and
			transitive.

	dead(X)		X may not be referred to in any subsequent
			computation.

We use the following definitions and rules:

	free(X)		<=>	not bound(X)

	shared(X)	<=>	some [Y, Z] (X < Y, X < Z, Y \= Z)

	unique(X)	<=>	not shared(X)

	live(X)		<=>	not dead(X)

	X ~ Y, bound(Y)  =>	bound(X)

	X ~ Y, shared(Y) =>	shared(X)

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

	X ~ Y, dead(Y)   =>	dead(X)

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

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

Each atomic subgoal will have one of the following forms:

	X = Y		var/var unification

	X = f(Y, ...)	var/functor unification

	p(X, ...)	predicate call

Following STRIPS, we treat each type of atomic subgoal as a function
manipulating properties of variables: each subgoal has a precondition
dictating when it is legal to invoke it, and a postcondition giving the
properties that hold after successful execution of the subgoal (any
possible contradictions with the postcondition are taken to be
implicitly retracted and all other properties remain unaffected.)

Assignment Unification
X = Y
	Precondition:	live(X), live(Y), free(X), bound(Y)
	Postcondition:	X ~ Y

Comparison Unification
X = Y
	Precondition:	live(X), live(Y), bound(X), bound(Y)
	Postcondition:	true

Construction Unification
X = f(Y, ...)
	Precondition:	live(X), live(Y), ..., free(X), bound(Y), ...
	Postcondition:	bound(X), Y < X, ...

Comparison Construction Unification
X = f(Y, ...)
	Precondition:	live(X), live(Y), ..., bound(X), bound(Y), ...
	Postcondition:	true

Deconstruction Unification
X = f(Y, ...)
	Precondition:	live(X), live(Y), ..., bound(X), free(Y), ...
	Postcondition:	bound(Y), Y < X, ...
Here I'm slightly fudging things because Y may become shared depending
on X's inst.  The details should not be too complicated to work out.

Predicate Call
p(X, Y, Z, ...)
Preconditions and postconditions are defined in mode declarations, for
example mode p(in, di, uo, ...) would give
	Precondition:	live(X), live(Y), live(Z), ...,
			bound(X), unique(Y), free(Z), etc.
	Postcondition:	shared(X), dead(Y), unique(Z), etc.

The task of termination analysis for simple conjunctions is to find an
ordering of the conjuncts such that the preconditions for each conjunct
are met (if such an ordering exists.)

The initial head variable properties are given by the mode declaration for
the predicate and locals are unique, live and free; the final variable
properties must agree with those given in the mode declaration (local
mode declarations may be inferred if necessary from the predicate's call
sites.)

We extend the analysis to cover disjunction and conditional goals (and
hence negation) thus:

Disjunction
(P ; Q)
	If P binds any non-local X then Q must bind X also and vice
	versa.
	If P makes any non-locals X and Y aliases X ~ Y then X ~ Y is a
	postcondition of (P ; Q) and similarly for Q.
	If P makes any non-local X shared then X is shared as a
	postcondition of (P ; Q) and similarly for Q.
	If P makes any non-local X dead then X is dead as a 
	postcondition of (P ; Q) and similarly for Q.

Conditional Goals
( if P then Q else R )
	P may not bind any non-local X of the conditional goal.
	P may not make dead any non-local X of the conditional goal.
	P may not make any two non-locals X and Y aliases X ~ Y.
	Conjuncts from P may not be migrated into Q or vice versa.
	The effect of the conditional goal is equivalent to that of
	(P, Q ; R).

Negation
not P
	The effect of the negated goal is equivalent to that of
	( if P then false else true ).

It seems to me that analysis of this sort shouldn't be too hard to
implement in an efficient manner and integrate with the existing mode
analysis.

Any comments?

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