Proof of lemma 0.3 - Githubissues

I still got some problems with the proof the important Lemma 0.3 (changed as lemma 1.1 in the pdf). Here is my analysis and current solution, but not sure if it is correct. concatlemma.pdf

First, it's a little hard for me to read the note because you have apparently updated the definitions of ~^S and |><|^S, but they are not included in the pages you uploaded, nor is there an updated version of the whole document in the main GitHub tree. But I'll assume that they are more or less like what we talked about last week.

Second, Lemma 1.1 actually doesn't hold as stated even in the simple case where p is just a single transducer invocation and S is empty. The reason is the second rule in the transducer semantics (it would be nice if all the rules had names), which says that, when the control stream is empty, the output stream is always taken to be empty, even if there is still some (garbage) data in one or more of the input streams to be read. For example, with c = <()>, a1 = <2>, and a2 = <3,4>, we get MapTwo+(a1,a2) ↓^c <5>, so the extra <4> in the second stream is ignored. But if we concatenate two copies of the inputs, i.e, invoke "MapTwo+(a1++a1,a2++a2) ↓^(c++c) ?", we get MapTwo_+(<2,2>,<3,4,3,4>) ↓^<(),()> <5,6> instead of the <5,5> that the concatenation lemma would claim. (You should have discovered that when doing the proof for that case, if you did it carefully.)

The simplest fix is probably to require, in the second rule, that all the input streams are empty whenever the control stream is empty. Then the above situation cannot arise, because there cannot exist a derivation of "MapTwo_+(<2>,<3,4>) ↓^<()> <5>" in the first place. Note that this requirement corresponds to having an explicit runtime check in the interpreter to verify that the transducer has fully consumed all its input streams, once it reaches the end of the control stream. It may be possible to prove later that all SVcode generated from a SNesl program will be sufficiently well behaved that this check isn't strictly necessary, but then you'll need to generate specific extra code that checks for length mismatches in zip-like comprehensions, e.g. when compiling "{x+y : x in {2}, y in {3,4}}". (There's actually a separate issue in proving that if evaluation of a SNesl expression fails with a runtime error, such as mismatching lengths in "zip", applying "the" to a non-singleton stream, applying "iota" to a negative argument, etc., then the compiled SVcode will also fail, rather than return a random result; but let's not worry about that right now.)

Now back to the case for WithCtrl. Here we have the problem that when the new control stream is empty, the body code is not executed at all, thus bypassing any runtime checks within it. In other words, the semantics of WithCtrl with a special case for an empty control stream (which is only really needed to preserve the step cost, and to avoid infinite unfolding in recursive definitions, neither of which is an issue for Level 0), may differ from the naive semantics that uniformly executes the WithCtrl body, and for which it should be (relatively; see below) straightforward to prove the concatenation lemma.

