Martin-Löf 类型论的游戏语义
计算机科学中的逻辑
2021-06-18 v7 逻辑
摘要
我们为 Martin-Löf 类型论 (MLTT) 提出一种新的游戏语义，旨在给出 MLTT 的数学化与内涵性解释。具体而言，我们提出一种基于新型游戏变体的族范畴，该范畴可诱导对内涵式 MLTT 的满射与单射（当排除 Id-类型时）解释，该 MLTT 配备单位类型、空类型、N-类型、依赖积、依赖和、Id-类型以及宇宙的累积层级，据我们所知，这在文献中尚属首次，尽管满射性仅通过对某一类游戏与策略的归纳定义来实现。我们的游戏推广了现有的游戏概念，并以直观而数学上精确的方式实现了对依赖类型和宇宙层级的解释，我们的策略可视为 MLTT 中程序（或证明）背后的算法。对 Id-类型更精细的解释留待未来工作。
引用
@article{arxiv.1610.01669,
title = {Game Semantics for Martin-L\"of Type Theory},
author = {Norihiro Yamada},
journal= {arXiv preprint arXiv:1610.01669},
year = {2021}
}
备注
This paper has been withdrawn by the author due to a crucial error on linear implication between games