Computability

Stream: combinatorial-games

[Violeta Hernández]

I've just been informed that docs#Shrink is now computable, which through a chain of events implies that our operations on games (in particular the ofSets function) are now computable.

[Violeta Hernández]

Is this anything?

[Violeta Hernández]

I don't really expect this to do much for us. There's still the underlying problem that Set carries no data (it's a function into Prop, and any term in Prop carries no data).

[Violeta Hernández]

But hey, at least we don't have to open noncomputable section all over

[Aaron Liu]

yeah this does nothing for us

[Aaron Liu]

but it's certainly more convenient to not write noncomputable everywhere

[Violeta Hernández]

https://github.com/vihdzp/combinatorial-games/pull/232

[Violeta Hernández]

Actually, there's something I realize

[Violeta Hernández]

The functor trick could be used in FGame

[Violeta Hernández]

...or maybe not

[Violeta Hernández]

def FiniteGameFunctor (α : Type) : Type :=
  Player → Finset α

open Classical in
noncomputable instance : Functor FiniteGameFunctor where
  map f s := fun p ↦ (s p).image f

[Violeta Hernández]

Finset.image requires a decidability assumption that we just don't have

[Aaron Liu]

I guess that's tricky

[Violeta Hernández]

I have a potential fix

[Aaron Liu]

you could do what DFinsupp does and make it a quotient multiset

[Violeta Hernández]

You beat me to it

[Violeta Hernández]

...I don't think that works either

[Aaron Liu]

what's wrong

[Violeta Hernández]

Let me put it like this

[Violeta Hernández]

How would you give a QPF instance for Multiset?

[Violeta Hernández]

It should be a quotient of the polynomial functor Fin, I believe

[Violeta Hernández]

Small problem

[Violeta Hernández]

How do you computably define the function (m : Multiset α) → Fin m.size → α?

[Violeta Hernández]

I might be completely misunderstanding this, but I think this problem carries over to Finset

[Aaron Liu]

it's not computable

[Aaron Liu]

uhoh

[Aaron Liu]

you should be able to compute the map into the quotient though

[Violeta Hernández]

Again, maybe I misunderstand

[Aaron Liu]

I am trying to make this work but having universe issues

[Aaron Liu]

maybe Shrink can help me

[Violeta Hernández]

Universe issues? Everything here should be fully contained within universe 0.

[Aaron Liu]

Type is in universe one

[Aaron Liu]

and I don't know what universe α is in

[Aaron Liu]

but I do know that the universe of α is not in itself

[Violeta Hernández]

Maybe try writing it down when α is in universe 0