Trade Logic pick-boolean
I initially said that the basic choice operator in TL was
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 from infinite to minimal:
pick-boolean is analogous to
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
- 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.
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.
So let's define these built-ins:
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.
pick-positive-rational, similar but picking binarily from a Stern-Brocot tree.
pick-from-bell-curve, similar but picking lazily from the standard bell curve.