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.

翻译：在先前关于高阶博弈的研究中，我们通过使用携带隐式博弈树的连续结果函数，处理了无界长度的有限博弈。在本研究中，我们显式化这类博弈树。我们运用依赖类型论的概念来刻画历史依赖博弈——即博弈中特定位置处可用移动的集合取决于在此之前已完成的移动。具体而言，博弈通过W-类型建模，该类型本质上与Aczel用于建模构造性策梅洛-弗兰克尔集合论（CZF）的类型相同。我们还在依赖类型编程语言Agda中实现了所有定义、构造、结果与证明，这尤其使我们能够运行最优策略（即子博弈完美均衡策略）计算的具体实例。