Coq中余递归函数的诱导分量与余诱导分量
Inductive and Coinductive Components of Corecursive Functions in Coq
摘要：
在构造类型论中，递归和上递归的定义受到语法限制，这保证了递归函数的终止性和上递归函数的生产力。然而，许多终止函数和生产函数没有通过语法测试。Bove在她的论文中提出了一个优雅的可访问性谓词方法的重新表述，该方法拓宽了构造类型论中可形式化的终结递归函数的范围。在本文中，我们追求同样的目标生产的上递归函数。值得注意的是，我们的方法的形式化coq生产函数的共归纳定义不仅需要使用特设谓词，而且还需要一个系统的算法，分离归纳和共归纳部分的功能。
英文摘要：
In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and productive functions do not pass the syntactic tests. Bove proposed in her thesis an elegant reformulation of the method of accessibility predicates that widens the range of terminative recursive functions formalisable in Constructive Type Theory. In this paper, we pursue the same goal for productive corecursive functions. Notably, our method of formalisation of coinductive definitions of productive functions in Coq requires not only the use of ad-hoc predicates, but also a systematic algorithm that separates the inductive and coinductive parts of functions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
