search

hakaru-dev / hakaru

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

F to chiSq tests (base case and general) #196

Closed mkhattab940 closed 6 years ago

mkhattab940 commented 6 years ago

These tests have an interesting failure:

### Error in:   0:RoundTrip:0:3:t_F_to_chiSq_base:1
MapleException:
product:   "Cannot show that 1/2*2^(1/2)/Pi^(1/2)*exp(-1/2*Hakaru:-idx(q3,_)^2) is continuous on [0,infinity]"
_Inert_FUNCTION(_Inert_NAME("Weight"),_Inert_EXPSEQ(_Inert_NAME("undefined"),_Inert_FUNCTION(_Inert_NAME("Bind"),_Inert_EXPSEQ(_Inert_FUNCTION(_Inert_NAME("Lebesgue"),_Inert_EXPSEQ(_Inert_PROD(_Inert_NAME("infinity"),_Inert_INTNEG(1)),_Inert_NAME("infinity"))),_Inert_NAME("q507"),_Inert_FUNCTION(_Inert_NAME("Bind"),_Inert_EXPSEQ(_Inert_FUNCTION(_Inert_NAME("Plate"),_Inert_EXPSEQ(_Inert_NAME("infinity"),_Inert_NAME("_"),_Inert_FUNCTION(_Inert_NAME("Lebesgue"),_Inert_EXPSEQ(_Inert_PROD(_Inert_NAME("infinity"),_Inert_INTNEG(1)),_Inert_NAME("infinity"))))),_Inert_NAME("q3"),_Inert_FUNCTION(_Inert_NAME("Ret"),_Inert_EXPSEQ(_Inert_PROD(_Inert_POWER(_Inert_NAME("q507"),_Inert_INTPOS(2)),_Inert_NAME("infinity"),_Inert_POWER(_Inert_FUNCTION(_Inert_NAME("SumIE"),_Inert_EXPSEQ(_Inert_POWER(_Inert_FUNCTION(_Inert_ASSIGNEDLOCALNAME("idx","PROC",18446883770603012926),_Inert_EXPSEQ(_Inert_NAME("q3"),_Inert_NAME("i"))),_Inert_INTPOS(2)),_Inert_EQUATION(_Inert_NAME("i"),_Inert_RANGE(_Inert_INTPOS(0),_Inert_NAME("infinity"))))),_Inert_INTNEG(1)))))))))))

after sending to Maple:
use Hakaru, NewSLO in timelimit(90, RoundTrip(eval(eval(eval(app(app(`F`, 1), infinity), `F`=(lam(`n1`, HInt(Bound(`>=`,0)), lam(`n2`, HInt(Bound(`>=`,0)), Bind(app(`stdChiSq`, `n1`), `X1`, Bind(app(`stdChiSq`, `n2`), `X2`, Ret((`X1` * `n2` * 1/((`X2` * `n1`)))))))))), `stdChiSq`=(lam(`n`, HInt(Bound(`>=`,0)), app(app(app(`chiSq_iid`, `n`), 0), 1)))), `chiSq_iid`=(lam(`n`, HInt(Bound(`>=`,0)), lam(`mean`, HReal(), lam(`stdev`, HReal(Bound(`>=`,0)), Bind(Plate(`n`, `_`, Gaussian(`mean`, `stdev`)), `q`, Ret(Sum((((idx(`q`, `i`) + (-(`mean`))) * 1/(`stdev`)) ^ 2), `i`=0..(size(`q`))-1)))))))), HMeasure(HReal()), _command=Simplify)) end use;
Cases: 10  Tried: 8  Errors: 1  Failures: 5
Cases: 10  Tried: 9  Errors: 1  Failures: 5

