В программировании рекурсия Вальтера (названная в честь Кристофа Вальтера ) — это метод анализа рекурсивных функций, который может определить, является ли функция определенно завершающейся , учитывая конечные входные данные. Это позволяет использовать более естественный стиль выражения вычислений, чем простое использование примитивных рекурсивных функций .
Поскольку проблема остановки не может быть решена в общем случае, должны быть все еще программы, которые завершаются, но рекурсия Вальтера не может доказать, что они завершаются. Рекурсия Вальтера может использоваться в полных функциональных языках , чтобы обеспечить более либеральный стиль отображения примитивной рекурсии.
Смотрите также
Ссылки
- Вальтер, Кристоф (1991). «О доказательстве завершения алгоритмов машиной» (PDF) . Искусственный интеллект . 70 (1). doi :10.1016/0004-3702(94)90063-9.
- Wu, Alexander (1994). Автоматизированные доказательства завершения с использованием рекурсии Вальтера (диссертация). Массачусетский технологический институт . Получено 15 сентября 2014 г.
- McAllester, David ; Arkoudas, Kostas (1996). McRobbie, Michael A.; Slaney, JK (ред.). Рекурсия Вальтера. 13-я Международная конференция по автоматизированной дедукции (CADE-13). LNCS. Том 1104. Нью-Брансуик, Нью-Джерси, США: Springer-Verlag. стр. 643–657. CiteSeerX 10.1.1.46.5487 . doi :10.1007/3-540-61511-3_119. ISBN 3-540-61511-3.
