Jason (jcreed) wrote,

I keep thinking more vague thoughts about the ol' read-only access problem chrisamaphone brought up again.

The latest thing that occurred to me is to do the thing I love to do and represent ^P as q * P and vN as q -o N, and subsequently to that say that [P]N ("if P is true right now then you can focus on N on the left") is something like

q -o ((P -o 0) + N)

This resembles vN, except you've wedged in the additional requirement that you have to be able to prove P, while of course being able to sneak whatever resources you like into the garbage collector that is 0.

But, critically, you've spent the token q, which means it's not available during the proof of P, so you can't execute on transition rules that represent "real" changes in the state, which will by default all participate in the token discipline of slurping up and spitting back out q's. Also while decomposing N, you've already spent the token, but this is normally how focusing on something negative on the left works -- by the time you drill down to some ^P = q * P, you'll get the token back in that branch.

Now if you want to have some rules that derive a datalog-style IDB from an EDB, then you can maybe make them at a different mode-of-truth that have different shifts that don't require token-slinging, and they will still be available during the proof of P.
Tags: logic programming, math, read-only

  • (no subject)

    Didn't sleep well. Long day of work. Dinner with akiva at hanamichi.

  • (no subject)

    K was going to do a thing for her dad's birthday, but scheduling kept slipping and slipping so I guess we're going to try doing it tomorrow instead.

  • (no subject)

    Had a pleasant lunch with paul and gabe back from working-at-facebook times. Discussed the important issues of the day, by which I mean video games…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded