Tjark Weber and James Caldwell. In Maurice Bruynooghe, editor, Logic Based Program Synthesis and Transformation - 13th International Symposium LOPSTR 2003, Uppsala, Sweden, August 25-27, 2003, Revised Selected Papers, volume 3018 of Lecture Notes in Computer Science, pages 110-127. Springer, June 2004.
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{weber04constructively,
author = {Tjark Weber and James Caldwell},
title = {Constructively Characterizing Fold and Unfold},
editor = {Maurice Bruynooghe},
booktitle = {Logic Based Program Synthesis and Transformation~-- 13th International Symposium LOPSTR 2003, Uppsala, Sweden, August 25-27, 2003, Revised Selected Papers},
volume = {3018},
series = {Lecture Notes in Computer Science},
pages = {110--127},
publisher = {Springer},
month = jun,
year = {2004},
isbn = {3-540-22174-3}
}