依赖类型的博弈
计算机科学中的逻辑
2015-08-21 v1
摘要
我们提出了一个依赖类型论（DTT）模型，包含 Pi-、1-、Sigma- 和内涵 Id-类型，该模型基于 AJM-博弈与无历史获胜策略范畴的一个微小变体。该模型满足 Streicher 的内涵性准则并反驳了函数外延性。同一性证明的唯一性原理得到满足。我们证明它包含一个作为全子范畴的子模型，该子模型给出了包含 Pi-、1-、Sigma- 和内涵 Id-类型以及有限归纳类型族的 DTT 的忠实模型。这个较小的模型在不使用 Id-类型构建的类型层级上，以及在我们允许 Id-类型严格出现一次的类型类上，相对于语法是完全（且忠实）完备的。包含 Id-类型的完整类型层级的可定义性仍有待研究。
引用
@article{arxiv.1508.05023,
title = {Games for Dependent Types},
author = {Samson Abramsky and Radha Jagadeesan and Matthijs Vákár},
journal= {arXiv preprint arXiv:1508.05023},
year = {2015}
}
备注
revised version of ICALP 2015 publication