Trade logic: Objects are sampleable

All objects are sampleable

I mentioned earlier in passing that in trade logic, all things are sampleable. As I put it, "all variables are ultimately instantiatable".

Things can be finite sets of objects with some probability distribution over them. They can be trivially sampleable, such as single objects, where sampling them always gives the same object. It's even possible that they may measureable collections that have no distinct individuals, from which one selects measured extents.

And the time has come to nail down how Trade Logic is to do sampling (selection).

Population bets

Built-in predicate pick01

For a population to be sampled, we need some sort of random input, and it can't be vague where to get the random or how to use it. The purpose of pick01 is to provide the random parameters that sampling will use.

(pick01 +A) binds A to a real number between 0 and 1, lower-inclusive. Theoretically, A has infinite precision. In practice, precision should be provided lazily. There may need to be some provision against allowing requests for precision to tie up the system.

Settling population bets

I'll call a bet whose formula uses pick01 (explicitly or implicitly) a population bet. Population bets are useful for propositions that can easily be resolved for individuals but less easily for distributions.

Population bets that are trying to be resolved1 can pick particular individuals to resolve. Then they can settle probabilistically on the basis of that. It's basically using statistics.

The procedure for selecting an individual is to:

• independently choose a value for each pick01 directly or indirectly included in the proposition.
• Using those values, assess the issue's truth or falsity. (The Bettable selectors logic below should ensure that this step works)
• Repeat as wanted. We sample with replacement; for simplicity and generality, there is no provision for not looking at the same individual again.
• Using statistical logic (outside the scope here), settle the bet (maybe sometimes just partly settle it)

Selector bets

Of course randoms on the unit interval are not the only kind of random selection one might want. We have to build all sorts of selectors from them. At the same time, we want selection to be uniquely resolved. It won't do for a given selector to select more than one individual for the same randoms, or to select no individual at all.

So I introduce a different sort of bet: selector bets. They are bets that a given selector "works OK".

Any predicate that has only outputs can be the basis of a selector bet. In my current thinking, for each such bet, every output of the predicate would be associated with an equivalence predicate. That's needed so we have a principled way to distinguish individuals.

Unlike issues, the bet is asymmetric and its interpretation is adversarial: One side (challengers) tries to pick values for pick01 that they think give no result or too many results. The other side is betting that no such problems arise. I haven't fleshed out the exact rules for this.

best redux

It seems that I didn't adapt epsilon enough when I borrowed it as best. It doesn't make a sampleable output. Rather, its output is the set of all the most suitable objects in the universe. That's not neccessarily finite, much less measureable. So there's no good general distribution over that. It would be paradoxical if there were.

So best needs another parameter: a sampleable collection of objects. That can be any object in Trade Logic. This parameter will generally be quite boring; often it's simply the whole universe of discourse. Nevertheless, it's needed.

So =(best Pred From To)=² is now true just if:

• Pred is a unary predicate
• To is the part of From that satisfies Pred as well as anything else in From does

NB, I have not called To a "member" of From, as if From were a set. In general, From is a collection. To should be collection in general too. And we don't want to need an identity predicate as another parameter. And finally, we don't try to resolve "sub-part boundaries" here; those are addressed via structurally similar bets that replace calls of best with suitable particularizations. Nevertheless, I am not 100% sure I have supported collections adequately in this mechanism.

Footnotes:

¹ When a bet is "trying to be resolved" is beyond the scope here, but I have some ideas on the topic.

² I took the opportunity to put the arguments into in/out order.