Abstract
In previous work on higher-order games, we accounted for finite games of unbounded length by working with continuous outcome functions, which carry implicit game trees. In this work we make such trees explicit. We use concepts from dependent type theory to capture history-dependent games, where the set of available moves at a given position in the game depends on the moves played up to that point. In particular, games are modelled by a W-type, which is essentially the same type used by Aczel to model constructive Zermelo-Frankel set theory (CZF). We have also implemented all our definitions, constructions, results and proofs in the dependently-typed programming language Agda, which, in particular, allows us to run concrete examples of computations of optimal strategies, that is, strategies in subgame perfect equillibrium.
Original language | English |
---|---|
Article number | 114111 |
Journal | Theoretical Computer Science |
Volume | 974 |
Early online date | 2 Aug 2023 |
DOIs | |
Publication status | Published - 29 Sept 2023 |
Bibliographical note
Funding Information:We thank the anonymous referee for a number of helpful comments and questions. We would also like to thank Ohad Kammar for discussions. He also implemented [19] part of the above in the dependently typed programming language Idris [6].
Publisher Copyright:
© 2023 The Author(s)
Keywords
- Agda
- Computational game theory
- Dependent type theory
- Optimal strategies
- Selection function
- Subgame perfect equilibrium
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science