Different notions of computable binary sequence 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!
 A: You can look at automatic structures, replacing Turing machines by finite automata. In that setting, the whole first order theory is decidable (in particular you can add existential quantifiers like you describe), by a Theorem of Hodgson.
Hodgson, Bernard R., On direct products of automaton decidable theories, Theor. Comput. Sci. 19, 331-335 (1982). ZBL0493.03002.
A: 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 


*

*Solving the Halting problem for whatever notion of computability we work with (as explained in the question)

*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.
