formalization of Statistics

[gusl]

Yesterday, 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 fail
ev_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?

Comments

[gustavolacerda.livejournal.com]

comment