patternMinor
Is well-founded recursion enough for practical total functional programming?
Viewed 0 times
totalrecursionprogrammingforwellpracticalfunctionalenoughfounded
Problem
Total functional programming is a paradigm of non-Turing-complete programming languages where any program that type checks is proven to halt.
Well-founded recursion is a recursive definition of a function such that the definition of $f(x)$ only ever makes a recursive call $f(y)$ when $y<x$ for some well-founded relation $<$.
But the wikipedia page of Total functional programming refers also to other types of provably-terminating recursion:
[Termination is guaranteed by] 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.
Are there any ways that one can do better than well-founded recursion, for practical total functional programming? I've always thought of well-founded recursion as "the most general provably terminating recursion"
Well-founded recursion is a recursive definition of a function such that the definition of $f(x)$ only ever makes a recursive call $f(y)$ when $y<x$ for some well-founded relation $<$.
But the wikipedia page of Total functional programming refers also to other types of provably-terminating recursion:
[Termination is guaranteed by] 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.
Are there any ways that one can do better than well-founded recursion, for practical total functional programming? I've always thought of well-founded recursion as "the most general provably terminating recursion"
Solution
Let's restrict ourselves to the model of Turing machines (or, in general, of state machines). Consider complete states $s_1, s_2$ of the Turing machine (a complete state is a state specifying the full configuration of the Turing machine). We say that $s_1 \gets s_2$ if and only if we transition from $s_2$ directly to $s_1$.
It is easy to see that the Turing machine will terminate from any state if, and only if, $\gets$ is a well-founded relation.
A similar result holds for a strict language based on the $\lambda$-calculus. It's possible to determine whether a given term $T$ will reduce to a normal form by considering the $\beta$-reduction relation $\gets_\beta$ on all terms which $T$ can be reduced to. $T$ will reduce to a normal form under any reduction order if and only if $\gets_\beta$ is well-founded.
Thus, it's really not possible to get any more general than well-founded relations for proving termination.
It is easy to see that the Turing machine will terminate from any state if, and only if, $\gets$ is a well-founded relation.
A similar result holds for a strict language based on the $\lambda$-calculus. It's possible to determine whether a given term $T$ will reduce to a normal form by considering the $\beta$-reduction relation $\gets_\beta$ on all terms which $T$ can be reduced to. $T$ will reduce to a normal form under any reduction order if and only if $\gets_\beta$ is well-founded.
Thus, it's really not possible to get any more general than well-founded relations for proving termination.
Context
StackExchange Computer Science Q#132414, answer score: 2
Revisions (0)
No revisions yet.