Is it the case that values *must* relates to an input?

[aubertc]

The issue on declarations echoed with a more fundamental question that I have, and that is "must values inside the program relates to an input?".

Let me explain: as of now, we are interpreting x = <any value>; as "reset the coefficient for x to 0", because there is now no connection between the inputs and x.
However, I'm not sure that this is permitted, for three reasons:

• There is no rule for that case in the original paper, and as far as I can tell it's not even discussed,
• In On Decidable Growth-Rate Properties of Imperative Programs, Ben-Amram "just" works on adding a "reset" instruction to a similar language and shows that it is not easy to do so,
• When discussing constants, they write:

To deal with constants, just replace the program’s constants by variables and regard the replaced constants as input to these variables.

as if (my reading), values had to be linked to the program's input.

All of that being said, they have an example of re-initialization (Example 3.1)

C′′ ≡ X1 := 1; loop X 2 { X1 := X1 +X1 }

as if it was no big deal.

I may simply be confused. Thoughts?

[aubertc]

Closed during discussion on sept. 6th.
Essentially, "internal variables" that are not related to input have no impact on the main theorem, they can be assimilated to constant overhead as they do not grow with the input.

[seiller]

We need to reconsider constants. Here are two examples of programs:

int x=1000;
compute x=x!;
y=x*y;
for x: do y=y+1

int x=1000!;
y=x*y;
for x: do y=y+1

Intuitively both programs should be analysed the same because the value in x is a constant. This means we have to analyse the internal variables, not writing zeroes for constants because it may cancel interesting values (I put the y=x*y; lines for this, but maybe this needs to be tweaked), and removing possibly infinite value because they do not impact the dependency to inputs.

In the end, I would suggest translating declarations "int x;" as x <--m -- x (identity on x, just acknowledging its existence), and dealing with assignments to constants separately. If we do this in a naive way we would like to interpret "x=1000;" as a reinitialisation of x (i.e. remove all previous dependencies, and add an "m" dependency of x on itself) but this is not done by a matrix multiplication. One complex way is to consider each constant as a separate inner variable (one that we do not care about at the end), in which case "x=1000;" becomes x <-- m -- 1000 which does the job. But this may introduce many variables. The last resort is having a single variable "cst" used for all constants in the program. Then "x=1000;" becomes "x <-- m -- cst" and the following "y=2345;" becomes "y <-- m -- cst", etc. I am guessing this should be enough.

Lastly, one the matrix with all variables (i.e. inner / outer / accounting for constants) is computed, we search for non-infinite values only concerned with output/input variables. Here again we should be careful. We do not care that the output "z" depends superpolynomially on "cst" because it is a constant. But we care if an inner variable "x" depends superpolynomially on an input (!), even if it is not part of the output. So the condition should probably be: "no variables (inner / outer / constants even if this latter case cannot arise because constants are not on the left-hand side of assignments) depends on inputs with an "i" coefficient. (We could potentially also allow internal variable to be super-polynomially dependent on inputs, but this would not be coherent with what we decided for the value of 0 times infinity.)
This restriction implies an adaptation of the construction of the delta_graph (we should only add to the delta_graph those monomials for which an infinite coefficient appears for a dependency on an input of the program).

[seiller]

I commented without reopening; cf. above.