This HTML5 document contains 31 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

PrefixNamespace IRI
dcthttp://purl.org/dc/terms/
yago-reshttp://yago-knowledge.org/resource/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
dbpedia-wikidatahttp://wikidata.dbpedia.org/resource/
yagohttp://dbpedia.org/class/yago/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n6http://rdf.freebase.com/ns/m.
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n12http://en.wikipedia.org/wiki/Total_functional_programming?oldid=
owlhttp://www.w3.org/2002/07/owl#
wikipedia-enhttp://en.wikipedia.org/wiki/
dbchttp://dbpedia.org/resource/Category:
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/
Subject Item
dbr:TFP
dbo:wikiPageDisambiguates
dbr:Total_functional_programming
Subject Item
dbr:Total_functional_programming
rdf:type
yago:LivingThing100004258 yago:CausalAgent100007347 yago:YagoLegalActor yago:YagoLegalActorGeo yago:Worker109632518 yago:PhysicalEntity100001930 yago:Assistant109815790 yago:WikicatProofAssistants yago:Object100002684 yago:Whole100003553 yago:Person100007846 yago:Organism100004475
rdfs:label
Total functional programming
rdfs:comment
Total functional programming (also known as strong functional programming, to be contrasted with ordinary, or weak functional programming) is a programming paradigm that restricts the range of programs to those that are provably terminating. Termination is guaranteed by the following restrictions: for division); adding another argument to specify the result for those inputs; or excluding them by use of type system features such as refinement types. To make it substructural recursive using the length of the vector as a limit, we could do:
owl:sameAs
n6:02rl3rf yago-res:Total_functional_programming wikidata:Q17146827 dbpedia-wikidata:Q17146827
dct:subject
dbc:Functional_programming dbc:Proof_assistants dbc:Programming_paradigms
dbo:wikiPageID
11599902
dbo:wikiPageRevisionID
738858026
foaf:isPrimaryTopicOf
wikipedia-en:Total_functional_programming
prov:wasDerivedFrom
n12:738858026
dbo:abstract
Total functional programming (also known as strong functional programming, to be contrasted with ordinary, or weak functional programming) is a programming paradigm that restricts the range of programs to those that are provably terminating. Termination is guaranteed by the following restrictions: 1. * 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. 2. * Every function must be a total (as opposed to partial) function. That is, it must have a definition for everything inside its domain. 3. * 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 for division); adding another argument to specify the result for those inputs; or excluding them by use of type system features such as refinement types. 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 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 O(n2)). A quicksort implementation on lists (which would be rejected by a substructural recursive checker) is, using Haskell: qsort [] = []qsort [a] = [a]qsort (a:as) = let (lesser, greater) = partition a as in qsort lesser ++ [a] ++ qsort greater To make it substructural recursive using the length of the vector as a limit, we could do: qsort x = qsortSub x x-- minimum caseqsortSub [] as = as -- shows termination-- standard qsort casesqsortSub (l:ls) [] = [] -- nonrecursive, so acceptedqsortSub (l:ls) [a] = [a] -- nonrecursive, so acceptedqsortSub (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 Some classes of algorithms that have no theoretical upper bound but 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. In total functional programming, a distinction is made between data and 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. Both Epigram and Charity could be considered total functional programming languages, even though they don't work in the way Turner specifies in his paper. So could programming directly in plain System F, in Martin-Löf type theory or the Calculus of Constructions.
Subject Item
dbr:Total_FP
dbo:wikiPageRedirects
dbr:Total_functional_programming
Subject Item
dbr:Elementary_strong_functional_programming
dbo:wikiPageRedirects
dbr:Total_functional_programming
Subject Item
dbr:Total_language
dbo:wikiPageRedirects
dbr:Total_functional_programming
Subject Item
wikipedia-en:Total_functional_programming
foaf:primaryTopic
dbr:Total_functional_programming