I think the simplest solution will be to also add a runtime check to WithCtrl, i.e., in the rule for WithCtrl(s,p) where sigma(s) = <>, there should be an additional requirement in the side condition that all the free variables of p are also bound to empty streams in sigma. That will ensure that prepending or appending them to streams from the other derivation will have no effect, so that you can just reuse that derivation directly. (You'll probably need a separate lemma saying something like, if two sigmas agree on all the free variables of a program p, then executing p in them will also yield output stores that agree on all thew new streams added by p.) Again, it may be possible to prove later that this runtime check can safely be omitted, which would simplify the streaming interpreter a bit.

Note also that, in the case for concatenating two non-empty executions of WithCtrl, you will probably need to adjust the set S when invoking the IH on the body program. It may be relevant to already now only consider programs where every WithCtrl has been explicitly annotated with an import list (which should be a conservative over-approximation of the actual set of free variables of the WithCtrl body). That could make it easier to keep track of what S should be at each point in the proof; and possibly the lemma only actually holds for well-annotated programs (which should include all the ones generated by the compiler), rather than all syntactically well-formed ones.

As for your specific questions, maybe incorporating the above changes will be enough, but in case not:

Q1: It is true that the current semantics ensures that a program will never be executed with an empty control stream. However, I don't think it should be necessary to formalize that invariant in either the semantics or the proofs, as it probably wouldn't simplify anything. And it may actually be nice to leave the possibility open to also have a "quick" variant of the WithCtrl instruction, that doesn't check for emptiness at runtime (which is a fairly involved process in the streaming interpreter), but always executes the body, even if the new control stream happens to be empty. This could be used, e.g., for the WithCtrl in iota, and possibly also the one in pack, where it might end up costing more in practice to detect and handle packing of already empty streams as a special case.

Q2: I'm not sure if you are simply proposing a change of notation (which would have no effect on the actual semantics or proofs), or something deeper. In the former case, however, I would say that the current notation is preferable, because otherwise in some contexts psi will have k arguments and in others it will have k+1, which is likely to lead to confusion.

Q3: I don't think EmptyCtrl should present any new problems that are not already introduced by iota(0), i.e., essentially by generating an empty control stream with Usum(<T>). So if everything works out for iota, it shouldn't be necessary to worry separately about EmptyCtrl.

If we fix the 2nd rule of transducer semantics P-X-Termi as \psi(<>,...,<>)↓^<> <>, and add the side condition forall s in Sin. sigma(s) = <> to the evaluation rule P-Wc-Emp, then it seems possible to prove this lemma.

Something unclear to me:

Note that this requirement corresponds to having an explicit runtime check in the interpreter to verify that the transducer has fully consumed all its input streams, once it reaches the end of the control stream.

In the code, we have rinx only to check that when the control stream has not reached EOS the input streams cannot be EOS either. But we don't have a runtime check to verify the situation you mentioned here. And then you also pointed out:

It may be possible to prove later that all SVcode generated from a SNesl program will be sufficiently well behaved that this check isn't strictly necessary, ... (There's actually a separate issue in proving that if evaluation of a SNesl expression fails with a runtime error, ... then the compiled SVcode will also fail...)

So it's a little bit confusing what we need to do or not.

Q1-Q3 makes sense.
In the latest code, I changed the STree in WithCtrl to [(PType, SId)] instead of just [SId] for two reasons. First, it is easier to code. Second, if we don't know the PType of the return SIds, we may only be able to infer that type information from the SVCODE program/instructions for each of them, which may have trouble for some cases, for example, look at the SVCODE for {}{{bool}}
```
> :c {}{{bool}}
...
S1 := EmptyCtrl;
WithCtrl S1 (import []):
Return: [S2,S3,S4];
S5 := Const T PBool
Return: [S2,S3,S4,S5]
```
It seems impossible to infer the types of S2-S4 as there are no instruction definitions for them.

In P-Wc-Emp and P-Wc-Nonemp, I tried to add another side condition (marked with ???) which says that only the newly defined SIds from p will be added to the new store. This is also what actually happens in the code:

sInstrInterp (WithCtrl c _ code retSids) =
do ctrl@(SUVal bs) <- lookupSid c 
 if null bs  
   then emptyStream $ filter (\(_,s) -> s > c) retSids  -- this filter should be unnecessary, 
                                                        -- just to keep uniform with P-Wc-Emp
   else localCtrl ctrl $ mapM_ sInstrInterp code      --  will only add new SIds from `code` to context

But I'm not quite sure if it is a good idea to do so.

I have added the proof of this lemma in the pdf. Please let me know if there is some problem. Also, if necessary, we can meet later today? Or I think I can start Level-1 with Packs and Distrs?

This looks much better now. There are still a couple of things to fix, but I don't think it should be necessary to meet about them today:

