set_theory/game

Stream: general

[Yury G. Kudryashov]

What do you think about moving set_theory/game to something like set_theory/conway_game (and possibly renaming the types)?

[Yury G. Kudryashov]

(probably, after port)

[Yury G. Kudryashov]

My motivation is simple: there are many notions of a "game", and docs#game is not the most widely known.

[Patrick Massot]

Does that remark applies even within the context of a folder named set_theory?

[Yury G. Kudryashov]

Not sure about the folder name but using the name game in the root namespace seems a little bit too ambitious.

[Yury G. Kudryashov]

I mean, there are games on graphs (several players take turns etc; with probabilities or not), games in social choice theory etc.

[Yury G. Kudryashov]

Also, the module docstrings can take a little about other notions of games and how docs#game is (not) related to them (and why it is called a "game").

[Patrick Massot]

Indeed this has nothing to do in the root namespace.

[Yury G. Kudryashov]

I see that the module docstring of file#set_theory/game/pgame has more text

[Kevin Buzzard]

As well as Conway games there are the games which show up in the axiom of determinacy (which is very much set theory, indeed it contradicts the axiom of choice), which says that for every game (in a totally different sense to Conway) one of the players has a winning strategy

[Jon Eugster]

Yury G. Kudryashov said:

What do you think about moving set_theory/game to something like set_theory/conway_game (and possibly renaming the types)?

Is there already a PR for this? I'd create one myself otherwise, I need Game available in the root namespace :sweat_smile:

[Jon Eugster]

#6365