Computing Haar Measures

Authors Arno Pauly , Dongseong Seon, Martin Ziegler

Thumbnail PDF


  • Filesize: 0.71 MB
  • 17 pages

Document Identifiers

Author Details

Arno Pauly
  • Swansea University, UK
Dongseong Seon
  • KAIST, Daejeon, Republic of Korea
Martin Ziegler
  • KAIST, Daejeon, Republic of Korea

Cite AsGet BibTex

Arno Pauly, Dongseong Seon, and Martin Ziegler. Computing Haar Measures. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


According to Haar’s Theorem, every compact topological group G admits a unique (regular, right and) left-invariant Borel probability measure μ_G. Let the Haar integral (of G) denote the functional ∫_G:?(G)∋ f ↦ ∫ f d μ_G integrating any continuous function f:G → ℝ with respect to μ_G. This generalizes, and recovers for the additive group G=[0;1)mod 1, the usual Riemann integral: computable (cmp. Weihrauch 2000, Theorem 6.4.1), and of computational cost characterizing complexity class #P_1 (cmp. Ko 1991, Theorem 5.32). We establish that in fact, every computably compact computable metric group renders the Haar measure/integral computable: once using an elegant synthetic argument, exploiting uniqueness in a computably compact space of probability measures; and once presenting and analyzing an explicit, imperative algorithm based on "maximum packings" with rigorous error bounds and guaranteed convergence. Regarding computational complexity, for the groups SO(3) and SU(2), we reduce the Haar integral to and from Euclidean/Riemann integration. In particular both also characterize #P_1.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Mathematics of computing → Continuous mathematics
  • Computable analysis
  • topological groups
  • exact real arithmetic
  • Haar measure


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Vasco Brattka, Peter Hertling, and Klaus Weihrauch. A Tutorial on Computable Analysis. In S. Barry Cooper, Benedikt Löwe, and Andrea Sorbi, editors, New Computational Paradigms: Changing Conceptions of What is Computable, pages 425-491. Springer, New York, 2008. URL:
  2. Vasco Brattka, Joseph Miller, Stéphane Le Roux, and Arno Pauly. Connected Choice and Brouwer’s Fixed Point Theorem. Journal for Mathematical Logic, 2019. URL:
  3. Franz Brauße, Pieter Collins, Johannes Kanig, SunYoung Kim, Michal Konecny, Gyesik Lee, Norbert Müller, Eike Neumann, Sewon Park, Norbert Preining, and Martin Ziegler. Semantics, Logic, and Verification of "Exact Real Computation". CoRR, abs/1608.05787, 2016. URL:
  4. Pieter Collins. Computable Stochastic Processes. CoRR, abs/1409.4667, 2014. URL:
  5. Abbas Edalat. A computable approach to measure and integration theory. Information and Computation, 207(5):642-659, 2009. URL:
  6. Martín Escardó. Synthetic Topology of Data Types and Classical Spaces. Electronic Notes in Theoretical Computer Science, 87:21-165, 2004. URL:
  7. Martín Escardó. Algorithmic solution of higher type equations. J. Logic Comput., 23(4):839-854, 2013. URL:
  8. Hugo Férée and Martin Ziegler. On the Computational Complexity of Positive Linear Functionals on C[0;1]. In Mathematical Aspects of Computer and Information Sciences - 6th International Conference, MACIS 2015, Berlin, Germany, November 11-13, 2015, Revised Selected Papers, pages 489-504, 2015. URL:
  9. Stefano Galatolo, Mathieu Hoyrup, and Cristobal Rojas. Dynamics and abstract computability: computing invariant measures. Discrete Contin. Dyn. Syst., 29(1):193-212, 2011. URL:
  10. Xiaolin Ge and Anil Nerode. On extreme points of convex compact Turing located set. In Anil Nerode and Yu. V. Matiyasevich, editors, Logical Foundations of Computer Science, pages 114-128, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg. Google Scholar
  11. Paul R. Halmos. Measure Theory, volume 018 of GTM. Springer, 1950. URL:
  12. Akitoshi Kawamura and Stephen A. Cook. Complexity Theory for Operators in Analysis. TOCT, 4(2):5:1-5:24, 2012. URL:
  13. Akitoshi Kawamura, Florian Steinberg, and Martin Ziegler. Complexity Theory of (Functions on) Compact Metric Spaces. In Proc. 31st Ann. Symposium on Logic in Computer Science, LICS, pages 837-846. ACM, 2016. URL:
  14. Ker-I Ko. Complexity Theory of Real Functions. Progress in Theoretical Computer Science. Birkhäuser, Boston, 1991. URL:
  15. Ulrich Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer, Berlin, 2008. URL:
  16. A.N. Kolmogorov and V.M. Tikhomirov. ℰ-Entropy and ℰ-Capacity of Sets in Functional Spaces. Uspekhi Mat. Nauk, 14(2):3-86, 1959. URL:
  17. Davorin Lešnik. Haar Measure in Synthetic Topology. presentation at CCC 2019, 2019. Google Scholar
  18. Norbert Th. Müller. The iRRAM: Exact Arithmetic in C++. In Jens Blanck, Vasco Brattka, and Peter Hertling, editors, Computability and Complexity in Analysis, volume 2064 of Lecture Notes in Computer Science, pages 222-252, Berlin, 2001. Springer. 4th International Workshop, CCA 2000, Swansea, UK, September 2000. URL:
  19. Vladimir P. Orevkov. A constructive mapping of the square onto itself displacing every constructive point (Russian). Doklady Akademii Nauk, 152:55-58, 1963. translated in: Soviet Math. - Dokl., 4 (1963) 1253-1256. Google Scholar
  20. Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994. Google Scholar
  21. Arno Pauly. On the topological aspects of the theory of represented spaces. Computability, 5(2):159-180, 2016. URL:
  22. Arno Pauly. Bi-invariant metrics on compact Polish group. MathOverflow, February 2019. URL:
  23. Arno Pauly. Effective local compactness and the hyperspace of located sets. CoRR, abs/1903.05490, 2019. URL:
  24. Arno Pauly and Willem Fouché. How constructive is constructing measures? Journal of Logic & Analysis, 9, 2017. URL:
  25. Arno Pauly and Hideki Tsuiki. T^ω-representations of compact sets. CoRR, abs/1604.00258, 2016. URL:
  26. Florian Pausinger. Uniformly distributed sequences in the orthogonal group and on the Grassmannian manifold. Mathematics and Computers in Simulation, 160:13-22, 2019. URL:
  27. Marian B. Pour-El and J. Ian Richards. A computable ordinary differential equation which possesses no computable solution. Annals Math. Logic, 17:61-90, 1979. URL:
  28. William H Press. Numerical recipes: The art of scientific computing. Cambridge university press, 2007. Google Scholar
  29. Matthias Schröder. Admissible Representations in Computable Analysis. In A. Beckmann, U. Berger, B. Löwe, and J.V. Tucker, editors, Logical Approaches to Computational Barriers, volume 3988 of Lecture Notes in Computer Science, pages 471-480, Berlin, 2006. Springer. Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006. URL:
  30. Matthias Schröder and Alex Simpson. Representing probability measures using probabilistic processes. Journal of Complexity, 22(6):768-782, 2006. URL:
  31. Ernst Specker. Nicht konstruktiv beweisbare Sätze der Analysis. The Journal of Symbolic Logic, 14(3):145-158, 1949. URL:
  32. Ernst Specker. Der Satz vom Maximum in der rekursiven Analysis. In A. Heyting, editor, Constructivity in mathematics, Studies in Logic and the Foundations of Mathematics, pages 254-265, Amsterdam, 1959. North-Holland. Proc. Colloq., Amsterdam, Aug. 26-31, 1957. URL:
  33. Florian Steinberg. Complexity theory for spaces of integrable functions. Logical Methods in Computer Science, Volume 13, Issue 3, September 2017. URL:
  34. Klaus Weihrauch. Computability on computable metric spaces. Theoretical Computer Science, 113:191-210, 1993. Fundamental Study. URL:
  35. Klaus Weihrauch. Computable Analysis. Springer, Berlin, 2000. URL:
  36. Klaus Weihrauch. Computational complexity on computable metric spaces. Mathematical Logic Quarterly, 49(1):3-21, 2003. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail