Higher-order games with dependent types

Martín Escardó, Paulo Oliva*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

55 Downloads (Pure)

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 languageEnglish
Article number114111
JournalTheoretical Computer Science
Volume974
Early online date2 Aug 2023
DOIs
Publication statusPublished - 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

Fingerprint

Dive into the research topics of 'Higher-order games with dependent types'. Together they form a unique fingerprint.

Cite this