1
$\begingroup$

It's well known in Type 2 Effectivity that integration over a compact interval is computable. So what about integration over an open interval? What rigorous computability results exist?

My thoughts were that, morally, that should also be computable to some degree. The reason is because it seems that it's often easy to apply a Direct Comparison Test or a Dirichlet Test and then conclude convergence from that. For instance, the integral $\Gamma(4)=\int_{0}^\infty x^3 e^{-x}\,dx$ can easily be compared to the convergent integral $\int_{0}^\infty \frac{dx}{1+x^2} = \pi/2$ which dominates it in the tails. The thing about convergence tests in general is that they are constructive, so they actually provide a way of numerically evaluating such integrals and series.

A possible approach to automatically computing $\int_{0}^\infty f(x)\,dx$ would be to figure out a $g(x)$ such that $f(x) \in O(g(x))$ and $\int_{0}^\infty g(x)\,dx$ exists.

Additionally, there are sets of function like the Schwartz functions that look especially "integrable". Maybe these are the functions for which integration can be done efficiently.

$\endgroup$
7
  • $\begingroup$ I guess you mean the Riemann integral on a compact interval? Similar results also exist of open intervals. Perhaps the easiest way to see this is via realizability $\endgroup$ Sep 28, 2019 at 21:58
  • $\begingroup$ @BasSpitters You mean you supply a constructive proof that a convergence test applies, and it spits out an integral? Essentially, proofs as programs. The proof of the test is a program in itself $\endgroup$
    – wlad
    Sep 29, 2019 at 5:17
  • $\begingroup$ @BasSpitters The Riemann integral is only over compact intervals, so it's hard to know what you mean by "similar results" $\endgroup$
    – wlad
    Sep 29, 2019 at 5:27
  • $\begingroup$ Yes, an extensive theory of integration exists. See e.g. the book by Bishop and Bridges, or the book by YK Chan These results can be compiled to TTE by realizability. $\endgroup$ Sep 29, 2019 at 12:30
  • $\begingroup$ That's not what I had in mind. You could then say that differentiation or the halting problem are also computable because of realisability. That's not how it's usually meant $\endgroup$
    – wlad
    Sep 29, 2019 at 15:05

1 Answer 1

2
$\begingroup$

Suppose $f$ is Riemann-integrable on every closed interval $[a,b]$.

Proposition: $\int_0^\infty f(x) \, dx$ exists, if and only if, for every $\epsilon > 0$ there exists $b \geq 0$ such that for all $c \geq b$, $\left|\int_b^c f(x) \, dx \right| < \epsilon$.

Proof. Let us write $I(a,b) = \int_a^b f(x) \, dx$ because it's annoying to write lots of LaTeX code.

Suppose $I(0, \infty)$ exists, i.e., the limit $\lim_{b \to \infty} I(0,b)$ exists. Notice that then $I(x, \infty)$ exits for all $x \geq 0$. Consider any $\epsilon > 0$. There is $b \geq 0$ such that, for all $c \geq b$, we have $|I(0,\infty) - I(0,c)| < \epsilon/2$. Now it follows that $|I(b,c)| = |I(b,\infty) - I(c,\infty)| \leq |I(0,\infty) - I(b, \infty)| + |I(0,\infty) - I(c,\infty)| < \epsilon$.

For the converse, consider an arbitrary $\epsilon > 0$. By assumption there is $b > 0$ such that for all $c \geq b$ we have $|I(b,c)| < \epsilon/2$. Thus, for all $d \geq c \geq b$ we have $|I(0,c) - I(0,d)| \leq |I(0,c) - I(0,b)| + |I(0,d) - I(0,b)| = |I(b,c)| + |I(b,d)| < \epsilon$. We have established that the map $b \mapsto I(0,b)$ satisfies the Cauchy condition at $b \mapsto \infty$, therefore the desired limit $I(0, \infty)$ exists. $\Box$

The previous proof is constructive. Therefore, by interpreting above in the realizability model of Type Two Effectivty (the Kleene-Vesley topos), we may conclude that in TTE the represented space of functions which are Riemann-integrable on $[0,\infty]$ is computably isomorphic to the represented space of functions $f : [0,\infty) \to \mathbb{R}$, which are realized by a pair $\langle \alpha, \beta\rangle \in \mathbb{N}^\mathbb{N} \times \mathbb{N}^\mathbb{N}$ such that:

  • $\alpha$ realizes $f$ (as a function that is Riemann-integrable on every closed interval, but in TTE they all are, so $\alpha$ just realizes $f$ as a map),
  • $\beta$ realizes $\forall k \in \mathbb{N} . \exists m \in \mathbb{N} . \forall c \geq m . |I(m,c)| < 2^{-k}$. Concretely $\beta$ is a sequence such that, for all $k \in \mathbb{N}$ and all $c \geq \beta_k$ we have $|I(\beta_k, c)| < 2^{-k}$.

If you do not like the above representation, you are free to massage it into some other form that is computably isomorphic to it. However, in view of the above proposition, you won't be able to considerably cut down on the computational content of the realizer $\beta$.

$\endgroup$
5
  • $\begingroup$ The advantage of the the theorem over closed intervals is that it holds unconditionally. The condition here seems complicated to use $\endgroup$
    – wlad
    Sep 29, 2019 at 9:50
  • $\begingroup$ It's like saying that differentiation is computable once you've shown that all the conditions have been met. That's hardly a surprise $\endgroup$
    – wlad
    Sep 29, 2019 at 9:51
  • $\begingroup$ It's still an interesting demonstration of realisability, fleshed out in quite some detail. I'll read your tutorial on it $\endgroup$
    – wlad
    Sep 29, 2019 at 9:59
  • 1
    $\begingroup$ Re your remark about differentiability: exactly! If you have a realizer of a differentiable $f$ as a map only, then the realizers contains zero information about the derivative. It's similar here. To be able to compute the integral is computationally equivalent to knowing how quickly it converges. If you only have the realizer for $f$ as a map, you have no information about its integral. It's a psychologically unpleasant fact, which is why I phrased it as a Proposition with a proof, so that it is more inevitably accepted. $\endgroup$ Sep 29, 2019 at 19:04
  • 1
    $\begingroup$ By the way, there will be subspaces of functions integrable on $[0, \infty)$ whose representation goes more along the lines of having a majorizing function (like the ones you suggest in your question). Those are "suboptimal" because they contain too much information to make $[0, \infty)$ computable. The above proposition proves that the representation I suggested is optimal. $\endgroup$ Sep 29, 2019 at 19:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.