|This article needs additional citations for verification. (September 2011)|
|This computer programming–related article is a stub. You can help Wikipedia by expanding it.|
In computer programming, Walther recursion 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 functions.
Since the halting problem cannot be solved in general, there need to be still programs that will 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.
- Walther, Christoph (1991). "On Proving the Termination of Algorithms by Machine". Artificial Intelligence 70 (1).
- Wu, Alexander (1994). Automated termination proofs using Walther recursion (Thesis). Massachusetts Institute of Technology. Retrieved 2014-09-15.
- McAllester, David A.; Arkoudas, Kostas (1996). McRobbie, Michael A., and Slaney, J.K., ed. "Walther Recursion". Proceedings of the 13th International Conference on Automated Deduction. New Brunswick, NJ, USA: Springer-Verlag. pp. 643––657. ISBN 3-540-61511-3.