Tjark Weber and James Caldwell. In Maurice Bruynooghe, editor, LOPSTR 2003 Preproceedings of the International Symposium on Logic Based Program Synthesis and Transformation, pages 149-164, Leuven, Belgium, August 2003. Department of Computer Science, K.U. Leuven. Report CW 365.
In this paper we formally state and prove theorems characterizing when a function can be constructively reformulated using the recursion operators fold and unfold, i.e. given a function h, when can a function g be constructed such that h = fold g or h = unfold g? These results are refinements of the classical characterization of fold and unfold given by Gibbons, Hutton and Altenkirch in [6]. The proofs presented here have been formalized in Nuprl's constructive type theory [5] and thereby yield program transformations which map a function h (accompanied by the evidence that h satisfies the required conditions), to a function g such that h = fold g or, as the case may be, h = unfold g.
@inproceedings{weber03constructively,
author = {Tjark Weber and James Caldwell},
title = {Constructively Characterizing Fold and Unfold},
editor = {Maurice Bruynooghe},
booktitle = {LOPSTR 2003 Preproceedings of the International Symposium on Logic Based Program Synthesis and Transformation},
pages = {149--164},
address = {Leuven, Belgium},
publisher = {Department of Computer Science, K.U.\ Leuven},
note = {Report CW 365},
month = aug,
year = {2003}
}
A revised version of this paper is available.