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