SHARE

TWEET

# Untitled

a guest
Jun 19th, 2019
68
Never

**Not a member of Pastebin yet?**

**, it unlocks many cool features!**

__Sign Up__- 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 specication 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 dened functions, mainly because it is dicult to refer to
- the recursion scheme in isolation. The algorithmic structure is obscured by using unstructured
- recursive denitions. 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 dened 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
- denitions. 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 identied several laws for specic 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 dened 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 (dened as initial algebras) and innite
- data types (dened as nal co-algebras) constitute two dierent worlds. In that case it is not
- possible to dene functions by induction (catamorphisms) that are applicable to both nite and
- innite data types, and arbitrary recursive denitions 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 innite 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.