Karl Palmskog (Sep 11 2020 at 18:04): Karl Palmskog (Sep 11 2020 at 18:04):given that I dug up some old game theory results, I was thinking of writing an ongoing thread in the Coq Discourse about "current status of game theory in Coq". For example, there is https://arxiv.org/abs/0705.3316 by Le Roux from 2007 which has no links to code. @Erik Martin-Dorel do you know if this code/paper is superceded by https://arxiv.org/abs/1709.02096 (GandALF 2017 paper)?
Erik Martin-Dorel (Sep 11 2020 at 18:13):Hi @Karl Palmskog good question, actually the answer is no: both papers deal with Nash equilibria (probably the most typical solution concept in game theory) but the GandALF 2017 paper https://arxiv.org/abs/1709.02096 is actually a follow-up (and a dual formalization (in Coq+Isabelle) of part) of the following article: http://dx.doi.org/10.1002/malq.201300034
BTW we are precisely working on an extension of the GandALF 2017 paper which could lead to a new release of our Coq and Isabelle formalizations ;)
(currently, the GandALF 2017 code was only available on my IRIT webpage: https://www.irit.fr/~Erik.Martin-Dorel/winning2ne/)
Karl Palmskog (Sep 11 2020 at 18:17):@Erik Martin-Dorel thanks, and how large is the gap to the work by Stewart et al. (e.g., https://jfr.unibo.it/article/view/7235 and https://github.com/gstew5/games), do you use similar definitions? It seems you and them are both using MathComp, at least.
Erik Martin-Dorel (Sep 11 2020 at 18:50):@Karl Palmskog good question again :) so Stewart et al.'s library is available at https://github.com/gstew5/games as well as in opam, both libraries use MathComp but the two main differences lie in the choice for modelling the games themselves, and the overall aim:
* The games library use less dependent types (in particular, the definition of a game assume the "actions" (aka "strategies") for all players are taken in the same codomain T, albeit some actions are not admissible… which is modelled by means of a relation move that describes admissible moves between strategies) and uses realFieldType-valued outcomes (aka "costs");
* while in the winning2ne library we focused on providing first the most generic definitions (with arbitrary outcomes and dependently-typed strategies (which as always, can introduce some "dependently-typed technicalities")):
Variables (Agt : Type) (Strat : Agt→Type) (Outc : Type).
Definition strategy := ∀a : Agt, Strat a.
[…]
* In winning2ne we specifically worked on formalizing [LeRoux 2014], instantiating the general definitions above with 2-player multi-outcome games, to formalize LeRoux's Nash equilibria transfer theorem, after introducing e.g. the notion of determinacy.
* While games rather aims at being a general-purpose library AFAICT, providing a nice, comprehensive library of many results in game theory.
BTW I have precisely started developing a small theory attempting to "bridge the gap" between the two games definitions, e.g. to be able later on, to port one theorem already available in one library to the other; assuming obviously that the result can be expressed in both contexts! (but this development is still work-in-progress)
Karl Palmskog (Sep 11 2020 at 18:53):@Erik Martin-Dorel very nice comparison, do you mind if I sum this up in a Discourse post and lift some stuff verbatim?
Erik Martin-Dorel (Sep 11 2020 at 18:55):no worries, please do! :)
BTW, are you specifically interested in game theory in general, or maybe in specific results?
Karl Palmskog (Sep 11 2020 at 18:56):I was interested in what has been done so far, not really any specific results. Mainly due to my ongoing work on blockchains
Karl Palmskog (Sep 11 2020 at 19:00):it looks like auction theory is not covered so well at present, this is a bit unfortunate since I think this is where Coq constructivity actually makes a lot of sense (verified algorithms). I'm sure somebody somewhere is already doing work in this direction though.
Erik Martin-Dorel (Sep 11 2020 at 19:03):yes indeed
Karl Palmskog (Sep 12 2020 at 13:17):unfortunately games doesn't work with Coq 8.12 / MC 1.11, e.g., fails on 8.11+MC-1.11.
Karl Palmskog (Sep 14 2020 at 10:16):yesterday, I managed to track down (and port to recent Coq) 3 out of 4 old game theory Coq developments. Those 4 together with winning2ne and games seem to be everything there is on Coq. Beyond Coq, there is also the work by Parsert and Kaliszyk in Isabelle. Waiting for some info on the missing 4th, then I will probably put everything on GitHub.
Karl Palmskog (Sep 17 2020 at 13:22):ah, got them all now working on at least 8.10 to 8.12:
Now just to add some metadata/CI, probably over the weekend
Last updated: Oct 13 2024 at 01:02 UTC