重写序列：一种范畴论解释
计算机科学中的逻辑
2015-02-17 v2 范畴论
摘要
在 Martin-Löf 内涵类型论中，同一类型是一个被广泛使用和研究的概念。原因在于它对最近发现的类型论与同伦论之间的联系起到了关键作用。同一类型最初表述时的主要问题在于它们理解和使用起来十分复杂。以此为动机，Queiroz & Gabbay (1994) 提出了一种更为简单的同一类型表述，并由 de Queiroz & de Oliveira (2013) 进一步发展。在该表述中，同一类型的元素被视为重写序列（或计算路径）。与这一新实体的逻辑规则一起，存在一个重写序列之间的归约规则系统，称为 LND_{EQS}-RWS。该系统使用标号自然演绎（即 Prawitz 的自然演绎加上“推导即项”）构建，负责确立重写序列如何被重写，从而产生新的重写序列。在此背景下，我们对该新实体提出了一种范畴论解释，将类型作为对象，重写规则作为态射。此外，我们表明我们的解释与一些已知结果相符，例如类型具有广群结构。我们还解释了更复杂的结构，例如由重写序列的重写所形成的结构。
引用
@article{arxiv.1412.2105,
title = {Sequences of Rewrites: A Categorical Interpretation},
author = {Arthur Ramos and Ruy J. G. B. de Queiroz and Anjolina G. de Oliveira},
journal= {arXiv preprint arXiv:1412.2105},
year = {2015}
}
备注
13 pages, submitted to a scientific conference (WoLLIC 2015); corrected typos; Moved part of Section 2.4 to the appendix; corrected small issues in Section 3 (typos and some compositions order), results unchanged