Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain
Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain
复制标题
序数算术：高阶域中波纹的案例研究
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
T. Abdelzaher
中科院分区：
文献类型：
--
作者：
Shuochao Yao;Shaohan Hu;Shen Li;Yiran Zhao;Lu Su;Lance M. Kaplan;A. Yener;T. Abdelzaher
本文报告了一个在高阶句法背景下使用证明计划的案例研究。涟漪是一种启发式方法，用于指导归纳中的重写步骤，已成功地用于证明计划中使用一阶表示的归纳证明。序数算术提供了一组自然的高阶示例，在这些示例上可以尝试使用涟漪进行超限归纳。以前，Boyer-Moore式的自动化不能应用于这样的领域。我们证明了涟漪启发式的高阶扩展足以自动计划这样的证明。相应地，序数算法已经在归纳的高阶证明规划系统λCLAM中实现，并成功地规划了标准的本科课本问题。我们展示了正常序数函数的不动点的合成，这表明我们的自动化可以如何扩展以产生比迄今尝试的教科书示例更有趣的结果。
This paper reports a case study in the use of proof planning in the context of higher order syntax. Rippling is a heuristic for guiding rewriting steps in induction that has been used successfully in proof planning inductive proofs using first order representations. Ordinal arithmetic provides a natural set of higher order examples on which transfinite induction may be attempted using rippling. Previously Boyer-Moore style automation could not be applied to such domains. We demonstrate that a higher-order extension of the rippling heuristic is sufficient to plan such proofs automatically. Accordingly, ordinal arithmetic has been implemented in λClam, a higher order proof planning system for induction, and standard undergraduate text book problems have been successfully planned. We show the synthesis of a fixpoint for normal ordinal functions which demonstrates how our automation could be extended to produce more interesting results than the textbook examples tried so far.