An analogue of Scott continuity for infinite-time-Turing-computable functions

Question

$\newcommand{\tb}{2_{\!\bot}}\newcommand{\tbO}{\tb^{\,\omega}}$Let $2 = \{0,1\}$ and $\tb = \{0,\bot,1\}$.

Scott continuity is important for defining models of lambda calculus, a formalism for defining Turing-computable functions. That is because every Turing/lambda-computable function is Scott-continuous, and there are domains such that $$D \cong [D \to D]\,,$$ where $[D \to D]$ is the set of Scott-continuous functions on $D$.

Infinite time Turing machines (ITTMs) are more expressive than Turing machines, and are capable of computing functions that are not Scott-continuous. Take the function $z\colon 2^\omega \to 2$ that returns 0 iff its argument is a tape of zeros. (An ITTM may cycle moving left, return 1 if it finds 1 on the tape, or return 0 if it finds itself in the limit state. However, $z$ is not Scott-continuous, see below.)

Question: Is there some other continuity $Y$ that would similarly be to ITTM-computable functions what Scott continuity is to Turing-computable functions?

It would have to be the case that all ITTM-computable functions are $Y$-continuous. Presumably, there would also be domains isomorphic to their $Y$-continuous function spaces, containing all ITTM-computable functions. (I don't know what other, if any, requirements I should have.)

---

Definitions:

Let $<$ be a partial order on $\tb$ such that only $\bot < 0$ and $\bot < 1$ hold. Let $\tbO$ be ordered pointwise.

A pointed directed-complete partial order (CPO) is a partially ordered set with a least element, such that every directed set has a supremum. $\tbO$ and $\tb$ are CPOs.

Let $D$ and $E$ be CPOs. A function $f\colon D \to E$ is Scott continuous iff for every directed subset $P$ of $D$, its image has a supremum $\sqcup f(P)$ and it equals $f(\sqcup P)$.

I believe it is reasonable to extend the definition of Scott continuity to functions $g\colon 2^\omega \to 2$ as follows, but if I'm wrong here, please correct me: $g$ is continuous iff the following function is: \begin{align} g'\colon \tbO &\to \tb \\ x &\mapsto \sqcap g(\{ y \in 2^\omega \mid x \leq y \}) \end{align}

(I believe this corresponds with how continuity of $g$ is defined in this answer using the product topology on $2^\omega$, and has the intuitive explanation that we are treating elements of $\tb^\omega$ as sequences of finite pieces of information about some element of $2^\omega$, each piece telling us the value of the corresponding digit (if it's 0 or 1) or that the digit is unknown (if it's $\bot$). If this is unreasonable (or incorrect), then unfortunately I don't know how one might extend the definition of Scott continuity to functions from $2^\omega$ to $2$; hopefully my question can still be salvaged.)

With this definition, we might show why $z$ from above is not Scott-continuous: for every $n \in \mathbb{N}$, let $Z_n = 0^n \cdot \bot^\omega$, where $\cdot$ is concatenation. For every $n$, $z'(Z_n) = \bot$, so $\sqcup_n z'(Z_n) = \bot$, however $z'(\sqcup_n Z_n) = z'(0^\omega) = 0$.

Answer 1

The domain-theoretic considerations of the kind you are asking about can be carried out using synthetic domain theory. Related to it is syntehtic topology, and in fact the two share many common ideas.

The starting point of both synthetic approaches is the observation that the Sierpinski space $\Sigma$ classifies open sets, i.e., given a space or a domain $X$, the space $\mathcal{C}(X, \Sigma)$ of continuous maps is in bijective correspondence with the open subsets of $X$. The general approach then is as follows:

1. Pick a suitable category $\mathcal{E}$, to serve as an ambient in which we carry out the "synthetic" version of topology or domain theory.

2. Construct an object $\mathbb{S}$ in $\mathcal{E}$, together with a suitable additional structure, which plays the role of the Sierpinski space. The suitable additional structure is that of a dominance.

3. Use the exponential object $\mathbb{S}^X$ as the "topology" of $X$.

Examples of such setups can be found in the literature on synthetic domain theory. Another source is Davorin Lešnik's PhD (write him an email). The usual topology can be obtained by taking $\mathcal{E}$ to be a suitable topos of sheaves on topological spaces.

A computable version of domain theory and topology can be obtained by taking $\mathcal{E}$ to be the effective topos as follows. Let $W$ be a standard enumeration of the c.e. sets and $K$ the halting set

$$K = \{n \in \mathbb{N} \mid n \in W_n\}.$$

That is, $n \in K$ when the $n$-th Turing machine terminates on input $n$.

Define $\mathbb{S}$ to be the assembly $\mathbb{S} = (\{\bot, \top\}, {E_\mathbb{S}})$ whose existence predicate is $$E_\mathbb{S}(\top)= K \qquad\qquad E_\mathbb{S}(\bot)= \mathbb{N} \setminus K.$$ In the effective topos $\mathbb{S}^\mathbb{N}$ is the assembly of c.e. sets, and in general $\mathbb{S}$ behaves like a computable Sierpinski space.

Now we are ready to propose a suitable setup for infinite-time Turing machines (IITM). Let $K_\infty$ be the halting set for IITMS's:

$$K_\infty = \{n \in \mathbb{N} \mid \text{the $n$-th IITM halts on input $n$}\}.$$

If I were to investigate domain theory for IITM's, I would consider the realizability topos built over the partial combinatory algebra of IITM's (see these notes). The dominance is $\mathbb{S}_\infty = (\{\bot, \top\}, {E_{\mathbb{S}_\infty}})$ where $$E_{\mathbb{S}_\infty}(\top)= K_\infty \qquad\qquad E_{\mathbb{S}_\infty}(\bot)= \mathbb{N} \setminus K_\infty.$$ The resulting notion of synthetic topology is "intrinsic" to IITMs. For example $\mathbb{S}_\infty^\mathbb{N}$ will be those subsets of $\mathbb{N}$ which are the halting sets of an IITM, I think. I am not sure eactly, because with IITMs strange things happen. Is it the case that a set is the halting set of an IITM if and only if it is enumerated by an IITM?

There are many other possible variations, both on how we construct a topos from IITMs, and what we take as $\mathbb{S}$. I am not aware of any serious study of what works and what does not. Take everything I said here as just unbaked ideas that might show some promising directions.