Inductive Definitions: Automation and Application
Inductive Definitions: Automation and Application
复制标题
归纳定义：自动化和应用
DOI：
10.1007/3-540-60275-5_66
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
J. Harrison
中科院分区：
文献类型：
--
作者：
J. Harrison
本文展示了归纳定义在 HOL 中的巨大实用价值。我们以 Knaster-Tarski 定点定理为基础，描述了我们为自动归纳定义而实现的一个新软件包。举例来说，我们用它给出了有根据递归定理的简单证明。然后，我们将介绍如何仅从无穷公理出发生成自由递归类型。这与现有的 HOL 开发形成了鲜明对比，后者首先要开发若干特定的自由递归类型。
This paper demonstrates the great practical utility of inductive definitions in HOL. We describe a new package we have implemented for automating inductive definitions, based on the Knaster-Tarski fixpoint theorem. As an example, we use it to give a simple proof of the well-founded recursion theorem. We then describe how to generate free recursive types starting just from the Axiom of Infinity. This contrasts with the existing HOL development where several specific free recursive types are developed first.