Partial Recursive Functions in Higher-Order Logic
Partial Recursive Functions in Higher-Order Logic
复制标题
高阶逻辑中的部分递归函数
DOI：
10.1007/11814771_48
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Alexander Krauss
中科院分区：
文献类型：
--
作者：
Alexander Krauss
基于归纳定义，我们开发了一种自动化工具，用于在高阶逻辑中定义部分递归功能并为其提供适当的推理工具。我们的方法以统一的方式表示终止，并包括一种非常通用的模式匹配形式，其中模式可以是任意表达式。可以推迟终止证明，仅限于参数子集，并且可以与有关该功能的其他证据互换。我们表明，这种方法还可以促进总功能的终止论证，特别是对于嵌套递归。我们将工具作为Isabelle/Hol的定义规范机制实施。
Based on inductive definitions, we develop an automated tool for defining partial recursive functions in Higher-Order Logic and providing appropriate reasoning tools for them. Our method expresses termination in a uniform manner and includes a very general form of pattern matching, where patterns can be arbitrary expressions. Termination proofs can be deferred, restricted to subsets of arguments and are interchangeable with other proofs about the function. We show that this approach can also facilitate termination arguments for total functions, in particular for nested recursions. We implemented our tool as a definitional specification mechanism for Isabelle/HOL.