Teach KB about properties that hold of every element of an array

[ccshan]

See comments at 0a82647#commitcomment-21844243

As discussed there, one goal is to get

with(Hakaru): with(KB):
w, kb := genType(w, HArray(HInt(Bound(`>=`,0))), empty);
simplify_assuming(piecewise(idx(w,0)<0,a,b), kb);

to produce b

[ccshan]

(Similarly, replacing the first argument to simplify_assuming above with ceil(idx(w,0)) or floor(idx(w,0)) should produce just idx(w,0).)

[yuriy0]

As of 757562a:

> with(KB): with(Hakaru):
> w, kb := genType(w, HArray(HInt(Bound(`>=`,0))), empty):
> map(x->simplify_assuming(x, kb), [piecewise(idx(w,0)<0,a,b), ceil(idx(w,0)), floor(idx(w,0))]);
                                          [b, Hakaru:-idx(w, 0), Hakaru:-idx(w, 0)]
> simplify_assuming( piecewise(And(Not(idx(w,i)<0),r<t),a,b), kb );
                                                    { a          r < t
                                                    {
                                                    { b        otherwise

The last example is like the one in naive_bayes_gibbs.hk which originally triggered the creation of this issue; I haven't gotten around to making sure it works just as well in that case, but it seems like it would.

---

After investigating this briefly a while ago, and in more detail recently, I've come to believe that we can't do much better than to "add assumptions on the fly for those elements of w that are mentioned".

The issue with giving the needed knowledge to the assum{e/ing} facility is that, at the end of the day, after all of the simplification of properties/types (i.e. cleverness) done by Maple inside of assum{e/ing}, it will just save the assumed property of a particular term in a global table - namely property/object - and later delete it from that table when evaluation leaves the scope of assuming. We would have to eventually have an entry for every mentioned element of an array, even if that entry is derived from an entry for the name of the array itself (or alternatively, rewrite the entire mechanism ourselves somehow - ha!).

[JacquesCarette]

Nice. But there could be a third alternative: there are ways to 'teach' assum{e/ing} about properties of certain functions. So we could add handlers for size and idx, which could go a long way.

[ccshan]

I just confirmed that naive_bayes_gibbs.hk is now simplified better as desired. (For future reference, here's how I confirmed it:

git clone github.com:hakaru-dev/tcp.git
cd tcp
make -B src/NaiveBayes/naive_bayes_simp.hk
git diff --color-words src/NaiveBayes/naive_bayes_simp.hk

then compare and rejoice.) Unfortunately sum(piecewise(i丣严=docUpdate,0,1),i丣严=0..size(z)-1) didn't simplify to size(z)-1.

I also agree that the "third alternative" that @JacquesCarette pointed out is worth trying.

[yuriy0]

there are ways to 'teach' assum{e/ing} about properties of certain functions

I also agree that the "third alternative" that @JacquesCarette pointed out is worth trying.

These are the types of things I tried, in various ways. The only relevant documentation I found was here, but I couldn't even get that example to do anything (it seems a bit outdated). Other than that, I tried overloading various type-related functions; the success of that varied from 'does nothing' and 'breaks everything'.

If there is a particular mechanism of which you're aware that could help accomplish this, I'd very much like to know about it!

[JacquesCarette]

These extension mechanism are all undocumented. I just happen to know them from reading the source. They mainly involve writing property/ routines (for idx and/or size).

[JacquesCarette]

So should a new issue be made, or this one re-opened?

[yuriy0]

So should a new issue be made, or this one re-opened?

I think we need a new issue, which details:

• why the current solution is insufficient (besides being "ugly") - basically, if it isn't broken, there's no need to fix it
• how to access the "extension mechanism[s]" which "are all undocumented" which may be useful here (at least, which property/*/{idx/size} functions need to be defined, and where they are called)

I stumbled upon some propety/ routines that I though could be overloaded (basically by spotting uses of cat) but none of those worked out.

The mechanism by which we do this for idx or size may be entirely different; there is one size per HArray, but an entire parametric family for idx per HArray, so perhaps two issues are needed.

[JacquesCarette]

As a short-cut, I'll reopen this issue. Creating good issues that detail the above will take me a non-trivial amount of time. And I am not sure that this is the most-pressing issue.

For example, we don't want a property/idx, because idx is not (and should not be) a property. However, we will want to add new properties of 'containers', and some processing of these that would allow us to deduce properties of the elements of the containers. I think that coaxing assume to do this is possible, I believe. But it may require a little bit of surgery to get the dispatch done in the right places at the right time (inside assume).

[yuriy0]

Creating good issues that detail the above will take me a non-trivial amount of time. And I am not sure that this is the most-pressing issue.

Both very true statements.

we will want to add new properties of 'containers'

This seems to be stupidly easy; e.g. assume (w :: EveryElement(nonnegint)) works, where EveryElement is an unbound name (or, properties are actually just unbound globals).

some processing of these that would allow us to deduce properties of the elements of the containers

This is almost certainly the hard part. Giving a semantics to w :: EveryElement which allows us to derive facts about idx(w,..) doesn't seem to be the intended purpose of the assume facility. e :: t is a statement about e and only e.

Of course, there may be a different way of simply stating the fact we want that differs from the above, and makes the assume facility more amenable to be bent to our will. Perhaps a typing judgement is not the correct way to go, and we need something like assume(EveryElement(w, nonnegint)); but the former seems most obvious to me, and I couldn't get assume to even accept the latter as a valid property.

[JacquesCarette]

assume (w :: EveryElement(nonnegint)) would indeed be the way to tell assume about such information. Then the task is to figure out where in the flow of assume we can have idx(w,j) report having property nonnegint.

We can add new properties easily enough. I don't remember quite how (I think it's as simple as creating a property/foo routine). Getting them to "do the right thing" is harder. But definitely feasible.

Actually, there's an addproperty function. See also the ?assume,parametric help page.