Trade Logic - what mechanisms would a system need?

The mechanisms that a Trade Logic system would need

Previously

I introduced and specified Trade Logic, and posted a fair bit about it.

Now

Here's another post that's mostly a bullet-point list. In this post I try to mostly nail down all the mechanisms TL needs in order to function as intended. Some of it, notably the treatment of selector bids, is still only partly defined.

The mechanisms that a TL system needs

• Pre-market
  • Means to add definitions (understood to include selectors and bettable issues)
    • Initiated by a user
    • A definition is only accepted if it completely satisfies the typechecks
    • Definitions that are accepted persist.
• In active market
  • Holdings
    • A user's holdings are persistent except as modified by the other mechanisms here.
  • Trading
    • Initiated by a user
    • User specifies:
      • What to trade
      • Buy or sell
      • Price
      • How much
      • How long the order is to persist.
    • A trade is accepted just if:
      • The user holds that amount or more of what he's selling.
      • It can be met from booked orders
      • It is to be retained as a booked order
    • Booked orders persist until either:
      • Acted on
      • Cancelled
      • Timed out
  • Issue conversion
    • Initiated by a user
    • User specifies:
      • What to convert from
      • What to convert to
      • How much
    • A trade is accepted just if:
      • It's licensed by one of the conversion rules
      • User has sufficient holdings to convert from
