@Tyra Burgess and I wrote down a royalty-aware payout function yesterday:
For a type B, let L(B) be the “left closure under implication” or the admissible antecedents. I.e., the set of all the antecedents A in the public ledger such that A→B. p:Type→Money is the price that a proposition was listed for (admitting summing over duplicates). Suppose player 1,...,k have previously proven B1,...,Bk and L(A) is none other than the set of all Bi from 1 to k.
We would like to fix an ϵ (could be fairly big, like 15) and say that the royalty-aware payout given epsilon of A upon an introduction of α:A to the database is p(A)×(1−ϵ) such that, where k=|L(A)|, p(A)×ϵk is paid out to each player i∈1,...,k.
This seems vaguely like it has some desirable properties, like the decay of a royalty with length in implications separating it from the currently outpaying type. You might even be able to reconcile it with cartesian-closedness / currying, where A×B→C behaves equivalently to A→B→C under the payout function.
I think to be more theoretically classy, royalties would arise from recursive structure, but it may work well enough without recursion. It’d be fun to advance all the way to coherence and incentive-compatible proofs, but I certainly don’t see myself doing that.
@Tyra Burgess and I wrote down a royalty-aware payout function yesterday:
For a type B, let L(B) be the “left closure under implication” or the admissible antecedents. I.e., the set of all the antecedents A in the public ledger such that A→B. p:Type→Money is the price that a proposition was listed for (admitting summing over duplicates). Suppose player 1,...,k have previously proven B1,...,Bk and L(A) is none other than the set of all Bi from 1 to k.
We would like to fix an ϵ (could be fairly big, like 15) and say that the royalty-aware payout given epsilon of A upon an introduction of α:A to the database is p(A)×(1−ϵ) such that, where k=|L(A)|, p(A)×ϵk is paid out to each player i∈1,...,k.
This seems vaguely like it has some desirable properties, like the decay of a royalty with length in implications separating it from the currently outpaying type. You might even be able to reconcile it with cartesian-closedness / currying, where A×B→C behaves equivalently to A→B→C under the payout function.
I think to be more theoretically classy, royalties would arise from recursive structure, but it may work well enough without recursion. It’d be fun to advance all the way to coherence and incentive-compatible proofs, but I certainly don’t see myself doing that.
Sounds somewhat like a bucket brigade market economy.