Among the many styles and methodologies for the construction of computer programs the
Squiggol style in our opinion deserves attention from the functional programming community.
The overall goal of Squiggol is to calculate programs from their specication in the way a mathematician calculates solutions to dierential equations, or uses arithmetic to solve numerical
problems.
It is not hard to state, prove and use laws for well-known operations such as addition, multiplication and |at the function level| composition. It is, however, quite hard to state, prove
and use laws for arbitrarily recursively dened functions, mainly because it is dicult to refer to
the recursion scheme in isolation. The algorithmic structure is obscured by using unstructured
recursive denitions. We crack this problem by treating various recursion schemes as separate
higher order functions, giving each a notation of its own independent of the ingredients with
which it constitutes a recursively dened function.

University of Nijmegen, Department of Informatics, Toernooiveld 6525 ED Nijmegen, e-mail:
erik@cs.kun.nl
y
CWI, Amsterdam & University of Twente
z
Imperial College, London
1
This philosophy is similar in spirit to the `structured programming' methodology for imperative
programming. The use of arbitrary goto's is abandoned in favour of structured control
ow
primitives such as conditionals and while-loops that replace xed patterns of goto's, so that reasoning about programs becomes feasible and sometimes even elegant. For functional programs
the question is which recursion schemes are to be chosen as a basis for a calculus of programs.
We shall consider several recursion operators that are naturally associated with algebraic type
denitions. A number of general theorems are proven about these operators and subsequently
used to transform programs and prove their correctness.
Bird and Meertens [4, 18] have identied several laws for specic data types (most notably nite
lists) using which they calculated solutions to various programming problems. By embedding
the calculus into a categorical framework, Bird and Meertens' work on lists can be extended
to arbitrary, inductively dened data types [17, 12]. Recently the group of Backhouse [1] has
extended the calculus to a relational framework, thus covering indeterminancy.
Independently, Paterson [21] has developed a calculus of functional programs similar in contents
but very dissimilar in appearance (like many Australian animals) to the work referred to above.
Actually if one pricks through the syntactic dierences the laws derived by Paterson are the
same and in some cases slightly more general than those developped by the Squiggolers.
This paper gives an extension of the theory to the context of lazy functional programming, i.e.,
for us a type is an !-cpo and we consider only continuous functions between types (categorically,
we are working in the category CPO). Working in the category SET as done by for example
Malcolm [17] or Hagino [14] means that nite data types (dened as initial algebras) and innite
data types (dened as nal co-algebras) constitute two dierent worlds. In that case it is not
possible to dene functions by induction (catamorphisms) that are applicable to both nite and
innite data types, and arbitrary recursive denitions are not allowed. Working in CPO has
the advantage that the carriers of initial algebras and nal co-algebras coincide, thus there is a
single data type that comprises both nite and innite elements. The price to