• Selectors - where the system meets the outside world. Largely TBD.
  • As part of each selector issue, there is a defined mechanism that can be invoked.
    • Its actions when invoked are to:
      • Present itself to the outside world as invoked.
        • Also present its invocation parameters.
        • But not reveal whether it was invoked for settlement (randomly) or as challenge (user-selected values)
      • Be expected to act in the outside world:
        • Make a unique selection
        • Further query that unique result. This implies that selector issues are parameterized on the query, but that's still TBD.
        • Translate the result(s) of the query into language the system understands.
        • Present itself to the system as completed.
      • Accept from the real world the result(s) of that query.
        • How it is described to the system is TBD. Possibly the format it is described in is yet another parameter of a selector.
    • How an invocable mechanisms is described to the system is still to be decided.
    • (NB, a selector's acceptability is checked by the challenge mechanism below. Presumably those selectors that are found viable will have been defined in such a way as to be randomly inspectable etc; that's beyond my scope in this spec)
  • Challenge mechanism to settle selector bets
    • Initiated by challengers
      • (What's available to pro-selector users is TBD, but probably just uses the betting mechanism above)
    • Challenger specifies:
      • The value that the choice input stream should have. It is basically a stream of bits, but:
        • Where split-random-stream is encountered, it will split and the challenger will specify both branches.
        • Challenger can specify that from some point on, random bits are used.
      • Probably some form of good-faith bond or bet on the outcome
    • The selector is invoked with the given values.
    • Some mechanism queries whether exactly one individual was returned (partly undecided).
    • The challenge bet is settled accordingly.
  • There may possibly also be provision for multi-turn challenges ("I bet you can't specify X such that I can't specify f(X)") but that's to be decided.
• Settling (Usually post-market)
  • Public fair random-bit generating
    • Initiated as selectors need it.
    • For selectors, some interface for retrieving bits just as needed, so that we may use pick01 etc without physically requiring infinite bits.
      • This interface should not reveal whether it's providing random bits or bits given in a challenge.
  • Mechanism to invoke selectors wrt a given bet:
    • It decides:
      • Whether to settle it at the current time.
      • If applicable, "how much" to settle it, for statistical bets that admit partial settlement
    • Probably a function of:
      • The cost of invoking its selectors
      • Random input
      • An ancillary market judging the value of settlement
      • Logic that relates the settlement of convertible bets. (To be decided, probably something like shares of the ancillary markets of convertible bets being in turn convertible)
    • Being activated, it in fact invokes particular selectors with fresh random values, querying them.
    • In accordance with the results of the query:
      • Shares of one side of the bet are converted to units
      • Shares of the other side are converted to zeros.
      • But there will also be allowance for partial results:
        • Partial settlement
        • Sliding payoffs

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.

Kernel WYSIWYG Digraphs

Kernel WYSIWYG rooted digraphs

Previously

I said in comments that I view backquote as a WYSIWYG tree ctor, analogous to `list'.

That's not fully general

But backquote doesn't suffice to construct the most general form of open structure of pairs, a rooted digraph. Those require the ability to share objects between multiple parents.

Things that don't do the job

One could write shared objects by naming objects in a `let' form and including them by name. That's not WYSIWYG, though. WYSIWYG would at least present the objects in place once, as #N# / #N= reader notation does.

But that's in the reader. It's not available to general code.

What to do

One could:

• Enclose the whole construction in an empty `let'.
• Provide a combiner expanding to ($sequence ($define! x DEF) x)

Signals, continuations, and constraint-handling

Signals, continuations, constraint-handling, and more

Previously

I wrote about mutability and signals and automatically forcing promises where they conflict with required types.

Signals for Constraint-handling

Constraint-handling, and specifically the late-ordered evaluation it uses, could be treated by signals. Something like this:

• Promises are our non-ground objects. They are, if you think about it, analogous to Prolog variables.
  • They can be passed around like objects.
  • But they're not "really" objects yet.
  • For them to "succeed", there must be some value that they can take.
  • That value can be determined after they are passed.
  • Everything else is either ground or a container that includes one or more of them.
• As I already do in Klink, use of an non-ground argument is detected where it's unacceptable.
  • Generally, they're unacceptable where a type is expected (eg they're acceptable as arguments to cons)
• Unlike what I do now, non-ground unacceptables send signals to a scheduler.
  • This implies that each evaluation is uniquely related to (owned by) one scheduler.
  • That signal passes as objects
    • the continuation as object.
    • The promise to be forced.
• It is the job of the scheduler to ensure that the resulting computation completes.
  • In appropriate circumstances, eg with resource-quotas, or when doing parallel searches, it is reasonable to not complete.

An analogy

Computations whose flow can't be changed are analogous to constant objects and flow-changable ones analogous to mutable ones.

Another use: Precision

This mechanism could also be useful for "dataflow" precision management. Here the objects are not exactly promises, but they are incomplete in a very precise way. They are always numbers but their precision can be improved by steps.

Combiners that require more precision could signal to their generators, which could signal back their new values, propagating back their own requirements as needed. This is very manageable.

Apply-continuation and signals can mutually define

apply-continuation, while it could be used to implement signals, can also be implemented by signals between evaluations. It signals a scheduler to schedule the given continuation and deschedule the current continuation.

Done this way, it gives a scheduler flexibility. This might appear to make analysis more difficult. But a simple (brain-dead) scheduler could do it exactly the continuation way: exactly one evaluation is "in control" at all times. This might be the default scheduler.

In both cases this functionality is a neither-fish-nor-fowl hybrid between objects and computational flow. ISTM it has to be so.

signals allow indeterminate order

One mixed blessing about signals is that since they are "broadcast" 1-to-N, it can be indeterminate what is to be evaluated in what order.

• Pro: This gives schedulers flexibility.
• Con: Computations can give different results.
  • Continuation-based scheduling doesn't neccessarily do better. It could consult "random" to determine the order of computations.
• Pro: Signals and their schedulers give us another handle to manage evaluation order dependency. A scheduler could co-operate with analysis by:
  • Promising that evaluations will behave "as if" done in some particular order.
  • Taking into account analysis
  • Providing information that makes analysis easier, short of simulating the scheduler.
    • Probably promising that no signals escape the scheduler itself, or only a few well-behaved ones do.
• Pro: Regardless of the scheduler, analysis can treat signals as a propagating fringe. Everything not reached by the fringe is unaffected.

Should signal-blockers cause copies?

I suggested earlier that combiners might promise non-mutation by blocking mutation signals out.

One way to code this is to make such combiners deep-copy their arguments. Should this situation automatically cause copies to be made? ISTM yes.

• Not an issue: User confusion. There is no case where a user reasonably expects different functionality than he gets.
  • He might expect a function to mutate an object and it doesn't - but why is he expecting that of a function that doesn't claim to mutate anything and moreover explicitly blocks that from happening? Bad docs could mislead him, but that's a documentation issue.
• Not an issue: Performance.
  • Performance is always secondary to correctness.
  • Performance can be rescued by
    • copy-on-write objects
    • immutable objects
    • Analysis proving that no mutation actually occurs.