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

General Recursion in Type Theory

Ana Bove (Institutionen för datavetenskap, Programmeringslogik)
Lecture Notes in Computer Science. International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24–28, 2002 (0302-9743). Vol. 2646 (2003), p. 39-58.
[Konferensbidrag, refereegranskat]

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.

Nyckelord: general recursion, partial functions, type theory

Denna post skapades 2007-09-10. Senast ändrad 2013-01-14.
CPL Pubid: 47405


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för datavetenskap, Programmeringslogik (2002-2004)



Chalmers infrastruktur