formalization of Statistics
Oct. 11th, 2008 02:15 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslYesterday, ![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
chrisamaphone translated my type declarations & derivation for a confusing piece of notation in Statistics, namely regarding the meaning of E(E(X|Y)). She did this in Twelf, and improved upon my formalization, showing that only one type for 'expectedValue' is needed.
It is here.
I just checked it online with Twelf Live.
While syntactic type-checking is already useful by itself, I'd also like to plug-in actual distributions, and compute expected values. Naive numerical integration would be fine. It would be super-cool to be able to do symbolic integrations too, even if only for a small class of pdfs. More importantly, I'd want to express this distinction in the type system.
Remember: EV = expected value; RV = random variable
The above refers to the ideal, Platonic function. We will not implement it. In reality, we want to implement functions like:
or
The above type specifications are redundant, since it is clear that they are all attempting to compute
I want the type system to express:
* function f is an attempt to (approximately) compute function g, e.g. using a relation like
* the output of f (in case it succeeds) is an approximation to the output of g, i.e. something like
Any ideas?
chrisamaphone translated my type declarations & derivation for a confusing piece of notation in Statistics, namely regarding the meaning of E(E(X|Y)). She did this in Twelf, and improved upon my formalization, showing that only one type for 'expectedValue' is needed.It is here.
I just checked it online with Twelf Live.
While syntactic type-checking is already useful by itself, I'd also like to plug-in actual distributions, and compute expected values. Naive numerical integration would be fine. It would be super-cool to be able to do symbolic integrations too, even if only for a small class of pdfs. More importantly, I'd want to express this distinction in the type system.
Remember: EV = expected value; RV = random variable
ev : rv -> real.The above refers to the ideal, Platonic function. We will not implement it. In reality, we want to implement functions like:
ev_symbolic : rv -> real. #might failev_numeric_riemann : rv -> real. or
ev_numeric : numeric_integration_method -> rv -> real.The above type specifications are redundant, since it is clear that they are all attempting to compute
ev.I want the type system to express:
* function f is an attempt to (approximately) compute function g, e.g. using a relation like
approximates(f, g).?* the output of f (in case it succeeds) is an approximation to the output of g, i.e. something like
approximates(f X, g X).Any ideas?