On the bottom of p.2, I don't think it's a good idea to make S_in include the new control stream (unless s actually also occurs as a literal parameter in one of transducers in p1), because it mixes up the ''true" import list with the new control stream, which is already treated very specially in the operational semantics. The point is that both s and (the true) S_in should be available separately in the WithCtrl instruction. In some contexts it may be appropriate to treat s as another import, but that is easily accomplished by considering the set {s} U S_in. On the other hand, if s is always included in S_in, it is no longer possible to distinguish between the cases where s also occurs explicitly in p1, and when it's only implicit. If you make this adjustment, you should also change the definition of fv() in point (5) on p.3 to always include s_c in the set of free variables of a WithCtrl instruction, regardless of whether it occurs in S_in. I also think that the syntactic restriction for WithCtrl should only require that be fv(p1) subset S_in (in addition to what you have about S_out). The compiler is free to satisfy this by always taking S_in = fv(p1), but it could also pick a larger set, including streams that could potentially be used in the body, even if they are not. (For example, in the code compiled for {5 : x in &10}, it should also be correct -- though slightly less efficient -- to include integer the stream corresponding to x in the import list, just as if the body had been 5+0*x.) This may become important when extending the language with functions, because in {f(x) : x in &10}, it may turn out, on unfolding f, that it doesn't actually use its argument, so the set of free variables would effectively change by the unfolding, potentially leaving the WithCtrl ill-formed. I don't think any of the proofs rely on having S_in = fv(p1), so a subset inclusion should be fine.
Just to be on the safe side, I suggest that you also write out the proof of Lemma 2.2, which is used in the key case of Lemma 2.4. It should be quite easy to show with the new P-X-Termi rule.
In the "symmetric" subcase on p.10, don't you also need a symmetric version of Lemma 2,3? Maybe there's a generalization of that lemma that would cover both cases? Perhaps write out the proof (if only on paper, for now), to see exactly what assumptions you need.
In the translation of let-expressions on p.12, you still use the general ";" between programs, even though that's no longer in the target language. I think you'll need to define p1++p2 in the obvious way, and use that in the translation. That will also require an adjustment of the proof case for let-expressions in Theorem 3.1.
In the the proof of the subcase for k=0 on p.17, the notation is a mess. There should be an explicit induction the syntax of tau here.
In the proof of the subcase for k>0, after defining P_1, you should explicitly say that you still need to build P_1'. And therefore, you absolutely cannot use Theorem 2.1 on it a few lines later! Rather, it's actually (3.11) that gives you the required P_1', but I'm not sure the st1 and st2 sets in the "iterated butterfly notation" are properly updated and satisfy the requirements of Lemma 2.4.
(A minor thing, but it's getting a little hard to locate a specific definition, lemma, or theorem in the document, when they all use their own numbering. You should use the same counter for all (easy to do in LaTeX's \newtheorem), so that you have "Definition 1.1", "Lemma 1.2", "Lemma 1.3", "Theorem 1.4", etc.)

(There are a few other, minor presentational/notational issues, but those can easily wait to our next meeting.)

Assuming all of the above works out, I think you can indeed move on to supporting "using", I think in the first instance, it'll be enough to just consider Distr'ing int-typed using-variables, which is all that is allowed in general comprehensions. Once that's properly proved, I don't think it'll be particularly hard to extend to restricted comprehensions and Pack'ing; and so I think it may be better to start looking at function definitions and calls instead, to make sure there are no surprises there.

Most of these make sense. One small thing (but requires many small changes), about the 4th point: We now have changed SVCODE syntax like this:

This represents a program as a flat list of instructions, but I feel not very comfortable with this as it is not as close to our code representation as the first version (with four cases of p) does. For example, now we should formally represent a high-level const 3 in SVCODE as S1 := Const_3(); ε instread of just S1 := Const_3() ?

So if this syntax change is not essential, I would prefer to still use the first version syntax, which handles the sequential instructions separately and gives shorter evaluation rules for P-Xducer, P-Wc-Emp, P-Wc-Nonemp.

I think both approaches will ultimately work; it's just a matter of moving the work around: for each approach, some things will be easier, while others will require slightly more complicated proofs. The main concern is to be consistent, i.e., to pick one definition and stick with it.

That said, I think having arbitrarily tree-shaped sequences of Svcode instructions is both a bit unnatural for a low-level language, and also differs somewhat from what actually happens in the compiler. Note also that it leads to a more involved definition of fv(p1;p2) that also involves dv(), and thus might complicate the proofs for everything involving sequencing.

Maybe a nice middle ground will be to have a separate grammar for single instructions/commands (SDefs, WithCtrls, and later also SCalls), with a corresponding operational-semantics judgement, and also a separate grammar for programs, which would be just flat lists of instructions to be executed sequentially, exactly as in the actual code. That will avoid cluttering all the semantics rules for individual instructions with extra premises for executing the rest of the program, since that will be handled once and for all in the judgment for programs. And concatenating lists of instructions and reasoning about such concatenations should also be quite simple and uniform.

Ginko-X / Streaming_NESL

Proof of lemma 0.3 #26