[m-rev.] For review: State Variable Transformation

[Simon Taylor]

On 22-Apr-2002, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Simon Taylor, Sunday, 21 April 2002:
> These decisions were arrived at after some consideration.  There are two
> options: one is to have a simple rule for the transformation that can
> arguably lead to counter-intuitive situations as you point out, the
> other is to have a complicated rule which makes it less obvious what the
> transformation will turn out.
> 
> The simple rule is that within an atomic goal at the level of the source
> as provided by the programmer, all state variable references to !.X will
> map to the same logical variable, X0 for some X0, and all state variable
> references to !:X will map to the same logical variable X1 for some X1.
> The only exception to the rule is that all state variables in a lambda
> term are local to that lambda term.

A rule which is not consistent with the rest of the language is
not simple. The quantification rules for state variables in lambda
expressions are not consistent with the quantification rules for
ordinary variables.
 
> The alternative rule is much more complicated.  It would have to include
> exceptions like
> 
> *1* the simple rule applies to expressions, except for the condition goals
> of if-then-else expressions that reference some state variable X as
> both !.X and !:X where X does not appear in the enclosing scope;

I'm not suggesting performing a different transformation where
!:X occurs in the condition of an if-then-else expression, I'm
suggesting reporting an error.
 
> *2* the simple rule applies to lambda expressions, except where the body
> of the lambda expression refers to !.X (but not !:X) where neither !.X
> or !:X are referred to in the head of the lambda, in which case !.X
> should be defined in the scope enclosing the lambda expression.

That's the normal rule for quantification in lambda expressions.
 
> Exception *1* would lead to situations where
> 
> 	!:X = A, p((if q(!.X, !:X), r(!.X, !:X) then U else V)), ...
> 
> would be transformed into
> 
> 	X0 = A, p((if q(X0, X1), r(X0, X1) then U else V)), ...

No, that would be an error because !:X (where !X is non-local
to the condition of the if-then-else expression) is referenced inside the
condition of the if-then-else expression.
 
> but
> 
> 	!:X = A, p((if q(!.Y, !:Y), r(!.Y, !:Y) then U else V)), ...
> 
> where state variable Y appears only in this context would be
> transformed into
> 
> 	X0 = A, p((if q(Y0, Y1), r(Y1, Y2) then U else V)), ...

That would also be an error because !Y is not explicitly quantified.
That example should be written

    !:X = A, p((if some [!Y] ( q(!.Y, !:Y), r(!.Y, !:Y) ) then U else V)), ...

> Exception *2* would lead to situations where
> 
> 	!:X = A,
> 	F   = ( pred(A) :- !:Y = P, ... )
> 
> would have state variable Y considered local (since it doesn't make
> much sense for the body of a lambda to "update" the value of a state
> variable in the surrounding context), but

!Y needs to be quantified.

> 	!:X = A,
> 	F   = ( pred(A) :- !.X = P, ... )
> 
> where the body of the lambda does not refer to !:X would have !.X
> taken from the enclosing scope, yet
> 
> 	!:X = A,
> 	F   = ( pred(A) :- !:X = P0, ..., !.X = P, ... )
> 
> would again have state variable X local in the context of the lambda
> for the same reason as the example featuring !:Y.

No, that would be an error because !:X (where !X is non-local to the
lambda expression) is referenced inside the lambda expression.

> > Somewhere in make_hlds.m you should explain why you can't just copy
> > the method used by prog_io_dcg.m for the DCG transformation --
> > a forward pass over the goal inserting matching-up unifications
> > at the end of if-then-elses and disjunctions. If it wasn't possible
> > before, would it be possible with the requirement that state variables
> > be explicitly quantified, and the assumption state variables are live
> > throughout their scope?
> 
> The problem arises because state variables are more flexible than
> DCGs.  DCGs have the following properties that do not apply to state
> variables:
> * the DCG state thread always appears in the head of the clause;
> you cannot introduce a DCG thread in the middle of a clause (except
> using the rather ugly DCG-lambda trick);

This is where I think most of the complexity of the transformation
is coming from. I think requiring explicit quantification of
state variables will eliminate a large part of that complexity.

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