*Elementary Strong Functional Programming:* Summary

Professor D. A. Turner,

Computing Laboratory,
University of Kent,
Canterbury CT2 7NF, UK.

The project, funded by the UK Engineeering and Physical Sciences Research Council (EPSRC) from 14.10.96 to 13.10.99 under grant GR/L03279, was undertaken to investigate the practical viability of a discipline of strong functional programming proposed in [8]. The research associate was Alastair Telford.

In strong functional programming all expressions are guaranteed to have
normal form. In order to retain the possibility of programming with
infinite structures, which is an essential feature of pure functional
languages such as Haskell, a key part of the methodology of [8] is to
maintain a separation in the type system between *data*, which is
known to be finite, and *codata* which is permitted to be infinite.
This may be contrasted with the usual situation in lazy functional
programming in which infinite lists for example, have the same
compile-time type as ordinary finite lists.

The separation between data and codata leads to a distinction between
*recursion*, which to be "safe" must be **well-founded**, and
*corecursion*, which must be **productive**. Our main
achievements are the development of techniques of abstract
interpretation, which we demonstrate can recognise at compile time
sufficiently large classes of safe recursion and corecursion to permit
a wide range of standard functional algorithms to be accepted in their
"natural" form. Previous work on automatic termination detection, based
for example on *Walther recursion*, has required even quite simple
algorithms, for example *gcd*, to be rewritten in a special style.
We believe these results substantially advance the practical viability
of strong functional programming.

Our techniques for recognising productivity in corecursive definitions of infinitary structures are presented in [1,2] and those for well-founded recursion over finitary data structures in [3,4].

Alexander Kaganovsky, a PhD student
associated with the group, did outstanding work on the investigation of
an important class of corecursive algorithms over infinite lists of
integers. The problem area he studied is the efficient implementation
of *unbounded precision arithmetic* on real and complex numbers
represented as streams of signed digits. His results, which include
algorithms for many analytic functions and are a significant advance on
previous work, are described in two papers and his thesis [5,6,7].

For further information contact the investigator at the University of Kent.

Final report PDF [84K].

- A.J.Telford, D.A.Turner " Ensuring Streams Flow" Johnson, ed, Algebraic Methodology and Software Technology - AMAST '97. LNCS 1349, pages 509-523, Springer, 1997.
- A.J.Telford, D.A.Turner " Ensuring the Productivity of Infinite Structures" Technical Report TR 14-97, 37 pages, Computing Laboratory, University of Kent, March 1998.
- A.J.Telford, D.A.Turner " Ensuring Termination in ESFP", Journal of Universal Computer Science 6(4):474-488, April 2000 (originally presented at 15th British Colloquium in Theoretical Computer Science, Keele, April 1999).
- A.J.Telford, D.A.Turner " A Hierarchy of Elementary Languages with Strong Normalisation Properties", Technical Report TR 2-00, 66 pages, University of Kent Computing Laboratory, January 2000.
- A.Y.Kaganovsky " Exact Complex Arithmetic in an Imaginary Radix System", Technical Report TR 9-99, 30 pages, Computing Laboratory, University of Kent, July 1999.
- A.Y.Kaganovsky