User:IssaRice/Logical inductor construction: Difference between revisions
Line 83: | Line 83: | ||
What's up with the then-clause? Does it even trigger? | What's up with the then-clause? Does it even trigger? | ||
For the inf expression in the else-clause: the fact that we're in the else-clause means that for <math>n-1</math> in particular, the sum <math>\mathbb W(\sum_{i \leq n-1} T_i(\mathbb P_{\leq i})) > -b</math>. So the denominator <math>\mathbb W(\sum_{i \leq n-1} T_i(\mathbb P_{\leq i})) + b > 0</math>. | For the inf expression in the else-clause: the fact that we're in the else-clause means that for <math>n-1</math> in particular, the sum <math display="inline">\mathbb W(\sum_{i \leq n-1} T_i(\mathbb P_{\leq i})) > -b</math>. So the denominator <math display="inline">\mathbb W(\sum_{i \leq n-1} T_i(\mathbb P_{\leq i})) + b > 0</math>. | ||
==Lemma 5.2.2 (Properties of Budgeter)== | ==Lemma 5.2.2 (Properties of Budgeter)== |
Revision as of 21:32, 29 June 2019
Notes from the Logical Induction paper as I walk through the construction of LIA in section 5.
Lemma 5.1.1 (Fixed Point Lemma)
"Observe that is equal to the natural inclusion of the finite-dimensional cube in the space of all valuations ." -- I think what this is saying is that since , we can think of as being sort of a subset of . Except it's not strictly speaking a subset, since the functions in and have different domains. How can we make it a subset? The "natural" way to do this is to set everything outside of to zero. But that's exactly what is. One thing I'm still not sure about is the "finite-dimensional" part; doesn't having make the cube infinite-dimensional?
Definition of fix: I found it helpful to look at the graph of ; this looks like the identity function in the interval , but then becomes constant once it hits either of the endpoints. If you've already thought about the definition of continuous threshold indicator (definition 4.3.2), then you will recognize that .
"the compact, convex space " -- this intuitively makes sense, since basically "looks like" a cube. But I'm not sure how to verify this.
For the fixed point reasoning: we don't actually have a fixed point of ; instead, it's a fixed point of , where and . If , then the graph of is just the graph of but shifted to the left. You will see that this intersects the graph of the identity function at ; this is the fixed point. On the other hand, if , then we shift the graph of to the right, and now the fixed point is at .
The key property of that we use in the proof:
- If buys a share of on day , then the price of on day is 1 (the maximum possible).
- If sells a share of on day , then the price of on day is 0 (the minimum possible).
One question to ask is, couldn't we just avoid using Brouwer's fixed point theorem by just setting the prices to obey the above property? There are two problems with this. One is that the definition of the th day prices would depend on 's behavior, which depends on the th day prices! So the definition would be circular. The other problem is that we can't guarantee that the map would be continuous if we just magically set it to obey some property.
Something else I got confused about: I was thinking that the above key property only talks about day . Couldn't the trader make a lot of money on previous days, and then just make no money on day , so that it would still be making lots of money? The answer is that we are only dealing with a trading strategy in this lemma, not a full trader. Later, in lemma 5.1.3, we recursively use this idea to deal with a full trader.
How do we come up with the definition of fix? Here's one way to think about it. Let be the market price (of some sentence on day ) and be the trading volume of that sentence on the same day. We want to return some quantity that fixes up the price, after the fact, so that the trader would have earned less money. Why after the fact? Because doing it in real time is confusing! The trader depends on the prices for day n, which is what we want to decide. But we want to know what the trader does on day n in order to determine the prices. So there is a circular dependency. This sort of thing happens in game theory too, where everything does eventually take place in real time, but we can think iteratively by "pressing pause" and considering counterfactuals and going down different paths in the game tree. Here is another way to think about it. We get an infinite number of "retries". We first set the price to something arbitrary. Then we get to see what the trader would do in that situation. Ah, it buys some shares, making money in expectation. We want to prevent that, so we pretend that wasn't the real market price, and see what the trader does in the new, adjusted price. It's also a hint that fixed points are going to appear. Ideally we would like to say something like:
This will work, but it's after the fact. We eventually would like to fix the prices in real time. So one way to think about this is to adjust the prices a little at a time, querying the trading strategy each time to see if we should nudge the prices up or down. Here is one idea:
where is some small adjustment. In other words, if a trader buys at the current price, then nudge it up a little to make it a slightly worse deal for the trader. And if the trader sells at the current price, then nudge it down. Now, there are three problems with this map. As a function of , it's still discontinuous (ugly). Also, we don't check whether the values we return stay within the allowed interval of valuations. But most importantly, if we only adjust the prices a little, that means the trader can still make money from us. So what can we do? Well, we can apply the map many times: (actually, maybe we should allow the s to change as well, to react in response). Now it's like a turn-based game: the trader says he's going to buy, so we adjust up; the trader still says he's buying, so we adjust up again; the trader now says he's going to sell, so we adjust down (oops, now we're in exactly the same spot, leading to an infinite loop...).
We can fix the second problem above with the following:
Now if the prices go out of bounds, they get adjusted back to the bound, but otherwise they are unaffected.
Let be a trading strategy that takes the price of a sentence and outputs how much it would trade at that price. So then we start with some price , which gets fed into to get . Then we have the next price . And the next trade volume is and so on. So we get .
So what can we do to avoid the infinite loop? One idea might be to decrease the step size with time (the number of iterations). This sort of thing is reminiscent of some versions of gradient descent. Another idea is to make the step size a function of : if the trader trades a lot, then we adjust a lot, but if the trader trades only a little, it signals that we're getting close to ... a fixed point!
This turns out to be equivalent to , which is the form of fix given in the paper. To see this, just split into cases based on , , or . The version in the paper makes it obvious that the function is continuous, but it is more difficult to see what is going on.
We want some such that , i.e. we are satisfied with the price so that we don't try to change it. Thanks to both being continuous, this is guaranteed by Brouwer's fixed point theorem.
We imagined that we were working with just one sentence, but it turns out that (for some reason) basically the same thing works when dealing with all sentences.
Another thing to wonder is that the rate of adjustment is just . What if we did instead? or ? or ? It seems like these would change the slope of the graph of , which means we might introduce more fixed points (just graph the identity function with the new functions); one of the nice things about slope=1 is that it is parallel to the identity function, so we get exactly one fixed point, or infinitely many. Actually, the scalar on x is still 1, so this probably doesn't matter.
The following is used in the Fixed Point Lemma (5.1.1):
Writing the -strategy as
we have
But so the two sums cancel to obtain .
Definition/Proposition 5.1.2 (MarketMaker)
Define by (this is the same map given in the proof).
Let's see what does to . By the Fixed Point Lemma, for any we have . This means that as we max over these worlds, we will never exceed 0. So . Or in other words . (I had two confusions here: first, for some reason I mistakenly thought was negative for a while, so got confused about why was always contained in the interval. Second, I wondered why the left endpoint was minus infinity; couldn't any negative number also work? it couldn't, because we don't know how negative the trader could be; in other words, the trader could perform arbitrarily badly and we don't have a lower bound on that.)
"Hence there is some neighborhood in around with image in ." -- This uses one of the equivalent definitions of continuity (often called the topological definition of continuity), namely, is continuous iff for every open set such that , there exists an open set such that and . Here we know that is open and . So there exists an open set such that and .
One thing I'm unclear on is, are we using a metric on ? If so, what is the metric?
Lemma 5.1.3 (MarketMaker Inexploitability)
This proof is pretty simple.
We use the geometric series . (Then subtract since index starts at 1 rather than 0.)
Definition/Proposition 5.2.1 (Budgeter)
Why does Budgeter get all of ? It seems to use only up to .
What's up with the then-clause? Does it even trigger?
For the inf expression in the else-clause: the fact that we're in the else-clause means that for in particular, the sum . So the denominator .
Lemma 5.2.2 (Properties of Budgeter)
Part 1
If the trader never overspends, then budgeter does nothing.
Part 2
If we inductively alter the trader on every single day, then we never overspend.
Part 3
If the trader can exploit the market, then we can give it the budget it needs so that it can do its thing.