论文标题
宇宙的游戏语义
Game semantics of universes
论文作者
论文摘要
这项工作将当前作者的Martin-Löf类型理论的计算游戏语义扩展到了宇宙的累积层次结构。该扩展名在30年的现代游戏语义历史上首次完成了所有标准类型的Martin-Löf类型理论的游戏语义。结果，游戏语义的强大组合推理可用于研究宇宙和类型的研究。实现宇宙游戏语义的主要挑战是身份类型与宇宙之间的冲突：通过宇宙对身份类型进行编码的天真游戏语义引起了关于功能之间平等的决策程序，这是对回归理论中众所周知的事实的矛盾。我们通过新颖的游戏来克服这个问题的宇宙，这些游戏在不决定平等的情况下编码游戏类型的游戏。
This work extends the present author's computational game semantics of Martin-Löf type theory to the cumulative hierarchy of universes. This extension completes game semantics of all standard types of Martin-Löf type theory for the first time in the 30 years history of modern game semantics. As a result, the powerful combinatorial reasoning of game semantics becomes available for the study of universes and types generated by them. A main challenge in achieving game semantics of universes comes from a conflict between identity types and universes: Naive game semantics of the encoding of an identity type by a universe induces a decision procedure on the equality between functions, a contradiction to a well-known fact in recursion theory. We overcome this problem by novel games for universes that encode games for identity types without deciding the equality.
