An implementation of modal UDT

post by Benya_Fallenstein (Benja_Fallenstein) · 2015-02-11T06:02:22.000Z · LW · GW · 0 comments

Contents

No comments

One of the great advantages of working with Gödel-Löb provability logic is that it's possible to implement an evaluator which efficiently checks whether a sentence in the language of GL is true. Mihaly and Marcello used this to write a program that checks whether two modal agents cooperate or defect against each other. Today, Nate and I extended this with an implementation of modal UDT, which allows us to check what UDT does on different decision problems---see Program.hs in the Github repository. No guarantees for correctness, since this was written rather quickly; if anybody is able to take the time to check the code, that would be very much appreciated!

---

The implementation of UDT is rather pleasing, I think. Here's the informal definition of modal UDT, using PA + $\ell$:

• For every possible outcome $j$, from best to worst:
  • For every possible action $i$, in order:
    • If it's provable in PA + $\ell$ that "UDT takes action $i$" implies "the universe returns outcome $j$", then take action $i$.
• If you're still here, return a default action.

Here is the corresponding Haskell code:

udt :: (Enum a,Ord b,Show b,Enum b)
    => Int -> ModalProgram b a -> b -> ModalProgram b b
udt level univ dflt = modalProgram dflt $
  mFor $ \a ->
    mFor $ \b ->
      mIf (boxk level (Var b %> univ a)) (mReturn b)

Being able to write modal UDT like this makes it very easy to implement and try small variations on the code.

---

We used this code to check what modal UDT would do in a version of Newcomb's problem where Omega uses proofs in PA (rather than simulations) to decide whether to put the money in the box; that is, it will put a million dollars in the first box if and only if it can prove that you will one-box. If our code is correct, it turns out that in this case, modal UDT will do whatever its default action was.

Earlier, we thought we had proved a different result on the whiteboard, but after the code disagreed with us, we went over it again and found a bug in our proof. After fixing that bug, we now have a manual proof that UDT will end up taking its default action in this scenario (which I'll write about some other time). So looks like this can be a useful tool for figuring out this sort of thing!

0 comments

Comments sorted by top scores.