Type-checking for many popular programming languages (e.g. Java, C++, C#, Rust, OCaml, Scala, Swift) is undecidable, and for practical purposes this fact is little more than a curiosity.
The question of whether, given a finite POMDP, any policy exists that achieves at least zero expected reward is undecidable, and for practical RL this is not even much of a curiosity.
Any function from {i∈N;i<n}→N that is well-defined is computable, because there exists a finite encoding of a lookup table. No Myhill–Nerode needed.
I think a more compelling formalization of the Busy Beaver problem’s hardness is that fori≥748, the value ofBB(i)is independent of ZF set theory. In some sense BB(748) alone is uncomputable, even though it’s just a single natural number rather than a function that has to work for infinitely many inputs.
Thanks for the examples and links! Hmm… the programming language examples definitely give me some more “grounding” for the concepts. I also just discovered your recent post, but to be honest a lot of it like the type two theory of effectivity is above my head at the moment.
I would say no.
Type-checking for many popular programming languages (e.g. Java, C++, C#, Rust, OCaml, Scala, Swift) is undecidable, and for practical purposes this fact is little more than a curiosity.
The question of whether, given a finite POMDP, any policy exists that achieves at least zero expected reward is undecidable, and for practical RL this is not even much of a curiosity.
Any function from {i∈N;i<n}→N that is well-defined is computable, because there exists a finite encoding of a lookup table. No Myhill–Nerode needed.
I think a more compelling formalization of the Busy Beaver problem’s hardness is that for i≥748, the value of BB(i) is independent of ZF set theory. In some sense BB(748) alone is uncomputable, even though it’s just a single natural number rather than a function that has to work for infinitely many inputs.
Thanks for the examples and links! Hmm… the programming language examples definitely give me some more “grounding” for the concepts. I also just discovered your recent post, but to be honest a lot of it like the type two theory of effectivity is above my head at the moment.