Martin-Löf类型论的博弈语义
逻辑
2021-06-08 v5 计算机科学中的逻辑
摘要
我们提出了Martin-Löf类型论（MLTT）的新博弈语义，该类型论配备有One类型、Zero类型、N类型、Pi类型、Sigma类型和Id类型。我们的博弈语义比现有语义更准确地解释了MLTT。与现有语义相比，我们的博弈语义的另一个优势在于其对Sigma类型的解释是直接的，并且与积类型的博弈语义兼容。此外，其数学结构新颖且有用；例如，我们博弈的范畴具有所有有限极限，这是将当前工作扩展到同伦类型论的关键步骤，并且我们的博弈首次在博弈语义中解释依赖类型上的子类型。最后，我们提供了一个新的博弈语义证明，证明了马尔可夫原理独立于MLTT，这展示了我们的博弈语义相对于MLTT的外延模型（如有效拓扑斯）的优势。
引用
@article{arxiv.1905.00993,
title = {Game Semantics of Martin-L\"of Type Theory},
author = {Norihiro Yamada},
journal= {arXiv preprint arXiv:1905.00993},
year = {2021}
}