In computer programming, Walther recursion (named after
Christoph Walther) is a method of analysing recursive functions that can determine if the function is definitely
terminating, given finite inputs. It allows a more natural style of expressing computation than simply using
primitive recursive function
In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop is fixed befor ...
s.
Since the
halting problem
In computability theory (computer science), computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run for ...
cannot be solved in general, there must still be programs that terminate, but which Walther recursion cannot prove to terminate. Walther recursion may be used in
total functional languages in order to allow a more liberal style of showing primitive recursion.
See also
*
BlooP and FlooP
*
Termination analysis
In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for ''each'' input. This means to determine whether the input program computes a ''total'' function.
It is ...
*
Total Turing machine
In computability theory, a decider is a Turing machine that halts for every input. A decider is also called a total Turing machineKozen, 1997 as it represents a total function.
Because it always halts, such a machine is able to decide whether a g ...
References
*
*
*
Recursion
{{compu-prog-stub