We revisit both the usual ``going-up'' induction principle and Manna and Waldinger's ``going-down'' induction principle for primitive recursion,`a la Goedel, and primitive iteration, `a la Church. We use 'Kleene's trick' to show that primitive recursion and primitive iiteration are as expressive as the other, even in the presence of accumulators. As a result, we can directly extract a variety of recursive and iterative functional programs of the kind usually written or optimized by hand.
@article{2225,
title = {A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration},
journal = {Journal of Formalized Reasoning},
volume = {4},
year = {2011},
doi = {10.6092/issn.1972-5787/2225},
language = {EN},
url = {http://dml.mathdoc.fr/item/2225}
}
Chiarabini, Luca; Danvy, Olivier. A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration. Journal of Formalized Reasoning, Tome 4 (2011) . doi : 10.6092/issn.1972-5787/2225. http://gdmltest.u-ga.fr/item/2225/