User loginNavigation 
Total Self Compiler via Superstitious LogicsAs we have another thread on avoiding the practical consequences of Godel incompleteness theorem, which seems like a worthwhile goal, I thought I'd post this fun little construction. To what extent can we implement a provably correct compiler for our language? If we start with axioms of the machine (physical or virtual), can we prove that a compiler correctly implements itself on this target machine? There's a simple construction that works for all sorts of systems that effectively allows you to prove selfconsistency without running afoul of Godel's theorem. Here's the idea: Let's start with your favorite system (set theory, type theory) to which we want to add selfevaluation (to, among other things, prove selfconsistency). As a first step, let's add a big set/type on top that's large enough to model that system. For example, in ZFC set theory, you can add an inaccessible cardinal. You're just looking at the original system from the outside and saying "ok, take all of the stuff in that system, and add the ability to quantify over that, getting a new system." Now this new system that you end up with can model and prove the consistency of the original system, but still cannot prove the consistency of itself. This leads to a simple "practical selfcompilation": perform this jump to bigger and bigger systems 2^64 times and start with a version of the compiler at level N=2^64. Whenever you want to do a new compiler, you prove the consistency of the axioms at level N1. Each version of the compiler has N as part of its axioms and can prove the consistency of "itself" (but for versions with smaller N). No compiler ever proves its own consistency, but, as a practical matter, if the only thing you use these levels compile new versions of the compiler, then you won't ever run out of levels. But there is an inelegance in having to keep track of levels in such a scheme. The number of levels itself clearly isn't important, and even if it's only a version number that's changing, we clearly haven't really created a "self" compiler. Do we really need that number? What's important is just that the scheme prevents infinite descent of the levels. So here's the proposed fix: Step 1. Start with some finite number N (leave this N a parameter of the construction; later we'll notice that we can pretend it's infinity) of these inaccessible sets/nested universes and index them so that the biggest one is index 0, the next smallest contained inside it is index 1, etc. Index N is the smallest universe that's just big enough to serve as a model for the original theory. Step 2. We write a semantic eval function that maps terms in the language into our biggest universe and use it to establish the soundness of the logic/type system. Terms reference 'universe 0' gets mapped to universe 1, 'universe 1' gets mapped to universe 2, etc. Our model of the term for 'N' is N1 in the model. This step works just like the "first practical solution" above, except now we're counting down and we don't use actual numbers for N in our logic. Step 3. How do we establish that the new 'N' (N1) is positive? We make our compiler superstitious as follows: we pick an unused noop of the target machine that should never occur in normal generated code and add an axiom that says that running this noop 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. Then we can have an inference rule in the logic that allows us to conclude that N > M for any particular M:Nat, without any way to infer that (forall M:Nat. N > M), which would lead to contradiction. The implementation of this inference rule invokes the magic noop until it's confident that enough such levels exist. Rather than a direct statement that the compiler works, we will have a clause that says "if there are enough levels, then the compiler terminates and works." Any human reading this clause can safely this clause (we know there are always sufficiently many levels), and just as importantly, we can instruct the compiler to allow execution of functions that terminate if there are enough levels and that will make things total. i.e. We can have a total selfcompiler. I have a logic that I'm working with that I'd like to try building this scheme with, but I have quite a bit of work left on the machinery I'd need to complete it. Please let me know if you know of someone who does something similar. Apologies for the long post. I've argued here that this is possible, but with fewer details. Let me know if I need more details. Hopefully someone finds this interesting. By Matt M at 20130729 01:40  LtU Forum  previous forum topic  next forum topic  other blogs  5912 reads

Browse archivesActive forum topics 
Recent comments
47 min 39 sec ago
3 hours 36 min ago
5 hours 35 min ago
6 hours 34 min ago
1 day 11 hours ago
1 day 14 hours ago
2 days 16 hours ago
2 days 23 hours ago
3 days 58 min ago
3 days 1 hour ago