„Informacje możliwe do zweryfikowania”: czy jest to znana koncepcja?

Poniższe wydaje mi się naturalną definicją i zastanawiam się, czy gdzieś to zbadano

Rozważać $\mathsf{X} \subset 2^{\lbrace 0, 1 \rbrace^*}$zestaw języków. Następnie$K \subset \lbrace 0, 1 \rbrace^\omega$ nazywa się "$\mathsf{X}$-weryfikowalne informacje ”, gdy są $L \in \mathsf{X}$ św

(i) Biorąc pod uwagę $x \in L$, każdy prefiks $x$ jest w $L$

(ii) Biorąc pod uwagę $f \in K$, każdy prefiks $f$ jest w $L$

(iii) Biorąc pod uwagę $f \notin K$, długość $n$ przedrostek $f$ jest na zewnątrz $L$ dla $n >> 0$

Na przykład $\lbrace f \rbrace$ jest $\mathsf{R}$-weryfikowalne informacje iff $f$jest obliczalny. Można to zaobserwować, konstruując algorytm, który uruchamia weryfikację na wszystkich ciągach długości$n$ i zbiera prefiksy długości $m$tych ciągów, które przeszły weryfikację. Dla$n >> m$, jedynym pozostałym przedrostkiem jest poprawny

Jeśli jednak $K$ jest $\mathsf{R}$-weryfikowalne informacje, nie oznacza to wszystkich $f \in K$ jest obliczalny: na przykład rozważ $K = \lbrace 0, 1 \rbrace^\omega$

Nietrywialny przykład $\lbrace f \rbrace$ który jest $\mathsf{P}$-weryfikowalna jest następująca. Rozważać$L \in \mathsf{NP} \cap \mathsf{coNP}$ i pozwól $f$ być kodowaniem $L$ wraz z odpowiednim $\mathsf{NP}$ i $\mathsf{coNP}$ świadkowie (tj. dla każdego $x \in \lbrace 0, 1 \rbrace^*$, $f$ koduje albo $\mathsf{NP}$-dowodowanie świadka $x \in L$ lub a $\mathsf{coNP}$-dowodowanie świadka $x \notin L$)

$K\subseteq\{0,1\}^\omega$ jest $\mathsf{R}$-weryfikowalne wtedy i tylko wtedy $K$ jest $\Pi^0_1$klasa (w przestrzeni Cantora), koncepcja, która była szeroko badana wteoria obliczalności. Są również nazywane zestawami skutecznie zamkniętymi.

Zbiór $K$ jest $\Pi^0_1$ klasa iff jest to zestaw nieskończonych ścieżek przez rekurencyjne (obliczalne) drzewo i jest to wersja zdefiniowanej przez ciebie koncepcji.

Monografia poświęcona im:

Efektywnie zamknięte zestawy (Douglas Cenzer i Jeffrey B. Remmel), Perspectives in Logic, Cambridge U. Press, 350 stron.