Current browse context:
cs.GT
Change to browse by:
References & Citations
Computer Science > Computer Science and Game Theory
Title: Higher-order Games with Dependent Types
(Submitted on 15 Dec 2022 (v1), last revised 7 Jul 2023 (this version, v2))
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 equilibrium.
Submission history
From: Paulo Oliva [view email][v1] Thu, 15 Dec 2022 11:34:57 GMT (58kb)
[v2] Fri, 7 Jul 2023 12:38:50 GMT (26kb)
Link back to: arXiv, form interface, contact.