论文标题
具有依赖类型的高阶游戏
Higher-order Games with Dependent Types
论文作者
论文摘要
在以前的高阶游戏中的工作中，我们通过使用连续的结果功能来考虑有限长度的有限游戏，这些功能携带了隐性的游戏树。在这项工作中，我们明确地使这样的树木。我们使用依赖类型理论的概念来捕获与历史相关的游戏，在该游戏中，在游戏中给定位置的一组可用移动取决于到达这一点上的动作。特别是，游戏是由W型建模的，W型基本上与Aczel用于建模建设性Zermelo-Frankel Set理论（CZF）相同。我们还在相关的编程语言AGDA中实施了所有定义，构造，结果和证明，特别是使我们能够运行最佳策略计算的具体示例，即子游戏中完美平衡中的策略。
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.
