使用结构递归进行协递归
Using Structural Recursion for Corecursion
摘要：
我们提出了一个（有限的）解决方案的问题，构造流值定义的递归方程，不尊重guardedness条件。在Coq、AGDA和其他高阶证明助手中，对上递归函数的定义施加了保护性条件。在本文中，我们特别集中在那些非守护方程递归调用下出现的功能。我们使用的流和函数之间的对应关系自然数表明，一些类的非保护的定义可以通过结构递归函数的编码建模。在实践中，这项工作扩展了流值类，可以在基于构造性类型论的定理证明器中定义归纳和共归纳类型，结构递归和保护共递归
英文摘要：
We propose a (limited) solution to the problem of constructing stream values defined by recursive equations that do not respect the guardedness condition. The guardedness condition is imposed on definitions of corecursive functions in Coq, AGDA, and other higher-order proof assistants. In this paper, we concentrate in particular on those non-guarded equations where recursive calls appear under functions. We use a correspondence between streams and functions over natural numbers to show that some classes of non-guarded definitions can be modelled through the encoding as structural recursive functions. In practice, this work extends the class of stream values that can be defined in a constructive type theory-based theorem prover with inductive and coinductive types, structural recursion and guarded corecursion
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
