依赖类型论中良基树的拓扑对应物
计算机科学中的逻辑
2024-02-14 v2
摘要
在依赖类型论中,我们利用在形式拓扑中以归纳生成基本覆盖之名引入的归纳生成上格概念的一个证明相关版本,给出了良基树(简称 W 类型)的一个拓扑对应物。更具体地,我们首先证明,在同伦类型论中,W 类型与证明相关的归纳生成基本覆盖在命题上可相互编码。其次,我们证明在 intensional Martin-Loef 类型论的 Agda 实现中,它们在定义上可相互编码。最后,我们在极简基础(Minimalist Foundation)框架中重构该等价,通过引入良基谓词作为依赖 W 类型谓词的逻辑对应物。所有结果均已在 Agda 证明辅助器中验证。
引用
@article{arxiv.2308.08404,
title = {A topological counterpart of well-founded trees in dependent type theory},
author = {Maria Emilia Maietti and Pietro Sabelli},
journal= {arXiv preprint arXiv:2308.08404},
year = {2024}
}
备注
To be published in the post-proceedings of the 39th Conference on Mathematical Foundations of Programming Semantics