Walther recursion
From Wikipedia, the free encyclopedia
Page Module:Message box/ambox.css has no content.
This article includes a list of general references, but it lacks sufficient corresponding inline citations. (September 2011) |
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 functions.
Since the halting problem 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
References
- Page Module:Citation/CS1/styles.css has no content.Walther, Christoph (1991). "On Proving the Termination of Algorithms by Machine" (PDF). Artificial Intelligence. 70 (1). doi:10.1016/0004-3702(94)90063-9.
- Page Module:Citation/CS1/styles.css has no content.Wu, Alexander (1994). Automated termination proofs using Walther recursion (Thesis). Massachusetts Institute of Technology. Retrieved 2014-09-15.
- Page Module:Citation/CS1/styles.css has no content.McAllester, David; Arkoudas, Kostas (1996). McRobbie, Michael A.; Slaney, J.K. (eds.). Walther recursion. 13th International Conference on Automated Deduction (CADE-13). LNCS. Vol. 1104. New Brunswick, NJ, USA: Springer-Verlag. pp. 643–657. CiteSeerX 10.1.1.46.5487. doi:10.1007/3-540-61511-3_119. ISBN 3-540-61511-3.
