Coq中共递函数的归纳和余归纳组成部分
摘要：构造性类型理论中，递归和共递归定义受到语法限制，以确保递归函数的终止和共递函数的生产力。然而，许多终止和有产生力的函数未通过语法测试。Bove在她的论文中提出了一种优雅的可达性谓词方法的重新格式化，扩大了可以在构造性类型理论中形式化的终止递归函数的范围。在本文中，我们为有产生力的共递函数追求同样的目标。值得注意的是，我们在Coq中对有产生力函数的共归定义的形式化方法不仅需要使用临时谓词，还需要一个系统的算法来将函数的归纳部分和共归部分分离开来。
作者：Yves Bertot (INRIA Sophia Antipolis), Ekaterina Komendantskaya (INRIA Sophia Antipolis)
论文ID：0807.1524
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-07-10