Loop synthesis: more declarative than functional programming?

As part of the FTL language, I've been playing with the idea of declarative loops. For example, I'd like to write:

for i in range(0, n):
b[i + 1] = g(a[i]);
a[i - 1] = f(b[i - 4]);

First, the synthesizer should figure out that the problem is under-constrained. It should report that the following values are undefined:

a[0..2] = ??
b[0] = ??
a[n] = ??

If, as suggested by the synthesizer, I refined the program to be consistent:

a[0..2] = 0
b[0] = 0
a[n] = 0
for i in range(0, n):
b[i + 1] = g(a[i]);
a[i - 1] = f(b[i - 4]);

I'd like to get:

a[0] = 0
a[1] = 0
a[2] = 0
b[0] = 0
b[1] = g(a[0])
b[2] = g(a[1])
b[3] = g(a[2])
for (int i = 3; i < n - 1; i++) {
a[i] = f(b[i - 3]);
b[i + 1] = g(a[i])
a[n] = 0

Note that the synthesizer performed loop peeling -- it figured out to do loop peeling to emit assignments for b[1], b[2], and b[3]. Furthermore, it reordered the assignments in the loop and performed loop skewing -- it changed the indices of the assignments, such as from a[i - 1] to a[i], to ensure an array value is written before it is read.

Milind and I just worked out most of the theory for this today. You can think of it as a generalization of attribute grammar synthesis to loop code. Basically, if we assume the input code is singly assigned -- array values should have one unique value -- this is a matter of unrolling the intermediate steps of the loop, scheduling their dependency graph, and reconstructing the Von Neumann-friendly loop. The weekend may be busy :)

A fun question is whether a functional program could declaratively handle the above. For example, it could expand the for loop into a dependency graph and then use demand-driven evaluation. However, there are two problems. First, the interpretation of indices would have to change: my code correctly skewed the loop indices to make sure "a[i - 1]" and "b[i - 4]" are never negative. Second, the loop would be unsafe: in my approach, the synthesizer can statically check that the array is fully defined. Either way, traditional functional languages force programmers to explicitly handle these (arguably) low-level loop details. Go synthesis!