关于计算路径与类型的基本广群
计算机科学中的逻辑
2015-09-23 v1
摘要
这项工作的首要目标是研究计算路径的数学性质。计算路径最初由 de Queiroz & Gabbay (1994) 提出作为‘重写序列’，可被视为两个计算对象之间命题等式成立的基础。利用计算路径与范畴语义，我们取类型论中的任意类型 并为该类型构造一个广群。我们称此广群为类型 的基本广群，因为它类似于利用恒等类型的同伦解释所获得的广群。主要区别在于，计算路径不是单纯的语义解释，而是类型论语法中的实体。我们还扩展了结果，使用计算路径构造更高层级的基本广群。
引用
@article{arxiv.1509.06429,
title = {On Computational Paths and the Fundamental Groupoid of a Type},
author = {Arthur F. Ramos and Ruy J. G. B. de Queiroz and Anjolina de Oliveira},
journal= {arXiv preprint arXiv:1509.06429},
year = {2015}
}
备注
15 pages, submitted to LFCS