Error in KB:-assert_deny:-rel_coulditbe

[yuriy0]

This error is found by hk-maple examples/gmm_gibbs.hk. Strangely, the follow call from the Maple test suite doesn't cause it:

(gmm_gibbs, gmm_gibbs_t) := Concrete("examples/gmm_gibbs.hk"):
gmm_gibbs := value(eval(gmm_gibbs)):
TestEfficient( gmm_gibbs, gmm_gibbs_t, KB:-empty, label="gmm gibbs" ):

The bottom of the stack causing the error is

KB:-assert_deny:-rel_coulditbe(0 <= Hakaru:-size(as)-1, 
   [i = Hakaru:-size[as]-1, Hakaru:-size[z] = Hakaru:-size[t], 
    docUpdate::integer, 0 <= docUpdate, docUpdate <= Hakaru:-size[z]-1, 
    t::TopProp, z::TopProp, as::TopProp, (Hakaru:-size[as])::nonnegint, 
    (Hakaru:-size[t])::nonnegint, (Hakaru:-size[z])::nonnegint])

The callstack is fromLO:59 -> unproducts:146 -> unproduct:204 -> assert_deny:563 -> rel_coulditbe.

[yuriy0]

The only difference between the test suite call is the call to value(eval(..)); this makes a Product into a product. I'm still not sure what happens to produce the error. There are multiple errors; even if the one in rel_coulditbe is avoided (which was caused by 5d6897a, a very much necessary change) there is another error in unproduct:

Error, (in Loop:-unproduct) invalid input: wrap expects its 4th argument, kb1,
to be of type t_kb, but received NotAKB()

For the time being, I've put in a quick fix, but I don't consider this closed (this is basically the same issue as #88 - the exact details of that one are also unclear).

[ccshan]

I understand the "quick fix" to be relaxing the condition under which the Maple simplifier allows the inert Product in the Hakaru input to become the reactive product. Before the fix, Product would become product only if it would immediately evaluate away. Now certain products would be allowed to stick around (namely those that involve idx or size). Is my understanding correct? Is the drawback to letting product stick around merely slower performance? I guess this is basically the same issue as #88 indeed.

[yuriy0]

Before the fix, Product would become product only if it would immediately evaluate away. Now certain products would be allowed to stick around (namely those that involve idx or size). Is my understanding correct?

Yes

Is the drawback to letting product stick around merely slower performance?

That is one drawback; another is that Product vs. product and Sum vs. sum cause different code paths to be taken for the 'same' program. Sometimes the different code path makes the program simplify differently (as in #88); sometimes it makes simplification crash (as in this issue).

Sometimes we need the inert version to avoid a crash, and sometimes we need a non-inert version. Things are further complicated by the fact that these issues only occur with very large programs (there is no minimal example triggering the issue); by the fact that, in those programs, the code paths begin to diverge very deep down in the simplification; and for this case, simplification (i.e. reduce) is not where the error happens (which is only a complication because I am much less familiar with e.g. fromLO and toLO than I am with reduce)

[JacquesCarette]

t::TopProp, z::TopProp, as::TopProp worry me a little. I guess we know these are some kind of array (which I think can be said to Maple).

One possibility comes to mind: instead of size[z], we could encode these as size/z (i.e. as a symbol instead of an indexed name). That might actually help, as Maple's handling of indexed names isn't as good as one would hople.

This is somewhat orthogonal to product vs Product; but it might be an aggravating factor.

[yuriy0]

t::TopProp, z::TopProp, as::TopProp worry me a little. I guess we know these are some kind of array (which I think can be said to Maple).

Those are indeed the type generated by the array types. But the correct assumption is present - (Hakaru:-size[as])::nonnegint. I think the actual problem is the fact that 0 <= Hakaru:-size(as)-1 is not chilled. When the chilled version is passed instead, it gives the correct result. Why that's related to product vs. Product, I'm not sure.

One possibility comes to mind: instead of size[z], we could encode these as size/z (i.e. as a symbol instead of an indexed name).

There seem to be Maple functions which do that - freeze and thaw. I tried replacing chill and warm with those a while back, but it seemed to break things. Maybe it's worth revisiting.

[JacquesCarette]

The reason to use size[z] (and companions) is that depends(size[z],z) is still true. If you go to size/z, then that now is false -- and that breaks things, badly.

What is needed is one method to deal with things like size(z) when dependencies matter (which I think chill/warm are probably best), and potentially another when they don't (where freeze/thaw might actually work better.)

[yuriy0]

The reason to use size[z] (and companions) is that depends(size[z],z) is still true. If you go to size/z, then that now is false -- and that breaks things, badly.

That makes sense.

What is needed is one method to deal with things like size(z) when dependencies matter (which I think chill/warm are probably best), and potentially another when they don't (where freeze/thaw might actually work better.)

A potential solution is to override depends to look at names of the form freeze/* (which are generated by freeze) and to perform the appropriate depends check if that name thaws to an idx or size (assuming we won't freeze any other things).

Actually verifying that a particular Maple function doesn't somehow use depends seems very hard (least of all because it requires examining the source code). For example, even if the arguement to is doesn't contain any binding forms (which we could check), it may use depends to check upon which assumptions its argument depends. Or it may use a multitude of other functions to achieve the same thing (indets, has) or some other method that is so esoteric that it can't be easily recognized.

[JacquesCarette]

Right - most of the time, we have to assume that the dependency structure matters. Only in purely algebraic contexts (like SemiAlgebraic) is it clear that this doesn't matter.

There is another heuristic we can use: the only time dependency really matters is when we have binding-like things (sum, int, product, diff and their inert versions) around.