The standard definition of computability, for a sequence $s\in\{0,1\}^\omega$, is that there is a Turing machine outputting $s[i]$ on input $i$.


I'm looking for strengthenings of this notion; for example, in the above definition it's not decidable whether there is a $1$ in $s$; or, given $i$, whether there is a $1$ in $s$ at position $\ge i$. I would be happy to be shown a "natural" definition of computability that makes these predicates computable.


To the above: if there were an algorithm that, from the Turing machine producing $s$, tells us whether $s$ contains a $1$ then I could do the following: from any Turing machine $M$, program a Turing machine outputting $s[i]=1$ if $M$ stops after $\le i$ steps. This sequence $s$ is obviously computable --- I said how to compute it --- but an algorithm determining if the sequence contains a $1$ would solve the Halting problem.


A search through the literature didn't show anything, so links and references are most welcome!



Different notions of computable binary sequence
What a *computable sequence* is essentially follows from what computability is, and from what a sequence is.


Let us first agree that a sequence over $\mathbf{X}$ is a function $s : \mathbb{N} \to \mathbf{X}$. Then asking that whether or not a sequence over $\{0,1\}$ is constant be decidable amounts to 


1. Solving the Halting problem for whatever notion of computability we work with (as explained in the question)
2. Demanding that $\mathbb{N}$ is compact (in the sense of synthetic topology)


This tells us that any notion of computability with this property is extremely weird, and probably should not be considered a notion of computability at all.


Of course, we could use a mixed view, where we use a restricted version of computability on the sequence, and a more powerful one to decide whether its constant. In that case, we just need that the second notion can decide the Halting problem for the first.


Alternatively, we could replace $\{0,1\}^\omega$ by something different, but similar. We can view this as $\mathcal{P}(\omega)$, but all standard notions of computability on this are weaker than $\{0,1\}^\omega$. Using Joseph Miller's $\Pi$-topology on $\{0,1\}^\omega$, we could get that whether sequence is constant becomes decidable. Unfortunately, there are no computable points in the $\Pi$-topology at all.


We could brute-force it, say by tagging any $p \in \{0,1\}^\omega$ by the cardinality of $|\{n \in \mathbb{N} \mid p(n) = 1\}|$, but I fail to see how this would be interesting.


