April 4th, 2013

beartato phd

(no subject)

Oh huh you can also really easily make a contract whose value is the geometric mean of two assets. Interestingly, I don't know how to encode this into the Peyton-Jones/Eber/Seward framework. Here's how it goes:

"I, the undersigned, promise to deliver, at any time my counterparty requests, a quantity X of shares of XCision and a quantity Y of shares of YonedaCo such that X * Y = 1000"

Suppose Alice gives Bob that contract, and Bob calls Alice on it and asks for his shares. What does Alice do? Making the simplifying assumption of infinite market depth, that XCision and YonedaCorp just have share prices p_X and p_Y that aren't affected by Alice buying stock, Alice wants to choose an X such that

X p_X + (1000 / X) p_Y

is minimized. So we set the derivative to zero,

0 = p_X - (1000 / X^2)p_Y

and discover

X = sqrt(1000(p_Y / p_X))

and so the total amount of value Alice gives to Bob is

sqrt(1000(p_Y / p_X)) p_X + (1000 / sqrt(1000(p_Y / p_X))) p_Y

= 2 sqrt(1000 p_X p_Y)

which is proportional to the geometric mean of the prices of the two original assets, as required.


and the "median of a basket of goods" game from yesterday admits a stupidly simple direct description.

Alice and Bob take turns choosing elements of the basket of goods to eliminate, and the last one left, Alice must give one of those to Bob. It's always in Alice's best interest to choose the most expensive remaining item, and it's always in Bob's best interest to choose the cheapest; what remains is the median.
beartato phd

(no subject)

Talked some more with Rowan today in which I discovered the fascinating fact that the modal Diamond in "Pfenning-Davies K" according to the recent "Weather Report" draft is not quite what I would have predicted from the modal encoding I worked out with Sean last summer. A shibboleth proposition is:

<><>0 |- <>0

which my system (given a krikpe relation with no particular properties) will nonetheless prove, and which Pfenning-Davies K does not.

This is because their <>L rule is like

A |- C
G, <>A |- C poss

and mine turns out to be something way weirder, which is close to being like

A |- poss
G, <>A |- C poss

with some sort of abomination where the conclusion is poss (thus permitting further <>L decompositions) but there's nothing there, so my system still does refuse to prove

<><>A |- <>A

in general, just like you'd expect from K.