Are there analogues of Specker sequences for other complexity classes?

Consider the standard definition of computable real numbers: a real number $r$ is computable just in case $r$ is the limit of a sequence $(a_i)_{i \in \mathbb{N}}$ such that (1) the function $i \mapsto a_i$ is recursive and (2) there exists a recursive function $\xi$ such that, for all $j,k,n \in \mathbb{N}$, if $j,k<\xi(n)$, then $\vert a_j - a_k \vert < n^{-1}$.

Specker (1949) showed that there exist sequences of recursive reals that converge to a nonrecursive real.

Given any complexity class $\mathsf{C}$, however, we can define a notion of $\mathsf{C}$-computable real number by uniformly replacing 'recursive function' in the definition above with 'function in $\mathsf{C}$'.

Do analogues of Specker's result hold for the most obvious such notions? I.e., do there exist sequences of $\mathsf{C}$-computable reals that converge to non-$\mathsf{C}$-computable limits when $\mathsf{C} = \mathsf{P}, \mathsf{NP}, \mathsf{PSPACE}, \mathsf{EXP}$, etc.?

I have not been able to find any discussions of this question in the literature; if some exist, I'd be very grateful for any pointers. I don't think there's any trivial way to generalize Specker's proof since it relies on the existence of a recursive enumeration of a nonrecursive set.

• Yes, see Ker-I Ko's book "Complexity Theory of Real Functions" or chapter 6 of Klaus Weihrauch's book "Computable Analysis" – Kaveh May 14 '16 at 1:39
• Simultaneously cross-posted to mathoverflow.net/questions/238803 . – Emil Jeřábek May 14 '16 at 9:34
• Your defintion of computable real has a mistake, it should say $j, k > \xi(n)$, not $<$. And Specker proved more than what you claim: the recursive sequence is a strictly increasing rational sequence, contained in $[0,1]$ and computably away from every computable real. – Andrej Bauer May 14 '16 at 9:46
• And it should say that $a_i$ are ratonals, presumably. – Andrej Bauer May 14 '16 at 9:47