Total functional programming

Total functional programming (also known as strong functional programming, to be contrasted with ordinary, or weak functional programming) is a programming paradigm which restricts the range of programs to those which are provably terminating.

Termination is guaranteed through a restricted form of recursion, which operates only upon ‘reduced’ forms of its arguments. One such form is Walther recursion. In addition, every function must be a total (as opposed to partial) function—i.e. it must have a definition for everything inside its domain. This may lead to unexpected or arbitrary definitions such as $\forall x\subset \mathbb {N} .x\div 0=0$

These restrictions mean that total functional programming is not Turing-complete. However, the set of algorithms which can be used is still huge. For example, any algorithm which has had an asymptotic upper bound calculated for it can be trivially transformed into a provably-terminating function by using the upper bound as an extra argument which is decremented upon each iteration or recursion.

Another outcome of total functional programming is that there is no longer a separation between strict evaluation and lazy evaluation.

Total functional programming must necessarily also make a distinction between data and co-data—the former is finitary, which the latter is potentially infinite. Such potentially infinite data structures are needed for applications such as I/O.

References

• Turner, D.A. (2004-07-28), "Total Functional Programming", Journal of Universal Computer Science, 10 (7): 751–768 {{citation}}: Check date values in: |date= (help)