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