imported>SilkPyjamas: Adding local short description: "Programming paradigm restricted to provably terminating programs", overriding Wikidata description "non-Turing-complete programming paradigm restricted to provably terminating programs"

2025-05-20T14:49:04Z

Adding local short description: "Programming paradigm restricted to provably terminating programs", overriding Wikidata description "non-Turing-complete programming paradigm restricted to provably terminating programs"

New page

{{Short description|Programming paradigm restricted to provably terminating programs}}
'''Total functional programming''' (also known as '''strong functional programming''',<ref>This term is due to: {{Cite conference|last1=Turner|first1=D.A.|author-link=David Turner (computer scientist)|title=Elementary Strong Functional Programming|conference=First International Symposium on Functional Programming Languages in Education|date=December 1995|series=Springer LNCS|volume=1022|pages=1–13}}.</ref> to be contrasted with ordinary, or ''weak'' [[functional programming]]) is a [[computer programming|programming]] paradigm that restricts the range of programs to those that are [[Machine that always halts|provably terminating]].<ref name="TFP">{{Citation|last=Turner|first=D.A.|author-link=David Turner (computer scientist)|title=Total Functional Programming|journal=[[Journal of Universal Computer Science]]|volume=10|date=2004-07-28|pages=751–768|url=http://www.jucs.org/jucs_10_7/total_functional_programming|doi=10.3217/jucs-010-07-0751|issue=7}}</ref>

==Restrictions==
Termination is guaranteed by the following restrictions:

# A restricted form of [[recursion]], which operates only upon 'reduced' forms of its arguments, such as [[Walther recursion]], [[substructural recursion]], or "strongly normalizing" as proven by [[abstract interpretation]] of code.<ref name="ETinESFP">{{Citation|last=Turner|first=D. A.|author-link=David Turner (computer scientist)|title=Ensuring Termination in ESFP|journal=Journal of Universal Computer Science|volume=6|date=2000-04-28|pages=474–488|url=http://www.jucs.org/jucs_6_4/ensuring_termination_in_esfp|doi=10.3217/jucs-006-04-0474|issue=4}}</ref>
# Every function must be a total (as opposed to [[partial function|partial]]) function. That is, it must have a definition for everything inside its domain.
#* There are several possible ways to extend commonly used partial functions such as division to be total: choosing an arbitrary result for inputs on which the function is normally undefined (such as <math>\forall x \in \mathbb{N}. x \div 0 = 0</math> for division); adding another argument to specify the result for those inputs; or excluding them by use of type system features such as [[refinement type]]s.<ref name="TFP"/>

These restrictions mean that total functional programming is not [[Turing-complete]]. However, the set of algorithms that can be used is still huge. For example, any algorithm for which an [[Upper bound|asymptotic upper bound]] can be calculated (by a program that itself only uses Walther recursion) can be trivially transformed into a provably-terminating function by using the upper bound as an extra argument decremented on each iteration or recursion.

For example, [[quicksort]] is not trivially shown to be substructural recursive, but it only recurs to a maximum depth of the length of the vector (worst-case time complexity [[Big O notation|O]](''n''<sup>2</sup>)). A quicksort implementation on lists (which would be rejected by a substructural recursive checker) is, using [[Haskell (programming language) | Haskell]]:
<syntaxhighlight lang="haskell">
import Data.List (partition)

qsort [] = []
qsort [a] = [a]
qsort (a:as) = let (lesser, greater) = partition (<a) as
in qsort lesser ++ [a] ++ qsort greater
</syntaxhighlight>

To make it substructural recursive using the length of the vector as a limit, we could do:
<syntaxhighlight lang="haskell">
import Data.List (partition)

qsort x = qsortSub x x
-- minimum case
qsortSub [] as = as -- shows termination
-- standard qsort cases
qsortSub (l:ls) [] = [] -- nonrecursive, so accepted
qsortSub (l:ls) [a] = [a] -- nonrecursive, so accepted
qsortSub (l:ls) (a:as) = let (lesser, greater) = partition (<a) as
-- recursive, but recurs on ls, which is a substructure of
-- its first input.
in qsortSub ls lesser ++ [a] ++ qsortSub ls greater
</syntaxhighlight>

Some classes of algorithms have no theoretical upper bound but do have a practical upper bound (for example, some heuristic-based algorithms can be programmed to "give up" after so many recursions, also ensuring termination).

Another outcome of total functional programming is that both [[strict evaluation]] and [[lazy evaluation]] result in the same behaviour, in principle; however, one or the other may still be preferable (or even required) for performance reasons.<ref>The differences between lazy and eager evaluation are discussed in: {{cite book|last=Granström|first=J. G.|title=Treatise on Intuitionistic Type Theory|series=Logic, Epistemology, and the Unity of Science|volume=7|year=2011|url=https://www.springer.com/philosophy/book/978-94-007-1735-0|isbn=978-94-007-1735-0}} See in particular pp. 86–91.</ref>

In total functional programming, a distinction is made between [[data]] and [[codata (computer science)|codata]]—the former is [[finitary]], while the latter is potentially infinite. Such potentially infinite data structures are used for applications such as [[I/O]]. Using codata entails the usage of such operations as [[corecursion]]. However, it is possible to do [[I/O]] in a total functional programming language (with [[dependent types]]) also without codata.<ref>{{Citation|last=Granström|first=J. G.|title=A New Paradigm for Component-based Development|date=May 2012|journal=Journal of Software|volume=7|issue=5|pages=1136–1148|doi=10.4304/jsw.7.5.1136-1148}} [https://web.archive.org/web/20200709203859/http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.369.3459&rep=rep1&type=pdf Archived copy]</ref>

Both [[Epigram (programming language)|Epigram]] and [[Charity (programming language)|Charity]] could be considered total functional programming languages, even though they do not work in the way [[David Turner (computer scientist)|Turner]] specifies in his paper. So could programming directly in plain [[System F]], in [[Martin-Löf type theory]] or the [[Calculus of Constructions]].

== See also ==
* [[Termination analysis]]

==References==
{{reflist}}

{{DEFAULTSORT:Total Functional Programming}}
[[Category:Programming paradigms]]
[[Category:Functional programming]]
[[Category:Proof assistants]]

Total functional programming - Revision history

imported>SilkPyjamas: Adding local short description: "Programming paradigm restricted to provably terminating programs", overriding Wikidata description "non-Turing-complete programming paradigm restricted to provably terminating programs"