范畴中的非良基树
摘要：非良基树在数学和计算机科学中被用于建模非良基集合，以及非终止的进程或无限的数据结构。范畴论上，它们作为多项式自函子的最终余代数，我们称之为M类型。为了对树进行推理，我们需要路径的概念，它可以在具有自然数对象的任何局部笛卡尔闭前拓扑的内部逻辑中形式化。在这样的范畴中，我们推导出关于M类型的存在结果，从而导致具有自然数对象和M类型在切片、余代数形成(对于笛卡尔余单子)和内部站点的剪枝下的局部笛卡尔闭前拓扑的稳定性。
作者：Benno van den Berg and Federico de Marchi
论文ID：math/0409158
分类：Category Theory
分类简称：math.CT
提交时间：2007-05-23