En programación informática, la recursión de Walther (que recibe su nombre de Christoph Walther ) es un método de análisis de funciones recursivas que puede determinar si la función es definitivamente terminal , dadas entradas finitas. Permite un estilo más natural de expresar el cálculo que simplemente usar funciones recursivas primitivas .
Dado que el problema de la detención no se puede resolver en general, debe haber programas que finalizan, pero que la recursión de Walther no puede demostrar que finalizan. La recursión de Walther se puede utilizar en lenguajes totalmente funcionales para permitir un estilo más liberal de mostrar la recursión primitiva.
Véase también
Referencias
- Walther, Christoph (1991). "Sobre la demostración de la terminación de algoritmos por máquinas" (PDF) . Inteligencia artificial . 70 (1). doi :10.1016/0004-3702(94)90063-9.
- Wu, Alexander (1994). Pruebas de terminación automatizadas usando recursión de Walther (Tesis). Instituto Tecnológico de Massachusetts . Consultado el 15 de septiembre de 2014 .
- McAllester, David ; Arkoudas, Kostas (1996). McRobbie, Michael A.; Slaney, JK (eds.). Recursión de Walther. 13.ª Conferencia Internacional sobre Deducción Automatizada (CADE-13). LNCS. Vol. 1104. New Brunswick, NJ, EE. UU.: Springer-Verlag. pp. 643–657. CiteSeerX 10.1.1.46.5487 . doi :10.1007/3-540-61511-3_119. ISBN 3-540-61511-3.
