“Información verificable”: ¿es este un concepto conocido?

Lo siguiente me parece una definición natural y me pregunto si se ha estudiado en alguna parte

Considere un conjunto de idiomas. Entonces se llama " -información verificable" cuando hay st$\mathsf{X} \subset 2^{\lbrace 0, 1 \rbrace^*}$$K \subset \lbrace 0, 1 \rbrace^\omega$$\mathsf{X}$$L \in \mathsf{X}$

(i) Dado , cada prefijo de está en$x \in L$$x$$L$

(ii) Dado , cada prefijo de f está en $f \in K$$f$$L$

(iii) Dado , la longitud n prefijo de f está fuera L para n > > $f \notin K$$n$$f$$L$$n >> 0$

Por ejemplo, es información verificable por R si f es computable. Esto se puede ver al construir un algoritmo que ejecute la verificación en todas las cadenas de longitud n y recopile los prefijos de longitud m de esas cadenas que pasaron la verificación. Para n > > m , el único prefijo que queda es la correcta$\lbrace f \rbrace$$\mathsf{R}$$f$$n$$m$$n >> m$

Sin embargo, si es información verificable por R , no significa que cada f ∈ K sea ​​computable: por ejemplo, considere K = { 0 , 1 } $K$$\mathsf{R}$$f \in K$$K = \lbrace 0, 1 \rbrace^\omega$

Un ejemplo no trivial de que es P- verificable es el siguiente. Considere L ∈ N P ∩ c o N P y deje que f sea ​​una codificación de L junto con los testigos correspondientes de N P y c o N P (es decir, para cada x ∈ { 0 , 1 } ∗ , f codifica una N P - testigo que prueba x ∈ L o a$\lbrace f \rbrace$$\mathsf{P}$$L \in \mathsf{NP} \cap \mathsf{coNP}$$f$$L$$\mathsf{NP}$$\mathsf{coNP}$$x \in \lbrace 0, 1 \rbrace^*$$f$$\mathsf{NP}$$x \in L$ testigo que demuestra x ∉ L )$\mathsf{coNP}$$x \notin L$

$K\subseteq\{0,1\}^\omega$ es$\mathsf{R}$ verificable si y solo si$K$ es unaclase$\Pi^0_1$ (en el espacio de Cantor), un concepto que se ha estudiado ampliamente enla teoría de la computabilidad. También se les llama conjuntos efectivamente cerrados.

Un conjunto $K$ es una clase $\Pi^0_1$ si es el conjunto de caminos infinitos a través de un árbol recursivo (computable), y esta es la versión del concepto que usted definió.

Una monografía dedicada a ellos:

Conjuntos efectivamente cerrados (Douglas Cenzer y Jeffrey B. Remmel), Perspectives in Logic, Cambridge U. Press, 350 páginas, para que aparezcan.