Recursive Function Definition over Coinductive Types
Recursive Function Definition over Coinductive Types
复制标题
共导类型的递归函数定义
DOI：
10.1007/3-540-48256-3_6
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
John Matthews
中科院分区：
文献类型：
--
作者：
John Matthews
利用唯一不动点、收敛等价关系和收缩函数的概念，推广了成立良好的递归技术。我们可以在伊莎贝尔定理证明中定义函数，递归地无限次调用自己。特别是，我们可以很容易地定义在协归纳定义的类型上操作的递归函数，例如无限列表。以前在Isabelle中，这样的函数只能递归地定义，或者必须对包含“额外”底部元素的类型进行操作。最后，我们证明了无限列表的滤波和平坦函数具有简单的递归定义。
Using the notions of unique fixed point, converging equivalence relation, and contracting function, we generalize the technique of well-founded recursion. We are able to define functions in the Isabelle theorem prover that recursively call themselves an infinite number of times. In particular, we can easily define recursive functions that operate over coinductively-defined types, such as infinite lists. Previously in Isabelle such functions could only be defined corecursively, or had to operate over types containing "extra" bottom-elements. We conclude the paper by showing that the functions for filtering and flattening infinite lists have simple recursive definitions.