Trade Logic pick-boolean

Trade Logic pick-boolean

Previously

I initially said that the basic choice operator in TL was pick01, which outputs a random scalar between 0 and 1.

What's wrong with pick01 as basic

It occurs to me that picking a random scalar is not the most basic thing we could do.

It also occurred to me that pick01 as defined needs to provide infinite precision, which of course isn't physically realizable.

It couldn't be sensibly defined to generate both exact 0 and exact 1.

And the fact that I forget whether its interval was left-closed or right-closed suggests that there's a problem there.

So pick-boolean

So from infinite to minimal: pick-boolean is analogous to pick01, except that it outputs a bit, not a scalar.

But it shouldn't be unary

The temptation is to make pick-boolean unary. But if we did, it wouldn't be like other unary predicates. When two instances of these pick-boolean have the same inputs (ie, none), the outputs are not neccessarily the same. This lack of referential transparency potentially infects the outputs of any predicate that uses pick-boolean. This would restrict and complicate the conversions we are allowed to make.

So instead, let's provide a system random stream. A "random output" predicate such as pick-boolean will actually be ternary; its args will be:

• Input bitstream
• Output bitstream
• Output random

This has the nice property that it gives us an upper bound on a proposition's sample space: It's the difference in position between the input stream and the output stream. Of course, that is not always predetermined.

We said earlier that bettable propositions had no arguments, and we need these to be bettable, so we have to revise slightly: A definition is bettable if its only inputs and outputs are system random streams, which will be a type.

There's another way this treatment is helpful: Sometimes we want to sample to settle issues (population bets). Such issues can sample by using the random stream argument, which feeds any selectors that are involved.

Random stream arguments also help validate selectors by challenge - the challenger specifies the bitstream. In this one case, the output bitstream is useful. It gives the various random calls an ordering, otherwise the challenger couldn't specify the bitstream.

Stream splitting

But sometimes a single stream doesn't work nicely. A predicate like pick01 may need to use arbitrarily many bits to generate arbitrary precision. So what can it do? It shouldn't consume the entire stream for itself, and it shouldn't break off just a finite piece and pass the rest on.

So let's provide split-random-stream. It inputs a random stream and outputs two random streams. We'll provide some notation for a challenger to split his specified stream accordingly.

Can't be built by users

We will provide no way to build an object of this new type from first principles. Users can get two of them from one by using split-random-stream, but can't get one from none. So the only way to have one is to get it from an input. Ultimately any proposition that uses a random stream must get it from system mechanisms of proposition resolution such as sampling and challenging.

New pieces

So let's define these built-ins:

• Type: random-stream, the type of the system's random stream. No built-in predicate has any mode that outputs this type but doesn't also input it.
• split-random-stream, ternary predicate that inputs a random stream and outputs two random streams.
• pick-boolean, a ternary predicate outputting a bit.
• Type: lazy scalar. A lazy scalar can only be compared with given precision, not compared absolutely. So any comparison predicates that take this also manage precision, possibly by inputting an argument giving the required precision.
• pick01, ternary, outputs a lazy scalar.
• Convenience
  • Maybe pick-positive-rational, similar but picking binarily from a Stern-Brocot tree.
  • Maybe pick-from-bell-curve, similar but picking lazily from the standard bell curve.