“Informasi yang dapat diverifikasi”: apakah ini konsep yang dikenal?

Bagi saya, berikut ini sepertinya definisi alami dan saya ingin tahu apakah ini telah dipelajari di suatu tempat

Pertimbangkan sekumpulan bahasa. Kemudian K ⊂ { 0 , 1 } ω disebut " informasi yang dapat diverifikasi X " ketika ada 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) Diberikan , setiap awalan x ada di $x \in L$$x$$L$

(ii) Dengan , setiap awalan f ada di $f \in K$$f$$L$

(iii) Mengingat , panjang n awalan f berada di luar L untuk n > > $f \notin K$$n$$f$$L$$n >> 0$

Misalnya adalah informasi yang dapat diverifikasi R jika f dapat dihitung. Ini dapat dilihat dengan membangun sebuah algoritma yang menjalankan verifikasi pada semua string panjang n dan mengumpulkan awalan panjang $\lbrace f \rbrace$$\mathsf{R}$$f$$n$$m$ dari string-string yang melewati verifikasi. Untuk , satu-satunya awalan yang tetap adalah yang benar$n >> m$

Namun jika adalah R informasi -verifiable itu tidak berarti setiap f ∈ K adalah dihitung: misalnya mempertimbangkan K = $K$$\mathsf{R}$$f \in K$$K = \lbrace 0, 1 \rbrace^\omega$

Contoh non-sepele dari yang dapat diverifikasi P adalah sebagai berikut. Pertimbangkan L ∈ N P ∩ c o N P dan biarkan f menjadi pengkodean L bersama-sama dengan N P dan c o N P saksi yang sesuai (yaitu untuk setiap x ∈ { 0 , 1 } ∗ , f menyandikan salah satu N P - saksi pembuktian x ∈ L atau 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$ saksi membuktikan$\mathsf{coNP}$ )$x \notin L$

$K\subseteq\{0,1\}^\omega$ adalah$\mathsf{R}$ diverifikasi jika dan hanya jika$K$ adalah$\Pi^0_1$ kelas(dalam ruang Cantor), sebuah konsep yang telah dipelajari secara luas dalamteori komputabilitas. Mereka juga disebut set tertutup efektif.

Himpunan $K$ adalah kelas $\Pi^0_1$ jika himpunan jalur tak terbatas melalui pohon rekursif (dapat dihitung), dan ini adalah versi konsep yang Anda tetapkan.

Sebuah monograf yang dikhususkan untuk mereka:

Set Tertutup Efektif (Douglas Cenzer dan Jeffrey B. Remmel), Perspektif dalam Logika, Cambridge U. Tekan, 350 halaman, untuk muncul.