Trade Logic pickboolean
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 leftclosed or rightclosed suggests that there's a problem there.
So pickboolean
So from infinite to minimal: pickboolean
is analogous to pick01
,
except that it outputs a bit, not a scalar.
But it shouldn't be unary
The temptation is to make pickboolean
unary. But if we did, it
wouldn't be like other unary predicates. When two instances of these
pickboolean
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
pickboolean
. 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 pickboolean
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 splitrandomstream
. 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
splitrandomstream
, 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 builtins:

Type:
randomstream
, the type of the system's random stream. No builtin predicate has any mode that outputs this type but doesn't also input it. 
splitrandomstream
, ternary predicate that inputs a random stream and outputs two random streams. 
pickboolean
, 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
pickpositiverational
, similar but picking binarily from a SternBrocot tree. 
Maybe
pickfrombellcurve
, similar but picking lazily from the standard bell curve.

Maybe
No comments:
Post a Comment