List objects and recursive algorithms in elementary topoi

Abstract

The paper generalizes results of [B] by formulating their background in categories with a sufficiently rich internal logic, e. g. elementary topoi, using the well known initial algebra approach. Thus the right setting for program transformations in the sense of [B] is given by embedding them into the generalisation of primitive recursion over the naturals in the sense of [F] to lists. Particularly there is a simple concept of tail recursion, hence an outline on a systematic transformation of naive recursive programs into tail recursive i. e. more efficient iterative forms.