“Informação verificável”: esse é um conceito conhecido?

A seguir, parece-me uma definição natural e me pergunto se ela foi estudada em algum lugar.

Considere um conjunto de idiomas. Então K ⊂ { 0 , 1 } ω é chamado de " informação verificável em X " quando existe L ∈ X st$\mathsf{X} \subset 2^{\lbrace 0, 1 \rbrace^*}$$K \subset \lbrace 0, 1 \rbrace^\omega$$\mathsf{X}$$L \in \mathsf{X}$

(i) Dado , todo prefixo de x está em $x \in L$$x$$L$

(ii) Dado , todo prefixo de f está em $f \in K$$f$$L$

(iii) Tendo em conta , o comprimento n prefixo de f está fora G para n > > $f \notin K$$n$$f$$L$$n >> 0$

Por exemplo, é uma informação verificável em R se if é computável. Isso pode ser visto através da construção de um algoritmo que executa a verificação em todas as cadeias de comprimento n e coleta os prefixos de comprimento m daquelas cadeias que passaram na verificação. Para n > > m , o único prefixo que permanece é o correcto$\lbrace f \rbrace$$\mathsf{R}$$f$$n$$m$$n >> m$

No entanto, se é informação verificável por R , isso não significa que todo f ∈ K é computável: por exemplo, considere K = { 0 , 1 } $K$$\mathsf{R}$$f \in K$$K = \lbrace 0, 1 \rbrace^\omega$

Um exemplo não trivial de que é P- verificável é o seguinte. Considere G ∈ N P ∩ C O N P e deixá- f ser uma codificação de G em conjunto com o correspondente N P e C O N P testemunhas (isto é, para cada x ∈ { 0 , 1 } * , f codifica quer uma N P - testemunha que prova x ∈ L ou$\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$ testemunha provando x ∉ L )$\mathsf{coNP}$$x \notin L$

$K\subseteq\{0,1\}^\omega$ é$\mathsf{R}$ verificável se e somente se$K$ for umaclasse$\Pi^0_1$ (no espaço Cantor), um conceito que foi estudado extensivamente nateoria da computabilidade. Eles também são chamados de conjuntos efetivamente fechados.

Um conjunto $K$ é uma classe $\Pi^0_1$ se for o conjunto de caminhos infinitos através de uma árvore recursiva (computável) e esta é a versão do conceito que você definiu.

Uma monografia dedicada a eles:

Conjuntos efetivamente fechados (Douglas Cenzer e Jeffrey B. Remmel), Perspectives in Logic, Cambridge U. Press, 350 páginas, para aparecer.