I found this interesting post over at lambda the ultimate about constructing a provably total (terminating) self-compiler. It looked quite similar to some of the stuff MIRI has been doing with the Tiling Agents thing. Maybe someone with more math background can check it out and see if there are any ideas to be shared?
This is the same basic idea as Benja’s Parametric Polymorphism, with N in the post corresponding to kappa from parametric polymorphism.
The “superstition” is:
We make our compiler superstitious as follows: we pick an unused no-op of the target machine that should never occur in normal generated code and add an axiom that says that running this no-op actually bumps a counter that exists in the ether, and, if this unseen counter exceeds N, then it halts execution of the machine. Since we could have started with an arbitrary N, we will never reach a contradiction if we take the bottom out of the level descent, so long as we don’t let the logic know we took the bottom out.
And from the section in Tiling Agents about parametric polymorphism (recommended if you want to learn about parametric polymorphism):
It is difficult to see what “believing in” $T_\kappa$ could correspond to in terms of the epistemic state of a rational agent. We believe from outside the system that $\kappa$’s intended interpretation is “any natural number,” but this realization is apparently forbidden to the agent to whom $\kappa$ refers to some specific finite number about which nothing is known except that it plays a vital role in the agent’s goal system. This seems like an odd mental state for a rational agent.
Anyway, it’s interesting that someone else has a very similar idea for this kind of problem. But as mentioned in Tiling Agents, the “superstitious belief” seems like a bad idea for an epistemically rational agent.
It is neat that this problem is coming up elsewhere. It reminds me that MIRI’s work could be relevant to people working in other sub-fields of math, which is a good sign and a good opportunity.
I found this interesting post over at lambda the ultimate about constructing a provably total (terminating) self-compiler. It looked quite similar to some of the stuff MIRI has been doing with the Tiling Agents thing. Maybe someone with more math background can check it out and see if there are any ideas to be shared?
The post: Total Self-Compiler via Superstitious Logics
This is the same basic idea as Benja’s Parametric Polymorphism, with N in the post corresponding to kappa from parametric polymorphism.
The “superstition” is:
And from the section in Tiling Agents about parametric polymorphism (recommended if you want to learn about parametric polymorphism):
Anyway, it’s interesting that someone else has a very similar idea for this kind of problem. But as mentioned in Tiling Agents, the “superstitious belief” seems like a bad idea for an epistemically rational agent.
It is neat that this problem is coming up elsewhere. It reminds me that MIRI’s work could be relevant to people working in other sub-fields of math, which is a good sign and a good opportunity.