Higher-Order Feedback Computation

Feedback Turing machines are Turing machines which can query a halting oracle which has information on the convergence or divergence of feedback computations. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A natural question to ask is: what about feedback Turing machines which can ask if computations of the same type converge, diverge, or freeze? We define \(\alpha \)th order feedback Turing machines for each computable ordinal \(\alpha \). We also describe feedback computable and semi-computable sets using inductive definitions and Gale–Stewart games.

1. 1.

   See the definition of subcomputation trees below.

This study was funded by FWF project TAI-797.

Authors and Affiliations

1. TU Wien, Vienna, Austria

   Juan P. Aguilera & Leonardo Pacheco

2. Florida Atlantic University, Boca Raton, USA

   Robert S. Lubarsky

Corresponding author

Correspondence to Leonardo Pacheco .

Editors and Affiliations

1. The Mathematics Institute of Jussieu, Paris, France

   Ludovic Levy Patey

2. University College London, London, UK

   Elaine Pimentel

3. University of Amsterdam, Amsterdam, The Netherlands

   Lorenzo Galeotti

4. University of Göttingen, Göttingen, Germany

   Florin Manea

Disclosure of Interests

The authors have no competing interests to declare that are relevant to the content of this article.

A Proof of Theorem 2

Let \(A\subseteq \omega \) and \(\alpha <\omega _1^\textrm{ck}\). We show that, if A is \(\varSigma ^\mu _{\alpha }\)-definable, then A is \(\alpha \)-feedback semi-computable.

We begin by defining an evaluation function \(\texttt{eval}\) for \(\varSigma ^\mu _\alpha \)-formulas. We then prove by induction on \(\beta \le \alpha \) that the \(\varSigma ^\mu _\beta \)-definable sets are \(\alpha \)-feedback semi-computable.

For this proof, we work with a fixed set of set variables \(\{X_i\mid i\in \omega \}\). We also assume that the \(\mu \)-formulas are in normal form. We do not consider formulas with free number variables. \(\texttt{eval}\) is defined by recursion on the structure of the \(\varSigma ^\mu _\alpha \)-formulas: we begin at the first order formulas and go up level-by-level.

The function \(\texttt{eval}(\varphi ,s)\) takes as input a formula \(\varphi \), and a sequence s of natural numbers. The sequence s is a sequence of indices of (possibly partial) characteristic function of sets. If \(i< \textrm{length}(s)\) then \(s_i\) denotes the index in the ith position of s. If \(i\ge \textrm{length}(s)\), then \(s_i\) is the index for the characteristic function of the empty set. s will be useful when evaluating the fixed-point operators.

We define \(\texttt{eval}\) for first-order formulas, along with auxiliary functions \(\texttt{exists}\) and \(\texttt{forall}\):

