通过共析类型实现通用递归
计算机科学中的逻辑
2017-01-11 v6
摘要
理论计算机科学中一个富有成果的研究领域探讨了在 intensional 类型论中表示通用递归函数的方法。最成功的几种方法包括：使用良构关系、实现操作语义、形式化域论、以及对域谓词的归纳定义。本文提出了另一种解决方案：利用共析类型来建模无限计算。对于每个类型 A，我们关联一种部分元素类型 Partial(A)，通过两个构造函数共析生成：第一个构造函数 return(a) 仅返回元素 a:A；第二个构造函数 step(x) 为递归元素 x:Partial(A) 添加一个计算步骤。我们展示了这一简单机制足以形式化两个给定类型之间的所有递归函数。它允许对原始的、即连续算子的固定点进行定义。我们将将此方法与文献中不同的方法进行比较。最后，我们指出，具有适当的结构映射，此形式化定义了一个强单子。
关键词
引用
@article{arxiv.cs/0505037,
title = {General Recursion via Coinductive Types},
author = {Venanzio Capretta},
journal= {arXiv preprint arXiv:cs/0505037},
year = {2017}
}
备注
28 pages