### Error in:   0:RoundTrip:0:4:t_F_to_chiSq_general:1
MapleException:
product:   "Cannot show that 1/2*2^(1/2)/Pi^(1/2)*exp(-1/2*Hakaru:-idx(q5,_)^2) is continuous on [0,infinity]"
_Inert_FUNCTION(_Inert_NAME("lam"),_Inert_EXPSEQ(_Inert_NAME("v1"),_Inert_FUNCTION(_Inert_NAME("HInt"),_Inert_EXPSEQ(_Inert_FUNCTION(_Inert_NAME("Bound"),_Inert_EXPSEQ(_Inert_ASSIGNEDNAME(">=","PROC"),_Inert_INTPOS(0))))),_Inert_FUNCTION(_Inert_NAME("Weight"),_Inert_EXPSEQ(_Inert_NAME("undefined"),_Inert_FUNCTION(_Inert_NAME("Bind"),_Inert_EXPSEQ(_Inert_FUNCTION(_Inert_NAME("Plate"),_Inert_EXPSEQ(_Inert_NAME("v1"),_Inert_NAME("_"),_Inert_FUNCTION(_Inert_NAME("Gaussian"),_Inert_EXPSEQ(_Inert_INTPOS(0),_Inert_INTPOS(1))))),_Inert_NAME("q7"),_Inert_FUNCTION(_Inert_NAME("Bind"),_Inert_EXPSEQ(_Inert_FUNCTION(_Inert_NAME("Plate"),_Inert_EXPSEQ(_Inert_NAME("infinity"),_Inert_NAME("_"),_Inert_FUNCTION(_Inert_NAME("Lebesgue"),_Inert_EXPSEQ(_Inert_PROD(_Inert_NAME("infinity"),_Inert_INTNEG(1)),_Inert_NAME("infinity"))))),_Inert_NAME("q5"),_Inert_FUNCTION(_Inert_NAME("Ret"),_Inert_EXPSEQ(_Inert_PROD(_Inert_FUNCTION(_Inert_NAME("SumIE"),_Inert_EXPSEQ(_Inert_POWER(_Inert_FUNCTION(_Inert_ASSIGNEDLOCALNAME("idx","PROC",18446884132473680830),_Inert_EXPSEQ(_Inert_NAME("q7"),_Inert_NAME("i"))),_Inert_INTPOS(2)),_Inert_EQUATION(_Inert_NAME("i"),_Inert_RANGE(_Inert_INTPOS(0),_Inert_NAME("v1"))))),_Inert_NAME("infinity"),_Inert_POWER(_Inert_FUNCTION(_Inert_NAME("SumIE"),_Inert_EXPSEQ(_Inert_POWER(_Inert_FUNCTION(_Inert_ASSIGNEDLOCALNAME("idx","PROC",18446884132473680830),_Inert_EXPSEQ(_Inert_NAME("q5"),_Inert_NAME("i"))),_Inert_INTPOS(2)),_Inert_EQUATION(_Inert_NAME("i"),_Inert_RANGE(_Inert_INTPOS(0),_Inert_NAME("infinity"))))),_Inert_INTNEG(1)))))))))))))

after sending to Maple:
use Hakaru, NewSLO in timelimit(90, RoundTrip(eval(eval(eval(lam(`v1`, HInt(Bound(`>=`,0)), Bind(app(app(`F`, `v1`), infinity), `Y`, Ret((`Y` * `v1`)))), `F`=(lam(`n1`, HInt(Bound(`>=`,0)), lam(`n2`, HInt(Bound(`>=`,0)), Bind(app(`stdChiSq`, `n1`), `X1`, Bind(app(`stdChiSq`, `n2`), `X2`, Ret((`X1` * `n2` * 1/((`X2` * `n1`)))))))))), `stdChiSq`=(lam(`n`, HInt(Bound(`>=`,0)), app(app(app(`chiSq_iid`, `n`), 0), 1)))), `chiSq_iid`=(lam(`n`, HInt(Bound(`>=`,0)), lam(`mean`, HReal(), lam(`stdev`, HReal(Bound(`>=`,0)), Bind(Plate(`n`, `_`, Gaussian(`mean`, `stdev`)), `q`, Ret(Sum((((idx(`q`, `i`) + (-(`mean`))) * 1/(`stdev`)) ^ 2), `i`=0..(size(`q`))-1)))))))), HFunction(HInt(Bound(`>=`,0)), HMeasure(HReal())), _command=Simplify)) end use;
Cases: 10  Tried: 10  Errors: 2  Failures: 5
JacquesCarette commented 6 years ago

That is a very interesting error! I wonder what variable it is attempting to use as the one to check continuity.