General Recursion in Type Theory
General Recursion in Type Theory
复制标题
类型论中的一般递归
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Ana Bove
中科院分区：
文献类型：
--
作者：
Ana Bove
在这项工作中，一种方法来正式一般递归算法的建设性类型理论的例子。该方法将定义的计算部分和逻辑部分分开。因此，得到的类型理论算法是清晰，紧凑和易于理解的。它们和函数式编程语言中的等价物一样简单，在函数式编程语言中，对递归调用没有限制。给定一个一般的递归算法，该方法包括定义一个归纳的专用可访问性谓词，该谓词表征算法终止的输入。该算法的类型论版本可以通过结构递归来定义，证明输入值满足该谓词。当形式化嵌套算法时，特殊用途的可访问性谓词和算法的类型理论版本必须同时定义，因为它们相互依赖。由于该方法将定义的计算部分与逻辑部分分开，因此部分函数的形式化也成为可能。
In this work, a method to formalise general recursive algorithms in constructive type theory is presented throughout examples. The method separates the computational and logical parts of the definitions. As a consequence, the resulting type-theoretic algorithms are clear, compact and easy to understand. They are as simple as their equivalents in a functional programming language, where there is no restriction on recursive calls. Given a general recursive algorithm, the method consists in defining an inductive special-purpose accessibility predicate that characterises the inputs on which the algorithm terminates. The type-theoretic version of the algorithm can then be defined by structural recursion on the proof that the input values satisfy this predicate. When formalising nested algorithms, the special-purpose accessibility predicate and the type-theoretic version of the algorithm must be defined simultaneously because they depend on each other. Since the method separates the computational part from the logical part of a definition, formalising partial functions becomes also possible.