List Objects and Recursive Algorithms in Elementary Topoi

Christian E. G. Maurer

Institut für Informatik
Freie Universität Berlin
Takustr. 9
14195 Berlin
email: maurer@inf.fu-berlin.de

Report B 96-05
June 1996

Get the report here or by anonymous ftp: 
Server: fubinf.inf.fu-berlin.de
File:   pub/reports/tr-b-96-05.ps.gz
List Objects and Recursive Algorithms in Elementary Topoi 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.

[B] E. T. P. Burton
"Verification and Transformation of Simple Recursive Programs - An Algebraic Approach", in "Mathematical Structures for Software Engineering", eds. B. Neumann, D. Simpson, G. Slater Clarendon Press, Oxford (1991), 17-4

[F] P. Freyd
"Aspects of topoi", Bull. Austral. Math. Soc. 7 (1972) 1-76