On Fragments of Analysis with Strengths of Finitely Iterated Inductive Definitions

Klaus Aehlig

(München, visiting Oxford)

The polymorphic lambda-calculus (System F) is a very expressive functional programming language. All inductive types can be encoded directly in system F. A natural restriction of the polymorphic types consists in allowing quantification only for types with at most the quantified variable free. This fragment is still strong enough to host all inductive types, but on the other hand all number theoretic functions definable in this system are provably recursive in systems of finitely iterated inductive definition. So a simple fragment capturing precisely inductive data types has been identified. Similarly, a fragment of second order arithmetic can be defined with the same restriction on second order quantification. This fragment is proof theoretically equivalent to the system of finitely iterated inductive definitions.
Tuesday 20th April 2004, 14:00
Robert Recorde Room
Department of Computer Science