Higher-order Games with Dependent Types

TL;DR

This paper introduces a formal framework for modeling history-dependent higher-order games using dependent types, explicitly representing game trees and enabling computation of optimal strategies in Agda.

Contribution

It makes the implicit game trees explicit using dependent type theory and models history-dependent games with a W-type, implemented in Agda for concrete strategy computation.

Findings

Explicit game trees improve modeling of history-dependent games.

Implementation in Agda allows computation of subgame perfect equilibria.

Framework generalizes previous continuous outcome function approaches.

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.