Point-free measure theory using valuations

12 October 2011
Steve Vickers
<p>In topos-valid point-free topology there is a good analogue of regular measures and associated measure theoretic concepts including integration. It is expressed in terms of valuations, essentially measures restricted to the opens. A valuation $m$ is $0$ on the empty set and Scott continuous, as well as satisfying the modular law $$ m(U \cup V) + m(U \cap V) = m(U) + m(V). $$</p>\\ <p>Of course, that begs the question of why one would want to work with topos-valid point-free topology, but I'll give some general justification regarding fibrewise topology of bundles and a more specific example from recent topos work on quantum foundations.</p>\\ <p>The focus of the talk is the valuation locale, an analogue of hyperspaces: if $X$ is a point-free space (locale) then its valuation locale $VX$ is a point-free space whose points are the valuations on $X$. It was developed by Heckmann, by Coquand and Spitters, and by myself out of the probabilistic powerdomain of Jones and Plotkin.</p>\\ <p>I shall discuss the following results, proved in a draft paper "A monad of valuation locales" available at <a href="http://www.cs.bham.ac.uk/~sjv/Riesz.pdf">http://www.cs.bham.ac.uk/~sjv/Riesz.pdf</a>:<ul> <li> V is a strong monad, analogous to the Giry monad of measure theory.</li> <li> There is a Riesz theorem that valuations are equivalent to linear functionals on real-valued maps.</li> <li> The monad is commutative: this is a categorical way of saying that product valuations exist and there is a Fubini theorem.</li> </ul></p>\\ <p>The technical core is an analysis of simple maps to the reals. They can be used to approximate more general maps, and provide a means to reducing the calculations to finitary algebra. In particular the free commutative monoid $M(L)$ over a distributive lattice $L$, subject to certain relations including ones deriving from the modular law, can be got as a tensor product in a semilattice sense of $L$ with the natural numbers. It also satisfies the Principle of Inclusion and Exclusion (in a form presented without subtraction).</p>
  • Analytic Topology in Mathematics and Computer Science