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)

    ljdump finally managed to get all my posts, after about 24 hours continuously downloading them at a slow enough rate to not anger livejournal, but it…

  • (no subject)

    Anybody still here have any decent solutions for lj backup? I've tried pieces of code I've found in ruby, javascript, perl, go, and python, and…

  • (no subject)

    Aha, I thought that LJ was failing to send me comment notifications, but what actually happened was CMU's spam filtering started catching them all as…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded