search

hakaru-dev / hakaru

A probabilistic programming language
BSD 3-Clause "New" or "Revised" License
311 stars 30 forks source link

Failing assertion in Loop due to change in KB #56

Closed yuriy0 closed 7 years ago

yuriy0 commented 7 years ago

The assertion in question is the one removed by 5227a4f. The discussion there would indicate that we don't really understand why this ASSERT fails. Currently the only affect test case is "Conjugacy between rolled Dirichlet and multinomial".

The failing call is

%assert(i =-1,KB:-KB(KB:-Introduce(i,HInt(Bound(`>=`,0),Bound(`<=`,Hakaru:-size(as)-2))),KB:-Constrain(0< Hakaru:-size(as))))

Recent versions of both master and pw_simp return NotAKB for this call, which causes the ASSERT to fail; what used to be returned is 

KB(Constrain(0 <= Hakaru:-size(as)-1), Constrain(0 <= -1), Bound(i, `=`, -1), Introduce(i, HInt(Bound(`>=`, 0), Bound(`<=`, Hakaru:-size(as)-2))), Constrain(0 < Hakaru:-size(as)))

That result doesn't look correct to me; clearly i = -1 and i >= 0 is false. If Loop was relying on getting that result, both Loop and KB were bugged. If this result is actually correct, then one or multiple changes made to KB were incorrect (if this is the case, I need to understand why this result is correct).

yuriy0 commented 7 years ago

This was fixed at some point before a681439. The offending call now evaluates to the correct result; and this test case no longer ends up manipulating precisely that expression (i.e. trying to build that KB), so the ASSERT does not fail (perhaps the correctly-generated NotAKB is handled by something further up; the details aren't clear).