Define integral: $\mathcal{C}(X) \rightarrow \mathbb{R}$ to be a functional $f \mapsto \int_X f d\mu$ with a Borel probability measure $\mu$. Then, the usual Riemann integral on [0,1] is an integral on [0,1] with the Borel probability measure on the real line. This integral on [0,1] is known to be computable, and its complexity was analyzed. After that, more generally it is known that, on some spaces, an integral is computable if and only if its corresponding measure is computable. Consequently, to actually compute natural integrals on spaces, one should compute natural measures. Arguably, Haar measures can be seen as natural measures. This is because Haar's theorem states that for any compact topological group, there exists a unique Haar probability measure which is translation-invariant and regular. Thus, to compute natural integrals, we consider Haar measures to be natural and prove that these measures are computable. Another motivation to prove computability of Haar measures is that proving that Haar measures are computable can be interpreted as proving a computable version of Haar's theorem. In this paper, we prove that Haar integrals (integrals with their Haar measures) are computable under computable version of assumptions of Haar's theorem. Moreover, we prove computability, analyze complexity, and implement the Haar integral on arguably the most important compact topological group $\mathcal{SO}(3)$.
적분을 보렐 확률 측도 ($\mu$) 들에 대해 어떤 함수를 전체 공간 위의 보렐 확률 측도에 대한 적분값에 대응시키는 범함수 ($f \mapsto \int_X f d\mu$) 로 정의하자. 그러면 [0,1] 위의 리만적분은 [0,1] 위의 실직선의 보렐 확률 측도에 대한 적분이 된다. 이 [0,1] 위의 적분은 계산가능함이 알려져 있으며, 계산 복잡도마저 분석되어있다. 이후의 연구에서, 더 일반적으로 특정 공간들에서는 적분의 계산가능성과 대응하는 측도의 계산가능성이 동치임이 알려졌다. 따라서 공간들에서 실제로 어떤 자연스러운 적분들을 계산하려면, 해당하는 자연스러운 측도들을 계산해야한다. 하 측도는 자연스러운 측도라고 볼 수 있는데, 이는 하 정리가 하 측도는 평행변환불변인 정칙 확률 측도이며, 모든 옹골찬 위상군에 유일하게 존재함을 의미하기 때문이다. 따라서 자연스러운 적분들을 계산하기 위해 우리는 하 측도들을 자연스러운 측도들로 고려하고 이 측도들이 계산가능함을 증명한다. 하 측도의 계산가능성을 증명하려는 또 다른 동기는, 하 측도의 계산가능성을 증명하는 것이 하 정리의 계산적인 형태를 증명하는 것으로도 해석될 수 있기 때문이다. 이 논문에서 우리는 하 적분들 (하 측도들에 대한 적분들) 이 하 정리의 가정의 계산적인 형태를 가정하면 계산가능함을 보인다. 또한, 우리는 가장 중요한 옹골찬 위상군이라 할 수 있는 3차원 특수직교군의 하 적분의 계산가능성을 증명하고, 계산 복잡도를 분석하며, 알고리즘을 구현한다.
