[sv-ac] 1704, empty match, and local variable assignments

All:

I thought some this afternoon about 1704 and empty match 
assignments.

It seems intuitive to me that if a sequence matches empty, then
no local variable assignment within the sequence should be 
executed during that evaluation thread.  

It also seems intuitive that if a sequence matches empty, then 
we do not want a local variable assignment attached to the sequence 
to execute during that evaluation thread.  

I think these are consistent with what is written in 1704 now.

What we have currently in Annex E is

   (R, v=e)  \equiv  (R ##0 (1, v=e))

Notice that this says more, namely that if we attach a local
variable assignment to a sequence, then the underlying sequence 
is no longer allowed to match empty.  In other words, Annex E 
today implies that

(1)   (R, v=e)  \equiv  (R intersect 1[*1:$], v=e)

(This looks clear to me, although I haven't written a proof.)
I don't think there is anything wrong with this, but it might
be criticized as too restrictive.  It is certainly not saying the following: 

(2)  (R, v=e)  \equiv  (R intersect 1[*0]) or (R intersect 1[*1:$], v=e)

The righthand side of (2) says that if R matches empty, ignore the 
local variable assignment and go on; otherwise, perform the local variable 
assignment at the end of a non-empty match of R.

Applying the flow rules to the RHS of (2) does no seem to be the right
thing to do if R cannot match empty -- we get an artificial
requirement that v flow in in order for v to flow out of (R, v=e).
On the other hand, if R can match empty, then applying the flow rules
to the RHS of (2) seems to give the desirable condition that v 
flow out of (R, v=e) only if it flows in.

We may want to think about changing the semantics of (R, v=e) from
(1) to (2), but there may be some non-trivial work to adapt the flow
rules to work with this.  In any case, such a change should be made
with great care.

Best regards,

John H.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.