A computable approach to measure and integration theory

We introduce a computable framework for Lebesgue’s measure and integration theory in the spirit of domain theory. For an effectively given second countable locally compact Hausdorff space and an effectively given finite Borel measure on the space, we define a recursive measurable set, which extends the corresponding notion due to S˜anin for the Lebesgue measure on the real line. We also introduce the stronger notion of a computable measurable set, where a measurable set is approximated from inside and outside by sequences of closed and open subsets, respectively. The more refined property of computable measurable sets give rise to the idea of partial measurable subsets, which naturally form a domain for measurable subsets. We then introduce interval-valued measurable functions and develop the notion of recursive and computable measurable functions using interval-valued simple functions. This leads us to the interval versions of the main results in classical measure theory. The Lebesgue integral is shown to be a continuous operator on the domain of interval-valued measurable functions and the interval-valued Lebesgue integral provides a computable framework for integration.