a guest Jun 19th, 2019 68 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. Among the many styles and methodologies for the construction of computer programs the
  2. Squiggol style in our opinion deserves attention from the functional programming community.
  3. The overall goal of Squiggol is to calculate programs from their speci cation in the way a mathematician calculates solutions to di erential equations, or uses arithmetic to solve numerical
  4. problems.
  5. 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
  6. and use laws for arbitrarily recursively de ned functions, mainly because it is dicult to refer to
  7. the recursion scheme in isolation. The algorithmic structure is obscured by using unstructured
  8. recursive de nitions. We crack this problem by treating various recursion schemes as separate
  9. higher order functions, giving each a notation of its own independent of the ingredients with
  10. which it constitutes a recursively de ned function.
  12. University of Nijmegen, Department of Informatics, Toernooiveld 6525 ED Nijmegen, e-mail:
  14. y
  15. CWI, Amsterdam & University of Twente
  16. z
  17. Imperial College, London
  18. 1
  19. This philosophy is similar in spirit to the `structured programming' methodology for imperative
  20. programming. The use of arbitrary goto's is abandoned in favour of structured control
  21. ow
  22. 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
  23. the question is which recursion schemes are to be chosen as a basis for a calculus of programs.
  24. We shall consider several recursion operators that are naturally associated with algebraic type
  25. de nitions. A number of general theorems are proven about these operators and subsequently
  26. used to transform programs and prove their correctness.
  27. Bird and Meertens [4, 18] have identi ed several laws for speci c data types (most notably nite
  28. lists) using which they calculated solutions to various programming problems. By embedding
  29. the calculus into a categorical framework, Bird and Meertens' work on lists can be extended
  30. to arbitrary, inductively de ned data types [17, 12]. Recently the group of Backhouse [1] has
  31. extended the calculus to a relational framework, thus covering indeterminancy.
  32. Independently, Paterson [21] has developed a calculus of functional programs similar in contents
  33. but very dissimilar in appearance (like many Australian animals) to the work referred to above.
  34. Actually if one pricks through the syntactic di erences the laws derived by Paterson are the
  35. same and in some cases slightly more general than those developped by the Squiggolers.
  36. This paper gives an extension of the theory to the context of lazy functional programming, i.e.,
  37. for us a type is an !-cpo and we consider only continuous functions between types (categorically,
  38. we are working in the category CPO). Working in the category SET as done by for example
  39. Malcolm [17] or Hagino [14] means that nite data types (de ned as initial algebras) and in nite
  40. data types (de ned as nal co-algebras) constitute two di erent worlds. In that case it is not
  41. possible to de ne functions by induction (catamorphisms) that are applicable to both nite and
  42. in nite data types, and arbitrary recursive de nitions are not allowed. Working in CPO has
  43. the advantage that the carriers of initial algebras and nal co-algebras coincide, thus there is a
  44. single data type that comprises both nite and in nite elements. The price to
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand