A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration

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 pr...

Full description

Saved in:
Bibliographic Details
Published in:Journal of Formalized Reasoning 2011-01, Vol.4 (1), p.85-109
Main Authors: Chiarabini, Luca, Danvy, Olivier
Format: Article
Language:English
Subjects:
Accumulators
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1972-5787
1972-5787
DOI:10.6092/issn.1972-5787/2225