• \(\texttt{eval}(t=t', s) := \left\{ \begin{array}{ll} 1, &{} \text {if}\ t = t' \\ 0, &{} \text {otherwise} \end{array} \right. \)

• \(\texttt{eval}(t\in X_i, s) := \left\{ \begin{array}{ll} 1, &{} \text {if}\ {\langle s_i \rangle }^\alpha (t) = 1 \\ 0, &{} \text {otherwise} \end{array} \right. \)

• \(\texttt{eval}(\lnot \psi , s) := \left\{ \begin{array}{ll} 1, &{} \text {if}\ \texttt{eval}(\psi ,s) = 0 \\ 0, &{} \text {otherwise} \end{array} \right. \)

• \(\texttt{eval}(\psi \wedge \theta , s) := \left\{ \begin{array}{ll} 1, &{} \text {if}\ \texttt{eval}(\psi ,s) = \texttt{eval}(\theta ,s) = 1 \\ 0, &{} \text {otherwise} \end{array} \right. \)

• \(\texttt{eval}(\psi \vee \theta , s) := \left\{ \begin{array}{ll} 1, &{} \text {if}\ \texttt{eval}(\psi ,s) = 1 or \texttt{eval}(\theta ,s) = 1 \\ 0, &{} \text {otherwise} \end{array} \right. \)

• \(\texttt{forall}(\psi (x), s, i) := \left\{ \begin{array}{ll} 0, &{} \text {if}\ \texttt{eval}(\psi (i),s) = 0 \\ \texttt{forall}(\psi (x), s, i+1), &{} \text {otherwise} \end{array} \right. \)

• \(\texttt{eval}(\forall x.\psi , s) := \left\{ \begin{array}{ll} 1, &{} \text {if}\ \texttt{forall}(\psi (x), s, 0)\ \text {diverges} \\ 0, &{} \text {otherwise} \end{array} \right. \)

• \(\texttt{exists}(\psi (x), s, i) := \left\{ \begin{array}{ll} 1, &{} \text {if}\ \texttt{eval}(\psi (i),s) = 1 \\ \texttt{exists}(\psi (x),s,i+1), &{} \text {otherwise} \end{array} \right. \)

• \(\texttt{eval}(\exists x.\psi , s) := \left\{ \begin{array}{ll} 1, &{} \text {if }\ \texttt{exists}(\psi (x), s,0)\ \text {converges}\\ 0, &{} \text {otherwise} \end{array} \right. \)

On \(\texttt{forall}\) and \(\texttt{exists}\), \(\psi (i)\) is obtained by substituting the indicated number variable x by i.

We similarly define \(\texttt{eval}\) on infinitary formulas using auxiliary functions \(\texttt{conjunction}\) and \(\texttt{disjunction}\):

• \(\texttt{disjunction}(\bigvee _{i\in \omega }\psi _i, s,i) := \left\{ \begin{array}{ll} 1, &{} \text {if}\ \texttt{eval}(\psi _i,s) = 1\\ \texttt{disjunction}(\bigvee _{i\in \omega }\psi _i, s,i+1), &{} \text {otherwise} \end{array} \right. \)

• \(\texttt{eval}(\bigvee _{i\in \omega }\psi _i, s) := \left\{ \begin{array}{ll} 1, &{} \text {if}\ \texttt{disjunction}(\bigvee _{i\in \omega }\psi _i, s,0) \text {converges} \\ 0, &{} \text {otherwise} \end{array} \right. \)

• \(\texttt{conjunction}(\bigwedge _{i\in \omega }\psi _i, s,i) := \left\{ \begin{array}{ll} 0, &{} \text {if}\ \texttt{eval}(\psi (i),s) = 0\\ \texttt{conjunction}(\bigwedge _{i\in \omega }, s,i+1), &{} \text {otherwise} \end{array} \right. \)

• \(\texttt{eval}(\bigwedge _{i\in \omega }\psi _i, s) := \left\{ \begin{array}{ll} 0, &{} \text {if}\ \texttt{conjunction}(\bigwedge _{i\in \omega }\psi _i, s,0) \text {converges} \\ 1, &{} \text {otherwise} \end{array} \right. \)

Remember that as we only allow recursively enumerable conjunctions and disjunctions, we can recover \(\psi _i\) from a code of \(\bigwedge _{i\in \omega }\psi _i\) or \(\bigvee _{i\in \omega }\psi _i\).

We now extend \(\texttt{eval}\) to formulas with fixed-points. Suppose \(t\in \mu xX.\psi \) is a \(\varSigma ^\mu _{\beta +1}\)-formula, define:

Where \(s[X:=\emptyset ]\) is obtained by putting an index for the empty set in the ith position of s, and \(s[X_i:=\mu xX.\psi ]\) is obtained by putting an index for \(\lambda n.\texttt{eval}(n\in \mu x_iX_i.\psi )\) in the ith position of s. If s becomes a longer sequence by this procedure, fill the unused positions of s with indexes for the empty set.

If we have extended \(\texttt{eval}\) to \(\varSigma ^\mu _\beta \)-formulas, extend it to \(\varPi ^\mu _\beta \)-formulas by:

This finishes the definition of \(\texttt{eval}\).

We prove by bounded induction on \(\beta \le \alpha \) that the \(\varSigma ^\mu _\beta \)-definable sets are \(\alpha \)-feedback semi-computable. We slightly strengthen the induction hypothesis to show that, for \(\beta <\alpha \), \(\varPi ^\mu _\beta \)-definable sets are \(\alpha \)-feedback computable.

Reprints and permissions

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics