一句话：提出基于二阶代数理论的循环数据类型框架，提取 fold 规则并证明强正规化、Church-Rosser 模双模拟及等式可判定性。
循环数据结构（如循环列表）因环状共享而难以处理。本文研究循环数据类型的范畴、代数与计算基础，采用 Fiore 等人的二阶代数理论统一描述其语法、类型与计算规则，并从 Bloom 与 Ésik 迭代范畴的范畴语义中提取 fold 计算规则，使规则由构造保证正确。作者使用二阶计算规则的 General Schema 判据证明强正规化，特别是以 Bekic 律而非固定点律作为计算核心；还证明了计算规则满足“模双模拟的 Church-Rosser”性质。结合这些结果，论文得到循环数据与 fold 的等式理论的可判定性。
Cyclic data structures, such as cyclic lists, in functional programming are tricky to handle because of their cyclicity. This paper presents an investigation of categorical, algebraic, and computational foundations of cyclic datatypes. Our framework of cyclic datatypes is based on second-order algebraic theories of Fiore et al., which give a uniform setting for syntax, types, and computation rules for describing and reasoning about cyclic datatypes. We extract the "fold" computation rules from the categorical semantics based on iteration categories of Bloom and Esik. Thereby, the rules are correct by construction. We prove strong normalisation using the General Schema criterion for second-order computation rules. Rather than the fixed point law, we particularly choose Bekic law for computation, which is a key to obtaining strong normalisation. We also prove the property of "Church-Rosser modulo bisimulation" for the computation rules. Combining these results, we have a remarkable decidability result of the equational theory of cyclic data and fold.Comment: 38 pages
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Hamana17,
title = {Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories},
author = {Makoto Hamana},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:8)2017}
}