内涵等价性的博弈论探究
计算机科学中的逻辑
2017-05-04 v3
摘要
本文为马丁-洛夫类型论（MLTT）提出一种新的博弈语义，其中每个博弈都配备选定的同构策略，这些策略代表博弈上策略之间（内涵）等价的（计算）证明。这些同构策略解释 MLTT 中的命题等价。作为主要结果，我们获得了 MLTT 的第一个博弈语义，它反驳了身份证明唯一性原理（UIP）并验证了单值性公理（UA），尽管它并未建模非平凡的高阶等价。从范畴论角度看，我们的模型构成了 Hofmann 和 Streicher 经典 MLTT 广群模型的一个子结构。类似于从广群模型到 ω-广群模型的路径，我们计划推广该博弈语义以产生 ω-广群结构，从而解释同伦类型论（HoTT）中的非平凡高阶等价。
引用
@article{arxiv.1703.02015,
title = {Game-theoretic Investigation of Intensional Equalities},
author = {Norihiro Yamada},
journal= {arXiv preprint arXiv:1703.02015},
year = {2017}
}
备注
arXiv admin note: text overlap with arXiv:1610.01669