pgame.short

Stream: maths

[Violeta Hernández]

I don't think it's controversial that docss#pgame.short shouldn't be a class. As we've discussed before, typeclasses should only be used when most instances can be built compositionally. But since pre-games are very commonly built by induction (and hence by well_founded.fix), most instances have to be provided directly.

I do get why it was made a class though: we get some degree of computability on short games via docs#pgame.le_decidable and friends. That's why I propose the alternate approach of making a separate type for short games.

In order to avoid having to copy a lot of API, we could simply define short pre-games as a subtype of pre-games, satifsying the current definition of pgame.short. We can then provide these same decidability instances on the subtype.

[Violeta Hernández]

Now on this note, we had previously noticed that the current definition of short doesn't line up with the mathematical one. Proposition 4.9 of Schleicher-Stoll shows that a pre-game is short iff it has a finite birthday, but this isn't true with the current definition: the pre-game with infinitely many copies of 0 as left moves is not short by our definition, but has birthday 1. So if we're going to refactor this bit of the code, maybe we should go all the way.