Inductive and Coinductive Components of Corecursive Functions in Coq
Inductive and Coinductive Components of Corecursive Functions in Coq
复制标题
Coq 中核心递归函数的归纳和共归纳成分
DOI：
10.1016/j.entcs.2008.05.018
复制
发表时间：
2008
影响因子：
--
通讯作者：
Bertot Y
中科院分区：
文献类型：
--
作者：
Bertot Y
在构造型理论中，递归和共递定义受到句法限制，以保证递归函数的终止性和共递函数的生产力。然而，许多终止函数和生成函数不能通过语法测试。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.
登录
查看更多内容
DOI：
10.1016/j.tcs.2009.10.014
发表时间：
2007
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
J. Endrullis;C. Grabmayer;D. Hendriks;Ariya Isihara;J. Klop
通讯作者：
J. Klop
使用依赖类型系统进行验证检查
DOI：
--
发表时间：
2002
期刊：
影响因子：
--
作者：
H. Barendregt;H. Geuvers
通讯作者：
H. Geuvers
类型理论中的无限对象
DOI：
--
发表时间：
1986
期刊：
Logic in Computer Science
影响因子：
--
作者：
N. Mendler;P. Panangaden;R. Constable
通讯作者：
R. Constable
类型论中的一般递归
DOI：
--
发表时间：
2002
期刊：
Types for Proofs and Programs
影响因子：
--
作者：
Ana Bove
通讯作者：
Ana Bove
影响因子：
0.6
作者：
Capretta, Venanzio
通讯作者：
Capretta, Venanzio