共归纳类型的操作性解释
摘要：我们介绍了一种基于重写的操作语义，用于严格正向嵌套的高阶（协）归纳类型。该语义考虑了无限规约序列的“极限”。这可以看作是在具有高阶函数和由嵌套高阶归纳和协归纳定义指定的数据的背景下，对术语重写中生产力概念的细化和概括。直观上，我们通过对应于它们完整展开的潜在无穷术语来解释高阶函数语言中的惰性数据结构。 我们证明了一个近似定理，基本上是说如果一个术语在对应于协同类型解释中的无限对象的任意大有限近似上规约，则它在这个类型解释的无穷对象中会无穷规约（即在“极限”中）。我们引入了一个足够的语法正确性准则，以类型信息装饰的有限术语的形式呈现。利用近似定理，我们证明每个良好类型的术语在我们的语义中有一个良定义的解释。
作者：{L}ukasz Czajka
论文ID：1808.05059
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22