A Fixedpoint Approach to Implementing (Co)Inductive Definitions
A Fixedpoint Approach to Implementing (Co)Inductive Definitions
复制标题
实现（共）归纳定义的定点方法
DOI：
10.1007/3-540-58156-1_11
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
Lawrence Charles Paulson
中科院分区：
文献类型：
--
作者：
Lawrence Charles Paulson
本文提出了诱导定义的固定点方法。和其他便利。共同定义。
This paper presents a fixedpoint approach to inductive definitions. Instead of using a syntactic test such as ‘strictly positive,’ the approach lets definitions involve any operators that have been proved monotone. It is conceptually simple, which has allowed the easy implementation of mutual recursion and other conveniences. It also handles coinductive definitions: simply replace the least fixedpoint by a greatest fixedpoint. This represents the first automated support for coinductive definitions.