A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration

Authors

  • Luca Chiarabini Universita' degli studi di Parma
  • Olivier Danvy Aarhus University

DOI:

https://doi.org/10.6092/issn.1972-5787/2225

Abstract

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.

Downloads

Published

2011-12-21

How to Cite

Chiarabini, L., & Danvy, O. (2011). A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration. Journal of Formalized Reasoning, 4(1), 85-109. https://doi.org/10.6092/issn.1972-5787/2225

Issue

Section

Articles