| Nested general recursion and partiality in type theory (2001) | |||||||||||||||||
Abstract | |||||||||||||||||
| Abstract. We extend Bove's technique for formalising simple general recursive algorithms in constructive type theory to nested recursive algorithms. The method consists in dening an inductive special-purpose accessibility predicate, that characterises the inputs on which the algorithm terminates. As a result, the type-theoretic version of the algorithm can be dened by structural recursion on the proof that the input values satisfy this predicate. This technique results in denitions in which the computational and logical parts are clearly separated; hence, the type-theoretic version of the algorithm is given by its purely functional content, similarly to the corresponding program in a functional programming language. In the case of nested recursion, the special predicate and the type-theoretic algorithm must be dened simultaneously, because they depend on each other. This kind of denitions is not allowed in ordinary type theory, but it is provided in type theories extended with Dybjer's schema for simultaneous inductive-recursive denitions. The technique applies also to the formalisation of partial functions as proper type-theoretic functions, rather that relations representing their graphs. 1 | |||||||||||||||||
Details der Publikation | |||||||||||||||||
| |||||||||||||||||