CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Nested General Recursion and Partiality in Type Theory

Ana Bove (Institutionen för datavetenskap) ; Venanzio Capretta
Theorem Proving in Higher Order Logics (0302-9743). Vol. LNCS 2152 (2001), p. 121--135.
[Konferensbidrag, refereegranskat]

We extend Bove's technique for formalising simple general recursive algorithms in constructive type theory to nested recursive algorithms. The method consists in defining an inductive domain predicate, that characterises the inputs on which the algorithm terminates. As a result, the type-theoretic version of the algorithm can be defined by structural recursion on the proof that the input values satisfy this predicate. This technique results in definitions 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 defined simultaneously, because they depend on each other. This kind of definitions is not allowed in ordinary type theory, but it is provided in type theories extended with Dybjer's schema for simultaneous inductive-recursive definitions. The technique applies also to the formalisation of partial functions as proper type-theoretic functions, rather than relations representing their graphs.

Nyckelord: general recursion, nested recursion, partial functions, type theory

Denna post skapades 2007-09-10.
CPL Pubid: 47408


Institutioner (Chalmers)

Institutionen för datavetenskap (1993-2001)



Chalmers infrastruktur