Walther recursion
D. McAllester and K. Arkoudas
Abstract:
Primitive recursion is a well known syntactic
restriction on recursive definitions which guarantees termination. Unfortunately many
natural definitions, such as the most common definition of Euclid's GCD
algorithm, are not primitive recursive. Walther has recently given a
proof system for verifying termination of a broader class of definitions.
Although Walther's system is highly automatible, the class of acceptable
definitions remains only semi-decidable. Here we simplify Walther's
calculus and give a syntactic criterion on definitions which guarantees
termination. This syntactic criteria generalizes primitive recursion and handles
most of the examples given by Walther. We call the corresponding class
of acceptable definitions "Walther recursive".
BibTeX Entry
@Inproceedings{McAllesterAndArkoudas1996CadeWaltherRecursion,
author = {D. A. McAllester and K. Arkoudas},
title = {Walther Recursion},
booktitle = {Conference on Automated Deduction (CADE 1996)},
pages = {643-657},
year = 1996}
Back to the
publication list of Konstantine Arkoudas