Jason (jcreed) wrote,

Tried to twelf up a proof about encoding focusing in FOL. I thought it should have been "easy", since it doesn't really involve any substructural or algebraic or relational weirdness, but hit a bunch of early snags nonetheless. Probably need to cobble together a slightly nontrivial termination metric, and I'm experiencing some really bizarre coverage errors that I can't understand in terms of the paper proof. Often as not these sort of things point to some actual coverage problem in the proof, but I've stared really hard and I can't see it.

I had some other old thoughts stirred up by thinking about bitcoin and its recent explosive growth in market value; as much as that is prima facie good news for people that are long bitcoin, I hear tell volatility is considered a bad quality in a putative measure of value.


So, okay, how could one engineer a good measure of value? A naive proposal is to take the median of the prices of a big collection of quantities of commodities. Right now the price of each of {100 lbs of apples, 50 lbs of eggplant, 20 lbs of dates} is about $100, so the median is also $100. If the price of apples shoots up or down, (and eggplants and dates don't change) the median stays the same. So maybe volatility decreases if you median together more things?

The thing that made this measure seem interesting to me (in contrast to, like, the CPI or something which is a sum of prices of a basket of goods) was the fact that you can still realize median as a contract in the sense of that classic SPJ paper on "composing contracts" in a functional programming language.

Suppose there's two goods G1 and G2 of value V1 and V2. If you want to give me an amount of value equal to max(V1, V2), you promise me a G1 or a G2 of my choosing. If you want to give me an amount of value equal to min(V1, V2), you promise me a G1 or a G2 of your choosing. These functions suffice to find the median of any list because you can just take a sorting network and interpret each compare-and-swap edge as a circuit element that takes V1 and V2 and outputs min(V1, V2) and max(V1, V2). Then there's some expression on the output wire exactly half-way down the bundle of wires, which is an expression over all the Vs and mins and maxes, which is essentially a game-tree that you play with your counterparty that ends in them giving you some good.

And then I wandered off thinking about whether their little combinator language is actually a linear logic secretly and mumble pi calculus mumble and donno.
Tags: focusing, math, twelf

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded